Skip to main content
LibreTexts - Ukrayinska

9.4: Похідні

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

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

    Виведення речення\(A\) з припущень\(\Gamma\) - це дерево пропозицій, що задовольняють наступним умовам:

    1. Найверхні речення дерева знаходяться або в,\(\Gamma\) або вивантажуються висновком у дереві.

    2. Самим нижнім реченням дерева є\(A\).

    3. Кожне речення в дереві, крім речення\(A\) внизу, є передумовою правильного застосування правила висновку, висновок якого стоїть безпосередньо під цим реченням у дереві.

    Потім ми говоримо, що\(A\) це висновок похідного, і\(A\) це випливає з\(\Gamma\).

    Приклад\(\PageIndex{1}\)

    Кожне припущення само по собі є похідним. Так, наприклад, сама\(C\) по собі є похідною, і так само\(D\) по собі. Ми можемо отримати нове похідне від них, застосувавши, скажімо,\(\Intro{\land}\) правило,

    9.4.1.png

    Ці правила мають бути загальними: ми можемо замінити\(A\) і\(B\) в ньому будь-якими реченнями, наприклад, на\(C\) і\(D\). Тоді висновок буде\(C \land D\), і так

    9.4.2.png

    є правильним виведенням. Звичайно, ми також можемо змінити припущення, так що\(D\) грає роль\(A\) і\(C\) роль\(B\). Таким чином,

    9.4.3.png

    також є правильним виведенням.

    Тепер ми можемо застосувати інше правило, скажімо\(\Intro{\lif}\), яке дозволяє нам укласти умовне і дозволяє нам розрядити будь-яке припущення, ідентичне попереднику цього умовного. Таким чином, обидва наступні були б правильними виведеннями:

    9.4.4.пнг

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

    9.4.5.png