Infinitary Logic - Definition of Hilbert-type Infinitary Logics

Definition of Hilbert-type Infinitary Logics

A first-order infinitary logic 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:

• Given a set of variables and a formula then and are formulae (In each case the sequence of quantifiers has length ).
• Given a set of formulae then and are formulae (In each case the sequence has length ).

The concepts of bound variables apply in the same manner to infinite sentences. Note that the number of brackets in these formulae is always finite. Just as in finitary logic, a formula all of whose variables are bound is referred to as a sentence.

A theory T in infinitary logic is a set of statements in the logic. A proof in infinitary logic from a theory T is a sequence of statements of length which obeys the following conditions: Each statement is either a logical axiom, an element of T, 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:

• Given a set of statements which have occurred previously in the proof then the statement can be inferred.

The logical axiom schemata specific to infinitary logic are presented below. Global schemata variables: and such that .

• For each,
• Chang's distributivity laws (for each ): where and
• For, where is a well ordering of

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, however it is included as a natural way to allow natural weakenings to the logic.