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ł Uzupelnic lopolski|). Inną konsekwencją dwuwartościowości logiki klasycznej jest prawo wyłączonego środka. Akceptujemy alternatywę $p\vee \mathrm{\neg }p$, niezależnie od tego czy zdanie $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

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

Dowód

Jeśli ${\sqrt{2}}^{\sqrt{2}}$ jest wymierne, to można przyjąć $x=y=\sqrt{2}$,  niech $x={\sqrt{2}}^{\sqrt{2}}$ i $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 Uzupelnic izwierciadlo|.

Dowód 2: Dla $x=\sqrt{2}$ oraz $y=2{\log }_{2}3$ mamy $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 $\phi \wedge \psi$ polega na podaniu

konstrukcji dla $\phi$ i konstrukcji dla $\psi$;

• Konstrukcja dla $\phi \vee \psi$ polega na wskazaniu jednego

ze składników $\phi$, $\psi$ i podaniu konstrukcji dla tego składnika.

• Konstrukcja dla implikacji $\phi \to \psi$ to metoda (funkcja)

przekształcająca każdą konstrukcję przesłanki $\phi$ w konstrukcję dla konkluzji $\psi$.

• Nie ma konstrukcji dla fałszu $\mathrm{\perp }$.
• Konstrukcja dla $\mathrm{\forall }x\phi (x)$ to metoda, która każdej

potencjalnej wartości $a$ zmiennej $x$ przypisuje konstrukcję dla $\phi (a)$.

• Konstrukcja dla $\mathrm{\exists }x\phi (x)$ polega na wskazaniu pewnej

wartości $a$ zmiennej $x$, oraz konstrukcji dla $\phi (a)$.

Negacja intuicjonistyczna $\mathrm{\neg }\phi$ utożsamiana jest z implikacją $\phi \to \mathrm{\perp }$. A zatem

• Konstrukcja dla $\mathrm{\neg }\phi$ to metoda

obracająca każdą ewentualną konstrukcję $\phi$ w absurd

("rzecz, której nie ma").

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

Przykład

Konstrukcję 

dla formuły $p\to \mathrm{\neg }\mathrm{\neg }p$ możemy zapisać tak:

Przypuśćmy, że dana jest konstrukcja $C$ dla przesłanki $p$.

Wtedy konstrukcja dla konkluzji $\mathrm{\neg }\mathrm{\neg }p$ (czyli dla $(p\to \mathrm{\perp })\to \mathrm{\perp }$) jest następująca: daną konstrukcję dla formuły $p\to \mathrm{\perp }$ należy zastosować do $C$.

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

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

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

Proponujemy teraz Czytelnikowi wykonanie Ćwiczenia Uzupelnic szust|, a nastepnie próbę znalezienia konstrukcji dla formuł z Ćwiczenia Uzupelnic dowanny|.

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 Uzupelnic sysnatded|) przez odrzucenie reguły PS.{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.}

Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle (\arr } -intro Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle ) \hspace{.2cm} \frac{\Delta,\varphi\vdash\psi}{\Delta\vdash\varphi\arr\psi} \hspace{1cm} (\arr } -elim Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle ) \hspace{.2cm} \frac{\Delta\vdash\varphi\arr\psi\odstep \Delta\vdash\varphi}{\Delta\vdash\psi}} $(\wedge$ -intro Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\varphi\odstep \Delta\vdash\psi}{\Delta\vdash\varphi\wedge\psi} \hspace{1cm} (\wedge } -elim Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle ) \hspace{.2cm}\frac{\Delta\vdash\varphi\wedge\psi}{\Delta\vdash\varphi} \hspace{1cm} (\wedge } -elim Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle ) \hspace{.2cm}\frac{\Delta\vdash\varphi\wedge\psi}{\Delta\vdash\psi}} $(\vee$ -intro Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\varphi}{\Delta\vdash\varphi\vee\psi} \hspace{1cm} (\vee } -intro Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\psi}{\Delta\vdash\varphi\vee\psi} } $(\vee$ -elim Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\varphi\vee\psi\odstep \Delta,\varphi\vdash\vartheta\odstep \Delta,\psi\vdash\vartheta}{\Delta\vdash\vartheta}}

Ciekawy jest sposób w jaki z klasycznego rachunku sekwentów (Sekcja Uzupelnic rachseq|) 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 $\mathrm{\Gamma }⊢$ z pustą prawą stroną można utożsamiać z sekwentem $\mathrm{\Gamma }⊢\mathrm{\perp }$. Reguła $(\vee$ -prawa $)$ traci wtedy sens i trzeba ją zastąpić przez dwie reguły podobne do tych z Ćwiczenia Uzupelnic prawa-addytywna| w Rozdziale Uzupelnic paradygmaty|. Pozostałe reguły pozostają w zasadzie bez zmian.

Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle (\arr } -lewa Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\varphi\hspace{1cm} \Delta,\psi\vdash\vartheta}{\Delta,\varphi\arr\psi\vdash\vartheta} \hspace{1cm}(\arr } -prawa Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta,\varphi\vdash\psi}{\Delta\vdash\varphi\arr\psi}} $(\wedge$ -lewa Parser nie mógł rozpoznać (błąd składni): {\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ć (błąd składni): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash \varphi\hspace{1cm} \Delta\vdash\psi}{\Delta\vdash\varphi\wedge\psi}} $(\vee$ -lewa Parser nie mógł rozpoznać (błąd składni): {\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ć (błąd składni): {\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 $\mathrm{\neg }\phi$ jest zdefiniowana jako $\phi \to \mathrm{\perp }$, otrzymamy bardzo łatwo: wystarczy usunąć aksjomat $\mathrm{\neg }\mathrm{\neg }\phi \to \phi$ z systemu klasycznego i dodać jeden nowy:

 (A3i)  $\mathrm{\perp }\to \phi$.

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

 =   0pt 

(D1)

$\phi \to \phi \vee \psi$;

(D2)

$\psi \to \phi \vee \psi$;

(D3)

$(\phi \to \vartheta )\wedge (\psi \to \vartheta )\to (\phi \vee \psi \to \vartheta )$;

(C1)

$\phi \wedge \psi \to \phi$;

(C2)

$\phi \wedge \psi \to \psi$;

(C3)

$(\vartheta \to \phi )\wedge (\vartheta \to \psi )\to (\vartheta \to \phi \wedge \psi )$.

Fakt

Opisane powyżej intuicjonistyczne systemy dowodzenia (naturalna dedukcja, rachunek sekwentów oraz system Hilberta) są sobie równoważne: formuła $\phi$ 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 Uzupelnic krecic| do Rozdziału Uzupelnic aleksander|. Różnica polega na tym, że znaczeniami formuł mogą być jedynie zbiory otwarte.

Definicja

Niech Parser nie mógł rozpoznać (nieznana funkcja „\Oh”): {\displaystyle \displaystyle \Oh} będzie rodziną wszystkich podzbiorów otwartych zbioru liczb rzeczywistych Parser nie mógł rozpoznać (nieznana funkcja „\RR”): {\displaystyle \displaystyle \RR} . Dla Parser nie mógł rozpoznać (nieznana funkcja „\RR”): {\displaystyle \displaystyle A\subseteq\RR} , przez $\mathrm{I}\mathrm{n}\mathrm{t}(A)$ oznaczymy wnętrze zbioru $A$, tj. największy zbiór otwarty zawarty w $A$. Wartościowaniem w zbiorze Parser nie mógł rozpoznać (nieznana funkcja „\Oh”): {\displaystyle \displaystyle \Oh} nazwiemy dowolną funkcję Parser nie mógł rozpoznać (nieznana funkcja „\zmz”): {\displaystyle \displaystyle \varrho:\zmz\to\Oh} . Dla danego $\varrho$, możemy każdej formule zdaniowej przypisać wartość w Parser nie mógł rozpoznać (nieznana funkcja „\Oh”): {\displaystyle \displaystyle \Oh} :

• Parser nie mógł rozpoznać (nieznana funkcja „\wfz”): {\displaystyle \displaystyle \wfz\bot\varrho=\emptyset} oraz Parser nie mógł rozpoznać (nieznana funkcja „\wfz”): {\displaystyle \displaystyle \wfz\top\varrho=\RR} ;
• Parser nie mógł rozpoznać (nieznana funkcja „\wfz”): {\displaystyle \displaystyle \wfz{p}{\varrho}=\varrho(p)} , gdy $p$ jest symbolem zdaniowym;
• Parser nie mógł rozpoznać (nieznana funkcja „\wfz”): {\displaystyle \displaystyle \wfz{\neg\varphi}\varrho= {\rm Int}(\RR-\wfz{\varphi}\varrho)} ;
• Parser nie mógł rozpoznać (nieznana funkcja „\wfz”): {\displaystyle \displaystyle \wfz{\varphi\vee\psi}{\varrho}=\wfz{\varphi}{\varrho}\cup \wfz{\psi}{\varrho}} ;
• Parser nie mógł rozpoznać (nieznana funkcja „\wfz”): {\displaystyle \displaystyle \wfz{\varphi\wedge\psi}{\varrho}=\wfz{\varphi}{\varrho}\cap \wfz{\psi}{\varrho}} ;
• Parser nie mógł rozpoznać (nieznana funkcja „\wfz”): {\displaystyle \displaystyle \wfz{\varphi\to\psi}{\varrho}= {\rm Int}((\RR-\wfz{\varphi}\varrho) \cup\wfz\psi\varrho)} .

Powiemy, że formuła $\phi$ jest prawdziwa w Parser nie mógł rozpoznać (nieznana funkcja „\RR”): {\displaystyle \displaystyle \RR} , gdy jej wartością jest cały zbiór Parser nie mógł rozpoznać (nieznana funkcja „\RR”): {\displaystyle \displaystyle \RR} .

Twierdzenie

Formuła rachunku zdań jest intuicjonistycznym twierdzeniem, , gdy jest prawdziwa w Parser nie mógł rozpoznać (nieznana funkcja „\RR”): {\displaystyle \displaystyle \RR} .

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

Przykład

Aby się przekonać, że prawo wyłączonego środka nie jest twierdzeniem logiki intuicjonistycznej, przypuśćmy, że $\varrho (p)=(0,\mathrm{\infty })$. Wtedy Parser nie mógł rozpoznać (nieznana funkcja „\wfz”): {\displaystyle \displaystyle \wfz{p\vee\neg p}\varrho=\RR-\{0\}\neq \RR} .

Jeśli zaś Parser nie mógł rozpoznać (nieznana funkcja „\RR”): {\displaystyle \displaystyle \varrho(p)= \RR-\{1\}} to także Parser nie mógł rozpoznać (nieznana funkcja „\wfz”): {\displaystyle \displaystyle \wfz{\neg\neg p\to p}\varrho=\RR-\{1\}} , więc i formuła $\mathrm{\neg }\mathrm{\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:

   {(1)} =   1.2ex
                   =   3
                  {}
   
       {(2)} =   1.2ex
                   =   3
                  {,}
       
           {}
       {({}{ I})}
   
   {({}{ E})}

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 $\phi$ można po prostu wstawić całą część (1). Chociaż rozmiary nowego dowodu mogą być większe (założenie $\phi$ 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

Przyjmijmy, że mamy pewien przeliczalny nieskonczony 

zbior zmiennych przedmiotowych. Termy rachunku lambda (lambda-termy) określamy przez indukcję:

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

  jest termem.

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

-- opuszczamy zewnętrzne nawiasy;
-- aplikacja wiąze w lewo, tj. $MNP$ oznacza $(MN)P$;
-- piszemy $\lambda x_1\dots x_n.M$ zamiast $\lambda x_1(\dots (\lambda x_{n}M)\cdots )$.

Uwaga: kropka w wyrażeniu $\lambda x_1\dots x_n.M$ zastępuje lewy nawias, którego zasięg rozciąga się do końca wyrażenia $M$. Zwyczajowo używa się też notacji $\lambda x.M$.

Operator lambda-abstrakcji $\lambda$, podobnie jak kwantyfikator, wiąze zmienne, tj. wszystkie wystąpienia $x$ w wyrażeniu $\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 $M[N/x]$, która jest podobna do definicji stosowanej dla formuł z kwantyfikatorami.

Definicja

Relacja beta-redukcji to najmniejsza relacja 

w zbiorze lambda-termow, spełniająca warunki:

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

-- jesli $M{\to }_{\beta }{M}^{\prime }$, to $MN{\to }_{\beta }{M}^{\prime }N$, $NM{\to }_{\beta }N{M}^{\prime }$ oraz

  $\lambda xM{\to }_{\beta }\lambda x{M}^{\prime }$.

Inaczej mówiąc, $M{\to }_{\beta }{M}^{\prime }$ zachodzi gdy podterm termu $M$ postaci $(\lambda xP)Q$, czyli redeks, zostaje zamieniony na wynik podstawienia $P[Q/x]$. Znakiem Parser nie mógł rozpoznać (nieznana funkcja „\rarrow”): {\displaystyle \displaystyle \rarrow_\beta} oznaczamy domknięcie przechodnio-zwrotne relacji ${\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ą $(\lambda xP)Q{\to }_{\beta }P[Q/x]$ i wywołaniem procedury $P$, przy którym na miejsce parametru formalnego $x$ podstawiony zostaje parametr aktualny $Q$.

Definicja

Przyjmijmy pewien zbiór 

typów atomowych, który oznaczymy przez Parser nie mógł rozpoznać (nieznana funkcja „\zmz”): {\displaystyle \displaystyle \zmz} (zbieżność oznaczeń jest nieprzypadkowa). Powiemy teraz, że

• Typy atomowe są typami;
• Jeśli $\sigma$ i $\tau$ są typami, to $\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 $\sigma \to \tau \to \rho$ oznacza $\sigma \to (\tau \to \rho )$.

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

Parser nie mógł rozpoznać (nieznana funkcja „\przypadki”): {\displaystyle \displaystyle \Gamma(x{:}\sigma)(y) = \przypadki{\Gamma(y)}{} y = xParser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle }{\sigma}}

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

Aksjomat: $\mathrm{\Gamma }(x:\sigma )⊢x:\sigma$

Reguły:

Parser nie mógł rozpoznać (nieznana funkcja „\prooftree”): {\displaystyle \displaystyle \prooftree\Gamma(x{:}\sigma)\vdash M:\tau\justifies                   \Gamma\vdash(\lambda x\, M):\sigma\to\tau                  \using{\rm(Abs)}\endprooftree\displaystyle \prooftree\Gamma\vdash M: \sigma\to\tau\qquad\Gamma\vdash N: \sigma                 \justifies (MN) : \tau\using{\rm(App)}\endprooftree}

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

Fakt

Jeśli $\mathrm{\Gamma }⊢M:\tau$ oraz $M{\to }_{\beta }N$, to 

$\mathrm{\Gamma }⊢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

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

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

   {(1)} =   1.2ex
                   =   3
                  { Q: }
   
       {(2)} =   1.2ex
                   =   3
                  {,x{:} P:}
       
           { xP:}
       {(Abs)}
   
   ( xP)Q:{(App)}

Normalizacja tamtego dowodu daje w wyniku dowód, którego odpowiednikiem jest term $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

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

Wniosek z Twierdzeń Uzupelnic zrury|--Uzupelnic puscil| jest taki: aby ustalić czy formuła $\phi$ ma dowód, należy zbadać, czy istnieje zamknięty term typu $\phi$ w postaci normalnej. W ten sposób można np. rozstrzygnąć, które z formuł w Ćwiczeniu Uzupelnic wprawo| 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

W myśl interpretacji BHK, konstrukcją (dowodem) koniunkcji $\phi \wedge \psi$ jest para konstrukcji, jedna "typu $\phi$" a druga "typu $\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.

Parser nie mógł rozpoznać (nieznana funkcja „\prooftree”): {\displaystyle \displaystyle \prooftree\Gamma\vdash M:\varphi\qquad\Gamma\vdash N:\psi\justifies \Gamma\vdash\<M,N\>:\varphi\wedge\psi\endprooftree\qquad\qquad \prooftree\Gamma\vdash M:\varphi\wedge\psi\justifies \Gamma\vdash \pi_1(M):\varphi\endprooftree\qquad\qquad \prooftree\Gamma\vdash M:\varphi\wedge\psi\justifies \Gamma\vdash \pi_2(M):\psi\endprooftree}