Infinitary logic

An infinitary logic is a logic that allows infinitely long statements and/or infinitely long proofs.[1] Some infinitary logics may have different properties from those of standard first-order logic. In particular, infinitary logics may fail to be compact or complete. Notions of compactness and completeness that are equivalent in finitary logic sometimes are not so in infinitary logics. Therefore for infinitary logics, notions of strong compactness and strong completeness are defined. This article addresses Hilbert-type infinitary logics, as these have been extensively studied and constitute the most straightforward extensions of finitary logic. These are not, however, the only infinitary logics that have been formulated or studied.

Considering whether a certain infinitary logic named Ω-logic is complete promises[2] to throw light on the continuum hypothesis.

The axiom of choice is assumed (as is often done when discussing infinitary logic) as this is necessary to have sensible distributivity laws.

A first-order infinitary language Lα,β, α regular, β = 0 or ω ≤ βα, has the same set of symbols as a finitary logic and may use all the rules for formation of formulae of a finitary logic together with some additional ones:

The concepts of free and bound variables apply in the same manner to infinite formulae. Just as in finitary logic, a formula all of whose variables are bound is referred to as a sentence.

The last two axiom schemata require the axiom of choice because certain sets must be well orderable. The last axiom schema is strictly speaking unnecessary, as Chang's distributivity laws imply it,[4] however it is included as a natural way to allow natural weakenings to the logic.

A theory is any set of sentences. The truth of statements in models are defined by recursion and will agree with the definition for finitary logic where both are defined. Given a theory T a sentence is said to be valid for the theory T if it is true in all models of T.

In the language of set theory the following statement expresses foundation:

Unlike the axiom of foundation, this statement admits no non-standard interpretations. The concept of well-foundedness can only be expressed in a logic that allows infinitely many quantifiers in an individual statement. As a consequence many theories, including Peano arithmetic, which cannot be properly axiomatised in finitary logic, can be in a suitable infinitary logic. Other examples include the theories of non-archimedean fields and torsion-free groups.[5][better source needed] These three theories can be defined without the use of infinite quantification; only infinite junctions[6] are needed.