Logika dla informatyków/Logika intuicjonistyczna

Logika intuicjonistyczna

Logika klasyczna oparta jest na pojęciu wartości logicznej zdania. Poprawnie zbudowane i jednoznaczne stwierdzenie jest w tej logice klasyfikowane jako "prawdziwe" lub "fałszywe". Wartość logiczna zdania złożonego (np. implikacji) jest zaś ustalana na podstawie wartości jego składowych (niezależnie od ich faktycznej treści). W większości przypadków takie postępowanie jest naturalne i wygodne. Ale nie zawsze. Przypomnijmy na przykład, że klasyczna materialna implikacja nie zawsze odpowiada jakiejkolwiek faktycznej zależności pomiędzy przesłanką i konkluzją (Rozdział 3.1). Inną konsekwencją dwuwartościowości logiki klasycznej jest prawo wyłączonego środka. Akceptujemy alternatywę $\displaystyle p\vee \neg p$, niezależnie od tego czy zdanie $\displaystyle p$ jest faktycznie prawdziwe czy fałszywe, a nawet nie wiedząc, co dokładnie to zdanie wyraża. Zilustrujmy to na przykładzie:

Fakt 11.1

Istnieją takie liczby niewymierne $\displaystyle x$ i $\displaystyle y$, że $\displaystyle x^{y}$ jest liczbą wymierną.

Dowód

Jeśli $\displaystyle {\sqrt {2}}^{\sqrt {2}}$ jest wymierne, to można przyjąć $\displaystyle x=y={\sqrt {2}}$, w przeciwnym przypadku niech $\displaystyle x={\sqrt {2}}^{\sqrt {2}}$ i $\displaystyle y={\sqrt {2}}$.

Powyższy dowód, przy całej swojej prostocie i elegancji, ma pewną oczywistą wadę: nadal nie wiemy, jakie liczby naprawdę spełniają żądany warunek. A oto inny dowód Faktu $(11.1)$.

Dowód 2

Dla $\displaystyle x={\sqrt {2}}$ oraz $\displaystyle y=2\log _{2}3$ mamy $\displaystyle x^{y}=3$.

Mówimy, że drugi dowód, w odróżnieniu od pierwszego, jest konstruktywny. Oczywiście, konstruktywny dowód zawiera w sobie więcej przydatnej informacji niż niekonstruktywny, ale z punktu widzenia logiki klasycznej, oba te dowody są tak samo poprawne.

Logika, dopuszczająca tylko wnioskowania o charakterze konstruktywnym, znana jest pod tradycyjną, nieco mylącą, nazwą logiki intuicjonistycznej. W tej logice nie przypisujemy zdaniom wartości logicznych. Nieformalne objaśnienie zasad logiki intuicjonistycznej posługuje się pojęciem konstrukcji. Zdanie jest uważane za prawdziwe, gdy można podać jego konstrukcję, tworzoną według następujących zasad (od nazwisk Brouwera, Heytinga i Kołmogorowa zwanych interpretacją BHK):

• Konstrukcja dla $\displaystyle \varphi \wedge \psi$ polega na podaniu konstrukcji dla $\displaystyle \varphi$ i konstrukcji dla $\displaystyle \psi$;
• Konstrukcja dla $\displaystyle \varphi \vee \psi$ polega na wskazaniu jednego ze składników $\displaystyle \varphi$, $\displaystyle \psi$ i podaniu konstrukcji dla tego składnika.
• Konstrukcja dla implikacji $\displaystyle \varphi \to \psi$ to metoda (funkcja) przekształcająca każdą konstrukcję przesłanki $\displaystyle \varphi$ w konstrukcję dla konkluzji $\displaystyle \psi$.
• Nie ma konstrukcji dla fałszu $\displaystyle \bot$.
• Konstrukcja dla $\displaystyle \forall x\,\varphi (x)$ to metoda, która każdej potencjalnej wartości $\displaystyle a$ zmiennej $\displaystyle x$ przypisuje konstrukcję dla $\displaystyle \varphi (a)$.
• Konstrukcja dla $\displaystyle \exists x\,\varphi (x)$ polega na wskazaniu pewnej wartości $\displaystyle a$ zmiennej $\displaystyle x$, oraz konstrukcji dla $\displaystyle \varphi (a)$.

Negacja intuicjonistyczna $\displaystyle \neg \varphi$ utożsamiana jest z implikacją $\displaystyle \varphi \to \bot$. A zatem

• Konstrukcja dla $\displaystyle \neg \varphi$ to metoda obracająca każdą ewentualną konstrukcję $\displaystyle \varphi$ w absurd ("rzecz, której nie ma").

Nie od rzeczy jest tu nastepująca uwaga: o konstrukcji dla $\displaystyle \varphi \to \psi$ można myśleć jak o funkcji typu $\displaystyle \varphi \to \psi$, bo przecież konstrukcjom dla $\displaystyle \varphi$ (obiektom "typu $\displaystyle \varphi$") przypisuje ona konstrukcje dla $\displaystyle \psi$, czyli obiekty "typu $\displaystyle \psi$". Za chwilę wrócimy do tej analogii.

Przykład 11.2

Konstrukcję dla formuły $\displaystyle p\to \neg \neg p$ możemy zapisać tak:

Przypuśćmy, że dana jest konstrukcja $\displaystyle C$ dla przesłanki $\displaystyle p$. Wtedy konstrukcja dla konkluzji $\displaystyle \neg \neg p$ (czyli dla $\displaystyle (p\to \bot )\to \bot$) jest następująca: daną konstrukcję dla formuły $\displaystyle p\to \bot$ należy zastosować do $\displaystyle C$.

Próba podania konstrukcji dla implikacji odwrotnej $\displaystyle \neg \neg p\to p$ natrafia jednak na nieprzezwyciężalną trudność. Aby wykorzystać daną konstrukcję dla $\displaystyle (p\to \bot )\to \bot$, musielibyśmy mieć konstrukcję dla $\displaystyle p\to \bot$, a skoro jej nie mamy, to założenie jest bezużyteczne.

Niemożliwe jest też wskazanie konstrukcji dla schematu $\displaystyle p\vee \neg p$, nie znając $\displaystyle p$ nie możemy bowiem wskazać żadnego z członów alternatywy.

Podobnie będzie na przykład z implikacją $\displaystyle \forall x(q\vee p(x))\to q\vee \forall x\,p(x)$. Konstrukcja przesłanki dla każdej wartości $\displaystyle a$ zmiennej $\displaystyle x$ generuje albo konstrukcję dla $\displaystyle q$ albo konstrukcję dla $\displaystyle p(a)$. Ale skorzystać z niej można tylko dla konkretnych wartości $\displaystyle a$. Tymczasem, aby podać konstrukcję dla konkluzji, musielibyśmy umieć podjąć krytyczną decyzję "w ciemno".

Proponujemy teraz Czytelnikowi wykonanie Ćwiczenia 2, a nastepnie próbę znalezienia konstrukcji dla formuł z Ćwiczenia 5.

Intuicjonistyczny rachunek zdań

Objaśnienia odwołujące się do pojęcia konstrukcji są tylko nieformalne. Ścisłą definicję logiki intuicjonistycznej może stanowić system wnioskowania, na przykład w stylu naturalnej dedukcji. Dla uproszczenia ograniczymy się tutaj do intuicjonistycznego rachunku zdań. System naturalnej dedukcji dla takiego rachunku, przedstawiony poniżej można uważać za uściślenie interpretacji BHK. Otrzymujemy go z systemu klasycznego (Sekcja 5.2) przez odrzucenie reguły PS.<ref name="czternascie"> Robimy to, zauważając z pewną satysfakcją, że właśnie ta reguła "nie pasuje" do pozostałych, bo odbiega swoją formą od zasady wprowadzania i eliminacji spójników.</ref>

$\displaystyle (\to$ -intro Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle ) \hspace{.2cm} \frac{\Delta,\varphi\vdash\psi}{\Delta\vdash\varphi\to\psi} \hspace{1cm} (\to } -elim Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle ) \hspace{.2cm} \frac{\Delta\vdash\varphi\to\psi\qquad \Delta\vdash\varphi}{\Delta\vdash\psi}}

$\displaystyle (\wedge$ -intro Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\varphi\qquad \Delta\vdash\psi}{\Delta\vdash\varphi\wedge\psi} \hspace{1cm} (\wedge } -elim Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle ) \hspace{.2cm}\frac{\Delta\vdash\varphi\wedge\psi}{\Delta\vdash\varphi} \hspace{1cm} (\wedge } -elim Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle ) \hspace{.2cm}\frac{\Delta\vdash\varphi\wedge\psi}{\Delta\vdash\psi}}

$\displaystyle (\vee$ -intro Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\varphi}{\Delta\vdash\varphi\vee\psi} \hspace{1cm} (\vee } -intro Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\psi}{\Delta\vdash\varphi\vee\psi} }

$\displaystyle (\vee$ -elim Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\varphi\vee\psi\qquad \Delta,\varphi\vdash\vartheta\qquad \Delta,\psi\vdash\vartheta}{\Delta\vdash\vartheta}}

Ciekawy jest sposób w jaki z klasycznego rachunku sekwentów (Sekcja 5.3) można otrzymać system dla logiki intuicjonistycznej. Otóż należy w tym celu ograniczyć liczbę formuł występujących po prawej stronie sekwentów do (co najwyżej) jednej, przy czym sekwent $\displaystyle \Gamma \vdash \$ z pustą prawą stroną można utożsamiać z sekwentem $\displaystyle \Gamma \vdash \bot$. Reguła $\displaystyle (\vee$ -prawa $\displaystyle )$ traci wtedy sens i trzeba ją zastąpić przez dwie reguły podobne do tych z Ćwiczenia 11 w Rozdziale 5. Pozostałe reguły pozostają w zasadzie bez zmian.

$\displaystyle (\to$ -lewa Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\varphi\hspace{1cm} \Delta,\psi\vdash\vartheta}{\Delta,\varphi\to\psi\vdash\vartheta} \hspace{1cm}(\to } -prawa Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta,\varphi\vdash\psi}{\Delta\vdash\varphi\to\psi}}

$\displaystyle (\wedge$ -lewa Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta,\varphi,\psi\vdash\vartheta}{\Delta,\varphi\wedge\psi\vdash\vartheta} \hspace{1cm} (\wedge } -prawa Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash \varphi\hspace{1cm} \Delta\vdash\psi}{\Delta\vdash\varphi\wedge\psi}}

$\displaystyle (\vee$ -lewa Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta, \varphi\vdash\vartheta\hspace{1cm} \Delta,\psi\vdash\vartheta}{\Delta, \varphi\vee\psi \vdash\vartheta} \hspace{1cm} \frac{\Delta\vdash \varphi}{\Delta\vdash \varphi\vee\psi}\hspace{.2cm}(\vee } -prawa Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash \psi}{\Delta\vdash \varphi\vee\psi}}

Intuicjonistyczny system dowodzenia w stylu Hilberta dla logiki zdaniowej, w której występuje tylko implikacja i fałsz, a negacja $\displaystyle \neg \varphi$ jest zdefiniowana jako $\displaystyle \varphi \to \bot$, otrzymamy bardzo łatwo: wystarczy usunąć aksjomat $\displaystyle \neg \neg \varphi \to \varphi$ z systemu klasycznego i dodać jeden nowy:

$(A3i)\;\;\displaystyle \bot \to \varphi$.

Ale aksjomaty (B1)-(B4) z Rozdziału 5 do logiki intuicjonistycznej nie pasują, bo nie zgadzają się z interpretacją BHK. Trzeba więc przyjąć aksjomaty z Ćwiczenia 2 do Rozdziału 6, które zamiast definiować koniunkcję i alternatywę, wyrażają ich najważniejsze własności.

$(D1)\;\;\displaystyle \varphi \to \varphi \vee \psi$;

$(D2)\;\;\displaystyle \psi \to \varphi \vee \psi$;

$(D3)\;\;\displaystyle (\varphi \to \vartheta )\wedge (\psi \to \vartheta )\to (\varphi \vee \psi \to \vartheta )$;

$(C1)\;\;\displaystyle \varphi \wedge \psi \to \varphi$;

$(C2)\;\;\displaystyle \varphi \wedge \psi \to \psi$;

$(C3)\;\;\displaystyle (\vartheta \to \varphi )\wedge (\vartheta \to \psi )\to (\vartheta \to \varphi \wedge \psi )$.

Fakt 11.3

Opisane powyżej intuicjonistyczne systemy dowodzenia (naturalna dedukcja, rachunek sekwentów oraz system Hilberta) są sobie równoważne: formuła $\displaystyle \varphi$ jest twierdzeniem dowolnego z tych systemów , gdy jest twierdzeniem każdego z pozostałych.

Dowód

Ćwiczenie.

Semantyka topologiczna

Jak już powiedzieliśmy, logika intuicjonistyczna różni się od klasycznej tym, że nie odwołuje się do pojęcia wartości logicznej, a formalna definicja jest syntaktyczna (przez system dowodzenia) a nie semantyczna. Okazuje się jednak, że intuicjonistyczny rachunek zdań ma ciekawą semantykę topologiczną. Stanowi ona uogólnienie semantyki klasycznego rachunku zdań z  Ćwiczenia 7 do Rozdziału 1. Różnica polega na tym, że znaczeniami formuł mogą być jedynie zbiory otwarte.

Definicja 11.4

Niech $\displaystyle {\mathcal {O}}$ będzie rodziną wszystkich podzbiorów otwartych zbioru liczb rzeczywistych $\displaystyle \mathbb {R}$. Dla $\displaystyle A\subseteq \mathbb {R}$, przez $\displaystyle {\rm {Int}}(A)$ oznaczymy wnętrze zbioru $\displaystyle A$, tj. największy zbiór otwarty zawarty w $\displaystyle A$. Wartościowaniem w zbiorze $\displaystyle {\mathcal {O}}$ nazwiemy dowolną funkcję $\displaystyle \varrho :ZZ\to {\mathcal {O}}$. Dla danego $\displaystyle \varrho$, możemy każdej formule zdaniowej przypisać wartość w $\displaystyle {\mathcal {O}}$:

• $\displaystyle \left\Vert \bot \right\Vert _{\varrho }=\emptyset$ oraz $\displaystyle \left\Vert \top \right\Vert _{\varrho }=\mathbb {R}$;
• $\displaystyle \left\Vert p\right\Vert _{\varrho }=\varrho (p)$, gdy $\displaystyle p$ jest symbolem zdaniowym;
• $\displaystyle \left\Vert \neg \varphi \right\Vert _{\varrho }={\rm {Int}}(\mathbb {R} -\left\Vert \varphi \right\Vert _{\varrho })$;
• Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle \left\Vert\varphi\vee\psi\right\Vert_\varrho=\left\Vert\varphi\right\Vert_\varrho}\cup \left\Vert\psi\right\Vert_\varrho} ;
• Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle \left\Vert\varphi\wedge\psi\right\Vert_\varrho=\left\Vert\varphi\right\Vert_\varrho}\cap \left\Vert\psi\right\Vert_\varrho}} ;
• $\displaystyle \left\Vert \varphi \to \psi \right\Vert \varrho ={\rm {Int}}((\mathbb {R} -\left\Vert \varphi \right\Vert _{\varrho })\cup \left\Vert \psi \right\Vert _{\varrho })$.

Powiemy, że formuła $\displaystyle \varphi$ jest prawdziwa w $\displaystyle \mathbb {R}$, gdy jej wartością jest cały zbiór $\displaystyle \mathbb {R}$.

Twierdzenie 11.5

Formuła rachunku zdań jest intuicjonistycznym twierdzeniem wtedy i tylko wtedy, gdy jest prawdziwa w $\displaystyle \mathbb {R}$.

Uwaga: Implikacja "tylko wtedy" w Twierdzeniu 11.5 zachodzi nie tylko dla liczb rzeczywistych, ale także dla dowolnej przestrzeni topologicznej.

Przykład 11.6

Aby się przekonać, że prawo wyłączonego środka nie jest twierdzeniem logiki intuicjonistycznej, przypuśćmy, że $\displaystyle \varrho (p)=(0,\infty )$. Wtedy $\displaystyle \Vert p\vee \neg p\Vert _{\varrho }=\mathbb {R} -\{0\}\neq \mathbb {R}$.

Jeśli zaś $\displaystyle \varrho (p)=\mathbb {R} -\{1\}$ to także $\displaystyle \Vert \neg \neg p\to p\Vert _{\varrho }=\mathbb {R} -\{1\}$, więc i formuła $\displaystyle \neg \neg p\to p$ nie jest intuicjonistycznym twierdzeniem.

Normalizacja dowodów

Wróćmy teraz do systemu naturalnej dedukcji dla intuicjonistycznego rachunku zdań. Dla uproszczenia ograniczmy się na razie do tzw. minimimalnej logiki implikacyjnej, tj. do formuł zbudowanych z pomocą samej implikacji. Przypuśćmy, że mamy taki dowód:

W tym dowodzie najpierw wprowadzamy implikację, a zaraz potem ją eliminujemy. Można jednak zrobić inaczej. Tam gdzie w części (2) dowodu używane jest założenie $\displaystyle \varphi$ można po prostu wstawić całą część (1). Chociaż rozmiary nowego dowodu mogą być większe (założenie $\displaystyle \varphi$ mogło być używane kilkakrotnie), to jednak jego struktura będzie prostsza. Docelowo możemy uzyskać dowód, w którym takie sytuacje jak na rysunku w ogóle nie występują. Taki dowód nazwiemy dowodem normalnym. Proces normalizacji dowodu jest podobny do procesu eliminacji cięcia, a dowody normalne mają podobne zalety jak dowody bez cięcia. W szczególności, wyszukiwanie dowodu dla danej formuły staje się łatwiejsze, jeśli można się ograniczyć do dowodów normalnych.

Lambda-termy z typami

Normalizacja dowodów ma bliski związek z rachunkiem lambda. Przypomnijmy tu podstawowe definicje.

Definicja 11.7

Przyjmijmy, że mamy pewien przeliczalny nieskończony zbior zmiennych przedmiotowych. Termy rachunku lambda (lambda-termy) określamy przez indukcję:

• Zmienne przedmiotowe są termami.
• Jesli $\displaystyle M$ i $\displaystyle N$ są termami, to math>\displaystyle (MN)</math> tez.
• Jesli $\displaystyle M$ jest termem i $\displaystyle x$ jest zmienną, to $\displaystyle (\lambda xM)$ jest termem.

Wyrażenie postaci $\displaystyle (MN)$ nazywamy aplikacją, a wyrażenie postaci $\displaystyle (\lambda xM)$ to $\displaystyle \lambda$-abstrakcja. Stosujemy nastepujące konwencje notacyjne:

- opuszczamy zewnętrzne nawiasy;

- aplikacja wiąże w lewo, tj. $\displaystyle MNP$ oznacza $\displaystyle (MN)P$;

- piszemy $\displaystyle \lambda x_{1}\ldots x_{n}.M$ zamiast $\displaystyle \lambda x_{1}(\ldots (\lambda x_{n}M)\cdots )$.

Uwaga: kropka w wyrażeniu $\displaystyle \lambda x_{1}\ldots x_{n}.M$ zastępuje lewy nawias, którego zasięg rozciąga się do końca wyrażenia $\displaystyle M$. Zwyczajowo używa się też notacji $\displaystyle \lambda x.M$.

Operator lambda-abstrakcji $\displaystyle \lambda$, podobnie jak kwantyfikator, wiąże zmienne, tj. wszystkie wystąpienia $\displaystyle x$ w wyrażeniu $\displaystyle \lambda xM$ uwaza się za związane. Zazwyczaj lambda-termy rozważa się z dokładnością do alfa-konwersji, tj. utożsamia się termy różniące się tylko zmiennymi związanymi.

Pominiemy tu ścisłą definicję podstawienia $\displaystyle M[N/x]$, która jest podobna do definicji stosowanej dla formuł z kwantyfikatorami.

Definicja 11.8

Relacja beta-redukcji to najmniejsza relacja w zbiorze lambda-termów, spełniająca warunki:

- $\displaystyle (\lambda xP)Q\to _{\beta }P[Q/x]$;

- jeśli $\displaystyle M\to _{\beta }M'$, to $\displaystyle MN\to _{\beta }M'N$, $\displaystyle NM\to _{\beta }NM'$ oraz $\displaystyle \lambda xM\to _{\beta }\lambda xM'$.

Inaczej mówiąc, $\displaystyle M\to _{\beta }M'$ zachodzi, gdy podterm termu $\displaystyle M$ postaci $\displaystyle (\lambda xP)Q$, czyli redeks, zostaje zamieniony na wynik podstawienia $\displaystyle P[Q/x]$. Znakiem $\displaystyle \hookrightarrow _{\beta }$ oznaczamy domknięcie przechodnio-zwrotne relacji $\displaystyle \to _{\beta }$. Mówimy, że term jest w postaci normalnej, gdy nie zawiera żadnego redeksu, tj. nie redukuje się.

Zauważmy tu analogię pomiędzy redukcją $\displaystyle (\lambda xP)Q\to _{\beta }P[Q/x]$ i wywołaniem procedury $\displaystyle P$, przy którym na miejsce parametru formalnego $\displaystyle x$ podstawiony zostaje parametr aktualny $\displaystyle Q$.

Definicja 11.9

Przyjmijmy pewien zbiór typów atomowych, który oznaczymy przez $\displaystyle ZZ$ (zbieżność oznaczeń jest nieprzypadkowa). Powiemy teraz, że

• Typy atomowe są typami;
• Jeśli $\displaystyle \sigma$ i $\displaystyle \tau$ są typami, to $\displaystyle \sigma \to \tau$ jest typem.

A zatem nasze typy to po prostu formuły zdaniowe zbudowane przy pomocy samej implikacji. Stosujemy taką konwencję, że strzałka jest łączna w prawo, tj. napis $\displaystyle \sigma \to \tau \to \rho$ oznacza $\displaystyle \sigma \to (\tau \to \rho )$.

Przez otoczenie typowe rozumiemy zbiór deklaracji postaci $\displaystyle (x:\tau )$, gdzie $\displaystyle x$ jest zmienną (przedmiotową) a $\displaystyle \tau$ jest typem. Żądamy przy tym, aby otoczenie było funkcją, tj. aby jedna zmienna nie była deklarowana dwa razy. Przez $\displaystyle \Gamma (x{:}\sigma )$ oznaczamy otoczenie określone tak:

$\displaystyle \Gamma (x{:}\sigma )(y)={\begin{cases}\Gamma (y),&{\mbox{jeśli }}y\neq x;\\\sigma ,&{\mbox{w przeciwnym przypadku.}}\end{cases}}$

Lambda-termom można teraz przypisywać typy. Napis $\displaystyle M:\tau$ stwierdza, że $\displaystyle M$ jest termem typu $\displaystyle \tau$. Interpratecja operatora $\displaystyle \to$ jest taka: Term typu $\displaystyle \tau \to \sigma$ zaaplikowany do argumentu typu $\displaystyle \tau$ daje wynik typu $\displaystyle \sigma$. Ponieważ typ termu może zależeć od typów jego zmiennych wolnych, więc nasz system przypisania typów wyprowadza asercje postaci $\displaystyle \Gamma \vdash M:\tau$, gdzie $\displaystyle \Gamma$ jest otoczeniem typowym.

Aksjomat: $\;\;\displaystyle \Gamma (x:\sigma )\vdash x:\sigma$

Reguły:

$\displaystyle {\frac {\Gamma (x{:}\sigma )\vdash M:\tau }{\Gamma \vdash (\lambda x\,M):\sigma \to \tau }}(Abs)\qquad {\frac {\Gamma \vdash M:\sigma \to \tau \qquad \Gamma \vdash N:\sigma }{(MN):\tau }}(App)$

Ważne, że takie przypisanie typu zachowuje się przy beta-redukcji.

Fakt 11.10

Jeśli $\displaystyle \Gamma \vdash M:\tau$ oraz $\displaystyle M\to _{\beta }N$, to $\displaystyle \Gamma \vdash N:\tau$.

Izomorfizm Curry'ego-Howarda (formuły-typy)

Uderzające podobieństwo pomiędzy regułami przypisania typów i regułami dowodzenia w naturalnej dedukcji bywa nazywane izomorfizmem Curry'ego-Howarda. Lambda-termy z typami prostymi, to w istocie to samo co dowody w logice minimalnej. Bez wchodzenia w szczegóły sformułujmy tu najważniejszą konsekwencję tego izomorfizmu.

Fakt 11.11

Formuła implikacyjna $\displaystyle \varphi$ jest twierdzeniem intuicjonistycznym , gdy istnieje zamknięty (tj. bez zmiennych wolnych) lambda-term typu $\displaystyle \varphi$.

Związek pomiędzy dowodami i lambda-termami staje się jeszcze bardziej interesujący, gdy zauważymy podobieństwo dowodu ze strony 84 do beta-redeksu postaci $\displaystyle (\lambda xP)Q$:

Normalizacja tamtego dowodu daje w wyniku dowód, którego odpowiednikiem jest term $\displaystyle P[Q/x]$. Ewaluacja lambda-termów (beta-redukcja) ściśle więc reprezentuje zjawisko normalizacji dowodów. W szczególności okazuje się, że dowodom normalnym odpowiadają termy w postaci normalnej. Ma to niebagatelne znaczenie w związku z następującym twierdzeniem, którego (nietrywialny) dowód pomijamy.

Twierdzenie 11.12

Każdy term z typami prostymi można zredukować do postaci normalnej.

Wniosek z Twierdzeń 11.10-11.12 jest taki: aby ustalić czy formuła $\displaystyle \varphi$ ma dowód, należy zbadać, czy istnieje zamknięty term typu $\displaystyle \varphi$ w postaci normalnej. W ten sposób można np. rozstrzygnąć, które z formuł w Ćwiczeniu 6 są twierdzeniami intuicjonistycznymi.

Technika wyszukiwania dowodu danej formuły za pomocą konstrukcji odpowiedniego lambda-termu daje się uogólnić dla języków znacznie bogatszych niż zdaniowa logika implikacyjna i znajduje zastosowanie w systemach wspomagających dowodzenie, takich jak system Coq.

Przykład 11.13

W myśl interpretacji BHK, konstrukcją (dowodem) koniunkcji $\displaystyle \varphi \wedge \psi$ jest para konstrukcji, jedna "typu $\displaystyle \varphi$" a druga "typu $\displaystyle \psi$". W naturalnej dedukcji, reguła wprowadzania koniunkcji odpowiada tworzeniu takiej pary, a reguła eliminacji koniunkcji reprezentuje rzutowanie na jedną ze współrzędnych. A więc koniunkcja tak naprawdę to samo co produkt kartezjański. Jeśli rozszerzymy rachunek lambda o pary (rekordy) i rzutowania, będziemy mogli napisać takie reguły przypisania typów zawierających znak koniunkcji.

$\displaystyle {\frac {\Gamma \vdash M:\varphi \qquad \Gamma \vdash N:\psi }{\Gamma \vdash \langle M,N\rangle :\varphi \wedge \psi }}\qquad \qquad {\frac {\Gamma \vdash M:\varphi \wedge \psi }{\Gamma \vdash \pi _{1}(M):\varphi }}\qquad \qquad {\frac {\Gamma \vdash M:\varphi \wedge \psi }{\Gamma \vdash \pi _{2}(M):\psi }}$

Przypisy

<references/>