Editing Mathematical logic (section)

== Formal logical systems {{anchor|Formal logic}} ==
{{Logical connectives sidebar}}
At its core, mathematical logic deals with mathematical concepts expressed using [[logical system|formal logical system]]s. These systems, though they differ in many details, share the common property of considering only expressions in a fixed [[formal language]].  The systems of [[propositional logic]] and [[first-order logic]] are the most widely studied today, because of their applicability to [[foundations of mathematics]] and because of their desirable proof-theoretic properties.{{efn|name=FerreirósSurveys}}  Stronger classical logics such as [[second-order logic]] or [[infinitary logic]] are also studied, along with [[Non-classical logic]]s such as [[intuitionistic logic]].

=== First-order logic ===
{{Main|First-order logic}}
'''First-order logic''' is a particular [[logical system|formal system of logic]]. Its [[syntax]] involves only finite expressions as [[well-formed formula]]s, while its [[First-order logic#Semantics|semantics]] are characterized by the limitation of all [[Quantifiers (logic)|quantifiers]] to a fixed [[domain of discourse]].

Early results from formal logic established limitations of first-order logic. The [[Löwenheim–Skolem theorem]] (1919) showed that if a set of sentences in a countable first-order language has an infinite model then it has at least one model of each infinite cardinality. This shows that it is impossible for a set of first-order axioms to characterize the natural numbers, the real numbers, or any other infinite structure up to [[isomorphism]]. As the goal of early foundational studies was to produce axiomatic theories for all parts of mathematics, this limitation was particularly stark.

[[Gödel's completeness theorem]] established the equivalence between semantic and syntactic definitions of [[logical consequence]] in first-order logic.{{sfnp|Gödel|1929}} It shows that if a particular sentence is true in every model that satisfies a particular set of axioms, then there must be a finite deduction of the sentence from the axioms. The [[compactness theorem]] first appeared as a lemma in Gödel's proof of the completeness theorem, and it took many years before logicians grasped its significance and began to apply it routinely. It says that a set of sentences has a model if and only if every finite subset has a model, or in other words that an inconsistent set of formulas must have a finite inconsistent subset. The completeness and compactness theorems allow for sophisticated analysis of logical consequence in first-order logic and the development of [[model theory]], and they are a key reason for the prominence of first-order logic in mathematics.

[[Gödel's incompleteness theorems]] establish additional limits on first-order axiomatizations.{{sfnp|Gödel|1931}} The '''first incompleteness theorem''' states that for any consistent, effectively given (defined below) logical system that is capable of interpreting arithmetic, there exists a statement that is true (in the sense that it holds for the natural numbers) but not provable within that logical system (and which indeed may fail in some [[non-standard model of arithmetic|non-standard models of arithmetic]] which may be consistent with the logical system). For example, in every logical system capable of expressing the [[Peano axioms]], the Gödel sentence holds for the natural numbers but cannot be proved.

Here a logical system is said to be effectively given if it is possible to decide, given any formula in the language of the system, whether the formula is an axiom, and one which can express the Peano axioms is called "sufficiently strong." When applied to first-order logic, the first incompleteness theorem implies that any sufficiently strong, consistent, effective first-order theory has models that are not [[elementary substructure|elementarily equivalent]], a stronger limitation than the one established by the Löwenheim–Skolem theorem. The '''second incompleteness theorem''' states that no sufficiently strong, consistent, effective axiom system for arithmetic can prove its own consistency, which has been interpreted to show that [[Hilbert's program]] cannot be reached.

=== Other classical logics ===
Many logics besides first-order logic are studied.  These include [[infinitary logics]], which allow for formulas to provide an infinite amount of information, and [[higher-order logic]]s, which include a portion of set theory directly in their semantics.

The most well studied infinitary logic is <math>L_{\omega_1,\omega}</math>. In this logic, quantifiers may only be nested to finite depths, as in first-order logic, but formulas may have finite or countably infinite conjunctions and disjunctions within them. Thus, for example, it is possible to say that an object is a whole number using a formula of <math>L_{\omega_1,\omega}</math> such as
:<math>(x = 0) \lor (x = 1) \lor (x = 2) \lor \cdots.</math>

Higher-order logics allow for quantification not only of elements of the [[domain of discourse]], but subsets of the domain of discourse, sets of such subsets, and other objects of higher type. The semantics are defined so that, rather than having a separate domain for each higher-type quantifier to range over, the quantifiers instead range over all objects of the appropriate type.  The logics studied before the development of first-order logic, for example Frege's logic, had similar set-theoretic aspects. Although higher-order logics are more expressive, allowing complete axiomatizations of structures such as the natural numbers, they do not satisfy analogues of the completeness and compactness theorems from first-order logic, and are thus less amenable to proof-theoretic analysis.

Another type of logics are '''{{vanchor|fixed-point logic}}s''' that allow [[inductive definition]]s, like one writes for [[primitive recursive function]]s.

One can formally define an extension of first-order logic &mdash; a notion which encompasses all logics in this section because they behave like first-order logic in certain fundamental ways, but does not encompass all logics in general, e.g. it does not encompass intuitionistic, modal or [[fuzzy logic]].

[[Lindström's theorem]] implies that the only extension of first-order logic satisfying both the [[compactness theorem]] and the [[Löwenheim–Skolem theorem#Downward part|downward Löwenheim–Skolem theorem]] is first-order logic.

=== Nonclassical and modal logic ===
{{main|Non-classical logic}}
[[Modal logic]]s include additional modal operators, such as an operator which states that a particular formula is not only true, but necessarily true. Although modal logic is not often used to axiomatize mathematics, it has been used to study the properties of first-order provability{{sfnp|Solovay|1976}} and set-theoretic forcing.{{sfnp|Hamkins|Löwe|2007}}

[[Intuitionistic logic]] was developed by Heyting to study Brouwer's program of intuitionism, in which Brouwer himself avoided formalization. Intuitionistic logic specifically does not include the [[law of the excluded middle]], which states that each sentence is either true or its negation is true.  Kleene's work with the proof theory of intuitionistic logic showed that constructive information can be recovered from intuitionistic proofs. For example, any provably total function in intuitionistic arithmetic is [[computable]]; this is not true in classical theories of arithmetic such as [[Peano arithmetic]].

=== Algebraic logic ===
[[Algebraic logic]] uses the methods of [[abstract algebra]] to study the semantics of formal logics. A fundamental example is the use of [[Boolean algebra (structure)|Boolean algebras]] to represent [[truth value]]s in classical propositional logic, and the use of [[Heyting algebra]]s to represent truth values in intuitionistic propositional logic. Stronger logics, such as first-order logic and higher-order logic, are studied using more complicated algebraic structures such as [[cylindric algebra]]s.