Skip to main content
LibreTexts - Ukrayinska

9.12: Похідні з присудком ідентичності

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

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

    Похідні з присудком ідентичності вимагають додаткових правил висновку.

    9.12.1.PNG

    У вищевказаних правилах,\(t\),\(t_1\), і\(t_2\) є закритими термінами. \(\Intro{\eq[][]}\)Правило дозволяє вивести будь-яке посвідчення особи форми\(\eq[t][t]\) прямо, без припущень.

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

    Якщо\(s\) і\(t\) є закритими термінами, то\(A(s), \eq[s][t] \Proves A(t)\):

    9.12.2.png

    Це може бути знайомим як «принцип замінності ідентиків», або Закон Лейбніца.

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

    Довести, що\(=\) є одночасно симетричним і перехідним, тобто, дати похідні\(\lforall{x}{\lforall{y}{(\eq[x][y] \lif \eq[y][x])}}\) і\(\lforall{x}{\lforall{y}{\lforall{z}{}((\eq[x][y] \land \eq[y][z]) \lif \eq[x][z])}}\)

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

    виводимо вирок

    \[\lforall{x}{\lforall{y}{((A(x) \land A(y)) \lif \eq[x][y])}} \nonumber\]

    з речення

    \[\lexists{x}{\lforall{y}{(A(y) \lif \eq[y][x])}}\nonumber\]

    Ми розвиваємо деривацію назад:

    9.12.3.пнг

    Тепер доведеться скористатися головним припущенням: оскільки це екзистенціальна формула, ми використовуємо\(\Elim{\lexists{}{}}\) для виведення посередницького висновку\(\eq[a][b]\).

    9.12.4.пнг

    Піддеривація у верхньому правому куті завершується за допомогою його припущень, щоб показати, що\(\eq[a][c]\) і\(\eq[b][c]\). Для цього потрібні два окремих похідних. Виведення для виглядає\(\eq[a][c]\) наступним чином:

    9.12.5.png

    Від\(\eq[a][c]\) і\(\eq[b][c]\) ми\(\eq[a][b]\) виходимо\(\Elim{\eq[][]}\).

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

    Наведіть похідні за такими формулами:

    1. \(\lforall{x}{\lforall{y}{((\eq[x][y] \land A(x)) \lif A(y))}}\)

    2. \(\lexists{x}{A(x)} \land \lforall{y}{\lforall{z}{((A(y) \land A(z)) \lif \eq[y][z])}} \lif \lexists{x}{(A(x) \land \lforall{y}{(A(y) \lif \eq[y][x])})}\)