Intuicjonistyczny rachunek zdań

Zadanie 1 z laboratorium z Coqa. Termin wykonania: 28 marca 2002
Zadanie ma na celu wymodelowanie w Coqu intuicjonistycznego rachunku zdań wraz z semantyką Kripkego i systemem dowodzenia -- gentzenowskim rachunkiem sekwentów. Udowodnimy (udowodnicie :-) poprawność systemu formalnego względem tej semantyki oraz napiszemy funkcję tłumaczącą model formuł rachunku zdań na formuły Coqa.

1   Formuły rachunku zdań.

Mając dany zbior zmiennych X, zbiór formuł F definiujemy następująco:
F ::=  X   |   ^   |   FÚ F   |   FŮ F   |   F Ž F

2   Semantyka Kripkego.

Strukturą Kripkego nazywamy trójkę (G,Ł,|=) spełniającą następujące warunki: W powyższej trójce G zwane jest zbiorem światów, relacja Ł to relacja następstwa światów, gdzie g Ł h oznacza intuicyjnie, że h jest możliwą przyszłością dla g, lub po prostu następnikiem g. Warunek trzeci powyższej definicji oznacza, że jeśli zmienna zdaniowa x wystąpi w danym świecie, to wystąpi również we wszystkich jego następnikach.

Określimy teraz relację spełniania, która dla struktury Kripkego K=(G,Ł,|=) mówi, kiedy w strukturze K w stanie gÎ G spełniona jest formuła F, co (lekko nadużywając notacji) oznaczać będziemy przez K,g |= F lub po prostu g |= F. Relacja ta określona jest przez indukcję po budowie F:

Jeśli mówimy, że w K spełniona jest formuła F (co zapisujemy K|= F), to oznacza to, że jest ona spełniona w każdym świecie K. Zapis |= F oznacza, że F jest tautologią intuicjonistycznego rachunku zdań, czyli, że jest prawdziwe w każdej strukturze Kripkego (dla każdego K zachodzi K|= V).

3   Intuicjonistyczny rachunek sekwentów Gentzena

Sekwent to para, złożona ze zbioru formuł oraz formuły, zapisywana G |- F. Intuicjonistyczny rachunek sekwentów Gentzena zawiera jeden aksjomat oraz dla każdego spójnika logicznego, odpowiadające mu reguły lewe i prawe, mówiące jak taki spójnik uzyskać odpowiednio po lewej i prawej strone |-.

Uwaga! Notacja G,A oznacza tak naprawdę G Č {A} i nic nie mówi o tym, czy A Î G, czy nie!
  Aksjomat    G, A |- A
  Reguły:     
 
^-lewa   
G, ^ |- A
 
Ú-lewa   
G, A |- C    G, B |- C
G, A Ú B |- C
       Ú-prawa1   
G |- A
G |- AÚ B
   Ú-prawa2   
G |- B
G |- AÚ B
 
Ů-lewa1   
G, A |- C
G, A Ů B |- C
   Ů-lewa2   
G, B |- C
G, A Ů B |- C
       Ů-prawa   
G |- A    G |- B
G |- AŮ B
 
Ž-lewa   
G, B |- C    G |- A
G, AŽ B |- C
       Ž-prawa   
G, A |- B
G |- A Ž B
Jeżeli zachodzi |- A, to mówimy, że A jest twierdzeniem.

4   Polecenia

  1. Sformalizować w Coqu typ reprezentujący formuły rachunku zdań.
  2. Sformalizować semantykę Kripkego oraz podać kilka przykładów ciekawych formuł oraz ciekawych struktur, w ktorych te formuły są spełnione (i udowodnić to w Coqu).
  3. Sformalizować rachunek sekwentów Gentzena, podać wyprowadzenie sekwentu
    |- ((p Ú (pŽ^))Ž^)Ž^1 oraz kilku innych twierdzeń intuicjonistycznego rachunku zdań.
  4. Udowodnić poprawność systemu dowodzenia względem podanej semantyki, tj.
    Dla dowolnej formuły F, jeśli |- F, to|= F
  5. Napisać w Coqu funkcję F : (X Ž Prop) Ž Formula Ž Prop, tłumaczącą termy typu Formuła (z punktu 1), na formuły Coqa. Pierwszym argumentem funkcji F jest wartościowanie zmiennych.

    Funkcja F ma mieć następujące własności (dowiedzione w Coqu):
Myślę, że rozwiązanie zadania nie powinno sprawić (zbyt dużych) kłopotów. Jeśli znaleźlibyście w powyższej treści jakieś błędy, to bardzo proszę o poinformowanie mnie o tym fakcie.
Życzę powodzenia
Jacek Chrząszcz, 28 lutego 2002 ostatnia zmiana: March 4, 2002
1
Uwaga na uwagę!

This document was translated from LATEX by HEVEA.