10.8: Теорема про повноту
- Page ID
- 52760
Давайте об'єднаємо наші результати: дійдемо до теореми повноти.
Теорема\(\PageIndex{1}\): Completeness Theorem
\(\Gamma\)Дозволяти бути сукупністю речень. Якщо\(\Gamma\) послідовний, він задовольняється.
Доказ. \(\Gamma\)Припустимо, послідовно. За Lemma 10.4.1, існує насичений послідовний набір\(\Gamma' \supseteq \Gamma\). За Lemma 10.5.1\(\Gamma^* \supseteq {\Gamma'}\), існує послідовний і повний. Починаючи з\(\Gamma' \subseteq \Gamma^*\), for each formula \(A(x)\), \(\Gamma^*\) contains a sentence of the form \(\lexists{x}{A(x)} \lif A(c)\) and so \(\Gamma^*\) is saturated. If \(\Gamma\) does not contain \(\eq[][]\), then by Лемма 10.6.1,\(\Sat{M(\Gamma^*)}{A}\) іф\(A \in \Gamma^*\). З цього випливає, зокрема\(A \in \Gamma\), що для всіх\(\Sat{M(\Gamma^*)}{A}\), так\(\Gamma\) задовольняється. Якщо\(\Gamma\) does contain \(\eq[][]\), then by Lemma 10.7.1, for all sentences \(A\), \(\Sat{\equivclass{M}{\approx}}{A}\) iff \(A \in \Gamma^*\). In particular, \(\Sat{\equivclass{M}{\approx}}{A}\) for all \(A \in \Gamma\), so \(\Gamma\) is satisfiable. ◻
Слідство\(\PageIndex{1}\): Completeness Theorem, Second Version
Для всіх\(\Gamma\) і пропозицій\(A\): якщо\(\Gamma \Entails A\) тоді\(\Gamma \Proves A\).
Доказ. Зауважте,\(\Gamma\) що в Слідство\(\PageIndex{1}\) і Теорема\(\PageIndex{1}\) універсально кількісно оцінюються. Щоб переконатися, що ми не плутаємо себе, давайте повторно визначимо теорему,\(\PageIndex{1}\) використовуючи іншу змінну: для будь-якого набору речень\(\Delta\), якщо\(\Delta\) він послідовний, він задовольняється. За протиставленням, якщо\(\Delta\) не\(\Delta\) задовольняється, то непослідовно. Ми будемо використовувати це, щоб довести наслідок.
Припустимо, що\(\Gamma \Entails A\). Тоді\(\Gamma \cup \{\lnot A\}\) є незадовільним за пропозицією 5.14.2. \(\Gamma \cup \{\lnot A\}\)Беручи за нашу\(\Delta\), попередня версія Теореми\(\PageIndex{1}\) дає нам, що\(\Gamma \cup \{\lnot A\}\) є непослідовним. За пропозиціями 8.9.2 та 9.8.2,\(\Gamma \Proves A\). ◻
Проблема\(\PageIndex{1}\)
Використовуйте Слідство\(\PageIndex{1}\) для доведення теореми\(\PageIndex{1}\), показуючи тим самим, що дві формулювання теореми повноти еквівалентні.
Проблема\(\PageIndex{2}\)
Для того, щоб система деривації була повною, її правила повинні бути досить сильними, щоб довести, що кожен незадовільний набір непослідовний. Які з правил деривації були необхідні для доведення повноти? Чи будь-яке з цих правил не використовується ніде в доказі? Для того, щоб відповісти на ці питання, складіть список або діаграму, яка показує, які з правил деривації були використані в яких результатах, які призводять до доказу теореми\(\PageIndex{1}\). Обов'язково зверніть увагу на будь-яке мовчазне використання правил у цих доказах.