Skip to main content
LibreTexts - Ukrayinska

10.8: Теорема про повноту

  • Page ID
    52760
  • \( \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \) \( \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} \)\(\newcommand{\id}{\mathrm{id}}\) \( \newcommand{\Span}{\mathrm{span}}\) \( \newcommand{\kernel}{\mathrm{null}\,}\) \( \newcommand{\range}{\mathrm{range}\,}\) \( \newcommand{\RealPart}{\mathrm{Re}}\) \( \newcommand{\ImaginaryPart}{\mathrm{Im}}\) \( \newcommand{\Argument}{\mathrm{Arg}}\) \( \newcommand{\norm}[1]{\| #1 \|}\) \( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\) \( \newcommand{\Span}{\mathrm{span}}\) \(\newcommand{\id}{\mathrm{id}}\) \( \newcommand{\Span}{\mathrm{span}}\) \( \newcommand{\kernel}{\mathrm{null}\,}\) \( \newcommand{\range}{\mathrm{range}\,}\) \( \newcommand{\RealPart}{\mathrm{Re}}\) \( \newcommand{\ImaginaryPart}{\mathrm{Im}}\) \( \newcommand{\Argument}{\mathrm{Arg}}\) \( \newcommand{\norm}[1]{\| #1 \|}\) \( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\) \( \newcommand{\Span}{\mathrm{span}}\)

    Template:MathJaxZach

    Давайте об'єднаємо наші результати: дійдемо до теореми повноти.

    Теорема\(\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}\). Обов'язково зверніть увагу на будь-яке мовчазне використання правил у цих доказах.