9.8: Вихідність та послідовність

Last updated

Oct 27, 2022
Save as PDF
- 9.7: Доказно-теоретичні поняття
- 9.9: Похідність та пропозиційні зв'язки

$\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}$

Якщо $\Gamma \Proves A$ і $\Gamma \cup \{A\}$ є непослідовним, то $\Gamma$ непослідовно.

Доказ. Нехай виведенням $A$ від $\Gamma$ бути $\delta_1$ і виведенням $\lfalse$ від $\Gamma \cup \{A\}$ бути $\delta_2$ . Потім ми можемо вивести:

9.8.1.png

У новій похідній припущення $A$ виписується, тому воно є похідним від $\Gamma$ . ◻

Пропозиція $\PageIndex{2}$

$\Gamma \Proves A$ iff $\Gamma \cup \{\lnot A\}$ є непослідовним.

Доказ. По-перше $\Gamma \Proves A$ , припустимо, тобто є висновок $A$ з $\delta_0$ нерозряджених припущень $\Gamma$ . Отримаємо похідний $\lfalse$ від $\Gamma \cup \{\lnot A\}$ наступного:

9.8.2.png

Тепер припускаємо, що $\Gamma \cup \{\lnot A\}$ це непослідовно, і нехай $\delta_1$ буде відповідне виведення $\lfalse$ з нерозряджених припущень в $\Gamma \cup \{\lnot A\}$ . Ми отримуємо похідний $A$ від $\Gamma$ одного за допомогою $\FalseCl$ :

9.8.3.png

◻

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

Доведіть, що $\Gamma \Proves \lnot A$ iff $\Gamma \cup \{A\}$ є непослідовним.

Пропозиція $\PageIndex{3}$

Якщо $\Gamma \Proves A$ і $\lnot A \in \Gamma$ , то $\Gamma$ непослідовно.

Доказ. Припустимо $\Gamma \Proves A$ , і $\lnot A \in \Gamma$ . Потім відбувається виведення $\delta$ $A$ від $\Gamma$ . Розглянемо це просте застосування $\Elim{\lnot}$ правила:

9.8.4.png

Оскільки $\lnot A \in \Gamma$ , всі нерозряджені припущення знаходяться в $\Gamma$ , це показує, що $\Gamma \Proves \lfalse$ . ◻

Пропозиція $\PageIndex{4}$

Якщо $\Gamma \cup \{A\}$ і $\Gamma \cup \{\lnot A\}$ обидва несумісні, то $\Gamma$ непослідовні.

Доказ. Існують $\delta_2$ похідні $\delta_1$ і $\lfalse$ від $\Gamma \cup \{ A \}$ і $\lfalse$ від $\Gamma \cup \{ \lnot A \}$ відповідно. Потім ми можемо вивести

9.8.5.png

Так як припущення $A$ і $\lnot A$ виписані, то це виведення $\lfalse$ від $\Gamma$ одного. Отже $\Gamma$ , це непослідовно. ◻