Q0 (logika matematyczna)

Q ₀ jest sformułowaniem Petera Andrewsa dotyczącym rachunku lambda z prostym typem i zapewnia podstawy matematyki porównywalne z logiką pierwszego rzędu i teorią mnogości. Jest to forma logiki wyższego rzędu , ściśle powiązana z logiką rodziny dowodów twierdzeń HOL .

₀ Systemy dowodzenia twierdzeń TPS i ETPS opierają się na Q . W sierpniu 2009 roku TPS wygrał pierwszy w historii konkurs wśród systemów dowodzenia twierdzeń wyższego rzędu.

Aksjomaty Q₀

System ma tylko pięć aksjomatów, które można określić jako:

${\ Displaystyle (1)}$ ${\ displaystyle g_ {oo} T \ ziemia g_ {oo} F = \ forall x_ { o}[g_{oo}x_{o}]}$

${\ Displaystyle (2 ^ {\ alfa})}$ ${\ Displaystyle [x _ {\ alfa} = y _ {\ alfa }]\supset [h_{o\alpha }x_{\alpha }=h_{o\alpha }y_{\alpha }]}$

${\ Displaystyle (3 ^ {\ alfa \ beta})}$ ${\ Displaystyle f _ {\ alfa \beta }=g_{\alpha \beta }=\forall x_{\beta }[f_{\alpha \beta }x_{\beta }=g_{\alpha \beta }x_{\beta }]}$

${\ Displaystyle (4)}$ $\ alfa}} \ mathbf {B} _ {\ beta }]\mathbf {A} _{\alpha }=\mathbf {S} _{A_{\alpha }}^{\mathbf {x} _{\alpha }}\mathbf {B} _{\beta } }$

${\ Displaystyle (5)}$ ℩ ${\ Displaystyle _ {i (oi)} [{\ tekst {Q}} _ {oii} y_ {i}]=y_{i}\,}$

(Aksjomaty 2, 3 i 4 to schematy aksjomatów — rodziny podobnych aksjomatów. Instancje Aksjomatu 2 i Aksjomatu 3 różnią się jedynie typami zmiennych i stałych, ale instancje Aksjomatu 4 mogą mieć dowolne wyrażenie zastępujące A i B. )

Indeks dolny „ o ” jest symbolem typu wartości logicznych, a indeks dolny „ i ” jest symbolem typu pojedynczych wartości (innych niż logiczne). Sekwencje reprezentują typy funkcji i mogą zawierać nawiasy w celu rozróżnienia różnych typów funkcji. Litery greckie z indeksem dolnym, takie jak α i β, są zmiennymi składniowymi symboli typu. Pogrubione wielkie litery, takie jak $A$ , $B$ i $C$ są zmiennymi syntaktycznymi dla WFF, a pogrubione małe litery, takie jak $x$ , $y$ są zmiennymi syntaktycznymi dla zmiennych. $S$ oznacza podstawienie składniowe we wszystkich wolnych wystąpieniach.

Jedynymi stałymi pierwotnymi są $Q ((oα)α)$ , oznaczające równość elementów każdego typu α oraz $℩ (i(oi))$ , oznaczające operator opisu indywiduów, unikalny element zbioru zawierającego dokładnie jeden osobnik. Symbole λ i nawiasy („[” i „]”) określają składnię języka. Wszystkie pozostałe symbole są skrótami terminów je zawierających, łącznie z kwantyfikatorami ∀ i ∃.

W Aksjomacie 4 $x$ musi być wolne dla $A$ w $B$ , co oznacza, że podstawienie nie powoduje, że jakiekolwiek wystąpienia wolnych zmiennych $A$ zostają powiązane w wyniku podstawienia.

O aksjomatach

Aksjomat 1 wyraża pogląd, że $T$ i $F$ są jedynymi wartościami logicznymi.
Schematy aksjomatów 2 ^α i 3 ^αβ wyrażają podstawowe własności funkcji.
Schemat aksjomatu 4 definiuje naturę notacji λ.
Aksjomat 5 mówi, że operator selekcji jest odwrotnością funkcji równości na jednostkach. (Mając jeden argument, $Q$ odwzorowuje tę jednostkę na zbiór/predykat zawierający tę jednostkę. W Q ₀ , $x = y$ jest skrótem od $Qxy$ , które jest skrótem od $(Qx)y$ .) Ten operator jest również znany jako opis określony operator.

W Andrews 2002 Aksjomat 4 został rozwinięty w pięciu podczęściach, które opisują proces podstawienia. Podany tutaj aksjomat jest omawiany jako alternatywa i udowodniony na podstawie podczęści.

Rozszerzenia rdzenia logicznego

Andrews rozszerza tę logikę o definicje operatorów selekcji dla kolekcji wszystkich typów, tak że

${\ Displaystyle (5a)}$ ℩ ${\ Displaystyle _ {\ alfa (o \ alfa)} [{\ tekst {Q}} _ {o\alfa \alfa }y_{i}]=y_{i}\,}$

jest twierdzeniem (numer 5309). Innymi słowy, wszystkie typy mają określony operator opisu. Jest to rozszerzenie konserwatywne , więc rozszerzony system jest spójny, jeśli rdzeń jest spójny.

Przedstawia także dodatkowy Aksjomat 6 , który stwierdza, że istnieje nieskończenie wiele jednostek, wraz z równoważnymi alternatywnymi aksjomatami nieskończoności.

₀ W przeciwieństwie do wielu innych sformułowań teorii typów i asystentów dowodów opartych na teorii typów, Q nie przewiduje typów podstawowych innych niż o i i , więc na przykład skończone liczby kardynalne są konstruowane jako zbiory jednostek przestrzegających zwykłych postulatów Peano, a nie typu w sensie teorii typów prostych.

Wnioskowanie w Q₀

₀ Q ma jedną regułę wnioskowania.

Reguła R. Z $C$ i $A α = B α$ wywnioskować wynik zastąpienia jednego wystąpienia $A α$ w $C$ wystąpieniem $B α$ , pod warunkiem, że wystąpienie $A α$ w $C$ nie jest (wystąpieniem zmiennej) natychmiastowe poprzedzone $λ$ .

Wyprowadzona reguła wnioskowania R′ umożliwia wnioskowanie na podstawie zbioru hipotez H .

Linijka'. Jeżeli $H ⊦ A α = B α$ , oraz $H ⊦ C$ i $D$ otrzymamy z $C$ poprzez zastąpienie jednego wystąpienia $A α$ wystąpieniem $B α$ , to $H ⊦ D$ , pod warunkiem że:

Wystąpienie $A α$ w $C$ nie jest wystąpieniem zmiennej bezpośrednio poprzedzonej przez $λ$ i
żadna zmienna nie jest wolna w $A α = B α$ , a członek $H$ jest związany w $C$ w zastąpionym wystąpieniu $A α$ .

Uwaga: Ograniczenie zastąpienia $A α$ przez $B α$ w $C$ gwarantuje, że każda zmienna wolna zarówno w hipotezie, jak i w $A α = B α$ będzie nadal ograniczona tak, aby miała tę samą wartość w obu przypadkach po dokonaniu podstawienia.

₀ Twierdzenie o dedukcji dla Q pokazuje, że dowody hipotez wykorzystujące Regułę R′ można przekształcić w dowody bez hipotez i stosując Regułę R.

W przeciwieństwie do niektórych podobnych systemów, wnioskowanie w Q ₀ zastępuje podwyrażenie na dowolnej głębokości w WFF równym wyrażeniem. Na przykład dane aksjomaty:

1. $\existsx Px$ 2. $Px \supset Qx$

oraz fakt, że $A \supset B \equiv (A \equiv A \land B)$ , możemy kontynuować bez usuwania kwantyfikatora:

3. $Px \equiv (Px \land Qx)$ tworzenie instancji dla A i B 4. $\existsx (Px \land Qx)$ reguła R podstawienie do linii 1 przy użyciu linii 3.

Notatki

Andrews, Peter B. (2002). Wprowadzenie do logiki matematycznej i teorii typów: do prawdy poprzez dowód (wyd. 2). Dordrecht, Holandia: Kluwer Academic Publishers . ISBN 1-4020-0763-9 . Zobacz także [1]
Kościół, Alonzo (1940). „Sformułowanie prostej teorii typów” (PDF) . Journal of logiki symbolicznej . 5 : 56–58. doi : 10.2307/2266170 . Zarchiwizowane od oryginału (PDF) w dniu 2019-01-12.

Dalsza lektura

Bardziej szczegółowy opis Q ; ₀ część artykułu na temat teorii typów Churcha w Stanford Encyclopedia of Philosophy .
₀ Przegląd logiki matematycznej (w tym różnych następców Q ): Podstawy matematyki. Genealogia i przegląd doi: 10.4444/100.111 .