Cтраница 4
В качестве следствия из предложения б) и его обобщения получается, что осуществляемый средствами исчисления предикатов вывод любой квазипредваренной формулы, построенной из переменных и символов исчисления предикатов и, быть может, некоторых дополнительных индивидных, функциональных и предикатных символов, всегда может быть проведен следующим образом. Мы начинаем с некоторой истинной в логике высказываний бескванторной формулы, которая не содержит никаких других символов логики высказываний, кроме встречающихся в заданной формуле, а затем подходящим сбразом применяем правила ( ( г) и ( v) в сочетании с правилом вычеркивания повторений дизъюнктивных членов. Вывод любой не квазипредваренной формулы 5 теперь может быть проделан следующим образом. Эту формулу только что описанным способом выводим из некоторой истинной в логике высказываний бескванторной формулы &i, а затем надлежащими преобразованиями возвращаемся от 5i к 5 - Формула % i в свою очередь может быть получена преобразованиями из некоторой построенной из элементарных формул конъюнктивной нормальной формы, которая тоже является истинной в логике высказываний. [46]