basic constructions:
strong axioms
further
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
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$.
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.
propositional logic (0th order)
predicate logic (1st order)
second-order logic
Textbook account in view of the Curry-Howard correspondence:
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)
Last revised on December 30, 2022 at 21:20:48. See the history of this page for a list of all contributions to it.