10.2: Контур доказу
- Page ID
- 52827
Доказ теореми про повноту трохи складний, і при першому її прочитанні легко загубитися. Отже, виділимо доказ. Перший крок - це зсув перспективи, що дозволяє нам побачити шлях до доказу. Коли повнота розглядається як «коли б\(\Gamma \Entails A\) то не було»\(\Gamma \Proves A\), може бути важко навіть придумати ідею: бо показати, що\(\Gamma \Proves A\) ми повинні знайти деривацію, і це не схоже на гіпотезу, яка\(\Gamma \Entails A\) допомагає нам у цьому будь-яким чином . Для деяких доказових систем можна безпосередньо побудувати деривацію, але ми візьмемо дещо інший підхід. Необхідний зсув перспективи полягає в наступному: повнота також може бути сформульована як: «якщо\(\Gamma\) послідовна, вона задовольняється». Можливо, ми можемо використовувати інформацію\(\Gamma\) разом з гіпотезою, що вона послідовна для побудови структури, яка задовольняє кожне речення в\(\Gamma\). Адже ми знаємо, яку саме структуру ми шукаємо: таку, яка є такою, як її\(\Gamma\) описує!
Якщо\(\Gamma\) містить лише атомні речення, то для нього легко побудувати модель. Припустимо, атомні речення\(\Atom{P}{a_1,\dots,a_n}\) where the \(a_i\) are constant symbols. все форми Все, що нам потрібно зробити, це придумати домен\(\Domain{M}\) і призначення для\(P\) так що\(\Sat{M}{\Atom{P}{a_1,\ldots,a_n}}\). Але це не дуже складно: покласти\(\Domain{M} = \Nat\)\(\Assign{\Obj c_i}{M} = i\), і для кожного\(\Atom{P}{a_1,\ldots,a_n} \in \Gamma\), покласти кортеж\(\tuple{k_1, \dots, k_n}\) в\(\Assign{P}{M}\), де\(k_i\) індекс постійного символу\(a_i\) (тобто, \(a_i \ident \Obj c_{k_i}\)).
Тепер припустимо,\(\Gamma\) містить деяку формулу\(\lnot B\), з\(B\) атомарним. Ми можемо турбуватися, що будівництво\({\Struct{M}}\) заважає можливості\(\lnot B\) здійснити. Але ось де узгодженість\(\Gamma\) приходить: якщо\(\lnot B \in \Gamma\), то\(B \notin \Gamma\), або інакше\(\Gamma\) буде непослідовним. А якщо\(B \notin \Gamma\), то згідно з нашим будівництвом\({\Struct{M}}\)\(\SatN{M}{B}\), так\(\Sat{M}{\lnot B}\). Поки що добре.
Що робити, якщо\(\Gamma\) містить складні, неатомні формули? Скажімо, він містить\(A \land B\). Щоб зробити це правдою, ми повинні діяти так, ніби обидва\(A\) і\(B\) були в\(\Gamma\). А якщо\(A \lor B \in \Gamma\), то нам доведеться зробити хоча б один з них істинним, тобто діяти так, ніби один з них був в\(\Gamma\).
Це наштовхує на думку: ми додаємо додаткові формули\(\Gamma\) так, щоб (а) зберегти результуючий набір послідовним і (б) переконатися, що для кожного можливого атомного речення\(A\), або\(A\) є в результуючому множині, або\(\lnot A\) є, і (c) такий, що, всякий раз, коли\(A \land B\) знаходиться в\(A\) наборі\(B\), так і обидва і, якщо\(A \lor B\) є в наборі, принаймні один з\(A\) або\(B\) також, і т.д. ми продовжуємо робити це (потенційно назавжди). Викличте набір всіх формул, доданих таким чином\(\Gamma^*\). Тоді наша конструкція вище надала б нам структуру,\(\Struct{M}\) для якої ми могли б довести, шляхом індукції, що вона задовольняє всі речення в\(\Gamma^*\), а отже, і всі пропозиції\(\Gamma\) з тих пір\(\Gamma \subseteq \Gamma^*\). Виходить, що гарантування (а) і (б) досить. Набір речень, для яких (b) тримає, називається повним. Тож нашим завданням буде розширити послідовний набір\(\Gamma\) до послідовного та повного набору\(\Gamma^*\).
У цьому плані є одна зморшка: якщо\(\lexists{x}{A(x)} \in \Gamma\) ми будемо сподіватися, що зможемо вибрати якийсь постійний символ\(c\) і додати\(A(c)\) в цьому процесі. Але звідки ми знаємо, що завжди можемо це зробити? Можливо, у нас є лише кілька постійних символів у нашій мові, і для кожного з них у нас є\(\lnot A(c) \in \Gamma\). Ми також не можемо додати\(A(c)\), оскільки це зробить набір непослідовним, і ми не знали, чи\(\Struct{M}\) має зробити\(A(c)\) чи\(\lnot A(c)\) правда. Більше того, може статися так, що\(\Gamma\) містить лише речення мовою, яка взагалі не має постійних символів (наприклад, мова теорії множин).
Рішення цієї проблеми полягає в тому, щоб просто додати нескінченно багато констант на початку, плюс пропозиції, які пов'язують їх з кванторами правильним чином. (Звичайно, ми повинні переконатися, що це не може ввести невідповідність.)
Наша оригінальна конструкція добре працює, якщо у нас є лише постійні символи в атомних реченнях. Але мова може також містити символи функцій. У цьому випадку може бути складно знайти правильні функції,\(\Nat\) щоб призначити цим символам функцій, щоб все працювало. Отже, ось ще одна хитрість: замість того\(\Obj c_i\),\(i\) щоб використовувати для інтерпретації, просто візьміть набір постійних символів себе як домен. Потім\(\Struct M\) можна призначити кожен постійний символ собі:\(\Assign{\Obj c_i}{M} = \Obj c_i\). Але чому б не пройти весь шлях: нехай\(\Domain{M}\) будуть всі терміни мови! Якщо ми це зробимо, то існує очевидне призначення функцій (які приймають терміни як аргументи і мають терміни як значення) символам функцій: ми присвоюємо символу\(\Obj f^n_i\) функції функцію, яка, задані\(n\) терміни\(t_1\),...,\(t_n\) як input, виробляє термін\(\Obj f^n_i(t_1, \dots, t_n)\) як значення.
Останній шматок головоломки - що робити з\(\eq[][]\). Символ присудка\(\eq[][]\) має фіксоване тлумачення:\(\Sat{M}{\eq[t][t']}\) iff\(\Value{t}{M} = \Value{t'}{M}\). Тепер, якщо ми встановимо речі так, що значення терміна\(t\) є\(t\) самим собою, то ця структура не зробить жодного речення форми\(\eq[t][t']\) істинним, якщо\(t\) і не\(t'\) є одним і тим самим терміном. І звичайно, це проблема, оскільки в основному кожна цікава теорія в мові з символами функцій матиме як теореми речення,\(\eq[t][t']\) де\(t\) і не\(t'\) є одним і тим же терміном (наприклад, в теоріях арифметики:\(\eq[(\Obj 0+ \Obj 0)][\Obj 0]\)). Щоб вирішити цю задачу, ми змінюємо область\(\Struct M\): замість того, щоб використовувати терміни як об'єкти\(\Domain{M}\), ми використовуємо множини термінів, і кожен набір таким чином, щоб він містив усі ті терміни, яким речення\(\Gamma\) вимагають рівних. Так, наприклад, якщо\(\Gamma\) це теорія арифметики, то один з цих множин буде містити:\(\Obj 0\)\((\Obj 0 + \Obj 0)\)\((\Obj 0 \times \Obj 0)\),, і т.д. це буде набір\(\Obj 0\), якому ми присвоюємо, і вийде, що цей набір також є значенням всіх термінів в ньому, наприклад, також\((\Obj 0 + \Obj 0)\). Тому речення\(\eq[(\Obj 0+ \Obj 0)][\Obj 0]\) буде вірним в цій переглянутій структурі.
Так ось що ми будемо робити. Спочатку досліджуємо властивості повних послідовних множин, зокрема доведено, що повний узгоджений набір містить\(A \land B\), якщо він містить обидва\(B\),\(A\) і,\(A \lor B\) якщо містить хоча б одну з них тощо. ( Пропозиція 10.3.1). Потім визначаємо і досліджуємо «насичені» набори пропозицій. Насичений набір - це той, який містить умовні, які пов'язують кожне кількісне речення з екземплярами його (визначення 10.4.2). Ми показуємо, що будь-який послідовний набір Потім\(\Gamma\) can always be extended to a saturated set \(\Gamma'\) (Lemma 10.4.1). If a set is consistent, saturated, and complete it also has the property that it contains \(\lexists{x}{A(x)}\) iff it contains \(A(t)\) for some closed term \(t\) and \(\lforall{x}{A(x)}\) iff it contains \(A(t)\) for all closed terms \(t\) (Proposition 10.4.2). ми візьмемо насичений послідовний набір\({\Gamma'}\) і покажемо, що його можна розширити до насиченого, послідовного та повного набору\(\Gamma^*\) (Lemma 10.5.1). Цей набір\(\Gamma^*\) - це те, що ми будемо використовувати для визначення нашої моделі термінів\(\Struct M(\Gamma^*)\). Термінова модель має набір замкнутих термінів як свою область, а тлумачення його присудкових символів дається атомними реченнями в\(\Gamma^*\) (Визначення 10.6.1). Ми будемо використовувати властивості насичених, повних послідовних наборів, щоб показати, що дійсно\(\Sat{M(\Gamma^*)}{A}\) iff\(A \in \Gamma^*\) (Lemma 10.6.1), і, таким чином, зокрема,\(\Sat{M(\Gamma^*)}{\Gamma}\). Нарешті, ми розглянемо, як визначити термінову модель, якщо\(\Gamma\) contains \(\eq[][]\) as well (Definition 10.7.3) and show that it satisfies \(\Gamma^*\) (Lemma 10.7.1).