二階邏輯

语义

二阶逻辑的语义建立每个句子的意义。不像只有一个标准语义的一阶逻辑，二阶逻辑有两个常用的不同语义：“标准语义”和“Henkin语义”。在这些语义中，一阶量词和逻辑连结词的解释是同于一阶逻辑的。只有在二阶量词变量的新量词需要定义语义。
在标准语义中，量词取值于适当种类的“所有”集合或函数上。所以一旦确立了一阶变量的论域，余下的量词的意义就固定了。这种语义给予了二阶逻辑强大的表达能力，本文采用了这种语义。
在Henkin语义中，每个二阶变量种类都有它自己取值的特定论域，它可以是所有此类的所有集合或函数的真子集。Leon Henkin（1950）定义了这种语义并证明了对一阶逻辑成立的哥德尔完全性定理和紧致性定理，在有Henkin语义的二阶逻辑中继续有效。这是因为Henkin语义几乎等同于多种类一阶语义，它通过增加额外的变量种类来模拟二阶逻辑的新变量。带有Henkin语义的二阶逻辑不比一阶逻辑有更大表达能力。Henkin语义经常用在二阶算术的研究中。

演绎系统

逻辑的演绎系统是确定哪些公式序列构成有效证明的一组推理规则和逻辑公理。很多演绎系统可以用于二阶逻辑，尽管它们都不能针对标准语义（见后）是完备的。每个这种系统都是可靠的，这以为它们可以证明的任何句子在适当的语义中都是逻辑有效的。
可用的最弱的演绎系统由标准的一阶逻辑演绎系统（比如自然演绎）扩充上对二阶项的代换规则。这种演绎系统常用于二阶算术的研究中。
Shapiro (1991)和Henkin（1950）考虑的演绎系统想扩充的一阶演绎系统增加了内涵公理和选择公理二者。这些公理对于二阶语义是可靠的。它们对于Henkin语义是可靠的，只要考虑的是满足内涵和选择公理的Henkin模型。

二阶逻辑的历史和有争议的价值

当谓词逻辑被弗雷格（独立的和更有影响力的皮尔士，他提出了术语“二阶逻辑”）介绍给数学社区的时候，他确实使用不同的变量来区分在物体上量化和在属性和集合上的量化；但是他自己没有去区分出两类不同的逻辑。在发现罗素悖论之后，认识到了他的系统有些毛病。最终逻辑学家建立了以各种方式做限制的弗雷格逻辑—现在叫做一阶逻辑—除去了这个问题：集合和谓词在一阶逻辑中不能被单独量化。现在标准的逻辑的阶数等级就是从那时开始的。
发现了集合论可以在一阶逻辑的设施内公式化为公理化系统（损失了某种完备性，但是不至于象罗素悖论那么糟糕），并且真就这么做了（参见Zermelo-Fraenkel集合论），因为集合是数学的关键。算术、分体论和各种其他强力逻辑理论可以被公理化的公式化，而不用使用比一阶量化更多的逻辑设施，随着哥德尔和Skolem忠于一阶逻辑，导致了对二（或更高）阶逻辑的工作的普遍放弃。
这种舍弃由一些逻辑学家活跃的推动着，最著名的是蒯因。蒯因推进了这种观点，在谓词语言句子比如Fx中，x被认为是一个变量或指称一个物体的名字，所以可以被量化，如“对于所有的东西，情况是. . .”。但是F被认为是一个不完整句子的“一个缩写”，不是一个物体（甚至不是抽象的物体如性质）的名字。例如，它可能意味着“ . . .是个狗”，认为在这种事物上可以做量化是没有什么意义的。（这种立场同弗雷格自己对概念-物体区别的讨论是非常一致的）。所以要使用一个谓词作为变量就要让它占据只有个别的变量可以占据的一个名字的位置。这种推理被Boolos拒绝了。
近年来二阶逻辑有某种程度的恢复，由George Boolos把二阶量化解释为在同一阶量化一样的域上的复数量化所支持。Boolos进一步指出句子的非一阶可表达性，比如“有些罪犯只相互倾慕”和“有些Fianchetto人进入仓库而没有任何别人陪同”。这只能用二阶量化的完全力量来表达。（实际上这不是真的，因为一般性的量化和偏序的（或分支的）量化同样足以表达特定类的非一阶可表达的句子而不使用二阶量化)。
但是，已经说过在有些数学分支中比如拓扑学中，需要二阶逻辑的能力来做完整的表达。这方面的工作已经由Stephen G. Simpson在逆数学的名义下完成了。已经证明了二阶逻辑不只对表达经典数学的某些重要部分是必须的，而且它也可以用做模型论和数学基础的工具。

存在性片段在有限结构上的能力

单类二阶逻辑（MSO）的存在性片段（EMSO）是没有全称量词的二阶逻辑。在词之上，所有的MSO公式都可以转换成确定的有穷自动机。它可以再转换成EMSO公式。所以EMSO和MSO在这种词上是等价的。对于树作为输入，这个结果同样成立。但是，在有限网格之上，这个性质不再成立，因为瓦片系统识别的语言不闭合于补集之下。因为全称量词等价于否定的存在量词，它不能被表达，全称和存在量词的交替生成了在上的更大的一类语言。