无穷逻辑

将一阶逻辑中公式和推理的长度推广至无穷长而得的逻辑。在无穷逻辑的公式中，可以出现无穷多个公式的析取式或合取式，也可以出现无穷多个量词。一阶逻辑的公式都是有穷长的符号序列，这样，有的数学命题就不能用一阶逻辑的公式表达。例如，挠群有一条公理：每一元素都有有穷的阶(finite order)。这条公理的形式化具有形式：

x(x=0∨x·x

　　　　　　　　 =0∨(x·x)·x=0∨…)

这是一个有无穷多个析取项的公式，它不是一阶语言中的公式。为了增强表达能力，需要将一阶逻辑加以推广。无穷逻辑就是由于一阶模型论应用于数学分支受到限制，为克服这种限制而创立的。

设α，β是两个无穷基数，无穷逻辑L的形式语言与一阶语言L相似，但在L的语言中有α个变元，如果Φ是基数小于α的L的公式集合，则∨Φ和∧Φ也是L的公式。∨Φ(∧Φ)表示Φ中的公式的析取式(合取式)，并且允许在小于β个变元上加量词。L即是一阶逻辑。一个简单的无穷逻辑是Lωω。在Lωω的公式中可出现可数无穷多个公式的析取或合取，但只能有有穷多个量词。Lωω的初始符号是在一阶逻辑的符号中增加∨(无穷析取的符号)和∧(无穷合取的符号)；在公式形成规则中增加：如果Φ是至多可数的公式集合，则∨Φ和∧Φ是公式。在公式的解释方面，在可满足性的定义中增加：∨Φ当且仅当对某个φ∈Φ，φ；∧Φ当且仅当对所有φ∈Φ，φ。Lωω增强了表达能力，例如上面所举不能用一阶逻辑公式表示的挠群的公理，可以用Lωω的一个公式表示：x∨｛n·x=0｜0≤n＜ω｝。有许多结构类的特征，不能在一阶逻辑中表示，都能用Lωω的一个公式表示。关于Lωω的公理和推理规则，对每一公式∧Φ和φ∈Φ，增加公理

∧Φ→φ

和推理规则

　　从｛ψ→φ｜φ∈Φ｝推出ψ→∧Φ。

因为应用这个规则包含无穷多个前提，证明的长度也可以无穷。

对于Lωω的系统特性的研究有很多结果。C．卡普在1964年证明了Lωω的完全性：一个Lωω语句是定理，当且仅当它是有效的。对于Lωω还有更强的可证性概念和巴威斯完全性定理。Lωω有下面的累文海姆－司寇伦定理：每一可满足的Lωω语句有一论域至多可数的模型。但是紧致性定理对Lωω不成立。考虑Lωω语句

其中的φ≥是一个公式的缩写，满足φ≥的模型的论域至少有n个元素。于是，对每一有

Ψ当且仅当A是有穷的。因此语句集合｛ψ｝∪｛φ≥｜n≥2｝是一个例子，表明紧致性定理对Lωω不成立。适当地推广有穷性概念之后，J．巴威斯在Lωω的可允许片断上证明了紧致性定理。D．斯科特证明，可以用无穷逻辑Lωω的一个语句刻划可数模型的全部性质：对一可数语言L的每一可数模型，存在Lωω中的一个语句使得对于L的所有可数模型，当且仅当φ。