Система Генцена

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

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

антецедент - A₁, A₂,... A_{n ½¾} B₁, B₂,... B_n - сукцедент

­

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

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

A₁ & A₂&...& A_n ® B₁Ú B₂Ú...Ú B_n

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

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