Skip to main content
LibreTexts - Ukrayinska

Розділ 09: Обґрунтованість та повнота

  1. Last updated
  2. Save as PDF
  • Page ID
    52235

    • \( \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}}\)

    Цей інструментарій неймовірно зручний. Він також інтуїтивно зрозумілий, тому що здається природним, що доказовість і смисловий тягне за собою повинні погодитися. Тим не менш, не обманюйте себе подібністю символів '' і ''. Той факт, що ці два дійсно взаємозамінні, не проста річ, щоб довести.

    Чому ми повинні думати, що аргумент, який можна довести, обов'язково є вагомим аргументом? Тобто, чому думати,\(\mathcal{A}\) що\(\mathcal{B}\)\(\mathcal{A}\) означає\(\mathcal{B}\)?

    У цьому і полягає проблема надійності. Система доказування є надійною, якщо немає доказів недійсних аргументів. Демонстрація того, що система доказування є надійною, вимагатиме показати, що будь-який можливий доказ є доказом вагомого аргументу. Було б недостатньо просто досягти успіху при спробі довести багато вагомих аргументів і зазнати невдачі при спробі довести недійсні.

    На щастя, є спосіб наблизитися до цього поетапно. Якщо використання правила &E в останньому рядку доказу ніколи не може змінити дійсний аргумент на неприпустимий, тоді використання правила багато разів не може зробити аргумент недійсним. Аналогічно, якщо використання правил &E та E окремо на останньому рядку доказу ніколи не може змінити дійсний аргумент на неприпустимий, тоді використання їх у поєднанні також не може.

    Стратегія полягає в тому, щоб показати для кожного правила висновку, що воно поодинці не може зробити вагомий аргумент у неприпустимий. Звідси випливає, що правила, що використовуються в комбінації, не роблять допустимий аргумент недійсним. Оскільки доказ - це лише ряд рядків, кожен з яких виправдовується правилом висновку, це покаже, що кожен доказовий аргумент є дійсним.

    Розглянемо, наприклад, правило &I. Припустимо, ми використовуємо його, щоб додати\(\mathcal{A}\) &\(\mathcal{B}\) до дійсного аргументу. Для того, щоб правило застосовувалося,\(\mathcal{A}\) і\(\mathcal{B}\) повинно бути вже наявне в доказі. Оскільки аргумент поки що є дійсним,\(\mathcal{A}\) і\(\mathcal{B}\) є або передумовою аргументу, або вагомими наслідками приміщення. Таким чином, будь-яка модель, в якій приміщення є істинними, повинна бути моделлю, в якій\(\mathcal{A}\) і\(\mathcal{B}\) є правдою. Відповідно до визначення істини в ql, це означає, що\(\mathcal{A}\) &\(\mathcal{B}\) також вірно в такій моделі. Тому\(\mathcal{A}\) &\(\mathcal{B}\) справедливо випливає з приміщення. Це означає, що використання правила &E для розширення дійсного доказу створює ще один дійсний доказ.

    Для того, щоб показати, що система доказування є надійною, нам потрібно буде показати це для інших правил висновку. Оскільки похідні правила є наслідками основних правил, було б достатньо надати подібні аргументи для 16 інших основних правил. Це виснажлива вправа виходить за рамки цієї книги.

    З огляду на доказ того, що система доказування є доброю, випливає, що кожна теорема є тавтологією.

    Ще можна запитати: навіщо думати, що кожен вагомий аргумент - це аргумент, який можна довести? Тобто, чому думати,\(\mathcal{A}\) що\(\mathcal{B}\)\(\mathcal{A}\) означає\(\mathcal{B}\)?

    У цьому і полягає проблема повноти. Система доказування завершена, якщо є доказ кожного вагомого аргументу. Повнота для такої мови, як QL, вперше була доведена Куртом Геделем у 1929 році. Доказ виходить за рамки цієї книги.

    Важливим моментом є те, що, на щастя, система доказів для QL є одночасно звуковою і повною. Це не стосується всіх систем доказування та всіх формальних мов. Тому що це правда QL, ми можемо вибрати, щоб дати докази або побудувати models— залежно від того, що простіше для завдання під рукою.

    Короткий зміст визначень

    • Речення А - це теорема тоді і тільки тоді, коли\(\mathcal{A}\).
    • Два речення\(\mathcal{A}\) і\(\mathcal{B}\) є доказово еквівалентними тоді і тільки\(\mathcal{A}\) тоді,\(\mathcal{B}\) коли\(\mathcal{B}\) і\(\mathcal{A}\).
    • {\(\mathcal{A}\)1,\(\mathcal{A}\) 2,...} є доказово суперечливим тоді і лише тоді, коли для деякого речення\(\mathcal{B}\) {\(\mathcal{A}\)1,\(\mathcal{A}\) 2,...} (\(\mathcal{B}\)&¬\(\mathcal{B}\)).