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.