nLab second-order logic

Idea

Second-order logic(SOL) is an extension of first-order logic with quantifiers and variables that range over subsets of the universe of discourse, and hence is a higher-order logic of stage 2.

An important fragment is Monadic Second-order logic (MSOL), where second-order quantification is restricted to second-order unary relations between subsets i.e. MSOL quantifies only over set predicates e.g. $\forall X.\varphi(X)$ but not $\forall X\forall Y .\varphi(X,Y)$.

Second-order logic could be characterised as a first order theory with dependent types. There is a type $V$ called the domain of discourse, and for each term $x:V$, a dependent type $\mathcal{P}(x)$ whose terms $P(x):\mathcal{P}(x)$ are propositions depending on $x$.

Remark

As SOL permits characterisation of mathematical structures up to isomorphism, it is sometimes promoted as a contender to set theory for the foundations of mathematics (cf. references). However, characterising structures up to isomorphism is insufficient for category theory and higher category theory, as weak categories could only be characterised up to equivalence of categories, and weak ∞-groupoids could only be characterised up to homotopy equivalence.

Related concepts

• propositional logic (0th order)

• predicate logic (1st order)

• second-order logic

• higher-order logic

• dependent type theory

• System F

References

Textbook account in view of the Curry-Howard correspondence:

• Morten Heine Sørensen, Pawel Urzyczyn, Lectures on the Curry-Howard isomorphism, Studies in Logic 149, Elsevier (2006) [ISBN:9780444520777, pdf]

See also:

• Wikipedia, Second-order logic

• Stewart Shapiro, Do Not Claim Too Much: Second-Order Logic and First-Order Logic , Phil. Math. 3 no. 7 (1999) pp.42-64 . (pdf)

• Jouko Väänänen, Second-order Logic and Foundations of Mathematics , BSL 7 no. 4 (2001) pp.504-520. (ps)

• Jouko Väänänen, Second-order logic, set theory, and the foundations of mathematics , Ms. (pdf)