5.9: Структури для мов першого порядку

Template:MathJaxZach

Мови першого порядку самі по собі неінтерпретовані: постійні символи, символи функцій та символи предикатів не мають певного значення, що надається їм. Значення задаються вказівкою структури. Він визначає домен, тобто об'єкти, які виділяють постійні символи, функціональні символи працюють на, а квантифікатори перебувають у діапазоні. Крім того, він визначає, які постійні символи вибирають, які об'єкти, як символ функції відображає об'єкти з об'єктами та до яких об'єктів застосовуються символи предикатів. Структури є основою для смислових понять в логіці, наприклад, поняття слідства, валідності, задоволеності. Їх по-різному називають «структурами», «інтерпретаціями» або «моделями» в літературі.

Визначення\(\PageIndex{1}\): Structures

Структура\(\Struct M\), для мови\(\Lang{L}\) логіки першого порядку складається з наступних елементів:

1. Домен: непорожній набір,\(\Domain M\)

2. Тлумачення постійних символів: для кожного постійного\(c\) символу\(\Lang{L}\), елемент\(\Assign{c}{M} \in \Domain M\)

3. Інтерпретація символів присудків: для кожного\(n\) -місця\(R\) присудкового символу\(\Lang{L}\) (крім\(\eq[][]\)), відношення\(n\) -place\(\Assign{R}{M} \subseteq \Domain{M}^n\)

4. Інтерпретація символів функції: для кожного символу функції\(n\)\(f\) -place\(\Lang{L}\), функція\(n\) -place\(\Assign{f}{M} \colon \Domain{M}^n \to \Domain{M}\)

Приклад\(\PageIndex{1}\)

Структура\(\Struct M\) для мови арифметики складається з множини, елемента\(\Domain M\)\(\Assign{\Obj 0}{M}\), як інтерпретації постійного символу\(\Obj 0\), одномісної функції\(\Assign{\Obj \prime}{M} \colon \Domain{M} \to \Domain M\), двох двомісних функцій\(\Assign{\Obj +}{M}\) і\(\Assign{\Obj \times}{M}\), обидва\(\Domain M^2 \to \Domain M\), і двомісне відношення\(\Assign{\Obj <}{M} \subseteq \Domain{M}^2\).

Наочним прикладом такої конструкції є наступний:

1. \(\Domain N = \Nat\)

2. \(\Assign{\Obj 0}{N} = 0\)

3. \(\Assign{\Obj \prime}{N}(n) = n + 1\)для всіх\(n \in \Nat\)

4. \(\Assign{\Obj +}{N}(n, m) = n + m\)для всіх\(n, m \in \Nat\)

5. \(\Assign{\Obj \times}{N}(n, m) = n\cdot m\)для всіх\(n, m \in \Nat\)

6. \(\Assign{\Obj <}{N} = \Setabs{\tuple{n, m}}{n \in \Nat, m \in \Nat, n < m}\)

Структура\(\Struct N\) для\(\Lang L_A\) так визначена називається стандартною моделлю арифметики, оскільки вона інтерпретує нелогічні константи\(\Lang L_A\) саме того, як ви очікуєте.

Однак існує безліч інших можливих структур для\(\Lang L_A\). Наприклад, ми могли б взяти як домен набір\(\Int\) цілих чисел замість\(\Nat\), і визначити інтерпретації\(\Obj 0\),,\(\Obj \prime\),\(\Obj +\),\(\Obj \times\),\(\Obj <\) відповідно. Але ми також можемо визначити структури\(\Lang L_A\), для яких навіть віддалено нічого спільного з числами.

Приклад\(\PageIndex{2}\)

Структура\(\Struct M\) для мови\(\Lang L_Z\) теорії множин вимагає лише множини та співвідношення одного та двох місць. Так технічно, наприклад, набір людей плюс відношення «\(x\)старше\(y\)» може бути використаний як структура для\(\Lang L_Z\), а також\(\Nat\) разом з\(n \ge m\) for\(n, m \in \Nat\).

Особливо цікавою структурою, для\(\Lang L_Z\) якої елементи області насправді множини, а інтерпретація\(\Obj \in\) фактично\(x\) є відношення «є елементом\(y\)» є\(\Struct{ {HF} }\) структура спадково кінцеві множини:

1. \(\Domain{ { {HF} } } = \emptyset \cup \Pow{\emptyset} \cup \Pow{\Pow{\emptyset}} \cup \Pow{\Pow{\Pow{\emptyset}}} \cup \dots\);

2. \(\Assign{\Obj \in}{ { {HF} } } = \Setabs{\tuple{x, y}}{x, y \in \Domain{ { {HF} } }, x \in y}\).

Умови, які ми робимо щодо того, що вважається структурою, впливають на нашу логіку. Наприклад, вибір запобігання порожнім доменам забезпечує, враховуючи звичайний рахунок задоволення (або правди) для кількісних пропозицій,\(\lexists{x}{(A(x) \lor \lnot A(x))}\) тобто дійсний - тобто логічну істину. І умова про те, що всі постійні символи повинні посилатися на об'єкт в області гарантує, що екзистенціальне узагальнення є звуковою схемою висновку:\(A(a)\), отже\(\lexists{x}{A(x)}\). Якби ми дозволили іменам посилатися поза доменом або не посилатися, то ми були б на шляху до вільної логіки, в якій екзистенціальне узагальнення вимагає додаткової передумови:\(A(a)\) і\(\lexists{x}{\eq[x][a]}\), отже\(\lexists{x}{A(x)}\).