从IF到BI：依赖与分离的故事

我们重新审视了Hintikka和Sandu以及Vaananen的信息依赖与独立逻辑，以及Hodges对其的组合语义。我们展示了Hodges语义如何可以被视为一个一般构造的特例，该构造为关于更广泛模型类的有用完备性定理提供了背景。我们对逻辑的每个方面都提供了一些新的见解。我们表明，该语义所承载的自然命题逻辑是Pym和O'Hearn的Bunched Implications逻辑，它结合了直觉主义和乘法连接词。这引入了几个在信息依赖逻辑中先前未被考虑的新连接词，但我们展示了它们扮演着非常自然的角色，最显著的是直觉主义蕴含。关于量词，我们表明它们在Hodges语义中的解释是被迫的，因为它们是通常Tarski语义在该一般构造下的像；这意味着它们是替换的伴随，因此是唯一确定的。至于依赖谓词，我们表明它可以由一个更简单的谓词，即恒常性或无依赖来定义。这本质地使用了直觉主义蕴含。函数依赖的Armstrong公理随后被恢复为直觉主义蕴含的一组标准公理。我们还证明了Hodges风格的一个完全抽象结果，其中直觉主义蕴含扮演着非常自然的角色。