• 5

31. Пропозициональное исчисление.

 Если в число исходных символов исчисления F1 включены пропозициональные перемен­ные, то всякая теорема пропозиционального исчисления, построен­ного на импликации и отрицании как на исходных связках, яв­ляется также теоремой исчисления F1. Это непосредственно следует из результатов § 27, так как в число аксиом исчисления F1 входят аксиомы исчисления Р § 27 (в *302, *303 и *304), а единственное пра­вило вывода исчисления Р является также правилом вывода ис­числения F1.

Даже в тех случаях, когда пропозициональные переменные не входят в число исходных символов исчисления F1, мы все же можем получить аналогичное заключение, рассматривая подстановковые частные случаи теорем пропозиционального исчисления.

Под подстановковым частным случаем пп-формулы А произ­вольной формулировки пропозиционального исчисления мы по­нимаем выражение, или формулу

СЬ,Ь,.. .Ь„ Д I

где Ь1; Ь2, . .., Ь„ — полный перечень (различных) пропозициональ­ных переменных формулы А, а Вх, В2, . . ., Вп — произвольные пп-формулы рассматриваемой в конкретном контексте логисти­ческой системы, в этой главе — логистической системы F1.

Ясно, что подстановковый частный случай пп-формулы исчис­ления Р является пп-формулой исчисления F1. Более того, под­становковый частный случай

сь1ъг...ъпд|

®В1В,...В1,А|

теоремы А исчисления Р должен быть теоремой исчисления F1. Это следует из того, что всякий подстановковый частный случай аксиомы исчисления Р является (в силу * 302—* 304) аксиомой исчисления F1. Если же дано доказательство формулы А как теоре­мы исчисления Р, то пусть Ъ1; Ъ2, .. ., bn, с1( с2, ..., ст — полный перечень (различных) встречающихся в нем пропозициональных переменных. Выберем тогда произвольные пп-формулы Съ С2, ... ■ • Ст исчисления F1 и повсюду в данном доказательстве подста­вим одновременно Вх вместо Ьх, В2 вместо Ь2, .. ., Вп вместо Ьга, Сх вместо Cj, С2 вместо с2, . . ., Ст вместо ст. Результат этой подста­новки является доказательством пп-формулы

съ, ь,.. .ь» Д I °в1в>.. в«А I

как теоремы исчисления F1, поскольку правильные применения модус поненс в Р превращаются подстановкой в правильные при­менения модус поненс в F1.

Так как мы знаем (в силу **235, **239, *270, **271), что теоремы исчисления Р совпадают с тавтологиями исчисления Р (в смысле § 15), то мы без какого-либо урона можем предыдущим результатам придать следующую форму:

*310. Всякая тавтология исчисления Р является теоремой ис­числения F1, если она является пп-формулой F1.

*311. Всякий подстановковый частный случай тавтологии исчис­ления Р является теоремой исчисления F1.

Использованный выше произвольный выбор пп-формул С1; С2, . . ., Ст легко заменить выбором, производимым по некоторому определенному правилу. Так как п > 0, то мы можем, например, просто отождествить каждую из пп-формул С1( С2, . . ., Ст с Вх. Тем самым доказательство метатеоремы *311 становится эффектив­ным в смысле § 12, и поэтому *311 (так же как и *310) может применяться в качестве производного правила вывода.

Использование *311 как производного правила вывода облег­чается фактом существования эффективной процедуры для опре­деления того, является ли или не является данная пп-формула исчисления F1 подстановковым частным случаем некоторой тавто­логии исчисления Р, — и если да, то нахождения какой-либо тавтологии исчисления Р, подстановковым частным случаем ко­торой она являлась бы. Подробности мы предоставляем читателю. Мы будем ссылаться на эту процедуру в тех случаях, когда нам потребуется рассматривать какую-либо пп-формулу исчисления F1 как подстановковый частный случай тавтологии исчисления Р, предоставляя проверку читателю.

Мы часто будем использовать описанным образом *311 в ка­честве производного правила вывода. И обычно будем считать достаточным указанием на такое использование *311, будь то отдельно или с последующим однократным или многократным применением правила модус поненс, такие выражения, как „в си­лу Р" или „используя Р" ит. п.

Мы выписываем здесь для ссылок следующие пять метатеорем:

*312. Всякая пп-формула имеет один и только один из пяти приведенных ниже видов: отдельно взятая пропозицио­нальная переменная; f(aj, а2, ..., ап), где f есть п-арная функциональная переменная или л-арная функциональ­ная константа, а аь а2, . .., а„ — индивидные переменные, или индивидные константы, или и то и другое; ~ А; [АэВ]; (Va)A, где а есть индивидная переменная. Во

всех этих случаях она представима в таком виде одно­значно. .

**313. Пп-часть формулы  либо совпадает с *** А, либо

является пп-частью формулы А.

**314. Пп-часть формулы [A3В] либо совпадает с [А3В], либо является пп-частью формулы А, либо является пп-частью формулы В.

**315. Пп-часть формулы (Va)A либо совпадает с (Va)A, либо является пп-частью формулы А.

**316. Если Г получается из А подстановкой N вместо нуля или большего числа вхождений М в А (не обязательно вместо всех вхождений М в А), то Г правильно построена.

Эти метатеоремы используются, в частности, ниже при дока­зательстве метатеорем **323, **340 и **390. Их доказательство аналогично доказательству метатеорем **225—**228 и предо­ставляется читателю.

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

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