Logika dla informatyków/Logika intuicjonistyczna: Różnice pomiędzy wersjami

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
m
Linia 97: Linia 97:
 
System naturalnej dedukcji dla takiego rachunku, przedstawiony poniżej
 
System naturalnej dedukcji dla takiego rachunku, przedstawiony poniżej
 
można uważać za uściślenie interpretacji BHK. Otrzymujemy go z systemu  
 
można uważać za uściślenie interpretacji BHK. Otrzymujemy go z systemu  
klasycznego [[Logika dla informatyków/Paradygmaty dowodzenia#sekcja5.2|(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>  
+
klasycznego [[Logika dla informatyków/Paradygmaty dowodzenia#sekcja5.2|(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>  
  
 
<center><math>\displaystyle (\to </math> -intro <math>\displaystyle  ) \hspace{.2cm}
 
<center><math>\displaystyle (\to </math> -intro <math>\displaystyle  ) \hspace{.2cm}
Linia 253: Linia 253:
 
założenie <math>\displaystyle \varphi</math> można po prostu wstawić całą część (1).
 
założenie <math>\displaystyle \varphi</math> można po prostu wstawić całą część (1).
 
Chociaż rozmiary nowego dowodu mogą być
 
Chociaż rozmiary nowego dowodu mogą być
większe (założenie <math>\displaystyle \varphi</math> mogło być używane kilkakrotnie) to jednak  
+
większe (założenie <math>\displaystyle \varphi</math> mogło być używane kilkakrotnie), to jednak  
 
jego struktura będzie prostsza. Docelowo możemy uzyskać dowód, w którym  
 
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
 
takie sytuacje jak na rysunku w ogóle nie występują. Taki dowód nazwiemy
Linia 267: Linia 267:
  
 
{{definicja|11.7||
 
{{definicja|11.7||
Przyjmijmy, że mamy pewien przeliczalny nieskonczony zbior ''zmiennych przedmiotowych''. Termy rachunku lambda (''lambda-termy'') określamy przez indukcję:
+
Przyjmijmy, że mamy pewien przeliczalny nieskończony zbior ''zmiennych przedmiotowych''. Termy rachunku lambda (''lambda-termy'') określamy przez indukcję:
 
* Zmienne przedmiotowe są termami.
 
* Zmienne przedmiotowe są termami.
 
* Jesli <math>\displaystyle M</math> i <math>\displaystyle N</math> są termami, to math>\displaystyle (MN)</math> tez.
 
* Jesli <math>\displaystyle M</math> i <math>\displaystyle N</math> są termami, to math>\displaystyle (MN)</math> tez.
Linia 296: Linia 296:
  
 
{{definicja|11.8||
 
{{definicja|11.8||
Relacja ''beta-redukcji'' to najmniejsza relacja w zbiorze lambda-termow, spełniająca warunki:
+
Relacja ''beta-redukcji'' to najmniejsza relacja w zbiorze lambda-termów, spełniająca warunki:
  
 
- <math>\displaystyle (\lambda x P)Q \to_\beta P[Q/x]</math>;
 
- <math>\displaystyle (\lambda x P)Q \to_\beta P[Q/x]</math>;
  
- jesli <math>\displaystyle M\to_\beta M'</math>, to <math>\displaystyle MN \to_\beta M'N</math>, <math>\displaystyle NM \to_\beta NM'</math> oraz <math>\displaystyle \lambda x M \to_\beta \lambda x M'</math>.
+
- jeśli <math>\displaystyle M\to_\beta M'</math>, to <math>\displaystyle MN \to_\beta M'N</math>, <math>\displaystyle NM \to_\beta NM'</math> oraz <math>\displaystyle \lambda x M \to_\beta \lambda x M'</math>.
  
Inaczej mówiąc, <math>\displaystyle M\to_\beta M'</math> zachodzi gdy podterm termu&nbsp;<math>\displaystyle M</math> postaci
+
Inaczej mówiąc, <math>\displaystyle M\to_\beta M'</math> zachodzi, gdy podterm termu&nbsp;<math>\displaystyle M</math> postaci
 
<math>\displaystyle (\lambda x P)Q</math>, czyli ''redeks'', zostaje zamieniony na wynik
 
<math>\displaystyle (\lambda x P)Q</math>, czyli ''redeks'', zostaje zamieniony na wynik
 
podstawienia <math>\displaystyle P[Q/x]</math>. Znakiem <math>\displaystyle \hookrightarrow_\beta</math> oznaczamy domknięcie  
 
podstawienia <math>\displaystyle P[Q/x]</math>. Znakiem <math>\displaystyle \hookrightarrow_\beta</math> oznaczamy domknięcie  

Wersja z 09:35, 30 paź 2006

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ę , niezależnie od tego czy zdanie 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 i , że jest liczbą wymierną.

Dowód

Jeśli jest wymierne, to można przyjąć , w przeciwnym przypadku niech i .

End of proof.gif

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 .

Dowód 2

Dla oraz mamy .

End of proof.gif

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 polega na podaniu konstrukcji dla i konstrukcji dla ;
  • Konstrukcja dla polega na wskazaniu jednego ze składników , i podaniu konstrukcji dla tego składnika.
  • Konstrukcja dla implikacji to metoda (funkcja) przekształcająca każdą konstrukcję przesłanki  w konstrukcję dla konkluzji .
  • Nie ma konstrukcji dla fałszu .
  • Konstrukcja dla to metoda, która każdej potencjalnej wartości zmiennej przypisuje konstrukcję dla .
  • Konstrukcja dla polega na wskazaniu pewnej wartości zmiennej , oraz konstrukcji dla .


Negacja intuicjonistyczna utożsamiana jest z implikacją . A zatem

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


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

Przykład 11.2

Konstrukcję dla formuły możemy zapisać tak:

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

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

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

Podobnie będzie na przykład z implikacją . Konstrukcja przesłanki dla każdej wartości zmiennej generuje albo konstrukcję dla albo konstrukcję dla . Ale skorzystać z niej można tylko dla konkretnych wartości . 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>

-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}}


-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}}


-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} }


-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 z pustą prawą stroną można utożsamiać z sekwentem . Reguła -prawa 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.


-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}}


-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}}


-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 jest zdefiniowana jako , otrzymamy bardzo łatwo: wystarczy usunąć aksjomat z systemu klasycznego i dodać jeden nowy:

.

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.

;

;

;

;

;

.

Fakt 11.3

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

Dowód

Ćwiczenie. End of proof.gif

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 będzie rodziną wszystkich podzbiorów otwartych zbioru liczb rzeczywistych . Dla , przez oznaczymy wnętrze zbioru , tj. największy zbiór otwarty zawarty w . Wartościowaniem w zbiorze  nazwiemy dowolną funkcję . Dla danego , możemy każdej formule zdaniowej przypisać wartość w :

  • oraz ;
  • , gdy jest symbolem zdaniowym;
  • ;
  • 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}} ;
  • .

Powiemy, że formuła jest prawdziwa, gdy jej wartością jest cały zbiór .

Twierdzenie 11.5

Formuła rachunku zdań jest intuicjonistycznym twierdzeniem wtedy i tylko wtedy, gdy jest prawdziwa w .

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 . Wtedy .

Jeśli zaś to także , więc i formuła 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:

Dowód11.2.PNG

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 można po prostu wstawić całą część (1). Chociaż rozmiary nowego dowodu mogą być większe (założenie 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 i są termami, to math>\displaystyle (MN)</math> tez.
  • Jesli jest termem i jest zmienną, to jest termem.

Wyrażenie postaci nazywamy aplikacją, a wyrażenie postaci to -abstrakcja. Stosujemy nastepujące konwencje notacyjne:

- opuszczamy zewnętrzne nawiasy;
- aplikacja wiąże w lewo, tj. oznacza ;
- piszemy zamiast .

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

Operator lambda-abstrakcji , podobnie jak kwantyfikator, wiąże zmienne, tj. wszystkie wystąpienia  w wyrażeniu  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 , 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:

- ;

- jeśli , to , oraz .

Inaczej mówiąc, zachodzi, gdy podterm termu  postaci , czyli redeks, zostaje zamieniony na wynik podstawienia . Znakiem oznaczamy domknięcie przechodnio-zwrotne relacji . Mówimy, że term jest w postaci normalnej, gdy nie zawiera żadnego redeksu, tj. nie redukuje się.

Zauważmy tu analogię pomiędzy redukcją i wywołaniem procedury , przy którym na miejsce parametru formalnego podstawiony zostaje parametr aktualny .


Definicja 11.9

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

  • Typy atomowe są typami;
  • Jeśli i są typami, to 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 oznacza .

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

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

Aksjomat:

Reguły:

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

Fakt 11.10

Jeśli oraz , to .

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 jest twierdzeniem intuicjonistycznym , gdy istnieje zamknięty (tj. bez zmiennych wolnych) lambda-term typu .

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 :

Dowódstr84.PNG

Normalizacja tamtego dowodu daje w wyniku dowód, którego odpowiednikiem jest term . 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 ma dowód, należy zbadać, czy istnieje zamknięty term typu  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 jest para konstrukcji, jedna "typu " a druga "typu ". 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.


Przypisy

<references/>