10.1: Вступ

Last updated
Save as PDF

Page ID: 52797

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

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

У другій формулюванні це може бути заявлено як модельний результат існування: кожен послідовний набір речень є задовільним. Послідовність - це теоретико-теоретичне поняття: воно говорить про те, що наша система доказів не в змозі виробляти певні похідні. Але хто скаже, що тільки тому, що немає похідних певного роду\(\Gamma\), гарантовано, що існує структура\(\Struct{M}\)? До того, як теорема повноти була вперше доведена - фактично до того, як ми мали системи доказів, які ми зараз робимо - великий німецький математик Девід Гільберт вважав думку, що послідовність математичних теорій гарантує існування об'єктів, про які вони знаходяться. Він виклав його наступним чином в листі до Готтлоба Фреге:

Якщо довільно наведені аксіоми не суперечать один одному з усіма їх наслідками, то вони правдиві і існують речі, визначені аксіомами. Це для мене критерій істини і існування.

Фреж категорично не погодився. Друга формулювання теореми повноти показує, що Гільберт мав рацію принаймні в тому сенсі, що якщо аксіоми послідовні, то існує якась структура, яка робить їх все істинними.

Це не єдині причини, що теорема про повноту, а точніше, її доказ - важлива. Вона має ряд важливих наслідків, про деякі з яких ми поговоримо окремо. Наприклад, оскільки будь-яке похідне, яке показує,\(\Gamma \Proves A\) є кінцевим і тому може використовувати лише скінченно багато речень у\(\Gamma\), теорема повноти випливає\(\Gamma\), що якщо\(A\) є наслідком, це вже наслідок кінцевого підмножина\(\Gamma\). Це називається компактністю. Аналогічно, якщо кожна\(\Gamma\) кінцева підмножина послідовна, то\(\Gamma\) сама повинна бути послідовною.

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