Skip to main content
LibreTexts - Ukrayinska

8.5: Похідні

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

    • \( \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}\): \(\Log{LK}\) derivation

    A\(\Log{LK}\) -похідний послідовності\(S\) - це дерево послідовностей, що задовольняють наступним умовам:

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

    Потім ми говоримо, що\(S\) це кінцева послідовність похідного, і\(S\) це виводиться в\(\Log{LK}\) (або\(\Log{LK}\) -derivable).

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

    Кожна початкова послідовність, наприклад,\(C \Sequent C\) є похідною. Ми можемо отримати новий висновок від цього, застосувавши, скажімо,\(\LeftR{\Weakening}\) правило,

    8.5.1.PNG

    Правило, однак, має бути загальним: ми можемо замінити\(A\) в правилі будь-яким реченням, наприклад, також на\(D\). Якщо передумова відповідає нашій початковій послідовності\(C \Sequent C\), це означає, що\(\Delta\) обидва\(\Gamma\) і справедливі\(C\), і висновок буде тоді\(D, C \Sequent C\). Отже, наступне - це деривація:

    8.5.2.png

    Тепер ми можемо застосувати інше правило\(\LeftR{\Exchange}\), скажімо, яке дозволяє нам змінити два речення зліва. Отже, наступне також є правильним виведенням:

    8.5.3.png

    При цьому застосовується правило, яке було дано як

    8.5.4.png

    обидва\(\Gamma\) і\(\Pi\) були порожніми\(C\),\(\Delta\) є, і ролі\(A\) і\(B\) грають\(D\) і\(C\), відповідно. Багато в чому так само ми також бачимо, що

    8.5.5.png

    це деривація. Тепер ми можемо взяти ці два похідні, і об'єднати їх за допомогою\(\RightR{\land}\). Це правило було

    8.5.6.png

    У нашому випадку приміщення повинно збігатися з останніми послідовністю похідних, що закінчуються в приміщеннях. Це означає, що\(\Gamma\)\(\Delta\) є\(C, D\), порожній,\(A\) є\(C\) і\(B\) є\(D\). Отже, висновок, якщо висновок повинен бути правильним, є\(C, D \Sequent C \land D\).

    8.5.7.png

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

    8.5.8.png