|
An '''infinitary logic''' is a [[Formal logical system|logic]] that allows infinitely long [[statement (logic)|statements]] and/or infinitely long [[Mathematical proof|proofs]].<ref>{{cite book | last=Moore | first=Gregory| title=StructuresH. and Norms in Science|date=1997 |chapter=The Prehistoryprehistory of Infinitaryinfinitary Logiclogic: 1885–1955 |editor-last1=Dalla pagesChiara |editor-first1=105–123Maria Luisa |editor-link1=Maria yearLuisa Dalla Chiara |editor-last2=1997Doets |editor-first2=Kees |editor-last3=Mundici |editor-first3=Daniele |editor-last4=van Benthem |editor-first4=Johan |editor-link4=Johan van Benthem (logician) |title=Structures and Norms in Science |publisher=Springer-Science+Business Media |pages=105–123 |doi=10.1007/978-94-017-0538-7_7| |isbn=978-9094-481017-47870538-87 |s2cid=115693908}}</ref> The concept was introduced by Zermelo in the 1930s.<ref>A.{{cite journal |last=Kanamori, "[|first=Akihiro |author-link=Akihiro Kanamori |date=2004 |title=Zermelo and set theory |url=https://math.bu.edu/people/aki/10.pdf Zermelo and Set Theory]". pp.529--543.|journal=The Bulletin of Symbolic Logic vol. |volume=10, no. |issue=4 (2004)|pages=487–553 |doi=10.2178/bsl/1102083759 Accessed|s2cid=231795240 |access-date=22 August 2023.}}</ref>
Some infinitary logics may have different properties from those of standard [[first-order logic]]. In particular, infinitary logics may fail to be [[Compactness (logic)|compact]] or [[Completeness (logic)|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 system|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 to throw light on the [[continuum hypothesis]].<ref>{{cite web|book |last=Woodin| |first=W. Hugh|authorlink |author-link= W. Hugh Woodin |date=2011 title|chapter=The Continuum Hypothesis, the generic-multiverse of sets, and the Ω Conjecture| publisher=Harvard University Logic Colloquium| year=2009| chapter-url=https://dokumen.tips/documents/the-continuum-hypothesis-the-generic-multiverse-of-logic-continuum-hypothesis.html?page |editor-last1=Kennedy |editor-first1=Juliette |editor-link1=Juliette Kennedy |editor-last2=Kossak |editor-first2=Roman |title=Set Theory, Arithmetic, and Foundations of Mathematics: Theorems, Philosophies |publisher=Cambridge University Press |pages=13–42 |doi=10.1017/CBO9780511910616.003 |isbn=978-0-511-91061-6 |s2cid=7900557 |access-date=1 March 2024}}</ref>
==A word on notation and the axiom of choice==
A [[theory (mathematical logic)|theory]] ''T'' in infinitary language <math>L_{\alpha , \beta}</math> is a set of sentences in the logic. A proof in infinitary logic from a theory ''T'' is a (possibly infinite) [[sequence]] of statements that 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 <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.<ref>{{cite booksfn| journal=Studies in Logic and the Foundations of Mathematics| volume=36| pages=39–54| last=Karp| first=Carol| title=Languages with Expressions of Infinite Length| chapter=Chapter 5 Infinitary Propositional Logic| year=1964| doipp=10.1016/S0049-237X(08)70423-3| isbn=978044453401939–54}}</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>.
*[[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 journal|first=BulletinC. ofC. the|author-link=Chen AmericanChung MathematicalChang Society| volumedate=61|1957 pages=325–326| lasttitle=Chang|On first=Chenthe representation of α-Chung|complete title=AlgebraBoolean andalgebras Theory|journal=[[Transactions of Numbersthe American Mathematical Society]] |volume=85 year|issue=19551 |pages=208–218 url|doi=https://www.ams10.org/journals/bull/1955-61-041090/S0002-99049947-19551957-099320086792-4/S00021 |doi-9904access=free |s2cid=120348873 |s2cid-1955-09932-4.pdfaccess=free}}</ref> however it is included as a natural way to allow natural weakenings to the logic.
==Completeness, compactness, and strong completeness==
:<math>\forall_{\gamma < \omega}{V_{\gamma}:} \neg \land_{\gamma < \omega}{V_{\gamma +} \in V_{\gamma}}.\,</math>
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 field]]s and [[torsion-free group]]s.<ref>{{cite journalweb |url=https://arxiv.org/abs/1003.0360 |last=Rosinger| |first=Elemer E. |date=2010 |title=Four Departuresdepartures in Mathematics and Physics| year=2010| arxiv=1003.0360 | citeseerx=10.1.1.760.6726 |s2cid=17446826 |s2cid-access=free}}</ref>{{better source|date=January 2021}} These three theories can be defined without the use of infinite quantification; only infinite junctions<ref>{{cite journal |last=Bennett |first=David W. |date=1980 |title=Junctions |journal=[[Notre Dame Journal of Formal Logic]] | volume=XXI21 | numberissue=1 | pages=111–118| last=Bennett| first=David| title=Junctions| year=1980| url=https://projecteuclid.org/download/pdf_1/euclid.ndjfl/1093882943| doi=10.1305/ndjfl/1093882943 |doi-access=free doi|s2cid=218839738 |s2cid-access=free}}</ref> are needed.
Truth predicates for countable languages are definable in <math>\mathcal L_{\omega_1,\omega}</math>.<ref>J.{{cite Pogonowski,web "[|url=https://logic.amu.edu.pl/images/9/95/Pogonowski10vi2010.pdf |title=Inexpressible Longinglonging for the Intendedintended Model]"model (draft,|last=Pogonowski |first=Jerzy |date=10 June 2010), p|website=Zakład Logiki Stosowanej |publisher=[[Adam Mickiewicz University in Poznań|Uniwersytet im. Adama Mickiewicza w Poznaniu]] |page=4. |access-date=1 March 2024}}</ref>
==Complete infinitary logics==
==Sources==
* {{citationcite book |last=Karp |first=Carol R. |author-link=Carol Karp |date=1964 |title=Languages with expressionsExpressions of infiniteInfinite lengthLength |publisher=North-Holland Publishing Co.Company |locationdoi=Amsterdam10.1016/S0049-237X(08)70423-3 |mrisbn=0176910978-0-444-53401-9}}
* {{citationcite journal |last=Barwise |first=Kenneth Jon |author-link=Jon Barwise |date=1969 |title=Infinitary logic and admissible sets |journal=[[The Journal of Symbolic Logic]] |doivolume=10.2307/227109934 |jstorissue=22710992 |mrpages=0406760226–252 |volumedoi=3410.2307/2271099 |issuejstor=22271099 |pages=226–252|s2cid=38740720 }}
[[Category:Systems of formal logic]]
| 