Editing First-order logic (section)

==Restrictions, extensions, and variations==
There are many variations of first-order logic. Some of these are inessential in the sense that they merely change notation without affecting the semantics. Others change the expressive power more significantly, by extending the semantics through additional quantifiers or other new logical symbols. For example, infinitary logics permit formulas of infinite size, and modal logics add symbols for possibility and necessity.

===Restricted languages===
First-order logic can be studied in languages with fewer logical symbols than were described above:
* Because <math>\exists x \varphi(x)</math> can be expressed as <math>\neg \forall x \neg \varphi(x)</math>, and <math>\forall x \varphi(x)</math> can be expressed as <math>\neg \exists x \neg \varphi(x)</math>, either of the two quantifiers <math>\exists</math> and <math>\forall</math> can be dropped.
* Since <math>\varphi \lor \psi</math> can be expressed as <math>\lnot (\lnot \varphi \land \lnot \psi)</math> and <math>\varphi \land \psi</math> can be expressed as <math>\lnot(\lnot \varphi \lor \lnot \psi)</math>, either <math>\vee</math> or <math>\wedge</math> can be dropped. In other words, it is sufficient to have <math>\neg</math> and <math>\vee</math>, or <math>\neg</math> and <math>\wedge</math>, as the only logical connectives.
* Similarly, it is sufficient to have only <math>\neg</math> and <math>\rightarrow</math> as logical connectives, or to have only the [[Sheffer stroke]] (NAND) or the [[Peirce arrow]] (NOR) operator.
* It is possible to entirely avoid function symbols and constant symbols, rewriting them via predicate symbols in an appropriate way. For example, instead of using a constant symbol <math> \; 0 </math>  one may use a predicate  <math> \; 0(x) </math>  (interpreted as <math> \; x=0 </math> ) and replace every predicate such as <math>\; P(0,y) </math> with <math> \forall x \;(0(x) \rightarrow P(x,y)) </math>. A function such as <math> f(x_1,x_2,...,x_n) </math> will similarly be replaced by a predicate  <math> F(x_1,x_2,...,x_n,y) </math> interpreted as <math> y = f(x_1,x_2,...,x_n) </math>. This change requires adding additional axioms to the theory at hand, so that interpretations of the predicate symbols used have the correct semantics.<ref>[[Left-total]]ity can be expressed by an axiom <math>\forall x_1,...,x_n. \exists y. F(x_1,...,x_n,y)</math>; [[right-unique]]ness by <math>\forall x_1,...,x_n,y,y'.</math> <math>F(x_1,...,x_n,y) \land F(x_1,...,x_n,y') \rightarrow y=y'</math>, provided the equality symbol is admitted. Both also apply to constant replacements (for <math>n=0</math>).</ref>

Restrictions such as these are useful as a technique to reduce the number of inference rules or axiom schemas in deductive systems, which leads to shorter proofs of metalogical results. The cost of the restrictions is that it becomes more difficult to express natural-language statements in the formal system at hand, because the logical connectives used in the natural language statements must be replaced by their (longer) definitions in terms of the restricted collection of logical connectives. Similarly, derivations in the limited systems may be longer than derivations in systems that include additional connectives. There is thus a trade-off between the ease of working within the formal system and the ease of proving results about the formal system.

It is also possible to restrict the arities of function symbols and predicate symbols, in sufficiently expressive theories. One can in principle dispense entirely with functions of arity greater than 2 and predicates of arity greater than 1 in theories that include a [[pairing function]]. This is a function of arity 2 that takes pairs of elements of the domain and returns an [[ordered pair]] containing them. It is also sufficient to have two predicate symbols of arity 2 that define projection functions from an ordered pair to its components. In either case it is necessary that the natural axioms for a pairing function and its projections are satisfied.

===Many-sorted logic===
{{main|Many-sorted logic}}
Ordinary first-order interpretations have a single domain of discourse over which all quantifiers range. ''Many-sorted first-order logic'' allows variables to have different ''sorts'', which have different domains. This is also called ''typed first-order logic'', and the sorts called ''types'' (as in [[data type]]), but it is not the same as first-order [[type theory]]. Many-sorted first-order logic is often used in the study of [[second-order arithmetic]].<ref>{{Cite SEP|url-id=quantification|title=Quantifiers and Quantification|date=October 17, 2018|edition=Winter 2018|last=Uzquiano|first=Gabriel}} See in particular section 3.2, Many-Sorted Quantification.</ref>

When there are only finitely many sorts in a theory, many-sorted first-order logic can be reduced to single-sorted first-order logic.<ref>
[[Herbert Enderton|Enderton, H.]] ''A Mathematical Introduction to Logic'', second edition. [[Academic Press]], 2001, [https://books.google.com/books?id=dVncCl_EtUkC&pg=PT296 pp.296–299].</ref>{{rp|296–299}}
One introduces into the single-sorted theory a unary predicate symbol for each sort in the many-sorted theory and adds an axiom saying that these unary predicates partition the domain of discourse. For example, if there are two sorts, one adds predicate symbols <math>P_1(x)</math> and <math>P_2(x)</math> and the axiom:
:<math>\forall x ( P_1(x) \lor P_2(x)) \land \lnot \exists x (P_1(x) \land P_2(x))</math>.
Then the elements satisfying <math>P_1</math> are thought of as elements of the first sort, and elements satisfying <math>P_2</math> as elements of the second sort. One can quantify over each sort by using the corresponding predicate symbol to limit the range of quantification. For example, to say there is an element of the first sort satisfying formula <math>\varphi(x)</math>, one writes:
:<math>\exists x (P_1(x) \land \varphi(x))</math>.

===Additional quantifiers===
Additional quantifiers can be added to first-order logic.
* Sometimes it is useful to say that "{{math|''P''(''x'')}} holds for exactly one ''x''", which can be expressed as {{math|∃!''x'' ''P''(''x'')}}.  This notation, called [[uniqueness quantification]], may be taken to abbreviate a formula such as {{math|1=∃''x'' (''P''(''x'') {{and}} ∀''y'' (''P''(''y'') → (''x'' = ''y'')))}}.
*''First-order logic with extra quantifiers'' has new quantifiers ''Qx'',..., with meanings such as "there are many ''x'' such that ...". Also see [[branching quantifier]]s and the [[plural quantification|plural quantifier]]s of [[George Boolos]] and others.
* ''[[Bounded quantifier]]s'' are often used in the study of set theory or arithmetic.

===Infinitary logics===
{{Main|Infinitary logic}}
Infinitary logic allows infinitely long sentences. For example, one may allow a conjunction or disjunction of infinitely many formulas, or quantification over infinitely many variables. Infinitely long sentences arise in areas of mathematics including [[topology]] and [[model theory]].

Infinitary logic generalizes first-order logic to allow formulas of infinite length. The most common way in which formulas can become infinite is through infinite conjunctions and disjunctions. However, it is also possible to admit generalized signatures in which function and relation symbols are allowed to have infinite arities, or in which quantifiers can bind infinitely many variables. Because an infinite formula cannot be represented by a finite string, it is necessary to choose some other representation of formulas; the usual representation in this context is a tree. Thus, formulas are, essentially, identified with their parse trees, rather than with the strings being parsed.

The most commonly studied infinitary logics are denoted ''L''<sub>αβ</sub>, where α and β are each either [[cardinal number]]s or the symbol ∞. In this notation, ordinary first-order logic is ''L''<sub>ωω</sub>.
In the logic ''L''<sub>∞ω</sub>, arbitrary conjunctions or disjunctions are allowed when building formulas, and there is an unlimited supply of variables. More generally, the logic that permits conjunctions or disjunctions with less than κ constituents is known as ''L''<sub>κω</sub>. For example, ''L''<sub>ω<sub>1</sub>ω</sub> permits [[countable set|countable]] conjunctions and disjunctions.

The set of free variables in a formula of ''L''<sub>κω</sub> can have any cardinality strictly less than κ, yet only finitely many of them can be in the scope of any quantifier when a formula appears as a subformula of another.<ref>Some authors only admit formulas with finitely many free variables in ''L''<sub>κω</sub>, and more generally only formulas with <&nbsp;λ free variables in ''L''<sub>κλ</sub>.</ref> In other infinitary logics, a subformula may be in the scope of infinitely many quantifiers. For example, in ''L''<sub>κ∞</sub>, a single universal or existential quantifier may bind arbitrarily many variables simultaneously. Similarly, the logic ''L''<sub>κλ</sub> permits simultaneous quantification over fewer than λ variables, as well as conjunctions and disjunctions of size less than κ.

===Non-classical and modal logics===

{{main|Non-classical logic}} 

*''[[intuitionistic logic|Intuitionistic first-order logic]]'' uses intuitionistic rather than classical reasoning; for example, ¬¬φ need not be equivalent to φ and ¬ ∀x.φ is in general not equivalent to ∃ x.¬φ .
*First-order ''[[modal logic]]'' allows one to describe other possible worlds as well as this contingently true world which we inhabit. In some versions, the set of possible worlds varies depending on which possible world one inhabits. Modal logic has extra ''modal operators'' with meanings which can be characterized informally as, for example "it is necessary that φ" (true in all possible worlds) and "it is possible that φ" (true in some possible world). With standard first-order logic we have a single domain, and each predicate is assigned one extension. With first-order modal logic we have a ''domain function'' that assigns each possible world its own domain, so that each predicate gets an extension only relative to these possible worlds. This allows us to model cases where, for example, Alex is a philosopher, but might have been a mathematician, and might not have existed at all. In the first possible world ''P''(''a'') is true, in the second ''P''(''a'') is false, and in the third possible world there is no ''a'' in the domain at all.
*''[[t-norm fuzzy logics|First-order fuzzy logics]]'' are first-order extensions of propositional fuzzy logics rather than classical [[propositional calculus]].

===Fixpoint logic===
{{main|Fixed-point logic}}
Fixpoint logic extends first-order logic by adding the closure under the least fixed points of positive operators.<ref>{{cite book | title=Computer Science Logic: 6th Workshop, CSL'92, San Miniato, Italy, September 28 - October 2, 1992. Selected Papers | volume=702 | series=Lecture Notes in Computer Science | editor1-first=Egon | editor1-last=Börger | publisher=[[Springer-Verlag]] | year=1993 | zbl=0808.03024 | isbn=3-540-56992-8 | pages=100–114 | first=Uwe | last=Bosse | chapter=An Ehrenfeucht–Fraïssé game for fixpoint logic and stratified fixpoint logic }}</ref>

===Higher-order logics===
{{Main|Higher-order logic}}

The characteristic feature of first-order logic is that individuals can be quantified, but not predicates. Thus
:<math>\exists a ( \text{Phil}(a))</math>
is a legal first-order formula, but
:<math>\exists \text{Phil} ( \text{Phil}(a))</math>
is not, in most formalizations of first-order logic. [[Second-order logic]] extends first-order logic by adding the latter type of quantification. Other [[higher-order logic]]s allow quantification over even higher [[type theory|types]] than second-order logic permits. These higher types include relations between relations, functions from relations to relations between relations, and other higher-type objects.  Thus the "first" in first-order logic describes the type of objects that can be quantified.

Unlike first-order logic, for which only one semantics is studied, there are several possible semantics for second-order logic. The most commonly employed semantics for second-order and higher-order logic is known as ''full semantics''. The combination of additional quantifiers and the full semantics for these quantifiers makes higher-order logic stronger than first-order logic. In particular, the (semantic) logical consequence relation for second-order and higher-order logic is not semidecidable; there is no effective deduction system for second-order logic that is sound and complete under full semantics.

Second-order logic with full semantics is more expressive than first-order logic. For example, it is possible to create axiom systems in second-order logic that uniquely characterize the natural numbers and the real line. The cost of this expressiveness is that second-order and higher-order logics have fewer attractive metalogical properties than first-order logic. For example, the Löwenheim–Skolem theorem and compactness theorem of first-order logic become false when generalized to higher-order logics with full semantics.