An infinitary logic is a logic that allows infinitely long statements and/or infinitely long proofs.
In particular, infinitary logics may fail to be compact or complete.
This article addresses Hilbert-type infinitary logics, as these have been extensively studied and constitute the most straightforward extensions of finitary logic.
Considering whether a certain infinitary logic named Ω-logic is complete promises to throw light on the continuum hypothesis.
To get around this problem a number of notational conveniences, which, strictly speaking, are not part of the formal language, are used.
is used to point out an expression that is infinitely long.
Where it is unclear, the length of the sequence is noted afterwards.
Where this notation becomes ambiguous or confusing, suffixes such as
are used to indicate an infinite disjunction over a set of formulae of cardinality
The same notation may be applied to quantifiers, for example
The axiom of choice is assumed (as is often done when discussing infinitary logic) as this is necessary to have sensible distributivity laws.
, 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:[4] The language may also have function, relation, and predicate symbols of finite arity.
an infinite cardinal and some more complicated restrictions on
that allow for function and predicate symbols of infinite arity, with
controlling the maximum arity of a function symbol and
[6] 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.
is a (possibly infinite) sequence of statements that obeys the following conditions: Each statement is either a logical axiom, an element of
, or is deduced from previous statements using a rule of inference.
As before, all rules of inference in finitary logic can be used, together with an additional one: If
, forming universal closures may not always be possible, however extra constant symbols may be added for each variable with the resulting satisfiability relation remaining the same.
[8] To avoid this, some authors use a different definition of the language
The last axiom schema is strictly speaking unnecessary, as Chang's distributivity laws imply it,[10] however it is included as a natural way to allow natural weakenings to the logic.
The truth of statements in models are defined by recursion and will agree with the definition for finitary logic where both are defined.
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.
Truth predicates for countable languages are definable in
Moreover, it satisfies a variant of the Craig interpolation property.