Cтраница 3
Как и в прошлом разделе, рассмотрим сигнатуру СТА, которая получается добавлением к а констант для всех элементов интерпретации А. Рассмотрим теперь все бескванторные формулы сигнатуры а А, истинные в А. [31]
Семантика формул Я0 определяется индукцией по построению формулы. Всякая формула Я0 эквивалентна бескванторной формуле. [32]
В частности, Е - формулами будут все бескванторные формулы, построенные из термов, и все стандартные формулы. [33]
В качестве следствия из предложения б) и его обобщения получается, что осуществляемый средствами исчисления предикатов вывод любой квазипредваренной формулы, построенной из переменных и символов исчисления предикатов и, быть может, некоторых дополнительных индивидных, функциональных и предикатных символов, всегда может быть проведен следующим образом. Мы начинаем с некоторой истинной в логике высказываний бескванторной формулы, которая не содержит никаких других символов логики высказываний, кроме встречающихся в заданной формуле, а затем подходящим сбразом применяем правила ( ( г) и ( v) в сочетании с правилом вычеркивания повторений дизъюнктивных членов. Вывод любой не квазипредваренной формулы 5 теперь может быть проделан следующим образом. [34]
Свойство под-формулыюстп для LK обеспечивает основная теорема Г е н ц с н а ( теорема об устранимости сечен и я): по всякому выводу в LK можно построить вывод ( той же секвенции) без сечения. Эта теорема позволяет устанавливать разрешимость бескванторных систем: из подформул данной бескванторной формулы можно составить лишь конечное число несходных секвенций ( секвенции сходны, если они отличаются лишь порядком и повторениями членов в антецеденте и сукцеденте), из к-рых, в свою очередь, можно составить лишь конечное число кандидатов в выводы; данная формула доказуема, если среди этих кандидатов найдется вывод. [35]
Рассмотрим интерпретацию этой сигнатуры, носителем которой является множество действительных чисел, а предикаты и операции понимаются естественным образом. Тогда для каждой формулы существует эквивалентная ( выражающая тот же предикат) бескванторная формула. Это утверждение называют теоремой Тарского - Зайденберга. [36]
Другое доказательство тех же фактов дает элиминация кванторов ( теорема 30, с. Как мы отмечали в разделе 3.6, для каждой формулы ip нашей сигнатуры существует бескванторная формула if, эквивалентная if в любой нормальной интерпретации теории плотных линейно упорядоченных множеств без первого и последнего элементов. [37]
Отметим сразу же, что с такой сигнатурой элиминация кванторов невозможна. В самом деле, формула Ву ( х у у ], истинная для четных х, не эквивалентна никакой бескванторной формуле. Поэтому нам нужно, прежде чем проводить элиминацию кванторов, расширить сигнатуру. Приведенный пример формулы подсказывает, какое расширение нам необходимо. [38]
Формулы, находящиеся в почти нормальной форме, можно подвергнуть дальнейшему преобразованию. Именно, поскольку мы договорились обозначать все связанные переменные различными буквами, мы можем в силу задач 12.8 и 12.10 вынести кванторы так, что формула примет вид бескванторной формулы, к которой последовательно применяются кванторы. [39]
Теорема 16.4 называется теоремой об элиминации кванторов в формальных доказательствах. Теорема 16.4 утверждает, что если У - Открытая теория и открытая формула а имеет в У формальное доказательство, то а имеет также формальное доказательство, состоящее из бескванторных формул. [40]
Теперь, прежде чем перейти к арифметизации понятия вывода, мы рассмотрим вопрос о том, как с помощью арифметического перевода может быть оформлена процедура вычисления тех истинностных значений бескванторных формул, которые получаются в результате произвольного приписывания каждой элементарной формуле одного из значений истина или ложь и истолкования связок исчисления высказываний как истинностных функций. [41]
Теорема 16.4 называется теоремой об элиминации кванторов в формальных доказательствах. Теорема 16.4 утверждает, что если У - открытая теория и открытая формула а имеет в У формальное доказательство, то а имеет также формальное доказательство, состоящее из бескванторных формул. [42]
Свойство х у можно выразить как существует ненулевое z, для которого х z1 у. Таким образом, класс выразимых предикатов не изменится, если мы удалим символ из сигнатуры. Но предикатов, выразимых бескванторными формулами, станет меньше: свойство х 0, как легко понять, не эквивалентно никакой бескванторной формуле, содержащей константы, сложение, умножение и равенство. [43]
Свойство х у можно выразить как существует ненулевое z, для которого х z1 у. Таким образом, класс выразимых предикатов не изменится, если мы удалим символ из сигнатуры. Но предикатов, выразимых бескванторными формулами, станет меньше: свойство х 0, как легко понять, не эквивалентно никакой бескванторной формуле, содержащей константы, сложение, умножение и равенство. [44]
На этом пути было получено одно из первых доказательств непротиворечивости А. А без сечения истинно ( и даже доказуемо в А. Так как со-вывод без сечения замкнутой бескванторной формулы не содержит кванторов, отсюда следует непротиворечивость А. Применение второй теоремы Геделя о неполноте позволяет получить отсюда, что теорема об устранении сечения из любого вывода в А. [45]