Intuicjonistyczny rachunek zdań
(procedura decyzyjna)

Zadanie niniejsze jest kontynuacją zadania domowego numer 1. Wprowadzony zostanie inny system dowodzenia dla intuicjonistycznego rachunku zdań, LJT* z pracy R. Dyckhoff ``Contraction free sequent calculi for intuitionistic logic'' Journal of Symbolic Logic 57(3) 1992.1

Państwa zadaniem będzie:
  1. pokazanie równoważności obu systemów (rachunku Gentzena i LJT*)
  2. pokazanie rozstrzygalności LJT*
  3. (*) stworzyć taktykę dowodzącą tautologie intuicjonistyczne w Coqu
  4. (*) przyglądając się dowodowi rozstrzygalności spróbować udowodnić pełność LJT*
Poniżej podana jest definicja systemu LJT*. Sekwent LJT*, G |- D to para multizbiorów formuł. W systemie nie ma reguł strukturalnych (ale trzeba pamiętać, że multizbiory nie biorą pod uwagę kolejności). Jest jeden aksjomat
G,A |- D,A
Dla każdego symbolu jest pewna liczba reguł prawych i lewych.
Dla fałszu jest tylko reguła lewa, z pustym zbiorem przesłanek
G,^ |- D
Dla koniunkcji jest jedna reguła lewa i jedna prawa:
G, A, B |- D
G, A Ů B |- D
      
G |- D, A    G |- D, B
G |- D, A Ů B
Dla alternatywy -- podobnie:
G,A |- D    G, B |- D
G, A Ú B |- D
      
G |- D, A, B
G |- D, A Ú B
Dla implikacji jest jedna reguła prawa oraz aż cztery lewe, które intuicyjnie zastępują lewą regułę implikacji w systemie Gentzena. Każda z nich dopasowana jest do postaci poprzednika implikacji.
Reguła prawa
G, A |- B
G |- D, A Ž B
Reguły lewe
G, B, p |- D
G,p Ž B, p |- D
      
G, A1 Ž (A2 Ž B) |- D
G, (A1 Ů A2) Ž B |- D
G, A1 Ž B, A2 Ž B |- D
G, (A1 Ú A2) Ž B |- D
      
G, B |- D    G, A2 Ž B |- A1 Ž A2
G,(A1 Ž A2) Ž B |- D
W pierwszej regule symbol p oznacza formułę atomową -- czyli zmienną zdaniową.




Jacek Chrząszcz, 11 kwietnia 2002 ostatnia zmiana: April 18, 2002
1
Jest w bibliotece!
This document was translated from LATEX by HEVEA.