Editing Infinitary logic (section)

==Definition of Hilbert-type infinitary logics==

A [[theory (mathematical logic)|theory]] <math>T</math> in infinitary language <math>L_{\alpha , \beta}</math> is a set of sentences in the logic. A proof in infinitary logic from a theory <math>T</math> is a (possibly infinite) [[sequence]] of statements that obeys the following conditions: Each statement is either a logical axiom, an element of <math>T</math>, 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 <math>A=\{A_\gamma | \gamma < \delta <\alpha \}</math> that have occurred previously in the proof then the statement <math>\land_{\gamma < \delta}{A_{\gamma}}</math> can be inferred.{{sfn|Karp|1964|pp=39–54}}

If <math>\beta<\alpha</math>, forming [[Universal closure|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.{{sfn|Karp|1964|p=127}} To avoid this, some authors use a different definition of the language <math>L_{\alpha,\beta}</math> forbidding formulas from having more than <math>\beta</math> free variables.<ref>J. L. Bell, "[https://plato.stanford.edu/entries/logic-infinitary/ Infinitary Logic]". Stanford Encyclopedia of Philosophy, revised 2023. Accessed 26 July 2024.</ref>

The logical axiom schemata specific to infinitary logic are presented below. Global schemata variables: <math>\delta</math> and <math>\gamma</math> such that <math>0 < \delta < \alpha </math>.
*<math>((\land_{\epsilon < \delta}{(A_{\delta} \implies A_{\epsilon})}) \implies (A_{\delta} \implies \land_{\epsilon < \delta}{A_{\epsilon}}))</math>
*For each <math>\gamma < \delta</math>, <math>((\land_{\epsilon < \delta}{A_{\epsilon}}) \implies A_{\gamma})</math>
*[[Chen-Chung Chang|Chang]]'s distributivity laws (for each <math>\gamma</math>): <math>(\lor_{\mu < \gamma}{(\land_{\delta < \gamma}{A_{\mu , \delta}})})</math>, where <math>\forall \mu \forall \delta \exists \epsilon < \gamma: A_{\mu , \delta} = A_{\epsilon}</math> or <math>A_{\mu , \delta} = \neg A_{\epsilon}</math>, and <math>\forall g \in \gamma^{\gamma} \exists \epsilon < \gamma: \{A_{\epsilon} , \neg A_{\epsilon}\} \subseteq \{A_{\mu , g(\mu)} : \mu < \gamma\}</math>
*For <math>\gamma < \alpha</math>, <math>((\land_{\mu < \gamma}{(\lor_{\delta < \gamma}{A_{\mu , \delta}})}) \implies (\lor_{\epsilon < \gamma^{\gamma}}{(\land_{\mu < \gamma}{A_{\mu ,\gamma_{\epsilon}(\mu)})}}))</math>, where <math>\{\gamma_{\epsilon}: \epsilon < \gamma^{\gamma}\}</math> is a well ordering of <math>\gamma^{\gamma}</math>
The last two axiom schemata require the axiom of choice because certain sets must be [[well order]]able. The last axiom schema is strictly speaking unnecessary, as Chang's distributivity laws imply it,<ref>{{cite journal |last=Chang |first=C. C. |author-link=Chen Chung Chang |date=1957 |title=On the representation of α-complete Boolean algebras |journal=[[Transactions of the American Mathematical Society]] |volume=85 |issue=1 |pages=208–218 |doi=10.1090/S0002-9947-1957-0086792-1 |doi-access=free}}</ref> however it is included as a natural way to allow natural weakenings to the logic.