8.8: Доказно-теоретичні поняття
- Page ID
- 52919
Подібно до того, як ми визначили низку важливих семантичних понять (валідність, тяговість, задовільність), ми тепер визначаємо відповідні теоретичні поняття. Вони визначаються не апеляцією до задоволення вироків у структурах, а зверненням до похідності або непохідності певних послідовностей. Важливим відкриттям було те, що ці поняття збігаються. Те, що вони роблять, - це зміст теореми про обґрунтованість і повноту.
Визначення\(\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\). Якщо послідовність, що містить одну, є похідною, так само і інша, наприклад:
Відтепер ми скажемо, що якщо\(\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\). Розглянемо наступну деривацію:
З тих пір\(\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\).
\(\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\), що є непослідовним.
◻