Лекция: Система Генцена

В ее основе лежит понятие секвенции.

Секвенции имеют вид

антецедент — A1, A2,… An ½¾ B1, B2,… Bn — сукцедент

­

знак секвенции

Содержательно это равносильно выражению:

A1 & A2& ...& An ® B1Ú B2Ú ...Ú Bn

Аксиома (схема аксиом) в системе Генцена единственная и она имеет вид:

A½¾ A

Правила вывода:

(Из секвенций над чертой выводимы секвенции под чертой, а Г обозначает какое-то множество формул).

1) A, Г½¾ В 1)¢ Г½¾ A; Г½¾ А® В

Г½¾ А®B Г½¾ В

2) Г½¾ А; Г½¾ B 2)¢ Г½¾ А&В

Г½¾ А & В Г½¾ А

3) Г½¾ А 3)¢ Г, A½¾ B; Г, С½¾ B; Г½¾ A Ú В

Г½¾ A Ú B Г½¾ В

4) Г, А½¾ 4)¢ Г½¾ А; Г½¾ А

Г½¾ А Г½¾

5) Г, A, B½¾ C

Г, B, A½¾ C

6) A, A½¾ B 6)¢ A½¾ B, B

A½¾ B A½¾ B

7) Г½¾ B 7)¢ Г½¾ A

Г, A½¾ B Г½¾ A, B

Докажем ½¾ А ® А :

1) Из первой аксиомы, при Г = Æ и В = А:

A ½¾ A

½¾ А ® A

Теорема доказана.

Докажем ½¾ A Ú A

A½¾ A

½¾ A, A

½¾ A Ú A, A

½¾ A Ú A