Избранное
ЭБ Нефть
и Газ
Главная
Оглавление
Поиск +
Еще книги ...
Энциклопедия
Помощь
Для просмотра
необходимо:


Книга: Главная » Гильберт Д.N. Основания математики Теория доказательств
 
djvu / html
 

210 е-символ и ЛОГИЧЕСКИЙ ФОРМАЛИЗМ ггл ш
связанных с проблемой разрешимости, мы часто бываем вынуждены для характеристики типов формул привлекать к рассмотрению дизъюнкции предваренных формул, если речь идет о выводимости, а если речь идет о двойственных вопросах непротиворечивости (неопровеижимости) или о соответствующих неформальных вопросах «выполнимости», — конъюнкции предваренных формул.
В качестве следствия из предложения б) и его обобщения получается, что осуществляемый средствами исчисления предикатов вывод любой квазипредваренной формулы, построенной из переменных и символов исчисления предикатов и, быть может, некоторых дополнительных индивидных, функциональных и предикатных символов, всегда может быть проведен следующим образом. Мы начинаем с некоторой истинной в логике высказываний бескванторной формулы, которая не содержит никаких других символов логики высказываний, кроме встречающихся в заданной формуле, а затем подходящим образом применяем правила (р*) и (v*) в сочетании с правилом вычеркивания повторений дизъюнктивных членов. Вывод любой не квазипредваренной формулы § теперь может быть проделан следующим образом. Сначала мы строим некоторую квазипредваренную формулу Sit переводимую в g. Эту формулу только что описанным способом выводим из некоторой истинной в логике высказываний бескванторной формулы Если проанализировать шаги, на которые может быть разложено получение формулы g в соответствии со сказанным выше, то можно убедиться, что вполне достаточно пользоваться следующими правилами вывода:
а) Правила ассоциативности и коммутативности для конъюнкции и дизъюнкции.
б) В качестве исходных формул разрешается брать формулы вида
или конъюнкции таких формул; здесь ty — элементарная формула, а каждое Пг (t=l, .... г) — либо элементарная формула, либо отрицание элементарной формулы.
в) Выражение 51 & (23 V S) может быть заменено выражением (Я & S3) V (Я & ?);
выражение (81 V 23) & (51 V ®) - выражением 91 V (® & ®)-
г) Выражение 51 может быть заменено выражением ~] ~] 91; выражение 1 31 & ~] 23 — выражением 1 (91 V S3); выражение ~] 21 у ~| 33 — выражением 1 (81 & 33).

 

1 10 20 30 40 50 60 70 80 90 100 110 120 130 140 150 160 170 180 190 200 210 211 212 213 214 215 216 217 218 219 220 230 240 250 260 270 280 290 300 310 320 330 340 350 360 370 380 390 400 410 420 430 440 450 460 470 480 490 500 510 520 530 540 550 560 570 580 590 600 610 620 630 640 650


Математика