8.8: Доказно-теоретичні поняття

Last updated
Save as PDF

Page ID: 52919

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

Речення\(A\) - це теорема, якщо є виведення в\(\Log{LK}\) послідовності\(\quad \Sequent A\). Ми пишемо\(A\),\(\Proves A\) якщо це теорема, а\(\ProvesN A\) якщо це не так.

Визначення\(\PageIndex{2}\): Derivability

Речення\(A\) є похідним від набору пропозицій\(\Gamma\)\(\Gamma \Proves A\), якщо є скінченна підмножина\(\Gamma_0 \subseteq \Gamma\) і\(\Gamma_0'\) послідовність пропозицій в\(\Gamma_0\) такому, що\(\Log{LK}\) виводить\(\Gamma_0' \Sequent A\). Якщо\(A\) не виводиться з\(\Gamma\) пишемо\(\Gamma \ProvesN A\).

Через скорочення, ослаблення та правила обміну порядок і кількість пропозицій в\(\Gamma_0'\) не має значення: якщо послідовність\(\Gamma_0' \Sequent A\) є похідною, то так і\(\Gamma_0'' \Sequent A\) для будь-якого,\(\Gamma_0''\) що містить ті ж речення, що і \(\Gamma_0'\). Наприклад, якщо\(\Gamma_0 = \{B, C\}\) тоді обидва\(\Gamma_0' = \tuple{B, B, C}\) і\(\Gamma_0'' = \tuple{C, C, B}\) є послідовностями, що містять тільки речення в\(\Gamma_0\). Якщо послідовність, що містить одну, є похідною, так само і інша, наприклад:

8.8.1.PNG

Відтепер ми скажемо, що якщо\(\Gamma_0\) це кінцевий набір речень, то\(\Gamma_0 \Sequent A\) це будь-яка послідовність, де попередник - це послідовність речень\(\Gamma_0\) і мовчазно включають скорочення, обміни та ослаблення, якщо це необхідно.

Визначення\(\PageIndex{3}\): Consistency

Набір речень\(\Gamma\) є непослідовним, якщо існує кінцева підмножина,\(\Gamma_0 \subseteq \Gamma\) така, що\(\Log{LK}\) походить\(\Gamma_0 \Sequent \quad\). Якщо не\(\Gamma\) є суперечливим, тобто, якщо для кожного кінцевого\(\Gamma_0 \subseteq \Gamma\),\(\Log{LK}\) не виводить\(\Gamma_0 \Sequent \quad\), ми говоримо, що це послідовно.

Пропозиція\(\PageIndex{1}\): Reflexivity

Якщо\(A \in \Gamma\), то\(\Gamma \Proves A\).

Доказ. Початкова послідовність\(A \Sequent A\) є похідною, і\(\{A\} \subseteq \Gamma\). ◻

Пропозиція\(\PageIndex{2}\): Monotony

Якщо\(\Gamma \subseteq \Delta\) і\(\Gamma \Proves A\), то\(\Delta \Proves A\).

Доказ. Припустимо\(\Gamma \Proves A\), тобто є кінцеве\(\Gamma_0 \subseteq \Gamma\) таке, що\(\Gamma_0 \Sequent A\) є похідним. Так як\(\Gamma \subseteq \Delta\), то також\(\Gamma_0\) є кінцевим підмножиною\(\Delta\). Виведення при\(\Gamma_0 \Sequent A\) цьому також показує\(\Delta \Proves A\). ◻

Пропозиція\(\PageIndex{3}\): Transitivity

Якщо\(\Gamma \Proves A\) і\(\{A\} \cup \Delta \Proves B\), то\(\Gamma \cup \Delta \Proves B\).

Доказ. Якщо\(\Gamma \Proves A\), є кінцеве\(\Gamma_0 \subseteq \Gamma\) і\(\pi_0\) виведення\(\Gamma_0 \Sequent A\). Якщо\(\{A\} \cup \Delta \Proves B\), то для якоїсь скінченної підмножини\(\Delta_0 \subseteq \Delta\), є\(\pi_1\) виведення\(A, \Delta_0 \Sequent B\). Розглянемо наступну деривацію:

8.8.2.png

З тих пір\(\Gamma_0 \cup \Delta_0 \subseteq \Gamma \cup \Delta\), це показує\(\Gamma \cup \Delta \Proves B\). ◻

Зверніть увагу, що це означає, що зокрема якщо\(\Gamma \Proves A\) і\(A \Proves B\), то\(\Gamma \Proves B\). Звідси випливає також, що якщо\(A_1, \dots, A_n \Proves B\) і\(\Gamma \Proves A_i\) для кожного\(i\), то\(\Gamma \Proves B\).

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

\(\Gamma\)є непослідовним iff\(\Gamma \Proves {A}\) для кожного речення\(A\).

Доказ. Вправа. ◻

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

Доведіть пропозицію\(\PageIndex{4}\).

Пропозиція\(\PageIndex{5}\): Compactness

Якщо\(\Gamma \Proves A\) тоді є кінцева підмножина\(\Gamma_0 \subseteq \Gamma\) така, що\(\Gamma_0 \Proves A\).
Якщо кожна скінченна підмножина\(\Gamma\) послідовна,\(\Gamma\) то послідовна.

Доказ.

Якщо\(\Gamma \Proves A\), то існує кінцева підмножина\(\Gamma_0 \subseteq \Gamma\) така, що послідовність\(\Gamma_0 \Sequent A\) має деривацію. Отже,\(\Gamma_0 \Proves A\).
Якщо\(\Gamma\) є непослідовним, існує кінцева підмножина\(\Gamma_0 \subseteq \Gamma\) така, що\(\Log{LK}\) походить\(\Gamma_0 \Sequent \quad\). Але тоді\(\Gamma_0\) є кінцевим підмножиною\(\Gamma\), що є непослідовним.

◻