Logika nieskończona

Logika nieskończona to logika , która dopuszcza nieskończenie długie stwierdzenia i/lub nieskończenie długie dowody . Niektóre logiki nieskończone mogą mieć inne właściwości niż standardowa logika pierwszego rzędu . W szczególności logiki nieskończone mogą nie być zwarte lub kompletne . Pojęcia zwartości i zupełności, które są równoważne w logice skończonej czasami nie są takie w logikach nieskończonych. Dlatego dla logiki nieskończonej zdefiniowane są pojęcia silnej zwartości i silnej zupełności. Ten artykuł dotyczy typu Hilberta , ponieważ zostały one szeroko zbadane i stanowią najprostsze rozszerzenie logiki skończonej. Nie są to jednak jedyne nieskończone logiki, które zostały sformułowane lub zbadane.

Rozważenie, czy pewna nieskończona logika zwana Ω-logiką jest zupełna, może rzucić światło na hipotezę kontinuum .

Słowo o notacji i aksjomacie wyboru

Ponieważ prezentowany jest język z nieskończenie długimi formułami, nie jest możliwe jawne zapisanie takich formuł. Aby obejść ten problem, stosuje się szereg udogodnień notacyjnych, które, ściśle mówiąc, nie są częścią języka formalnego. ${\ displaystyle \ cdots}$ służy do wskazania wyrażenia, które jest nieskończenie długie. Tam, gdzie nie jest to jasne, długość sekwencji jest odnotowywana później. Tam, gdzie ten zapis staje się niejednoznaczny lub mylący, sufiksy takie jak ${\ Displaystyle \ bigvee _ {\ gamma <\ delta} {A_ {\ gamma}}}$ są używane do wskazania nieskończonej alternatywy nad zbiorem formuł liczności . ${\ displaystyle \ delta}$ . Tę samą notację można zastosować do kwantyfikatorów, na przykład ${\ Displaystyle \ forall _ {\ gamma <\ delta} }$ . $Displaystyle$ kwantyfikatorów: kwantyfikator dla każdego gdzie $V _ {\ gamma}}$ .

Wszelkie użycie przyrostków i ${\ displaystyle \ cdots}$ nie jest częścią formalnych języków nieskończonych.

Przyjmuje się aksjomat wyboru (jak to często bywa podczas omawiania logiki nieskończonej), ponieważ jest to konieczne, aby mieć rozsądne prawa rozdzielności .

Definicja logiki nieskończonej typu Hilberta

Język nieskończony pierwszego rzędu L _{α , β} , α regularny , β = 0 lub ω ≤ β ≤ α , ma taki sam zestaw symboli jak logika finitarna i może wykorzystywać wszystkie reguły tworzenia formuł logiki finitarnej wraz z kilka dodatkowych:

• Biorąc pod uwagę zestaw formuł ${\ Displaystyle A = \ {A _ {\ gamma} | \ gamma <\ delta <\ alfa \}}$ wtedy ${\ Displaystyle (A_ {0} \ lor A_ {1} \ lor \ cdots )}$ i ${\ Displaystyle (A_ {0} \ land A_ {1} \ land \ cdots)}$ są formułami. (W każdym przypadku sekwencja ma długość ${\ Displaystyle \ delta}$ .)
• Biorąc pod uwagę zbiór zmiennych ${\ Displaystyle V = \ {V _ {\ gamma} |\ gamma <\ delta <\ beta \}}$ i formuła ${\ Displaystyle A_ {0}},$ a następnie ${\ Displaystyle \ forall V_ {0}: \ forall V_ {1} \ cdots (A_ {0})}$ i ${\ Displaystyle \ istnieje V_ {0}: \ istnieje V_ {1} \ cdots (A_ {0})}$ to formuły. (W każdym przypadku sekwencja kwantyfikatorów ma długość ${\ displaystyle \ delta}$ .)

Pojęcia zmiennych swobodnych i związanych odnoszą się w ten sam sposób do nieskończonych formuł. Podobnie jak w logice skończonej, formuła, której wszystkie zmienne są powiązane, nazywana jest zdaniem .

Teoria T w języku nieskończonym $.$ zbiorem Dowód w logice nieskończonej z teorii T jest (prawdopodobnie nieskończoną) sekwencją stwierdzeń spełniających następujące warunki: Każde stwierdzenie jest albo aksjomatem logicznym, elementem T , albo jest wydedukowane z poprzednich stwierdzeń przy użyciu reguły wnioskowania. Tak jak poprzednio, można zastosować wszystkie reguły wnioskowania w logice skończonej, łącznie z dodatkową:

• Biorąc pod uwagę zestaw stwierdzeń ${\ Displaystyle A = \ {A _ {\ gamma} | \ gamma <\ delta <\ alfa \}},$ które miały miejsce wcześniej w dowodzie, a następnie stwierdzenie ${\ Displaystyle \ land _{\gamma <\delta }{A_{\gamma }}}$ można wywnioskować.

Schematy aksjomatów logicznych charakterystyczne dla logiki nieskończonej przedstawiono poniżej. Globalne zmienne schematu: i ${\ displaystyle$$\ gamma}$ takie, że $<\ alpha}$ .

• ${\ Displaystyle ((\ ziemia _ {\ epsilon <\ delta}} {(A_ {\ delta} \ implikuje A_{\epsilon })})\implikuje (A_{\delta }\implikuje \land _{\epsilon <\delta }{A_{\epsilon }})}}$
• γ ${\ Displaystyle \ gamma <\ delta}$ , $\ Displaystyle ((\ ziemia _ {\ epsilon <\ delta} {A_ {\ epsilon}} )\implikuje A_{\gamma})}$
• Prawa rozdzielności Changa (dla każdego ) $:$ ∨ $Displaystyle (\ lor _ {\ mu <\ gamma}} {(\ gamma} ziemia _{\delta <\gamma }{A_{\mu,\delta}})})}$ , gdzie ${\ Displaystyle \ forall \ mu \ forall \ delta \ istnieje \ epsilon <\ gamma: A _ {\ mu, \ delta} = A _ {\ epsilon}} lub ZA μ , δ =$ ¬ $mu ,\delta }=\neg A_{\epsilon }}$ i ${\ Displaystyle \ forall g \ in \ gamma ^ {\ gamma} \ istnieje \ epsilon <\ gamma: \ {A_ {\ epsilon}, \ neg A_ {\ epsilon} \} \ subseteq \ {A_ {\ mu ,g(\mu )}:\mu <\gamma \}}$
• dla ${\ Displaystyle \ gamma <\ alfa}$ , ${\ Displaystyle ((\ ziemia _ {\ mu <\ gamma} {(\ lor _ {\ delta <\ gamma}} {A _ {\ mu, \ delta}})}) \ implikuje (\ lor _ {\ epsilon < \gamma ^{\gamma }}{(\land _{\mu <\gamma }{A_{\mu ,\gamma _{\epsilon }(\mu )})}})}} ,$ gdzie ${\ Displaystyle \ {\ gamma _ {\ epsilon}: \ epsilon <\ gamma ^ {\ gamma} \}} jest dobrym$ uporządkowaniem ${\ Displaystyle \ gamma ^ {\ gamma}}$

Ostatnie dwa schematy aksjomatów wymagają aksjomatu wyboru, ponieważ pewne zbiory muszą być dobrze uporządkowane . Ostatni schemat aksjomatów jest ściśle mówiąc niepotrzebny, jak implikują to prawa rozdzielności Changa, jednak jest uwzględniony jako naturalny sposób dopuszczenia naturalnych osłabień logiki.

Kompletność, zwartość i silna kompletność

Teoria to dowolny zestaw zdań. Prawdziwość stwierdzeń w modelach jest definiowana przez rekurencję i będzie zgodna z definicją logiki skończonej, w której obie są zdefiniowane. Biorąc pod uwagę teorię T, mówi się, że zdanie jest ważne dla teorii T , jeśli jest prawdziwe we wszystkich modelach T .

Logika w języku jest $,$ jeśli dla każdego zdania S istnieje dowód . Jest silnie zupełna, jeśli dla dowolnej teorii T dla każdego zdania S ważnego w T istnieje dowód S z T . Logika nieskończona może być kompletna, nie będąc silnie kompletną.

Kardynał jest słabo zwarty , gdy dla każdej teorii T w $L _ {\ kappa, \ kappa}}$$Displaystyle$ co najwyżej $kappa}$ wiele formuł, jeśli każdy $\$ o liczności mniejszej niż $displaystyle \ kappa}$ ma model, to T ma model. Kardynał ${\ Displaystyle \ kappa \ neq \ omega}$ jest silnie zwarty , gdy dla każdej teorii T w ${\ Displaystyle L _ {\ kappa, \ kappa}}$ , bez ograniczeń co do rozmiaru, jeśli każdy S ${\ Displaystyle \subseteq }$ T o liczności mniejszej niż ${\ displaystyle \ kappa}$ ma model, to T ma model.

Pojęcia dające się wyrazić w logice nieskończonej

W języku teorii mnogości następujące stwierdzenie wyraża podstawę :

${\ Displaystyle \ forall _ {\ gamma <\ omega} {V_ {\ gamma}:} \ neg \ ziemia _ {\ gamma <\ omega} {V_ {\ gamma +} \ w V_ {\ gamma}}. \ ,}$

W przeciwieństwie do aksjomatu fundamentu, stwierdzenie to nie dopuszcza żadnych niestandardowych interpretacji. Pojęcie zasadności można wyrazić tylko w logice, która dopuszcza nieskończenie wiele kwantyfikatorów w pojedynczym zdaniu. W konsekwencji wiele teorii, w tym arytmetyka Peano , których nie można właściwie aksjomatyzować w logice skończonej, może znajdować się w odpowiedniej logice nieskończonej. Inne przykłady obejmują teorie pól niearchimedesowych i grup bez skrętu . Te trzy teorie można zdefiniować bez użycia nieskończonej kwantyfikacji; potrzebne są tylko nieskończone skrzyżowania.

Kompletna logika nieskończona

Dwie nieskończone logiki wyróżniają się kompletnością. To są logiki ${\ Displaystyle L _ {\ omega, \ omega}}$ i ${\ Displaystyle L _ {\ omega _ {1}, \ omega}}$ . Pierwsza to standardowa logika finitarna pierwszego rzędu, a druga to logika nieskończona, która dopuszcza tylko stwierdzenia o policzalnym rozmiarze.

Logika jest również silnie kompletna, $i$

Logika nie jest zwarta, ale jest kompletna (zgodnie $.$ Ponadto spełnia wariant właściwości interpolacji Craiga .

Jeśli logika $}}$$alfa$ jest silnie kompletna (zgodnie z aksjomatami podanymi powyżej), to jest silnie zwarta (ponieważ dowody w tych logikach nie mogą używać ${\ displaystyle \ alpha}$ lub więcej podanych aksjomatów).

•   Karp, Carol R. (1964), Języki z wyrażeniami o nieskończonej długości , Amsterdam: North-Holland Publishing Co., MR 0176910
•     Barwise, Kenneth Jon (1969), „Logika nieskończona i zbiory dopuszczalne”, Journal of Symbolic Logic , 34 (2): 226–252, doi : 10.2307/2271099 , JSTOR 2271099 , MR 0406760 , S2CID 38740720