10.6: Побудова моделі

Template:MathJaxZach

Зараз нас не турбує\(\eq[][]\), i.e., we only want to show that a consistent set \(\Gamma\) of sentences not containing \(\eq[][]\) is satisfiable. We first extend \(\Gamma\) to a consistent, complete, and saturated set \(\Gamma^*\). In this case, the definition of a model \(\Struct{M(\Gamma^*)}\) is simple: We take the set of closed terms of \(\Lang{L'}\) as the domain. We assign every constant symbol to itself, and make sure that more generally, for every closed term \(t\), \(\Value{t}{M(\Gamma^*)} = t\). The predicate symbols are assigned extensions in such a way that an atomic sentence is true in \(\Struct{M(\Gamma^*)}\) iff it is in \(\Gamma^*\). This will obviously make all the atomic sentences in \(\Gamma^*\) true in \(\Struct{M(\Gamma^*)}\). The rest are true provided the \(\Gamma^*\) we start with is consistent, complete, and saturated.

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

\(\Gamma^*\)Дозволяти бути повним і послідовним, насиченим набором пропозицій мовою\(\Lang L\). Термін модель\(\Gamma^*\) являє\(\Struct M(\Gamma^*)\) собою структуру, визначену наступним чином:

1. Домен\(\Domain{M(\Gamma^*)}\) являє собою сукупність всіх закритих умов домену\(\Lang L\).

2. Тлумачення постійного символу\(c\) саме\(c\) по собі:\(\Assign{c}{M(\Gamma^*)} = c\).

3. Символу функції\(f\) присвоюється функція, яка у вигляді аргументів замкнуті терміни\(t_1\),...\(t_n\), має як значення замкнутого члена\(f(t_1, \dots, t_n)\):\[\Assign{f}{M(\Gamma^*)}(t_1, \dots, t_n) = f(t_1,\dots, t_n)\nonumber\]

4. Якщо\(R\) є символом присудка\(n\) -place, то\[\tuple{t_1, \dots, t_n} \in \Assign{R}{M(\Gamma^*)} \text{ iff } \Atom{R}{t_1, \dots, t_n} \in \Gamma^*.\nonumber\]

Структура Структура\(\Struct{M}\) may make all instances \(A(t)\) of a universally quantified sentence \(\lforall{x}{A(x)}\) true, without making \(\lforall{x}{A(x)}\) true. Це пов'язано\(\Struct{M}\) may make an existentially quantified sentence \(\lexists{x}{A(x)}\) true without there being an instance \(A(t)\) that it makes true. з тим, що загалом не кожен елемент\(\Domain{M}\) є значенням закритого терміна (\(\Struct{M}\)може не охоплюватися). Це є причиною того, що відношення задоволеності визначається за допомогою змінних присвоєнь. Однак для нашої термінової моделі\(\Struct{M(\Gamma^*)}\) це не було б необхідно—тому що це покрито. Це зміст наступного результату.

Пропозиція\(\PageIndex{1}\)

\(\Struct M(\Gamma^*)\)Дозволяти термін модель визначення\(\PageIndex{1}\).

1. \(\Sat{M(\Gamma^*)}{\lexists{x}{A(x)}}\)iff принаймні\(\Sat{M}{A(t)}\) на один термін\(t\).

2. \(\Sat{M(\Gamma^*)}{\lforall{x}{A(x)}}\)iff\(\Sat{M}{A(t)}\) на всі терміни\(t\).

Доказ.

1. За пропозицією 5.12.4,\(\Sat{M(\Gamma^*)}{\lexists{x}{A(x)}}\) iff для принаймні однієї змінної присвоєння\(s\),\(\Sat[,s]{M(\Gamma^*)}{A(x)}\). Оскільки\(\Domain{M(\Gamma^*)}\) складається з закритих умов\(\Lang{L}\), це той випадок, якщо є хоча б один закритий термін\(t\) такий, що\(s(x) = t\) і\(\Sat[,s]{M(\Gamma^*)}{A(x)}\). За пропозицією 5.13.3,\(\Sat[,s]{M(\Gamma^*)}{A(x)}\) якщо\(\Sat[,s]{M(\Gamma^*)}{A(t)}\), де\(s(x) = t\). За пропозицією 5.12.3,\(\Sat[,s]{M(\Gamma^*)}{A(t)}\) iff\(\Sat{M(\Gamma^*)}{A(t)}\), оскільки\(A(t)\) є реченням.

2. Вправа.

◻

Проблема\(\PageIndex{1}\)

Заповніть доказ Пропозиції\(\PageIndex{1}\).

Лемма\(\PageIndex{1}\): Truth Lemma

Припустимо\(A\) does not contain \(\eq[][]\). Then\(\Sat{M(\Gamma^*)}{A}\), якщо\(A \in \Gamma^*\).

Доказ. Доведено обидва напрямки одночасно, і шляхом індукції на\(A\).

1. \(\indcase{A}{\lfalse}\) \({\SatN{M(\Gamma^*)}{\lfalse}}\) by definition of satisfaction. On the other hand, \(\lfalse \notin \Gamma^*\) since \(\Gamma^*\) is consistent.

2. \(\indcase{A}{R(t_1, \dots, t_n)}\) \(\Sat{M(\Gamma^*)}{\Atom{R}{t_1, \dots, t_n}}\) iff \(\tuple{t_1, \dots, t_n} \in \Assign{R}{M(\Gamma^*)}\) (by the definition of satisfaction) iff \(R(t_1, \dots, t_n) \in \Gamma^*\) (by the construction of \(\Struct M(\Gamma^*)\)).

3. \(\indcase{A}{\lnot B}\) \(\Sat{M(\Gamma^*)}{\indfrm}\) iff \({\SatN{M(\Gamma^*)}{B}}\) (by definition of satisfaction). By induction hypothesis, \({\SatN{M(\Gamma^*)}{B}}\) iff \(B \notin \Gamma^*\). Since \(\Gamma^*\) is consistent and complete, \(B \notin \Gamma^*\) iff \(\lnot B \in \Gamma^*\).

4. \(\indcase{A}{B \land C}\) exercise.

5. \(\indcase{A}{B \lor C}\) \(\Sat{M(\Gamma^*)}{\indfrm}\) iff \(\Sat{M(\Gamma^*)}{B}\) or \(\Sat{M(\Gamma^*)}{C}\) (by definition of satisfaction) iff \(B \in \Gamma^*\) or \(C \in \Gamma^*\) (by induction hypothesis). This is the case iff \((B \lor C) \in \Gamma^*\) (by Proposition 10.3.1(3)).

6. \(\indcase{A}{B \lif C}\) exercise.

7. \(\indcase{A}{\lforall{x}{B(x)}}\) exercise.

8. \(\indcase{A}{\lexists{x}{B(x)}}\) \(\Sat{M(\Gamma^*)}{\indfrm}\) iff \(\Sat{M(\Gamma^*)}{B(t)}\) for at least one term \(t\) (Proposition \(\PageIndex{1}\)). By induction hypothesis, this is the case iff \(B(t) \in \Gamma^*\) for at least one term \(t\). By Proposition 10.4.2, this in turn is the case iff \(\lexists{x}{B(x)} \in \Gamma^*\).

◻

Проблема\(\PageIndex{2}\)

Завершіть доказ Лемми\(\PageIndex{1}\).