Теория чистого равенства

В математической логике теория чистого равенства является теорией первого порядка . Его сигнатура состоит только из символа отношения равенства и вообще не содержит нелогических аксиом. ^[1]

Эта теория непротиворечива , но неполна, поскольку непустое множество с обычным отношением равенства обеспечивает интерпретацию, делающую определенные предложения истинными. Это пример разрешимой теории и фрагмент более выразительных разрешимых теорий, включая монадический класс логики первого порядка (который также допускает унарные предикаты и через нормальную форму Скулема связан ^[2] для установки ограничений в анализе программ ) и второго порядка монадическая теория чистого множества (которая дополнительно допускает количественную оценку предикатов и чья сигнатура распространяется на монадическую логику второго порядка из k последователей). ^[3]).

Историческое значение

теории чистого равенства была доказана Разрешимость Леопольдом Левенхаймом в 1915 году.

Если добавить дополнительную аксиому, говорящую, что существует ровно m объектов для фиксированного натурального числа m , или добавить схему аксиом, говорящую, что существует бесконечно много объектов, то полученная теория будет полной .

Определение как теория FOL

Чистая теория равенства содержит формулы логики первого порядка с равенством, где единственным символом-предикатом является само равенство и отсутствуют функциональные символы.

Следовательно, единственной формой атомной формулы является $x=y$ где $x,y$ являются (возможно, идентичными) переменными. Синтаксически более сложные формулы можно строить, как обычно, в логике первого порядка, используя пропозициональные связки, такие как $\land ,\lor ,\lnot$ и квантификаторы $\forall ,\exists$ .

Структура первого порядка с равенством, интерпретирующая такие формулы, представляет собой просто множество с отношением равенства на его элементах. Таким образом, изоморфные структуры с такой сигнатурой являются множествами одной мощности . Таким образом, мощность однозначно определяет, является ли предложение истинным в структуре.

Пример

Следующая формула:

\forall x,y,z.\ (z=x\lor z=y)

истинно, когда набор, интерпретирующий формулу, содержит не более двух элементов.

Выразительная сила

Эта теория может выразить тот факт, что область интерпретации имеет, по крайней мере, $k$ элементы для константы $k$ воспользовавшись формулой, которую мы обозначим $D_{k}$ для постоянного $k$ :

\exists x_{1},\ldots ,x_{k}.\ \bigwedge _{1\leq i<j\leq k}x_{i}\neq x_{j}

Затем, используя отрицание, можно выразить, что в области имеется более $k$ элементы. В более общем смысле, он может ограничить область наличием заданного конечного набора конечных мощностей.

Определение теории

С точки зрения моделей чистая теория равенства может быть определена как совокупность тех предложений первого порядка, которые верны для всех (непустых) множеств, независимо от их мощности. Например, следующая формула является допустимой в чистой теории равенства:

(\forall x,y,z.\ (z=x\lor z=y))\lor (\exists p,q,r.\ p\neq q\land p\neq r\land q\neq r)

По полноте логики первого порядка все действительные формулы доказуемы с использованием аксиом логики первого порядка и аксиом равенства (см. Также эквациональную логику ).

Разрешимость

Разрешимость можно показать, установив, что каждое предложение можно показать эквивалентным пропозициональной комбинации формул о мощности области. ^[4]

Чтобы добиться исключения кванторов , можно расширить сигнатуру языка, сохранив при этом определимые отношения (метод, который в более общем случае работает для монадических формул второго порядка). Другой подход к установлению разрешимости — использовать игры Эренфойхта–Фрессе .

См. также

Ссылки

^ Монк, Дж. Дональд (1976). «Глава 13: Некоторые разрешимые теории». Математическая логика . Тексты для аспирантов по математике. Берлин, Нью-Йорк: Springer-Verlag . п. 240. ИСБН 978-0-387-90170-1 .
^ Бахмайр, Л.; Ганцингер, Х.; Вальдманн, У. (1993). «Ограничения набора — это монадический класс». [1993] Материалы восьмого ежегодного симпозиума IEEE по логике в информатике . стр. 75–83. дои : 10.1109/LICS.1993.287598 . hdl : 11858/00-001M-0000-0014-B322-4 . ISBN 0-8186-3140-6 . S2CID 2351050 .
^ Рабин, Майкл О. (июль 1969 г.). «Разрешимость теорий второго порядка и автоматов на бесконечных деревьях» . Труды Американского математического общества . 141 : 1–35. дои : 10.2307/1995086 . JSTOR 1995086 .
^ Монк, Дж. Дональд (1976). «Глава 13: Некоторые разрешимые теории, Лемма 13.11». Математическая логика . Тексты для аспирантов по математике. Берлин, Нью-Йорк: Springer-Verlag . п. 241. ИСБН 978-0-387-90170-1 .

Эта математической логике статья, посвященная , незавершена . Вы можете помочь Википедии, расширив ее .

[1] Монк, Дж. Дональд (1976). «Глава 13: Некоторые разрешимые теории». Математическая логика . Тексты для аспирантов по математике. Берлин, Нью-Йорк: Springer-Verlag . п. 240. ИСБН 978-0-387-90170-1 .

[2] Бахмайр, Л.; Ганцингер, Х.; Вальдманн, У. (1993). «Ограничения набора — это монадический класс». [1993] Материалы восьмого ежегодного симпозиума IEEE по логике в информатике . стр. 75–83. дои : 10.1109/LICS.1993.287598 . hdl : 11858/00-001M-0000-0014-B322-4 . ISBN 0-8186-3140-6 . S2CID 2351050 .

[3] Рабин, Майкл О. (июль 1969 г.). «Разрешимость теорий второго порядка и автоматов на бесконечных деревьях» . Труды Американского математического общества . 141 : 1–35. дои : 10.2307/1995086 . JSTOR 1995086 .

[4] Монк, Дж. Дональд (1976). «Глава 13: Некоторые разрешимые теории, Лемма 13.11». Математическая логика . Тексты для аспирантов по математике. Берлин, Нью-Йорк: Springer-Verlag . п. 241. ИСБН 978-0-387-90170-1 .

[1]

[2]

[3]

[4]