Skip to main content
LibreTexts - Ukrayinska

7.5: Аксіоматичні похідні

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

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

    Аксіоматичні похідні - найдавніші і найпростіші логічні системи деривації. Його похідні - це просто послідовності пропозицій. Послідовність речень вважається правильним виведенням, якщо кожне речення\(A\) в ньому задовольняє одній з наступних умов:

    1. \(A\)є аксіомою, або

    2. \(A\)є елементом заданого набору\(\Gamma\) речень, або

    3. \(A\)виправдовується правилом умовиводу.

    Щоб бути аксіомою,\(A\) повинен мати вигляд однієї з ряду фіксованих схем речень. Існує безліч наборів схем аксіом, які забезпечують задовільну (звукову та повну) систему виведення логіки першого порядку. Деякі організовані відповідно до зв'язків, якими вони керують, наприклад, схеми\[A \lif (B \lif A) \qquad B \lif (B \lor C) \qquad (B \land C) \lif B\nonumber\] є загальними аксіомами, які керують\(\lif\),\(\lor\) і\(\land\). Деякі системи аксіом націлені на мінімальну кількість аксіом. Залежно від зв'язків, які приймаються за примітиви, можна навіть знайти системи аксіом, які складаються з єдиної аксіоми.

    Правило висновку - це умовне твердження, яке дає достатню умову для обґрунтування пропозиції в похідній. Modus ponens - одне дуже поширене таке правило: воно говорить про те, що якщо\(A\) і\(A \lif B\) вже виправдані,\(B\) то виправдано. Це означає, що рядок у похідній, що містить речення,\(B\) є виправданим за умови, що обидва\(A\) і\(A \lif B\) (для деякого речення\(A\)) фігурують у виведенні раніше\(B\).

    \(\Proves\)Відношення, засноване на аксіоматичних похідних, визначається наступним чином:\(\Gamma \Proves A\) якщо існує похідне з реченням\(A\) як його останньою формулою (і\(\Gamma\) приймається як сукупність речень у цій деривації, які виправдані (2) вище). \(A\)є теоремою, якщо\(A\) має похідну, де\(\Gamma\) порожня, тобто кожне речення у похідній виправдовується або (1), або (3). Наприклад, ось деривація, яка показує, що\(\Proves A \lif (B \lif (B \lor A))\):

    1. \(B \lif (B \lor A)\)
    2. \((B \lif (B \lor A)) \lif (A \lif (B \lif (B \lor A)))\)
    3. \(A \lif (B \lif (B \lor A))\)

    Речення в рядку 1 має форму аксіоми\(A \lif (A \lor B)\) (з ролями\(A\) і\(B\) зворотними). Речення на рядку 2 має форму аксіоми\(A \lif (B \lif A)\). Таким чином, обидві лінії виправдані. Рядок 3 виправданий модусом ponens: якщо скорочувати його як\(D\), то рядок 2 має вигляд\(C \lif D\), де\(C\) є\(B \lif (B \lor A)\), тобто рядок 1.

    Набір\(\Gamma\) суперечливий, якщо\(\Gamma \Proves \lfalse\). Повна система аксіом також доведе, що\(\lfalse \lif A\) для будь-якого\(A\), і так якщо\(\Gamma\) непослідовно, то\(\Gamma \Proves A\) для будь-якого\(A\).

    Системи аксіоматичних похідних для логіки були вперше дані Готтлобом Фреге в його 1879 р. Бегріфссхріфтом, який з цієї причини часто вважається першим твором сучасної логіки. Вони були вдосконалені в Альфред Норт Уайтхед і Бертран Рассел Principia Mathematica і Девід Гільберт і його учні в 1920-х роках. Таким чином, їх часто називають «системами Фреге» або «системами Гільберта». Вони дуже універсальні тим, що часто легко знайти аксіоматичну систему для логіки. Оскільки похідні мають дуже просту структуру і лише одне або два правила висновку, це також відносно легко довести речі про них. Однак їх дуже важко використовувати на практиці, тобто важко знайти і написати докази.