Second order logic

Second-order logic in mathematical logic is a formal system that extends first-order logic ^{[1] with the} possibility of quantifying generality and existence not only over variables, but also over predicates . Second-order logic is not reducible to first-order logic. In turn, it is expanded by higher order logic and type theory .

Content

1 Language and Syntax
2 Axiomatics and proof of formulas
3 Semantics
4 Properties
5 notes
6 Literature

Language and Syntax

Formal languages of second-order logic are built on the basis of many functional symbols ${\mathcal {F}}$ ${\ displaystyle {\ mathcal {F}}}$ and many predicate characters ${\mathcal {P}}$ ${\ displaystyle {\ mathcal {P}}}$ . Arity (the number of arguments) is associated with each functional and predicate symbol. Additional characters are also used.

Symbols of individual variables, usually $\ x,y,z,x_{1},y_{1},z_{1},x_{2},y_{2},z_{2}$ ${\ displaystyle \ x, y, z, x_ {1}, y_ {1}, z_ {1}, x_ {2}, y_ {2}, z_ {2}}$ etc.
Function Variable Symbols $\ F,G,H,F_{1},G_{1},H_{1},F_{2},G_{2},H_{2}$ ${\ displaystyle \ F, G, H, F_ {1}, G_ {1}, H_ {1}, F_ {2}, G_ {2}, H_ {2}}$ and so on. Each functional variable corresponds to a certain positive number — the arity of the function.
Symbols of predicate variables $\ P,R,S,P_{1},R_{1},S_{1},P_{2},R_{2},S_{2}$ ${\ displaystyle \ P, R, S, P_ {1}, R_ {1}, S_ {1}, P_ {2}, R_ {2}, S_ {2}}$ etc. Each predicate variable corresponds to a certain positive number - the arity of the predicate.
Positional Relations: $\lor ,\land ,\neg ,\to$ ${\ displaystyle \ lor, \ land, \ neg, \ to}$ ,
Community quantifiers $\forall$ ${\ displaystyle \ forall}$ and existence $\exists$ ${\ displaystyle \ exists}$ ,
Service characters: brackets and comma.

Listed characters along with characters ${\mathcal {P}}$ ${\ displaystyle {\ mathcal {P}}}$ and ${\mathcal {F}}$ ${\ displaystyle {\ mathcal {F}}}$ form the alphabet of first-order logic. More complex constructions are defined inductively .

A term is a symbol of an individual variable, or an expression that has the form $\ f(t_{1},\ldots ,t_{n})$ ${\ displaystyle \ f (t_ {1}, \ ldots, t_ {n})}$ where $\ f$ ${\ displaystyle \ f}$ - a functional symbol of arity $\ n$ ${\ displaystyle \ n}$ , but $\ t_{1},\ldots ,t_{n}$ ${\ displaystyle \ t_ {1}, \ ldots, t_ {n}}$ - terms or expression of the form $\ F(t_{1},\ldots ,t_{n})$ ${\ displaystyle \ F (t_ {1}, \ ldots, t_ {n})}$ where $\ F$ ${\ displaystyle \ F}$ - functional variable arity $\ n$ ${\ displaystyle \ n}$ , but $\ t_{1},\ldots ,t_{n}$ ${\ displaystyle \ t_ {1}, \ ldots, t_ {n}}$ - terms.
Atom - has the form $\ p(t_{1},\ldots ,t_{n})$ ${\ displaystyle \ p (t_ {1}, \ ldots, t_ {n})}$ where $p$ ${\ displaystyle p}$ - predicate symbol of arity $\ n$ ${\ displaystyle \ n}$ , but $\ t_{1},\ldots ,t_{n}$ ${\ displaystyle \ t_ {1}, \ ldots, t_ {n}}$ - terms or $\ P(t_{1},\ldots ,t_{n})$ ${\ displaystyle \ P (t_ {1}, \ ldots, t_ {n})}$ where $P$ ${\ displaystyle P}$ - predicate variable arity $\ n$ ${\ displaystyle \ n}$ , but $\ t_{1},\ldots ,t_{n}$ ${\ displaystyle \ t_ {1}, \ ldots, t_ {n}}$ - terms.
A formula is either an atom or one of the following constructions: $\neg A,(A_{1}\lor A_{2}),(A_{1}\land A_{2}),(A_{1}\to A_{2}),\forall xA,\exists xA,\forall FA,\exists FA,\forall PA,\exists PA$ ${\ displaystyle \ neg A, (A_ {1} \ lor A_ {2}), (A_ {1} \ land A_ {2}), (A_ {1} \ to A_ {2}), \ forall xA, \ exists xA, \ forall FA, \ exists FA, \ forall PA, \ exists PA}$ where $\ A,A_{1},A_{2}$ ${\ displaystyle \ A, A_ {1}, A_ {2}}$ - formulas, and $\ x,F,P$ ${\ displaystyle \ x, F, P}$ - individual, functional and predicate variables.

Axiomatics and proof of formulas

Semantics

In classical logic, the interpretation of second-order logic formulas is given on a second-order model, which is determined by the following data.

Base set ${\mathcal {D}}$ ${\ displaystyle {\ mathcal {D}}}$ ,
Semantic function $σ$ {\ displaystyle \ sigma} which displays
- everyone $n$ ${\ displaystyle n}$ -ar functional symbol $f$ ${\ displaystyle f}$ of ${\mathcal {F}}$ ${\ displaystyle {\ mathcal {F}}}$ at $n$ ${\ displaystyle n}$ -ary function $\sigma (f):{\mathcal {D}}\times \ldots \times {\mathcal {D}}\rightarrow {\mathcal {D}}$ ${\ displaystyle \ sigma (f): {\ mathcal {D}} \ times \ ldots \ times {\ mathcal {D}} \ rightarrow {\ mathcal {D}}}$ ,
- everyone $n$ ${\ displaystyle n}$ -ar predicate symbol $p$ ${\ displaystyle p}$ of ${\mathcal {P}}$ ${\ displaystyle {\ mathcal {P}}}$ at $n$ ${\ displaystyle n}$ -ary relationship $\sigma (p)\subseteq {\mathcal {D}}\times \ldots \times {\mathcal {D}}$ ${\ displaystyle \ sigma (p) \ subseteq {\ mathcal {D}} \ times \ ldots \ times {\ mathcal {D}}}$ .

Properties

Unlike first-order logic, second-order logic does not have the properties of completeness and compactness . Also in this logic is the statement of the Lowenheim-Skulem theorem .

Notes

↑ Shapiro (1991) and Hinman (2005) give complete introductions to the subject, with full definitions.

Literature

Henkin, L. (1950). "Completeness in the theory of types." Journal of Symbolic Logic 15 (2): 81-91.
Hinman, P. (2005). Fundamentals of Mathematical Logic. AK Peters. ISBN 1-56881-262-0 .
Shapiro, S. (2000). Foundations without Foundationalism: A Case for Second-order Logic. Oxford University Press. ISBN 0-19-825029-0 .
Rossberg, M. (2004). "First-Order Logic, Second-Order Logic, and Completeness." in V. Hendricks et al., eds .. First-order logic revisited. Berlin: Logos-Verlag.
Vaananen, J. (2001). "Second-Order Logic and Foundations of Mathematics." Bulletin of Symbolic Logic 7 (4): 504-520.

[1] Shapiro (1991) and Hinman (2005) give complete introductions to the subject, with full definitions.