Формула в исчислении предикатов в предваренном [1] нормальной форме ( ПНФ ) , если она записывается в виде строки из кванторов и связанных переменных , называется префиксом , за которым следует бескванторной часть, называемой матрицей . [2]
Каждая формула в классической логике эквивалентна формуле в преднормальной форме. Например, если, , а также являются бескванторными формулами с указанными свободными переменными, тогда
находится в предваренной нормальной форме с матрицей , пока
логически эквивалентен, но не в пренексированной нормальной форме.
Преобразование в предварительную форму
Каждая формула первого порядка логически эквивалентна (в классической логике) некоторой формуле в предваренной нормальной форме. [3] Существует несколько правил преобразования, которые можно рекурсивно применять для преобразования формулы в предваренную нормальную форму. Правила зависят от того, какие логические связки появляются в формуле.
Конъюнкция и дизъюнкция
Правила соединения и дизъюнкции говорят, что
- эквивалентно при (мягком) дополнительном состоянии , или, что то же самое, (это означает, что существует хотя бы один человек),
- эквивалентно ;
а также
- эквивалентно ,
- эквивалентно при дополнительном условии .
Эквивалентности действительны, когда не появляется в качестве свободной переменной в; если действительно кажется свободным в , можно переименовать границу в и получим эквивалент .
Например, в языке колец ,
- эквивалентно ,
но
- не эквивалентно
потому что формула слева верна в любом кольце, когда свободная переменная x равна 0, а формула справа не имеет свободных переменных и ложна в любом нетривиальном кольце. Так будет сначала переписан как а затем поместите в предваренную нормальную форму .
Отрицание
Правила отрицания говорят, что
- эквивалентно
а также
- эквивалентно .
Последствия
Есть четыре правила импликации : два, которые удаляют кванторы из антецедента, и два, которые удаляют кванторы из консеквента. Эти правила можно вывести, переписав импликацию в виде и применение приведенных выше правил дизъюнкции. Как и в случае с правилами дизъюнкции, эти правила требуют, чтобы переменная, указанная в одной подформуле, не появлялась свободной в другой подформуле.
Правила удаления кванторов из антецедента (обратите внимание на изменение кванторов):
- эквивалентно (в предположении, что ),
- эквивалентно .
Правила удаления кванторов из консеквента:
- эквивалентно (в предположении, что ),
- эквивалентно .
Пример
Предположим, что , , а также являются формулами без кванторов, и никакие две из этих формул не имеют одинаковых свободных переменных. Рассмотрим формулу
- .
Путем рекурсивного применения правил, начиная с самых внутренних подформул, можно получить следующую последовательность логически эквивалентных формул:
- .
- ,
- ,
- ,
- ,
- ,
- ,
- .
Это не единственная предварительная форма, эквивалентная исходной формуле. Например, имея дело с консеквентом перед антецедентом в приведенном выше примере, предваряющая форма
может быть получен:
- ,
- ,
- .
Интуиционистская логика
Правила преобразования формулы в предваренную форму интенсивно используют классическую логику. В интуиционистской логике неверно, что каждая формула логически эквивалентна предшествующей формуле. Связка отрицания - одно из препятствий, но не единственное. Оператор импликации также трактуется в интуиционистской логике иначе, чем в классической логике; в интуиционистской логике его нельзя определить с помощью дизъюнкции и отрицания.
Интерпретация ВНКА показывает , почему некоторые формулы не имеют интуиционистский-эквивалентные формы пренексных. В этой интерпретации доказательство
является функцией, которая при конкретном x и доказательстве, дает конкретное y и доказательство. В этом случае значение y может быть вычислено из заданного значения x . Доказательство
с другой стороны, производит одно конкретное значение y и функцию, которая преобразует любое доказательство в доказательство . Если каждый x удовлетворяетможно использовать для построения y, удовлетворяющегоно такой y не может быть построен без знания такого x, тогда формула (1) не будет эквивалентна формуле (2).
Правила преобразования формулы в предварительную форму, которые действительно терпят неудачу в интуиционистской логике, следующие:
- (1) подразумевает ,
- (2) подразумевает ,
- (3) подразумевает ,
- (4) подразумевает ,
- (5) подразумевает ,
( x не отображается как свободная переменнаяв (1) и (3); x не появляется как свободная переменная в (2) и (4)).
Использование предварительной формы
Некоторые исчисления доказательств имеют дело только с теорией, формулы которой записаны в предваренной нормальной форме. Эта концепция необходима для развития арифметической иерархии и аналитической иерархии .
Доказательство Гёделя его теоремы о полноте для логики первого порядка предполагает, что все формулы были преобразованы в предваренную нормальную форму.
Аксиомы геометрии Тарского - это логическая система, все предложения которой могут быть записаны в универсально-экзистенциальной форме , частный случай пренексной нормальной формы, в которой каждый универсальный квантор предшествует любому экзистенциальному квантору , так что все предложения могут быть переписаны в форме , где предложение, не содержащее квантификатора. Этот факт позволил Тарскому доказать разрешимость евклидовой геометрии .
Смотрите также
Заметки
Рекомендации
- Ричард Л. Эпштейн (18 декабря 2011 г.). Классическая математическая логика: семантические основы логики . Издательство Принстонского университета. С. 108–. ISBN 978-1-4008-4155-4.
- Питер Б. Эндрюс (17 апреля 2013 г.). Введение в математическую логику и теорию типов: к истине через доказательство . Springer Science & Business Media. С. 111–. ISBN 978-94-015-9934-4.
- Эллиотт Мендельсон (1 июня 1997 г.). Введение в математическую логику, четвертое издание . CRC Press. С. 109–. ISBN 978-0-412-80830-2.
- Хинман, П. (2005), Основы математической логики , А.К. Петерс , ISBN 978-1-56881-262-5