Editing Infinitary logic (section)

==Formal languages==

A first-order infinitary language <math>L_{\kappa,\lambda}</math>, <math>\kappa</math> [[regular cardinal|regular]], <math>\lambda = 0</math> or <math>\omega\leq\lambda\leq\kappa</math>, 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:{{sfn|Karp|1964|pp=1–2}}
*Given a set of formulae <math>A=\{A_\gamma | \gamma < \delta <\alpha \}</math> with <math>|\alpha| < \kappa</math> then <math>(A_0 \lor A_1 \lor \cdots)</math> and <math>(A_0 \land A_1 \land \cdots)</math> are formulae. (In each case the sequence has length <math>\delta</math>.)
*Given a set of variables <math>V=\{V_\gamma | \gamma< \delta < \beta \}</math> with <math>|\beta| < \lambda</math> and a formula <math>A_0</math> then <math>\forall V_0 :\forall V_1 \cdots (A_0)</math> and <math>\exists V_0 :\exists V_1 \cdots (A_0)</math> are formulae. (In each case the sequence of quantifiers has length <math>\delta</math>.)

The language may also have function, relation, and predicate symbols of finite arity.{{sfn|Karp|1964|p=1}} Karp also defined languages <math>L_{\kappa\,\lambda\omicron\pi}</math> with <math>\pi\leq\kappa</math> an infinite cardinal and some more complicated restrictions on <math>\omicron</math> that allow for function and predicate symbols of infinite arity, with <math>\omicron</math> controlling the maximum arity of a function symbol and <math>\pi</math> controlling predicate symbols.{{sfn|Karp|1964|pp=101–102}}

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 (mathematical logic)|sentence]]''.