• 5

33. Некоторые теоремные схемы исчисления F1.

Теоремная схема — это синтаксическое выражение, которое представляет множество теорем логистической системы (обычно — бесконечное число различных теорем) так же, как аксиомная схема представ­ляет множество различных аксиом. При изучении исчисления F1 мы будем оперировать не с отдельными теоремами, а с теоремными схемами, и для каждой теоремной схемы мы будем с помощью схемы доказательства эффективно показывать, что каждая пред­ставляемая ею отдельная теорема может быть доказана. Как и в слу­чае производных правил вывода (рассмотренных в главе I), это оправдывается упомянутой эффективностью, которая позволяет

12 2007

по первому требованию представить конкретное доказательство любой теоремы, выраженной данной теоремной схемой. Таким образом, наши действия будут заключаться не в фактическом формальном построении системы F1, а в указании эффективных инструкций, которыми следует руководствоваться при факти­ческом построении системы. Важно помнить, что теоремные схемы являются в действительности синтаксическими теоремами о си­стеме F1, и лишь их частные случаи — отдельные представляемые ими теоремы — суть теоремы исчисления F1.

*330. Ь S£A | ID (За) А, где а — индивидная переменная, b — индивидная переменная или индивидная константа и ни­какое свободное вхождение а в А не находится в пп-части формулы А вида (Ь) С.

Доказательство. По *306, \- (а) ~ A 3 ~ Sg А |. Следова­тельно, в силу Р sl9>, имеем h S£ А | з ~ (а) ~ А 320>.

*331. \- (а) А;э (За) А321).

Доказательство. По *306, Ь (а) А 3 А 322). По *330, \- AiD(3a)A 323).

Затем используется закон транзитивности импликации 324). *332. |- АЗаВЗ. (a) A ID В.

Доказательство. По *306, Ь Азавз„ АзВ 325). Вновь по *306, \- (а)Аз А 326). После этого используем Р 326).

*333. h AlDaBlD.(a) AID (а) В.

Доказательство. По *332 и правилу обобщения32", Ь А за В IDa . (a) A Z> В.

Следовательно, по *305, ЬАЗаВз (a) A ID, В з28). По *305, h (а) А За В =5. (а)А =5 (а) Й. После этого используется закон транзитивности импли­кации824».

*334. ЬА= BD,(a)A = (а) В.

Доказательство. По Р, Ь А = В ID. А 3 В. Следовательно, по правилу обобщения и *333 329), Ь А =а В 3. А ЗаВ. Следовательно, по *333 и закону транзитивности импли­кации, f-A=aBD,(a)AD(a)B. Далее, в силу Р, ЬА = ВЗВВЗА. Отсюда аналогичной серией шагов мы получаем |- А =а В 3. (а) В з (а) А. После этого используется Р.

*335. b А 3 (а) В = „ А За В, если а не свободно в А.

Доказательство. По *306, Ь (а)В 3 В. Следовательно, в силу Р, b А 3 (а) В 3. А 3 В. Следовательно, по правилу обобщения и *305, (- А 3 (а) В 3. А За В.

После этого используется *305 и Р. *336. h(a)(b)A = (b)(a)A.

Доказательство. По *306, \- (Ь)А 3 А.

Следовательно, по правилу обобщения и *333, Ь (а)(Ь)А з

(a)А.

Следовательно, по правилу обобщения и *305, (- (а)(Ь)А 3

(b)(а)А.

Аналогично получаем |-(Ь)(а)Аз(а)(Ь)А. После этого используется Р.

*337. (а)А = А, если а не свободно в А.

Доказательство. В силу Р, \- А з А.

Следовательно, в силу правила обобщения и *305, Ь А з

(а)А.

По *306, h (а)А 3 А. После этого используется Р.

*338. |-~(Эа)А = (а)~А.

Доказательство. В силу Р, Ь ~ ~ (а) ~ А = (а) ~ А.

*339. h (а)А == (Ь)В, если В есть S£A |, в А нет свободных вхож­дений b и никакое свободное вхождение а в А не входит в пп-часть формулы А вида (Ь)С.

Доказательство. По *306, |- (а)А 3 В. Следовательно, обоб­щая по переменной b и используя затем *305, мы получаем h (а)А 3 (Ь)В. Далее, отношение между пп-формулами (а)А и (Ь)В взаимно, т. е. А есть S^B|, в В нет свободных вхождений а и никакое свободное вхождение b в В не входит в пп-часть форму­лы В вида (a)D. Поэтому таким же образом получаем |- (Ь)В 3 (а)А. Поэтому, в силу Р, имеем \- (а)А =£ (Ь)В.

Авторы: 1379 А Б В Г Д Е З И Й К Л М Н О П Р С Т У Ф Х Ц Ч Ш Щ Э Ю Я

Книги: 1908 А Б В Г Д Е З И Й К Л М Н О П Р С Т У Ф Х Ц Ч Ш Щ Э Ю Я