9.7: Доказно-теоретичні поняття
- Page ID
- 52917
Подібно до того, як ми визначили низку важливих семантичних понять (валідність, тяговість, задовільність), ми тепер визначаємо відповідні теоретичні поняття. Вони визначаються не апеляцією до задоволення вироків у структурах, а зверненням до похідності або невід'ємності певних речень від інших. Важливим відкриттям було те, що ці поняття збігаються. Те, що вони роблять, - це зміст теорем про обґрунтованість та повноту.
Визначення\(\PageIndex{1}\): Theorems
Речення\(A\) - це теорема, якщо є виведення\(A\) в природному відрахуванні, в якому виписані всі припущення. Ми пишемо\(A\),\(\Proves A\) якщо це теорема, а\(\ProvesN A\) якщо це не так.
Визначення\(\PageIndex{2}\): Derivability
Речення\(A\) випливає з набору пропозицій\(\Gamma\)\(\Gamma \Proves A\), якщо є похідний з висновком\(A\) і в якому кожне припущення або виписано, або знаходиться в\(\Gamma\). Якщо\(A\) не виводиться з\(\Gamma\) пишемо\(\Gamma \ProvesN A\).
Визначення\(\PageIndex{3}\): Consistency
Сукупність пропозицій\(\Gamma\) є непослідовним iff\(\Gamma \Proves \lfalse\). Якщо не\(\Gamma\) є суперечливим, тобто, якщо\(\Gamma \ProvesN \lfalse\), ми говоримо, що це послідовно.
Пропозиція\(\PageIndex{1}\): Reflexivity
Якщо\(A \in \Gamma\), то\(\Gamma \Proves A\).
Доказ. Саме\(A\) по собі припущення є виведенням того,\(A\) де знаходиться кожне нерозряджене припущення (тобто\(A\))\(\Gamma\). ◻
Пропозиція\(\PageIndex{2}\): Monotony
Якщо\(\Gamma \subseteq \Delta\) і\(\Gamma \Proves A\), то\(\Delta \Proves A\).
Доказ. Будь-яке\(\Gamma\) похідне\(A\) від також є виведенням\(A\) від\(\Delta\). ◻
Пропозиція\(\PageIndex{3}\): Transitivity
Якщо\(\Gamma \Proves A\) і\(\{A\} \cup \Delta \Proves B\), то\(\Gamma \cup \Delta \Proves B\).
Доказ. Якщо\(\Gamma \Proves A\), є виведення\(\delta_0\) з усіма\(A\) нерозрядженими припущеннями в\(\Gamma\). Якщо\(\{A\} \cup \Delta \Proves B\), то відбувається виведення\(\delta_1\) з усіма\(B\) нерозрядженими припущеннями в\(\{A\} \cup \Delta\). Тепер розглянемо:
Нерозряджені припущення зараз всі серед\(\Gamma \cup \Delta\), так що це показує\(\Gamma \cup \Delta \Proves B\). ◻
Коли\(\Gamma = \{A_1, A_2, \ldots, A_k\}\) є кінцевим множиною, ми можемо використовувати спрощене позначення\(A_1,A_2,\ldots,A_k \Proves B\) для\(\Gamma \Proves B\), зокрема\(A \Proves B\) означає, що\(\{A\} \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\)є непослідовним.
-
\(\Gamma \Proves {A}\)за кожне речення\({A}\).
-
\(\Gamma \Proves {A}\)і\(\Gamma \Proves \lnot {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\), то відбувається виведення\(\delta\)\(A\) з\(\Gamma\). \(\Gamma_0\)Дозволяти бути безліччю нерозряджених припущень\(\delta\). Оскільки будь-яке похідне є кінцевим,\(\Gamma_0\) може містити лише скінченно багато речень. Отже,\(\delta\) є виведенням\(A\) від кінцевого\(\Gamma_0 \subseteq \Gamma\).
-
Це контрапозитив (1) для особливого випадку\(A \ident \lfalse\).
◻