Специальная математика. Соловьев А.Е. - 36 стр.

UptoLike

ВУЗ: 

ПНИПУ | Пермь

Составители: 

Рубрика: 

знак секвенции
Содержательно это равносильно выражению:
A
1
A
2
... A
n
B
1
B
2
... 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
— 36 —
                     знак секвенции

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

  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

                                            — 36 —

Страницы