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. X.φ(X)\forall X.\varphi(X) but not XY.φ(X,Y)\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 VV called the domain of discourse, and for each term x:Vx:V, a dependent type 𝒫(x)\mathcal{P}(x) whose terms P(x):𝒫(x)P(x):\mathcal{P}(x) are propositions depending on xx.

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.

References

  • 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)

Last revised on February 6, 2021 at 10:51:49. See the history of this page for a list of all contributions to it.