Skip to main content
LibreTexts - Ukrayinska

8.7: Похідні з кількісними показниками

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

    • \( \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}\) -виведення послідовності\(\lexists{x}{\lnot A(x)} \Sequent \lnot \lforall{x}{A(x)}\).

    Маючи справу з квантифікаторами, ми повинні переконатися, що не порушувати власну змінну умову, а іноді це вимагає від нас пограти з порядком проведення певних висновків. Загалом, це допомагає спочатку спробувати подбати про правила, що підлягають умові власної змінної (вони будуть нижче в готовому доказі). Крім того, це гарна ідея, щоб спробувати подивитися вперед і спробувати вгадати, як може виглядати початкова послідовність. У нашому випадку це повинно бути чимось на зразок\(A(a) \Sequent A(a)\). Це означає, що коли ми «змінюємо» правила квантора, нам доведеться вибрати той самий термін - що ми будемо називати\(a\) - як для правила, так\(\lforall{}{}\) і для\(\lexists{}{}\) правила. Якби ми підбирали різні терміни для кожного правила, ми б закінчилися чимось подібним\(A(a) \Sequent A(b)\), що, звичайно, не можна вивести.

    Починаючи як зазвичай, пишемо

    8.7.1.PNG

    Ми могли б або виконувати\(\LeftR{\exists}\) правило, або\(\RightR{\lnot}\) правило. Оскільки\(\LeftR{\exists}\) правило підлягає власній змінній умові, це гарна ідея, щоб подбати про нього раніше, а не пізніше, тому ми зробимо це спочатку.

    8.7.2.png

    Застосовуючи\(\RightR{\lnot}\) правила\(\LeftR{\lnot}\) і назад, отримуємо

    8.7.3.png

    На даний момент наш єдиний варіант - виконувати\(\LeftR{\forall}\) правило. Оскільки це правило не підлягає обмеженню власної змінної, ми в ясному вигляді. Пам'ятайте, що ми хочемо спробувати отримати початкову послідовність (форми\(A(a) \Sequent A(a)\)), тому ми повинні вибрати\(a\) як наш аргумент,\(A\) коли ми застосовуємо правило.

    8.7.4.png

    Важливо, особливо при роботі з квантифікаторами, двічі перевірити, що власна змінна умова не була порушена. Оскільки єдине правило, яке ми застосували, яке підпорядковується умові власної змінної\(\LeftR{\exists}\), було, а власна змінна\(a\) не зустрічається в її нижній послідовності (кінцевій послідовності), це правильне виведення.

    Проблема\(\PageIndex{1}\)

    Наведіть похідні наступних послідовностей:

    1. \(\lforall{x}{(A(x) \lif B)} \Sequent (\lexists{y}{A(y)} \lif B)\)

    2. \(\lexists{x}{(A(x) \lif \lforall{y}{A(y)})}\)