7.1: Вступ

Last updated
Save as PDF

Page ID: 52691

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

Логіка зазвичай має як семантику, так і систему деривації. Семантика стосується таких понять, як істина, задовільність, дійсність та тягне за собою. Метою дериваційних систем є забезпечення суто синтаксичного методу встановлення тягнень та валідності. Вони чисто синтаксичні в тому сенсі, що деривація в такій системі є кінцевим синтаксичним об'єктом, зазвичай послідовністю (або іншим скінченним розташуванням) пропозицій або формул. Хороші системи деривації мають властивість, що будь-яка задана послідовність або розташування пропозицій або формул можуть бути перевірені механічно, щоб бути «правильними».

Найпростіші (і історично перші) системи деривації для логіки першого порядку були аксіоматичними. Послідовність формул вважається виведенням у такій системі, якщо кожна окрема формула в ній знаходиться або серед фіксованого набору «аксіом», або випливає з формул, що надходять перед нею в послідовності, одним із фіксованого числа «правил висновку» - і це може бути механічно перевірено, якщо формула є аксіомою і чи правильно випливає з інших формул по одному з правил висновку. Аксіоматичні системи доказів легко описати, а також легко обробляти мета-теоретично - але похідні в них важко читати і розуміти, а також важко виробляти.

Інші системи деривації були розроблені з метою полегшення побудови похідних або легше зрозуміти похідні після їх завершення. Прикладами є природні вирахування, дерева істинності, також відомі як докази таблиць, і послідовне обчислення. Деякі системи деривації розроблені спеціально з урахуванням механізації, наприклад, метод роздільної здатності легко реалізувати в програмному забезпеченні (але його виведення по суті неможливо зрозуміти). Більшість з цих інших систем доказів представляють похідні як дерева формул, а не послідовності. Це полегшує розуміння того, які частини деривації залежать від яких інших частин.

Отже, для даної логіки, наприклад, логіки першого порядку, різні системи деривації дадуть різні пояснення того, що таке речення, щоб бути теоремою і що це означає для речення, щоб бути похідним від деяких інших. Однак це робиться (через аксіоматичні похідні, природні відрахування, послідовні похідні, дерева правди, спростування дозволу), ми хочемо, щоб ці відносини відповідали семантичним уявленням про дійсність та тягне за собою. Давайте напишемо\(\Proves A\) для «\(A\)це теорема» і «\(\Gamma \Proves A\)» для «\(A\)є похідним від»\(\Gamma\). Однак\(\Proves\) визначено, ми хочемо, щоб він збігався з\(\Entails\), тобто:

\(\Proves A\)якщо і тільки якщо\(\Entails A\)
\(\Gamma \Proves A\)якщо і тільки якщо\(\Gamma \Entails A\)

Напрямок «тільки якщо» вищевказане називається звучністю. Система деривації є надійною, якщо похідність гарантує тягне за собою (або дійсність). Кожна пристойна система деривації повинна бути здоровою; нездорові системи деривації зовсім не корисні. Адже вся мета деривації полягає в тому, щоб забезпечити синтаксичну гарантію дійсності або тягне за собою. Ми доведемо надійність для систем деривації, які ми представляємо.

Важливим є і зворотний напрямок «якщо»: його називають повнотою. Повна система деривації досить сильна, щоб показати, що\(A\) це теорема, коли\(A\) вона дійсна, і що\(\Gamma \Proves A\) коли завгодно\(\Gamma \Entails A\). Повноту встановити складніше, а деякі логіки не мають повних систем деривації. Логіка першого порядку робить. Курт Гедель першим довів повноту дериваційної системи логіки першого порядку у своїй дисертації 1929 року.

Ще одне поняття, пов'язане з системами деривації, - це послідовність. Набір речень називається непослідовним, якщо з нього може бути виведено що-небудь, і послідовним інакше. Невідповідність - синтаксичний аналог незадовільності: як і незадовільні множини, непослідовні набори речень не складають хороших теорій, вони дефектні фундаментальним чином. Послідовні набори речень можуть бути неправдивими або корисними, але принаймні вони проходять той мінімальний поріг логічної корисності. Для різних систем деривації конкретне визначення узгодженості множин речень може відрізнятися, але, як, ми хочемо\(\Proves\), щоб послідовність збігалася з його смисловим аналогом, задовільністю. Ми хочемо, щоб це завжди було випадком, який\(\Gamma\) є послідовним тоді і лише тоді, коли він задовольняється. Тут напрямок «якщо» дорівнює повноті (послідовність гарантує задовільність), а напрямок «тільки якщо» дорівнює надійності (задовільність гарантує послідовність). Насправді, для класичної логіки першого порядку дві версії обгрунтованості і повноти рівнозначні.