Една доказателствена процедура е коректна, когато във всяко доказателство с нея изводът следва логически от предпоставките. С други думи, ако в една коректна доказателствена процедура изведем дадено твърдение σ от множество от твърдения Δ, то имаме гаранцията, че σ ще следва логически от Δ. Съгласно дефиницията за логическо следване в 3.4 Синтаксис и семантика на предикатната логика, последното означава, че във всяка структура, в която са истинни твърденията в Δ, е истинно и твърдението σ.
Пълнотата е обратното на коректността. Една доказателствена процедура е пълна, когато всяко логическо следване между твърдения може да бъде доказано с процедурата. С други думи, ако някакво твърдение σ следва логически от множество от твърдения Δ, имаме гаранцията, че в процедурата съществува доказателство, което тръгва от твърденията в Δ и стига до твърдението σ (това обаче не значи, че имаме гаранцията, че ще успеем да открием това доказателство).
Ще покажем, че доказателствената процедура за предикатната логика, въведена в 3.5 Доказателствена процедура, е коректна и пълна.
Ще предпоставяме дефинициите на различните синтактични и семантични понятия, дадени в 3.4 Синтаксис и семантика на предикатната логика, като например тези на формула, твърдениe, свободни и свързани променливи, структура, универсум на дискурса, интерпретация, даване на стойности, модел, логическо следване, логическа еквивалентност, … и т.н.
С x, x1, …, xn обикновенно ще имаме предвид произволни променливи, а със c, c1, …, cn – произволни константи.
С изрази като α(x1…xn) ще имаме предвид формули, в които, ако има свободни променливи, те са измежду x1, …, xn. Важно при това означение е, че някои от променливите x1, …, xn може и да не са свободни във формулата α (в нея дори може да няма свободни променливи). По подобен начин с изрази като α(c1…cn) ще имаме предвид формули, в които (евентуално) участват константите c1, …, cn. Често последният вид изрази ще бъде употребяван в един и същ контекст с предишния вид изрази по следния начин. α(c1…cn) може да се получава от α(x1…xn) чрез заместване на всяко свободно участие на x1 с c1, на x2 с c2, … и т.н; както и обратно – α(x1…xn) да се получава от α(c1…cn) чрез заместване на константите c1, …, cn с новите променливи x1, …, xn (това че променливите са нови ни гарантира, че няма да бъдат свързани от квантори в α). Понякога, за краткост, след като сме започнали да говорим за α(x1…xn) или за α(c1…cn), ще говорим само за α, като ще подразбираме, че това е α(x1…xn) или α(c1…cn).
Ако А е някаква структура, a a1, …, an са някакви обекти от универсума на дискурса на А (не непременно различни), то с A ⊨ α(x1…xn)[a1…an] ще изразяваме това, че формулата α(x1…xn) е истинна в А, когато променливата x1 приеме като стойност a1, x2 приеме като стойност a2, …, xn приеме като стойност an. [a1…an] е определено даване на стойности на свободните променливи в α (ако има такива). Тук съответствието на променливите и обектите се определя от реда им отляво надясно в „x1…xn“ и „a1…an“, а не от индексите – първата променлива от ляво надясно взима за стойност първия обект от ляво надясно, втората – втория и т.н. Понякога, в съответствие със споменатото в горния параграф, ще изпускаме „(x1…xn)“, т.е. ще използваме само A ⊨ α[a1…an], като ще подразбираме, че α стои на мястото на α(x1…xn).
A ⊭ α(x1…xn)[a1…an] означава, че формулата α не е истинна в структурата A за това даване на стойности на свободните променливи в нея.
Ако F e n-местна буква за предикат, с FA ще имаме предвид интерпретацията на F в структурата А, т.е. това е множеството от наредени n-торки от обекти от универсума на А, което интерпретацията на символите в А дава на F.
„Термини“ ще наричаме свободните променливи и константите (когато искаме да остане неопределено дали говорим за променливи, или константи). За обозначаване на произволен термин ще използваме буквата „t“ (евентуално с индекс). В структурите термините обозначават обекти (ако терминът е свободна променлива, обектът е стойността, която променливата получава). Ще използваме изразите tА или tА(x1…xn)[a1…an] за обекта, който терминът t обозначава в структурата А. Вторият по-сложен израз е заради възможността t да е променлива. Ако t е константа, обозначаваният обект зависи само от интерпретацията и „(x1…xn)[a1…an]“ след tА е без значение. Ако обаче t е променлива, изразът t(x1…xn) показва, че тя трябва да една от променливите x1, …, xn, а „[a1…an]“ показва каква стойност получава всяка от тези променливи. Ако например t е x2, то tА(x1…xn)[a1…an] ще е a2 – t e втората променлива в поредицата x1, …, xn и затова получава като стойност втория обект от поредицата a1, …, an.
Ще използваме „iff“ като съкращение за „ако и само ако“ (от английското „if and only if“).
α1, …, αn ⇒ β означава, че формулата β следва логически от формулите α1, …, αn, т.е. във всяка структура, в която са истинни α1, …, αn, е истинна и β. Ако Δ е множество от формули (може и да е безкрайно), Δ ⇒ β означава, че от формулите в Δ следва логически β (във всяка структура, в която са истинни първите, е истинно и второто). Δ, α ⇒ β означава, че формулата β следва от формулите в Δ и формулата α.
α ⇔ β означава, че формулите α и β са логически еквивалентни, т.е. че имат една и съща истинностна стойност във всяка структура, за всяко даване на стойности на свободните им променливи (ако има такива).
α1, …, αn ⊢ β означава, че съществува доказателство (в рамките на някаква имана предвид доказателствена процедура), в което твърденията (формулите без свободни променливи) α1, …, αn са предпоставки и което завършва с твърдението β (заключението на доказателството). Ако Δ е множество (може и безкрайно) от твърдения, Δ ⊢ β означава, че съществува доказателство, в което твърдения от Δ са предпоставки, а твърдението β е заключение. Δ, α ⊢ β означава, че съществува доказателство, в което твърдения от Δ и твърдението α са предпоставки, а твърдението β е заключение.
Следното терминологично разграничение е важно в контекста на коректността и пълнотата. Ще казваме, че σ следва логически от Δ, за Δ ⇒ σ, и че σ е изводимо от Δ, за Δ ⊢ σ. Първото понятие е семантично, а второто се отнася до доказателствените процедури. Отношението между двете понятия поражда въпроса за коректността и пълнотата на доказателствените процедури.
Ще говорим за различни езици и тяхната лексика. Лексиката се състои от някакво множество букви за предикати (може и безкрайно – например „F1“, „F2“, …) и някакво множество константи (и то може да е безкрайно). Един език е напълно определен от неговата лексика. Езикът е множеството от всички формули (правилно образувани изрази, виж 3.4 Синтаксис и семантика на предикатната логика), които могат да се образуват от символите на лексиката, логическите символи („→“, „¬“, „∀“, …), спомагателните символи на скобите („(“ и „)“) и неограничено количесто променливи („x1“, „x2“, „x3“, …). Когато е дадено някакво множество от формули, ще предпоставяме, че то е част от някакъв език. Това би могъл да е езикът, чиято лексика се състои от предикатите и константите, участващи във формулите, но би могъл да е и език, чиято лексика освен тях включва букви за предикати или константи, които не участват във формулите.
Доказателствената процедура, чиято коректност и пълнота ще докажем, е доказателствената процедура за предикатната логика от 3.5 Доказателствена процедура. В нея се използват схеми за извод, схеми еквивалентности, една схема аксиома, една специална схема (екзистенциалната инстанциация) и два вида под-доказателства с допускане. По-определено, процедурата включва следното:
| Схеми за извод: |
| (От формулите отляво на „⊢“ може да се изведе формулата отдясно. α, β, γ и δ са произволни твърдения (формули без свободни променливи). „x“ е произволна променлива. „c“, „c1“ и „c2“ са произволни константи. α(x) е (евентуално) отворено изречение, в което променливата x е свободна.) |
| Модус поненс: α→β, α ⊢ β |
| Модус толенс: α→β, ¬β ⊢ ¬α |
| Дизюнктивен силогизъм: α∨β, ¬α ⊢ β |
| Хипотетичен силогизъм: α→β, β→γ ⊢ α→γ |
| Симплификация: α∧β ⊢ α |
| Добавяне: α ⊢ α∨β |
| Конюнкция: α, β ⊢ α∧β |
| Конструктивна дилема: α∨γ, (α→β)∧(γ→δ) ⊢ β∨δ |
| Абсорбиране: α→β ⊢ α→(α∧β) |
| Универсална инстанциация: ∀xα(x) ⊢ α(c) където α(c) е получено от α(x), като всички свободни участия на x в α(x) са заменени с константата c |
| Неразличимост на идентичните: c1=c2, α(c1) ⊢ α(c2) където α(c2) е получено от α(c1), като някои (не непременно всички) участия на c1 са заменени с c2 |
| Схеми еквивалентности: |
| (За разлика от схемите за извод, тук α, β и γ са формули, които могат да имат свободни променливи, т.е. трябва да се разглеждат като съкращения на α(x1…xn), β(x1…xn), γ(x1…xn). Схемите еквивалентности се използват въз основа на следното правило. Нека съответната схема е γ ⊣⊢ δ (или δ ⊣⊢ γ). Ако формулата γ е подформула на формулата φ и формулата ψ е получена от φ, като γ е заменена с δ, то ψ може да бъде изведена от φ. В частност подформулата на φ може да е самата φ. Тогава φ ще е γ, а ψ – δ. Неформално зад това правило стои принципа за заменимост на еквивалентните, съгласно който, ако в една формула заменим подформула с логически еквивалентна на нея, ще получим формула, която е логически еквивалентна на първата. Така че чрез схемите еквивалентности извеждаме твърдения, които са логически еквивалентни на предишни твърдения.) |
|
Транспозиция:
α→β ⊢ α→(α∧β) |
|
Двойно отрицание:
¬¬α ⊣⊢ α |
|
Експортиране:
(α∧β)→γ ⊣⊢ α→(β→γ) |
|
Материална импликация:
α→β ⊣⊢ ¬α∨β ¬(α→β) ⊣⊢ α∧¬β |
|
Де Морган:
¬(α∧β) ⊣⊢ ¬α∨¬β ¬(α∨β) ⊣⊢ ¬α∧¬β |
|
Комутация:
α∨β ⊣⊢ β∨α α∧β ⊣⊢ β∧α |
|
Асоциация:
α∧(β∧γ) ⊣⊢ (α∧β)∧γ α∨(β∨γ) ⊣⊢ (α∨β)∨γ |
|
Дистрибуция:
α∧(β∨γ) ⊣⊢ (α∧β)∨(α∧γ) α∨(β∧γ) ⊣⊢ (α∨β)∧(α∨γ) |
|
Материална еквивалентност:
α↔β ⊣⊢ (α→β)∧(β→α) α↔β ⊣⊢ (α∧β)∨(¬α∧¬β) |
|
Тавтология:
α∧α ⊣⊢ α α∨α ⊣⊢ α |
|
Връзка между кванторите:
¬∀xα ⊣⊢ ∃x¬α ∀x¬α ⊣⊢ ¬∃xα ¬∀x¬α ⊣⊢ ∃xα ∀xα ⊣⊢ ¬∃x¬α |
| Схеми аксиоми: |
| (Твърденията с тази форма могат да бъдат извеждани по всяко време без предпоставки.) |
| Идентичност със себе си: c=c където c е произволна константа |
| Други схеми: |
| Екзистенциална инстанциация: ∃α(x) ⊢ α(c) където α(c) е получена от α(x), като всички свободни участия на x са заменени с константата c и c не участва в предпоставките, заключението и предишни редове на доказателството или под-доказателството, в което се прилага тази схема |
| Под-доказателства с допускане: |
| (Γ е множеството от предпоставките, т.е. външните твърдения, използвани в под-доказателството. α и β са твърдения. α е допускането.) |
| Reductio ad absurdum: Ако Γ, α ⊢ β∧¬β, то Γ ⊢ ¬α |
| Условно доказателство: Ако Γ, α ⊢ β, то Γ ⊢ α→β |
Преди да се заемем с коректността и пълнотата, ще докажем един много базов факт за семантичните структури (че всяка структура е непротиворечива и определена) както и принципа за заменимост на еквивалентните, на който се базира използването на схемите еквивалентности.
В структурите формулите стават истинни или неистинни. Следната теорема ни гарантира, че всяка формула от езика на една структура е истинна или не в нея и че не е възможно една формула да е истинна и да не е истинна в нея. Поради семантичното правило за отрицанието (виж 3.4 Синтаксис и семантика на предикатната логика) това означава, че за всяка формула от езика на структурата важи, че или тя, или нейното отрицание са истинни в структурата, и че не е възможно една формула и нейното отрицание да са едновременно истинни в нея.
(1) Нека А е произволна структура, φ(x1…xn)1 е произволна формула от езика на A, и a1, …, an са произволни обекти от универсума на А. Тогава важи следното: А ⊨ φ[a1…an] или А ⊭ φ[a1…an], но не и двете.
Доказателство:
Ще използваме индукция по сложността на формулата φ. Условно определяме сложността на една формула по следния начин. Ако формулата е атомарна има сложност 0. Ако максималната сложност на подформулите ѝ, които са различни от нея, е s, то нейната сложност е s+1. Например, „Fx“ има сложност 0, „Fx ∧ Ga“ има сложност 1, „∃xFx ∧ Ga“ има сложност 2, „¬(Fx ∧ Ga)“ също има сложност 2, „∃x¬(Fx ∧ Ga)“ има сложност 3, … и т.н. Първо ще покажем, че доказваното положение е валидно за всички формули φ(x1…xn) със сложност 0. След това, допускайки, че е изпълнено за всички формули със сложност k (по-нататък ще наричаме това допускане „хипотеза на индикацията“), ще покажем, че е изпълнено и за всички формули със сложност k+1. Тогава се получава следното: положението е изпълнено за всички формули със сложност 0; значи е изпълнено за всички формули със сложност 1; значи е изпълнено за всички формули със сложност 2, … и т.н.; т.е. няма формула, за която да не е изпълнено. И така, нека φ(x1…xn) има сложност 0.
Случай 1, φ(x1…xn) е атомарна формула от вида Ft1…tm(x1…xn)2.
Разглеждаме произволна структура А и произволни обекти a1, …, an в нея. Нека t1A(x1…xn)[a1…an]3 е обектът b1, t2A(x1…xn)[a1…an] е обектът b2, …, tmA(x1…xn)[a1…an] е bm. Съгласно семантичните правила (виж 3.4 Синтаксис и семантика на предикатната логика), Ft1…tm(x1…xn)[a1…an] е истинно в А, ако и само ако наредената m-торка (b1, …, bm) е елемент на FA (множеството от наредени m-торки, които интерпретацията на А дава на буквата за предикат F). (b1, …, bm) е елемент или не е елемент на FA, но не и двете. Следователно А ⊨ Ft1…tm(x1…xn)[a1…an] или А ⊭ Ft1…tm(x1…xn)[a1…an], но не и двете (т.е. A ⊨ φ(x1…xn)[a1…an] или A ⊭ φ(x1…xn)[a1…an], но не и двете).
Случай 2, φ(x1…xn) е атомарна формула от вида t1=t2 (x1…xn).
Разглеждаме произволна структура А и произволни обекти a1, …, an в нея. Нека t1A(x1…xn)[a1…an] e обектът b1, а t2A(x1…xn)[a1…an] е обектът b2 в А. Съгласно семантичните правила А ⊨ t1=t2 (x1…xn)[a1…an], ако и само ако t1A(x1…xn)[a1…an] = t2A(x1…xn)[a1…an], т.е. ако и само ако b1 е същият обект като b2. b1 и b2 са различни обекти или един и същ обект, но не и двете. Следователно А ⊨ t1=t2 (x1…xn)[a1…an] или А ⊭ t1=t2 (x1…xn)[a1…an], но не и двете (т.е. в разглеждания случай положението е изпълнено).
Няма други формули със сложност 0. Затова сега допускаме, че доказваното положение важи за всички формули със сложност k и приемаме, че φ(x1…xn) има сложност k+1. Вече φ не може да атомарна формула (защото има сложност най-малко 1), а е или отрицание, или конюнкция, или дизюнкция, или импликация, или еквивалентност, или универсална формула, или екзистенциална формула. Ще покажем, че във всеки от тези случаи доказваното положение е изпълнено.
Случай 3, φ(x1…xn) има формата на отрицание, т.е. φ е ¬ψ(x1…xn).
Нека А е произволна структура и a1, …, an са произволни обекти в нея. Съгласно семантичните правила A ⊨ ¬ψ[a1…an], ако и само ако A ⊭ ψ[a1…an] (т.е. ако и само ако ψ[a1…an] не е истинно в А). От хипотезата на индукцията (понеже ψ(x1…xn) има сложност k), ψ[a1…an] или не е истинно в А, или е истинно в А (т.е. не е вярно, че не е истинно), но не и двете. Следователно, A ⊨ ¬ψ[a1…an] или A ⊭ ¬ψ[a1…an], но не и двете (т.е. в разглеждания случай положението е изпълнено).
Случай 4, φ(x1…xn) има формата на конюнкция, т.е. φ е ψ1∧ψ2(x1…xn).
Нека А е произволна структура и a1, …, an са произволни обекти в нея. Съгласно семантичните правила A ⊨ ψ1∧ψ2[a1…an], ако и само ако A ⊨ ψ1[a1…an] и A ⊨ ψ2[a1…an]. От хипотезата на индукцията, всяко от ψ1[a1…an] и ψ2[a1…an] или е истинно в A, или не е истинно в A, но не и двете. Следователно (взимайки предвид четирите възможни изключващи се случая за истинността или неистинността на ψ1[a1…an] и ψ2[a1…an] в A) A ⊨ ψ1∧ψ2[a1…an] или A ⊭ ψ1∧ψ2[a1…an], но не и двете (т.е. в разглеждания случай положението е изпълнено).
Случай 5, φ(x1…xn) има формата на дизюнкция, т.е. φ е ψ1∨ψ2(x1…xn).
Този случай е напълно аналогичен на Случай 4, като се използва семантичното правило за дизюнкцията вместо конюнкцията.
Случай 6, φ(x1…xn) има формата на импликация, т.е. φ е ψ1→ψ2(x1…xn).
Този случай е напълно аналогичен на Случай 4, като се използва семантичното правило за импликацията вместо конюнкцията.
Случай 7, φ(x1…xn) има формата на еквивалентност, т.е. φ е ψ1↔ψ2(x1…xn).
Този случай е напълно аналогичен на Случай 4, като се използва семантичното правило за еквивалентността вместо конюнкцията.
Случай 8, φ(x1…xn) е универсална формула, т.е. φ е ∀xiψ(x1…xi…xn).
Нека А е произволна структура и a1, …, an са произволни обекти в нея. Съгласно семантичните правила A ⊨ ∀xiψ(x1…xi…xn)[a1…an], ако и само ако за всеки обект b от универсума на А е изпълнено A ⊨ ψ(x1…xi…xn)[a1…b…an]. От хипотезата на индукцията за всеки обект b от А важи A ⊨ ψ(x1…xi…xn)[a1…b…an] или А ⊭ ψ(x1…xi…xn)[a1…b…an], но не и двете. Значи ψ(x1…xi…xn)[a1…b…an] ще бъде истинно за всеки обект b от А или това няма да е така, но не и двете. По семантичните правила, A ⊨ ∀xiψ(x1…xi…xn)[a1…an] или A ⊭ ∀xiψ(x1…xi…xn)[a1…an], но не и двете (т.е. в разглеждания случай положението е изпълнено).
Случай 9, φ(x1…xn) е екзистенциална формула, т.е. φ е ∃xiψ(x1…xi…xn).
Този случай е напълно аналогичен на Случай 8, като се използва семантичното правило за екзистенциалния квантор вместо за универсалния. С това индукцията и доказателството са завършени.
Върху този принцип почива използването на схемите еквивалентности в доказателствената процедура. Въпреки че формулата на всеки ред в едно доказателство е твърдение (т.е. в нея няма свободни променливи), когато използваме схеми еквивалентности бихме могли да заменим подформула на твърдение, в която има свободни променливи, така че ще докажем принципа за заменимост на еквивалентните за всякакви формули, не само за твърдения:
(2) Нека φ(x1…xn) е подформула на γ(x1…xn) и φ(x1…xn) ⇔ ψ(x1…xn). Нека още δ(x1…xn) е получено от γ(x1…xn) чрез замяната на φ(x1…xn)4 с ψ(x1…xn). Тогава γ(x1…xn) ⇔ δ(x1…xn).
Доказателство:
Както при доказателството на (1), ще използваме индукция, но този път тя няма да е по сложността на формулите, а по нещо, което ще наричаме „дълбочина“ на една подформула в една формула. Дефинираме дълбочината посредством сложността (дефинирана в доказателството на (1)) по следния начин: ако φ е подформула на γ, то дълбочинната на φ в γ е разликата между сложностите им. Като пример нека видим какви са дълбочините на различните подформули на „∀y(Gy ∧ ∃xFx)“. Тази формула има сложност 3. Подформулата ѝ „Fx“ (със сложност 0) има дълбочина 3 (3-0) в нея; „∃xFx“ (със сложност 1) има дълбочина 2 (3-1) в нея, „Gy ∧ ∃xFx“ (със сложност 2) има дълбочина 1 (3-2) в нея. Ако φ съвпада с γ, φ има дълбочина 0 в γ. Погледнато по-друг начин, дълбочината отговаря на нивото (отгоре-надолу, като се брои от 0), на което се намира подформулата в синтактичното дърво на формулата, от която е част (за синтактичните дървета виж 1.3 Таблици за истинност). Индукцията ще бъде по дълбочината на φ в γ в горната формулировка на принципа. И така, първо разглеждаме случая, когато φ(x1…xn) има дълбочина 0 в γ(x1…xn). Тогава γ съвпада с φ и ψ съвпада с δ и тъй като φ ⇔ ψ, то γ ⇔ δ.
Като следваща стъпка допускаме, че когато дълбочината на една подформула в една формула е k, принципът за заменимост на еквивалентните е валиден. Искаме да покажем, че тогава принципът ще е валиден и когато дълбочината на една подформула в една формула е k+1. Така че нека дълбочината на φ в γ е k+1. Тъй като дълбочината на φ в γ е най-малко 1, φ не може да съвпада с γ. Тогава непосредственият контекст на φ (най-простата, различна от нея формула, на която е подформула) е или отрицание, или конюнкция, или дизюнкция, или импликация, или еквивалентност, или екзистенциална формула, или универсална формула. Ще покажем, че във всички тези случаи доказваното положение, т.е. γ ⇔ δ, е изпълнено.
Случай 1, непосредственият контекст на φ(x1…xn) е отрицание, т.е. γ(x1…xn) е …¬φ…(x1…xn).
Нека А е произволна структура и a1, …, an са произволни обекти в нея. Тогава е изпълнено следното:
| A ⊨ ¬φ[a1…an] |
|
iff
(по семантичните правила) |
| A ⊭ φ[a1…an] |
|
iff
(от φ ⇔ ψ, защото φ и ψ имат еднаква истинностна стойност във всяка структура, за всяко даване на стойности на свободните им променливи) |
| A ⊭ ψ[a1…an] |
|
iff
(по семантичните правила) |
| A ⊨ ¬ψ[a1…an] |
Горната поредица от еквивалентности показва, че ¬φ и ¬ψ имат еднаква истинностна стойност във всяка структура, за всякакво даване на стойности на свободните им променливи, т.е. ¬φ ⇔ ¬ψ. Дълбочината на ¬φ в γ е k (за разлика от дълбочината на φ в γ, която е k+1) и значи (от хипотезата на индукцията) за тази формула заменимостта на еквивалентните важи. Тъй като в случая δ се получава от γ не само чрез замяна на φ с ψ, но и чрез замяна на ¬φ с ¬ψ, по заменимостта на еквивалентните получаваме γ ⇔ δ.
Случай 2, непосредственият контекст на φ(x1…xn) е конюнкция, т.е. γ(x1…xn) е …(φ∧χ)…(x1…xn) или …(χ∧φ)…(x1…xn).
Нека А е произволна структура и a1, …, an са произволни обекти в нея. Тогава е изпълнено следното:
| A ⊨ φ∧χ[a1…an] |
|
iff
(по семантичните правила) |
| A ⊨ φ[a1…an] и A ⊨ χ[a1…an] |
|
iff
(от φ ⇔ ψ) |
| A ⊨ ψ[a1…an] и A ⊨ χ[a1…an] |
|
iff
(по семантичните правила) |
| A ⊨ ψ∧χ[a1…an]5 |
Горната поредица от еквивалентности показва, че φ∧χ ⇔ ψ∧χ. Дълбочината на формулата φ∧χ в γ е k и значи (от хипотезата на индукцията) за тази формула заменимостта на еквивалентните важи. Тъй като в случая δ се получава от γ също и чрез замяна на φ∧χ с ψ∧χ (за които принципът важи), значи γ ⇔ δ.
Случай 3, непосредственият контекст на φ(x1…xn) е дизюнкция, т.е. γ(x1…xn) е …(φ∨χ)…(x1…xn) или …(χ∨φ)…(x1…xn).
Този случай е напълно аналогичен на Случай 2, като се използват семантичните правила за дизюнкцията вместо конюнкцията.
Случай 4, непосредственият контекст на φ(x1…xn) е импликация, в която φ(x1…xn) е антецедент, т.е. γ(x1…xn) е …(φ→χ)…(x1…xn).
Този случай е напълно аналогичен на Случай 2, като се използват семантичните правила за импликацията вместо конюнкцията.
Случай 5, непосредственият контекст на φ(x1…xn) е импликация, в която φ(x1…xn) е консеквент, т.е. γ(x1…xn) е …(χ→φ)…(x1…xn).
Този случай е напълно аналогичен на Случай 2, като се използват семантичните правила за импликацията вместо конюнкцията.
Случай 6, непосредственият контекст на φ(x1…xn) е еквивалентност, т.е. γ(x1…xn) е …(φ↔χ)…(x1…xn) или …(χ↔φ)…(x1…xn).
Този случай е напълно аналогичен на Случай 2, като се използват семантичните правила за еквивалентността вместо конюнкцията.
Случай 7, φ(x1…xn) е обхватът на екзистенциален квантор, т.е. γ(x1…xn) е …∃xiφ…(x1…xi…xn).
Нека А е произволна структура и a1, …, an са произволни обекти в нея. Тогава е изпълнено следното:
| A ⊨ ∃xiφ(x1…xi…xn)[a1…an] |
|
iff
(по семантичните правила) |
| За някакъв обект b от универсума на А, A ⊨ φ(x1…xi…xn)[a1…b…an] |
|
iff
(от φ ⇔ ψ) |
| За някакъв обект b от универсума на А, A ⊨ ψ(x1…xi…xn)[a1…b…an] |
|
iff
(по семантичните правила) |
| A ⊨ ∃xiψ(x1…xi…xn)[a1…an] |
Горната поредица от еквивалентности показва, че ∃xiφ(x1…xi…xn) ⇔ ∃xiψ(x1…xi…xn). Тъй като дълбочината на ∃xiφ(x1…xi…xn) в γ e k, заменимостта на еквивалентните важи за тази формула, и тъй като в случая δ се получава от γ също и чрез замяната на ∃xiφ(x1…xi…xn) с ∃xiψ(x1…xi…xn), то γ ⇔ δ.
Случай 8, φ(x1…xn) е обхватът на универсален квантор, т.е. γ(x1…xn) е …∀xiφ…(x1…xi…xn).
Този случай е напълно аналогичен на Случай 7, като се използват семантичните правила за универсалния квантор вместо за екзистенциалния.
Разгледахме всички случаи за една подформулата φ(x1…xn) на една формула γ(x1…xn), когато дълбочината ѝ в γ(x1…xn) е к+1, и видяхме, че принципът за заменимост на еквивалентните е изпълнен (при условие, че е изпълнен за подформули с дълбочина к). С това индукцията и доказателството са завършени.
Използвайки символиката, която въведохме в Понятия и означения по-горе, коректността на една доказателствена процедура може да се изрази накратко така:
За всяко множество от твърдения Δ и всяко твърдение σ, ако Δ ⊢ σ, то Δ ⇒ σ.
Ще покажем, че за нашата доказателствена процедура е изпълнено следното:
(3.1) Ако в едно доказателство няма под-доказателства с допускане и всеки ред, който не е предпоставка и не е изведен с екзистенциална инстанциация, следва логически от предишни редове или е логически валидно твърдение, то заключението на това доказателство следва логически от предпоставките му.
(3.2) Всички схеми за извод са логически валидни. (Т.е. във всяка структура, в която са истинни твърдения с формата на предпоставките им, са истинни и съответните твърдения с формата на заключенията им.)
(3.3) Всички схеми еквивалентности са логически валидни. (T.е., ако схемата е γ ⊣⊢ δ и някакви формули φ(x1…xn) и ψ(x1…xn) имат формата съответно на γ и δ, то φ(x1…xn) и ψ(x1…xn) са логически еквивалентни.)
(3.4) Всички схеми аксиоми са логически валидни. (T.е., ако едно твърдени има формата на схема аксиома, то е истинно във всяка структура.)
(3.5) За всяко под-доказателство с допускане „Ако Γ, p ⊢ r, то Γ ⊢ q“, където Γ e множеството от предпоставките на под-доказателството (т.е. използваните външни твърдения), p e допускането, а q е заключението му 6, важи: ако Γ, p ⇒ r, то Γ ⇒ q.
Тогава доказателствената процедура ще е коректна поради следното. Да разгледаме произволно доказателство в нея с предпоставки твърденията от някакво множеството Δ и заключение някакво твърдението σ. Искаме да покажем, че σ следва логически от Δ.
Първо, нека приемем, че в доказателството не се използват под-доказателства с допускане. Тогава (3.1)-(3.4) гарантират, че σ следва логически от Δ поради следното. В такова доказателство за всяко твърдение p, което не е част от предпоставките Δ и не е изведено с екзистенциална инстанциация, имаме три възможности. Първо, p може да има формата на схема аксиома и съответно да е изведено без предпоставки. Въз основа на (3.4) в този случай p е логически валидно твърдение. Второ, p може да е получено от предишни редове по някаква схема за извод, която въз основа на (3.2) е логически валидна, и значи в изводите, направени с нея, заключенията следват логически от предпоставките. Трето (и последно), p може да е получено от твърдението q на някакъв предишен ред по някаква схема еквивалентност, като някаква подформула φ(x1…xn) на q е била заменена с формулата ψ(x1…xn). Въз основа на (3.3), φ(x1…xn) и ψ(x1…xn) са логически еквивалентни и тогава от доказания в (2) принцип за заменимост на еквивалентните следва, че p и q са логически еквивалентни твърдения и значи p следва логически от q. Получава се, че всеки ред, който не е предпоставка и не е изведен с екзистенциална инстанциация, или следва логически от предишни твърдения, или е логически валидно твърдение. Въз основа на (3.1) тогава σ следва логически от Δ.
Нека сега премахнем ограничението в доказателството да няма под-доказателства с допускане. Напротив, нека си представим, че в него има под-доказателства, в рамките на които има други, в рамките на които има други, … и т.н. Ясно е, че при такива вериги от включени едно в друго под-доказателства винаги се стига до под-доказателства, в които няма други под-доказателства. Последните са всъщност обикновени доказателства от вида Γ, p ⊢ r, където Γ са външни за под-доказателството твърдения, а p е допускането. За такива доказателства в горния параграф показахме, че са коректни (при условието на (3.1)-(3.5)), т.е. имаме Γ, p ⇒ r, от което въз основа на (3.5) следва Γ ⇒ q, с други думи заключението на под-доказателството следва логически от някакви твърдения преди под-доказателството. Това ни дава възможност да елиминираме под-доказателството, като просто го изтрием и оставим само заключението му q. Единственото, което ни интересува е, че q следва логически от някакви предишни твърдения. Да си представим за момент, че няма други под-доказателства на нивото на изтритото, т.е. няма други под-доказателства, които са започнати в същото по-горно под-доказателство, в което е започнато изтритото. Въпросното по-горно под-доказателство ще се превърне в поредица от редове, която започва с допускането му и всеки следващ ред, който не е логически валиден и не е изведен с екзистенциална инстанциация, следва логически от някакви предишни редове7. Точно както с първото изтрито под-доказателство, от (3.1) и (3.5) следва, че заключението на това по-горно под-доказателство следва логически от някакво множество по-ранни, външни за него твърдения, което отново ни дава възможност да го изтрием, като оставим само заключението му. По този начин, тръгвайки от най-крайните под-доказателства и вървейки нагоре, като изтрием всички под-доказателства, това което ще остане накрая е една поредица от твърдения, започваща с предпоставките на цялото доказателство Δ и завършваща със заключението му σ, в която няма под-доказателства, и в която всяко твърдение, което не е част от Δ и не е изведено с екзистенциална инстанциация, или следва логически от някакви предишни твърдения, или е логически валидно. Но тогава, въз основа на (3.1), σ ще следва логически от Δ, което и искахме да покажем.
Доказателството за коректност ще е завършено, когато покажем, че положенията (3.1)-(3.5) са изпълнени за нашата доказателствена процедура. Най-същественото от тях е (3.1), което всъщност се отнася до използването на екзистенциална инстанциация по принцип.
Да разгледаме отново положение (3.1):
Ако в едно доказателство няма под-доказателства с допускане и всеки ред, който не е предпоставка и не е изведен с екзистенциална инстанциация, следва логически от предишни редове или е логически валидно твърдение, то заключението на това доказателство следва логически от предпоставките му.
Неговият смисъл е, че екзистенциалната инстанциация не компрометира доказателствената процедура. Въпреки че тази схема не е логически валидна, (3.1) ни гарантира, че ако останалите схеми са логически валидни, заключенията на доказателствата и под-доказателствата ни ще следват от предпоставките им въпреки тази невалидна схема за извод. Това е възможно благодарение на ограниченията върху използването ѝ. Както може да се види от Доказателствената процедура, тези ограничения са, че инстанциираната константа не трябва да участва 1) в предпоставките, 2) в заключението, 3) в предишни редове на доказателството или под-доказателството, в което прилагаме схемата.
Доказателство на (3.1):
Да разгледаме произволно доказателство, в което няма под-доказателства с допускане и в което всяко твърдение, което не е предпоставка и не е изведено с екзистенциална инстанциация, следва логически от предишни твърдения или е логически валидно. Нека предпоставките на това доказателство са твърдения от множеството Δ, a заключението му е твърдението σ. Искаме да покажем, че σ следва логически от Δ. Буквите за предикати и константите, участващи в твърденията от Δ и в σ, определят някакъв език L (те са неговата лексика). За да докажем, че Δ ⇒ σ, т.е. че всеки модел на Δ е модел и на σ, ще разгледаме произволна структура А с език L, в която всички твърдения в Δ са истинни, и ще покажем, че σ също е истинно в А. За целта ще конструираме структура, която е обогатяване на А.
По принцип, една структура А′ с език L′ се нарича обогатяване на една структура А с език L, когато А′ e същата структура като А с тази разлика, че в лексиката на езика ѝ (L′) има допълнителни символи, които тя интерпретира по някакъв начин. Така че лексиката на L е правилно подмножество на лексиката на L′. За структурите и техните обогатявания важи следното. Първо, твърденията, които са истинни в структурата А, са истинни и в обогатяването ѝ А′, защото допълнителните символи от L′ не участват в тези твърдения и нямат отношение към определянето на истинностната им стойност в А′, а абстрахирайки се от допълнителните символи в L′, двете структури са една и съща структура. Второ, всички твърдения от езика на структурата А, които са истинни в нейното обогатяване А′, са истинни и в A. Поради това, че по отношение на по-бедния език L двете структури не се различават, в тях са истинни едни и същи твърдения от този по-беден език. Обратният на обогатяване термин е обедняване – когато А′ е обогатяване на А, А е обедняване на А′.
Връщайки се към доказателството на (3.1), за да покажем, че във всяка структура А, в която са истинни твърденията от Δ, е истинно и σ, ще конструираме структура А′, която е обогатяване на А и в която всички редове от доказателството (включително редовете изведени с екзистенциална инстанциация) са истинни. Това значи, че и σ ще е истинно в А′. Тъй като твърдението σ е от езика на А и е истинно в А′, то ще бъде истинно и в А (обедняването на А′), което искаме да покажем. Допълнителните символи в А′ ще бъдат, въведените чрез екзистенциална или универсална инстанциация нови константи в извеждането на σ от Δ.8 Това е идеята на доказателството, следва самото то.
Нека c1, …, cn са всички нови (не от лексиката на L) константи, които са въведени чрез екзистенциална или универсална инстанциация в доказателството на σ от Δ, като редът им отговаря на последователността на появата им в доказателството. Като ги добавим към лексиката на L получаваме нов, по-богат език L′. Разглеждаме следната поредица от структури:
А, А1, А2, …, Аn (=A′)
Структурата А1 е обогатяване на структурата А, като езикът ѝ се получава от този на А, чрез добавянето на константата c1. А2 e обогатяване на А1, като езикът ѝ се получава от този на А1 чрез добавянето на константата c2, … и т.н. Структурата Аn е последната в тази редица и съвпада с А′ (обогатяването, за което говорихме в горния параграф). Всяка една константа ci от константите c1, …, cn се появява за първи път в някакъв ред на доказателството като част от твърдението φi(ci), което e изведено от ∃φi(x)9 на по-горен ред по екзистенциална инстанциация или от ∀xφi(x) по универсална инстанциация. Ще дефинираме всяка една структура Аi от структурите А1, А2, …, Аn, като в същото време ще покажем, че всички твърдения в доказателството до φi(ci) включително са истинни в Аi.
Първо, твърденията на всеки ред в доказателството до момента, в който се появява първата нова константа c1 в φ1(c1), са истинни в структурата A, защото са или предпоставки в доказателството (и са истинни в А според началното приемане), или са логически валидни твърдения (и са истинни във всяка структура, включително в А), или следват логически от предишни твърдения, които следват от предишни твърдения, … и т.н., като в началото на тези вериги стоят или предпоставките на доказателството или логически валидни твърдения (и двете истинни в А), а логическото следване гарантира истинност на заключенията в структурите, в които са истинни предпоставките. Щом всички твърдения преди φ1(c1) са истинни в А, то и твърдението, от което φ1(c1) е изведено – ∃xφ1(x) или ∀xφ1(x) (в зависимост от това, дали е изведено с екзистенциална или универсална инстанциация) – е истинно в А. Това (по семантичните правила) означава, че в универсума на A има (поне един) обект а1, за който важи А ⊨ φ1(x)[а1]. Определяме структурата А1 като обогатяване на A, като интерпретираме новата константа c1 с обекта а1. Тогава от А ⊨ φ1(x)[а1] следва А1 ⊨ φ1(c1), т.е. φ1(c1) е истинно в А1. Освен това всички предишни твърдения също са истинни в А1, защото са истинни в А, а А1 е обогатяване на А. С това едновременно определихме А1 и показахме, че всички твърдения в доказателството до φ1(c1) включително са истинни в А1. Продължаваме с А2. До момента, в който в доказателството се появява новата константа c2 като част от твърдението φ2(c2) (получено по екзистенциална или универсална инстанциация от ∃xφ2(x) или ∀xφ2(x)), всички твърдения са истинни в А1, защото са логически валидни или следват логически от твърдения, за които вече показахме, че са истинни в А1. Следователно в А1 е истинно и въпросното твърдение ∃xφ2(x) или ∀xφ2(x), от което е изведено φ2(c2). От семантичните правила следва, че в А1 има (поне един) обект а2, за който в изпълнено А1 ⊨ φ2(x)[а2]. А2 се получава от А1 като интерпретираме c2 с а2. Тогава от А1 ⊨ φ2(x)[а2] следва А2 ⊨ φ2(c2), т.е. φ2(c2) е истинно в А2 и освен това в А2 са истинни всички твърдения преди него, защото са истинни в А1, а А2 е обогатяване на А1. С това едновременно определихме А2 и показахме, че всички твърдения в доказателството до φ2(c2) включително са истинни в А2 … и така нататък. Продължаваме по същия начин докато стигнем до момента, в който в доказателството чрез екзистенциална или универсална инстанциация се извежда φn(cn). Тогава по същия начин едновременно определяме Аn (което по-рано нарекохме А′) и показваме, че всички твърдения в доказателството до φn(cn) включително са истинни в Аn. Ако твърдението φn(cn) е изведено с екзистенциална инстанциация, то не може да е заключението на доказателството σ, защото ограниченията върху екзистенциалната инстанциация забраняват в заключението на доказателството да участват константи, въведени с екзистенциална инстанциация, но (тъй като по-нататък в доказателството няма екзистенциални инстанциации) σ е изведено посредством логически валидни изводи и значи следва логически от твърдения, които са истинни в Аn. Следователно σ също е истинно в Аn. Но тогава, тъй като σ е от езика на А, a Аn е обогатяване на А (ясно е, че обогатяването на обогатяването на една структура е нейно обогатяване), то σ е истинно в А, което искахме да покажем. Тъй като A беше произволна структура, получава се, че във всяка структура, в която са истинни твърденията в Δ, е истинно и твърдението σ, т.е. σ следва логически от Δ. Доказателството на (3.1) е завършено.
До тук (тъй като не използвахме нищо специфично от нашата доказателствена процедура) всъщност показахме, че всяка доказателствена процедура, която използва валидни схеми за извод, валидни схеми еквивалентности и валидни схеми аксиоми, която използва коректни под-доказателства с допускане и в която единствената логически невалидна схема за извод е екзистенциалната инстанциация (с ограниченията върху нея) е коректна. Сега остава да покажем, че в частност нашата доказателствена процедура е такава, като покажем, че изпълнява (3.2)-(3.4) (използваните схеми са логически валидни) и (3.5) (двете под-доказателства с допускане са коректни).
За всяка схема за извод φ1, …, φn ⊢ ψ в Доказателствената процедура без последните две (универсална инстанциация и неразличимост на идентичните)10 може да се провери (с таблица за истинност или истинностно-функционален анализ), че ако свържем конюнкцията на предпоставите им в импликация със заключението им, ще получим тавтология, т.е. че (φ1∧…∧φn)→ψ е тавтология. Съгласно (1), всяко твърдение α, β, γ или δ във φ1, …, φn и ψ получава някаква истинностна стойност в която и да е структура А, което от своя страна определя по някакъв начин (по семантичните правила за логическите съюзи) истинностните стойности на φ1, …, φn и ψ. Тогава, ако предпоставките φ1, …, φn са истинни в А, (т.е. конюнкцията им φ1∧…∧φn е истинна в А), заключението ψ също трябва да е истинно в А, защото в противен случай импликацията (φ1∧…∧φn)→ψ би имала стойност Н, което противоречи на факта, че е тавтология. Следователно във всяка структура, в която са истинни предпоставките, е истинно и заключението, т.е. схемата за извод е логически валидна. Нека видим защо универсалната инстанциация и неразличимостта на идентичните също са валидни.
За универсалната инстанциация (∀xα(x) ⊢ α(c)). Нека твърдението ∀xα(x) е истинно в произволна структура A, т.е. A ⊨ ∀xα(x). Интерпретацията на А отнася към константата c някакъв обект b от универсума на А. По семантичните правила за универсалния квантор от A ⊨ ∀xφ(x) следва, че за всеки обект а от универсума на А е изпълнено A ⊨ φ[a]. Значи в частност за обекта b ще е изпълнено A ⊨ φ[b]. Тъй като константата c обозначава b, от A ⊨ φ[b] следва A ⊨ φ(c). Получихме, че във всяка структура, в която е истинно ∀xφ(x), е истинно и φ(c), т.е. ∀xα(x) ⇒ α(c).
За неразличимостта на идентичните (c1=c2, α(c1) ⊢ α(c2)). Нека твърденията c1=c2 и α(c1) са истинни в произволна структура А, т.е. A ⊨ c1=c2 и A ⊨ α(c1). Константата c1 обозначава някакъв обект а от универсума на А и от A ⊨ c1=c2 (по семантичните правила) следва, че c2 обозначава също a. Заменяйки тези участия на c1 в α(c1), които са заменени с c2, за да се поучи α(c2), с някаква нова променлива x, ще получим формулата α(x) (това, че x е нова, гарантира, че всичките ѝ участия са свободни в α(x)). Тогава от A ⊨ α(c1) следва A ⊨ α(x)[a] (т.е. α(x) е истинно в А, когато x приеме като стойност обекта, с който е интерпретирана c1). Но от последното и факта, че c2 е интерпретирана също с a, следва A ⊨ α(c2). Получихме, че във всяка структура, в която са истинни твърденията c1=c2 и α(c1), е истинно и α(c2), което означава, че последното твърдение следва логически от първите две. С това показахме, че всички схеми за извод в доказателствената ни процедура са логически валидни.
Преминаваме към схемите еквивалентности. За всяка схема еквивалентност φ ⊣⊢ ψ в Доказателствената процедура без последната (четирите форми на връзката между кванторите)11 може да се провери с таблица за истинност или истинностно-функционален анализ, че φ↔ψ е тавтология. Нека А е произволна структура и а1, …, а1 са произволни обекти в нея. Съгласно (1), формулите α(x1…xn), β(x1…xn) и γ(x1…xn)12, които участват като подформули в φ и ψ, са истинни ли неистинни в А за а1, …, аn, т.е. α(x1…xn)[а1…аn], β(x1…xn)[а1…аn] и γ(x1…xn)[а1…аn] са истинни или не в А. Това от своя страна определя по някакъв начин (съгласно семантичните правила за логическите съюзи) истинностните стойности на φ(x1…xn)[а1…аn] и ψ(x1…xn)[а1…аn] в А. Тези истинностни стойности трябва да са еднакви в А, защото обратното означава, че формулата φ↔ψ може да получи стойност Н, което противоречи на факта, че е тавтология. Получава се, че φ и ψ имат еднаква истинностна стойност във всяка структура за всякакви стойности на свободните им променливи, т.е. φ ⇔ ψ.
За връзката между кванторите. Относно ¬∀xα ⊣⊢ ∃x¬α: въз основа на семантичните правила за произволна структура А и произволни обекти a1, …, an в нея важи следното:
| A ⊨ ¬∀xiα(x1…xi…xn)[a1…an] |
| iff |
| A ⊭ ∀xiα(x1…xi…xn)[a1…an] |
| iff |
| За някакъв обект а от А, A ⊭ α(x1…xi…xn)[a1…a…an] |
| iff |
| За някакъв обект а от А, A ⊨ ¬α(x1…xi…xn)[a1…a…an] |
| iff |
| A ⊨ ∃xi¬α(x1…xi…xn)[a1…an] |
Получава се, че ¬∀xα и ∃x¬α имат една и съща истинностна стойност във всяка структура за всякакви стойности на свободните им променливи, т.е. ¬∀xα ⇔ ∃x¬α.
Относно ∀x¬α ⊣⊢ ¬∃xα: въз основа на семантичните правила за произволна структура А и произволни обекти a1, …, an в нея важи следното:
| A ⊨ ∀xi¬α(x1…xi…xn)[a1…an] |
| iff |
| За всеки обект а от А, A ⊨ ¬α(x1…xi…xn)[a1…a…an] |
| iff |
| За всеки обект а от А не е вярно, че A ⊨ α(x1…xi…xn)[a1…a…an] |
| iff |
| Не е вярно, че за някакъв обект а в А, A ⊨ α(x1…xi…xn)[a1…a…an] |
| iff |
| Не е вярно, че A ⊨ ∃xiα(x1…xi…xn)[a1…an] |
| iff |
| A ⊨ ¬∃xiα(x1…xi…xn)[a1…an] |
Получава се, че ∀x¬α и ¬∃xα имат една и съща истинностна стойност във всяка структура за всякакви стойности на свободните им променливи, т.е. ∀x¬α ⇔ ¬∃xα.
Относно ¬∀x¬α ⊣⊢ ∃xα: въз основа на семантичните правила за произволна структура А и произволни обекти a1, …, an в нея важи следното:
| A ⊨ ¬∀xi¬α(x1…xi…xn)[a1…an] |
| iff |
| Не е вярно, че A ⊨ ∀xi¬α(x1…xi…xn)[a1…an] |
| iff |
| Не е вярно, че за всеки обект а от А, A ⊨ ¬α(x1…xi…xn)[a1…a…an] |
| iff |
| Не е вярно, че за всеки обект а от А не е вярно, че A ⊨ α(x1…xi…xn)[a1…a…an] |
| iff |
| За някакъв обект a от A, A ⊨ α(x1…xi…xn)[a1…a…an] |
| iff |
| A ⊨ ∃xiα(x1…xi…xn)[a1…an] |
Получава се, че ¬∀x¬α и ∃xα имат една и съща истинностна стойност във всяка структура за всякакви стойности на свободните им променливи, т.е. ¬∀x¬α ⇔ ∃xα.
Относно ∀xα ⊣⊢ ¬∃x¬α: въз основа на семантичните правила за произволна структура А и произволни обекти a1, …, an в нея важи следното:
| A ⊨ ¬∃xi¬α(x1…xi…xn)[a1…an] |
| iff |
| Не е вярно, че A ⊨ ∃xi¬α(x1…xi…xn)[a1…an] |
| iff |
| Не е вярно, че за някакъв обект а от А, A ⊨ ¬α(x1…xi…xn)[a1…a…an] |
| iff |
| Не е вярно, че за някакъв обект а от А не е вярно, че A ⊨ α(x1…xi…xn)[a1…a…an] |
| iff |
| За всеки обект a от A, A ⊨ α(x1…xi…xn)[a1…a…an] |
| iff |
| A ⊨ ∀xiα(x1…xi…xn)[a1…an] |
Получава се, че ∀xα и ¬∃x¬α имат една и съща истинностна стойност във всяка структура за всякакви стойности на свободните им променливи, т.е. ∀xα ⇔ ¬∃x¬α. С това логическата валидност на връзката между кванторите и изобщо на схемите еквивалентности е доказана.
Що се отнася до единствената схема аксиома, идентичността със себе си (c=c), валидността ѝ е директно следствие от семантичното правило за знака за идентичност („=“).
Остава да покажем, че за двете под-доказателства с допускане, reductio ad absurdum (aко Γ, α ⊢ β∧¬β, то Γ ⊢ ¬α) и условно доказателство (ако Γ, α ⊢ β, то Γ ⊢ α→β) е валидно (3.5) (За всяко под-доказателство с допускане „Ако Γ, p ⊢ r, то Γ ⊢ q“ важи: ако Γ, p ⇒ r, то Γ ⇒ q), т.е. трябва да докажем:
Ако Γ, α ⇒ β∧¬β, то Γ ⇒ ¬α
Ако Γ, α ⇒ β, то Γ ⇒ α→β
За първото положение: нека Γ, α ⇒ β∧¬β и нека всяко твърдениe в Γ е истинно в произволна структура A (А ⊨ Γ). Ако α е истинно в А, от А ⊨ Γ и Γ, α ⇒ β∧¬β следва, че β∧¬β трябва да е истинно в А, което въз основа на (1) е невъзможно. Следователно α не е истинно в А, от което по семантичните правила следва А ⊨ ¬α. Получава се, че ако Γ, α ⇒ β∧¬β, то всеки модел на Γ е модел на ¬α, т.е. Γ ⇒ ¬α, което и трябваше да се докаже.
За второто положение: нека Γ, α ⇒ β и нека за произволна структура А, А ⊨ Γ. Ако α не е истинно в А, по семантичните правила α→β е истинно в А. Ако α е истинно в А, от А ⊨ Γ и Γ, α ⇒ β следва, че β също е истинно в А, и значи (по семантичните правила) α→β е истинно в А. Значи при всички положения α→β е истинно в А. Получава се, че ако Γ, α ⇒ β, то всеки модел на Γ е модел на α→β, т.е. Γ ⇒ α→β, което и трябваше да се докаже.
С това доказателството за коректността на доказателствената процедура е завършено. Преминаваме към доказателството за пълнотата ѝ.
Досега използвахме следните определения за коректност и пълнота. Една доказателствена процедура е коректна, когато за всяко множество от твърдения Δ и всяко твърдение σ е изпълнено, че ако σ е изводимо от Δ, σ следва логически от Δ:
| 1) | Ако Δ ⊢ σ, то Δ ⇒ σ. (коректност) |
Една доказателствена процедура е пълна, когато за всяко Δ и σ е изпълнено, че ако σ следва логически от Δ, σ е изводимо от Δ:
| 2) | Ако Δ ⇒ σ, то Δ ⊢ σ. (пълнота) |
Освен с термините изводимост и логическо следване, коректността и пълнотата могат да бъдат изразени и с термините консистентност и удовлетворимост, които в случая имат следното значение.
Едно множеството от твърдения Δ е консистентно, ако от него не може да се изведе противоречие, т.е. ако не съществува твърдение p, за което е изпълнено Δ ⊢ p∧¬p. Съответно, Δ е неконсистентно, ако съществува твърдение p, за което е изпълнено Δ ⊢ p∧¬p. Понятието за консистентност (в дефинирания смисъл) е от същата сфера като това за изводимост – то предпоставя някаква доказателственa процедура, по отношение на която множествата от твърдения са консистентни, или не. Едно множество от твърдения може да консистентно по отношение на една доказателствена процедура и неконсистентно по отношение на друга, така както едно твърдение може да е изводимо от някакви предпоставки при използването на една доказателствена процедура и да не е изводимо при използването на друга.
Едно множество от твърдения Δ е удовлетворимо, ако има модел (т.е., ако съществува структура, в която всяко твърдение в Δ е истинно). Съответно Δ е неудовлетворимо, ако няма модел. Вместо „удовлетворимо“ и „неудовлетворимо“ често ще използваме по-експлицитното „има модел“ и „няма модел“. Понятието за удовлетворимост е от същата сфера като това за логическо следване – и двете се отнасят до семантиката и не зависят от доказателствените процедури.
Коректността и пълнотата могат да се определят чрез термините консистентност и удовлетворимост по следния начин. Една доказателствена процедура е коректна, когато за всяко множество от твърдения Δ е изпълнено:
| 3) | Ако Δ е удовлетворимо (ако има модел), то Δ е консистентно. (коректност) |
Една доказателствена процедура е пълна, когато за всяко множество от твърдения Δ е изпълнено:
| 4) | Ако Δ е консистентно, то Δ е удовлетворимо (има модел). (пълнота) |
Ще покажем, че условията 1) и 3), от една страна, и 2) и 4), от друга, са еквивалентни и следователно е все едно кои от двете двойки понятия (изводимост – логическо следване или консистентност – удовлетворимост) ще използваме.
Относно еквивалентността на 1) и 3). Да приемем първо, че 1) е изпълнено (изводимостта имплицира логическо следване). Искаме да покажем, че тогава 3) също е изпълнено (удовлетворимостта имплицира консистентност). Да допуснем, че някакво множество от твърдения Δ е неконсистентно, т.е. Δ ⊢ p∧¬p (за някакво твърдение p). От 1) следва, че Δ ⇒ p∧¬p, т.е. всеки модел на Δ е модел и на p∧¬p, но тъй като, съгласно (1), всяка структура е непротиворечива, последното означава, че Δ няма модели. Това показва, че при условието на 1), ако едно множество от твърдения е неконсистентно, то не e удовлетворимо. Последното по контрапозиция е еквивалентно на 3) (ако едно множество е удовлетворимо, то е консистентно), така че от 1) следва 3).
Обратно, нека 3) е изпълнено (удовлетворимостта имплицира консистентност). Искаме да покажем, че тогава и 1) е изпълнено (изводимостта имплицира логическо следване). Да допуснем обратното – нека някакво твърдение σ е изводимо от някакво множество от твърдения Δ (Δ ⊢ σ), но σ не следва логически от Δ (Δ ⇏ σ). Последното значи, че има структура, която е модел на Δ, но не е модел на σ, и следователно (по семантичното правило за отрицанието) е модел на ¬σ. Следователно множеството от твърдения, получено като към Δ се добави ¬σ (такова множество често се означава с Δ∪{¬σ}13) е удовлетворимо. От последното и 3) следва, че Δ∪{¬σ} е консистентно, което противоречи на Δ ⊢ σ (тъй като σ е изводимо от Δ, добавянето на ¬σ към Δ прави полученото множество неконсистентно). Следователно, допускането ни (Δ ⇏ σ) е неистинно и значи, ако 3) е изпълнено, то и 1) е изпълнено. С това показахме, че двете формулировки на условието за коректност 1) и 3) са еквивалентни.
Преди да покажем, че условията за пълнота 2) и 4) също са еквивалентни, ще докажем следното положение.
(4) Ако твърдението σ не може да бъде изведено от множеството от твърдения Δ (т.е. ако Δ ⊬ σ), то Δ∪{¬σ}14 е консистентно.
Доказателство:
Ако едно множество е неконсистентно, от него може да се изведе всяко твърдение поради следното. По дефиниция, неконсистентността на множеството означава, че за някакво твърдение p от него може да се изведе p∧¬p. От последното твърдение може да се изведе произволно твърдение q например по следния начин:
| 1. p∧¬p |
| 2. p 1, симплификация |
| 3. ¬p 1, комутация и симплификация |
| 4. p∨q 2, добавяне |
| 5. q 3, 4, дизюнктивен силогизъм |
Нека условието на доказваното положение е изпълнено: Δ ⊬ σ. Множеството от твърдения Δ е консистентно, защото иначе всяко твърдение щеше да е изводимо от него, включително σ. Да допуснем отрицанието на това което искаме да покажем: Δ∪{¬σ} е неконсистентно. Значи за някакво твърдение p важи Δ∪{¬σ} ⊢ p∧¬p. Тогава от твърденията в Δ можем да изведем следното:
| 1. ¬σ допускане |
| 2. p∧¬p от Δ и 1, използвайки доказателството Δ∪{¬σ} ⊢ p∧¬p |
| 3. ¬¬σ 1-2, reductio ad absurdum |
| 4. σ 3, двойно отрицание |
Получихме Δ ⊢ σ, което противоречи на началното условие. Значи допускането ни не е вярно и Δ∪{¬σ} е консистентно. Доказателството е завършено.
Нека сега видим защо 2) и 4) са еквивалентни. Да приемем първо, че 2) е изпълнено (логическото следване имплицира изводимост) и с цел противоречие да допуснем, че 4) не е изпълнено, т.е. някакво множество от твърдения Δ е консистентно, но няма модел. От последното следва (тривиално), че всеки модел на Δ е модел на σ и че всеки модел на Δ е модел на ¬σ, т.е. че както σ, така и ¬σ следват логически от Δ. Но тогава, от 2), както σ, така и ¬σ ще са изводими от Δ (и значи, по схемата за извод конюнкция, ще е изводимо σ∧¬σ), т.е. Δ е неконсистентно, което противоречи на допускането, и значи допускането не е вярно, т.е. 4) e изпълнено, ако е изпълнено 2).
Обратно, нека 4) е изпълнено (консистентността имплицира удовлетворимост). С цел противоречие да допуснем, че 2) не е изпълнено, т.е. че някакво твърдение σ следва логически от някакво множество от твърдения Δ, но не може да бъде изведено от тях. Въз основа на (4) от последното следва, че Δ∪{¬σ} е консистентно и значи, въз основа на 4), има някакъв модел А. В А е истинно ¬σ, но в А е истинно и σ, защото σ следва логически от Δ, а А e модел на Δ. Това обаче противоречи на (1) (структурите са непротиворечиви). Следователно допускането ни не е вярно и 2) е изпълнено, когато е изпълнено 4). С това показахме, че 2) и 4), двете алтернативни формулировки на пълнотата на една доказателствена процедура, са еквивалентни.
По-горе доказахме коректността на нашата доказателствена процедура в термините на изводимост и логическо следване. За пълнотата на процедурата ще използваме другите два термина – консистентност и удовлетворимост. Преди това обаче ще въведем някои понятия и ще докажем някои положения от теория на множествата, които ще използваме в доказателството за пълнота.
Множествата се определят напълно от това, кои са елементите им, поради което стандартен начин за обозначаването им е като по някакъв начин се укаже кои са елементите им. Например, {a, b, c} е множеството, чиито елементи са обектите a, b и c. Понякога ще използваме същата нотация и за безкрайните множества. Например множеството на естествените числа може да се означи така: {0, 1, 2, …}. Третият начин за обозначаване, който ще използваме, е просто със символи – големи латински букви.
Ако X и Y са множества, тяхното обединение X∪Y е множеството, което съдържа елементите на X и елементите на Y и в което няма други елементи. Може да говорим за обединението на повече от две множества посредством множеството от тези множества, като сложим голям знак за обединение отпред. Например, ако X, Y и Z са някакви множества, тяхното обединение (събирането на елементите им в едно множество) е ⋃{X, Y, Z}. Тази нотация е особено полезна, когато искаме да говорим за обединението на безкрайно много множества. Например, ако X1, X2, X3, … е безкрайна поредица от множества, то ⋃{X1, X2, X3, …} е тяхното обединение – множеството от тези и само тези неща, които са елементи на поне едно от множествата X1, X2, X3, … .
Под функция ще разбираме определено отнасяне на всеки от елементите на едно множество към един и само един елемент от друго множество (двете множества може и да съвпадат). Например, ако X е множеството {1, 2, 3}, a Y е множеството {3, 4, 5}, то отнасянето на 1 към 4, на 2 към 3, и на 3 към себе си е една функция. Нека означим тази функция с f. Елементите на X се наричат аргументи на f (съответно X e множеството от аргументи на f), a елементите на Y, към които f отнася елементи на X, се наричат стойности на f (съответно Y е множеството от стойности на f). Всичко това накратко се означава така, f: X → Y. Елементът y от множеството Y, към който f отнася елементa x от множеството X, се означава с f(x) – оттам и добре познатата ни идентичност от средното училище f(x) = y.
Всяка функция отнася всеки един елемент на X (множеството от аргументите ѝ) към само един елемент на Y (множеството от стойностите ѝ), но би могла да отнесе два или повече елемента на X към един елемент на Y. Когато това не е така, т.е. когато няма елемент на Y, към който да е отнесен повече от един елемент на X, ще казваме, че функцията е one-to-one. Освен това всяка функция отнася всеки един елемент на X към някакъв елемент на Y, но сред елементите на Y може да има такива, към които не е отнесен елемент на X. Когато това не е така, т.е. когато към всеки елемент на Y е отнесен (един или повече от един) елемент на X, ще казваме, че функцията е on-to.
Ако една функция f: X → Y е едновременно one-to-one и on-to ще я наричаме биекция или взаимно-еднозначно съответствие между X и Y. Съществуването на (поне една) биекция между две множества X и Y (т.е. one-to-one и on-to функция, чието множество от аргументи и множество от стойности са съответно X и Y) ни гарантира, че елементите на X и Y могат да се съпоставят така, че на всеки елемент от едното множество да отговаря точно един елемент от другото – всеки елемент на X е съпоставен с един и само един елемент на Y и в Y няма елемент, на който не е съпоставен елемент на X. Когато множествата са крайни, изброяването на елементите им показва дали броят им е еднакъв, или не. Когато обаче са безкрайни, изброяване не е възможно. Тогава съществуването на биекция между тях е единственият начин, чрез който може да се осмисли твърдението, че „количеството“ на елементите им е едно и също. Независимо дали две множества са крайни или безкрайни, сравняването на броя на елементите им в теория на множествата се осмисля и дефинира посредством понятието за биекция. X и Y имат еднакъв брой елементи, когато съществува поне една биекция между тях; и имат различен брой елементи, когато не съществува биекция между тях.
Ще наричаме едно множество броимо, ако е крайно или ако е безкрайно, но съществува биекция между него и множеството на естествените числа {0, 1, 2, 3, …}. Във втория случай биекцията позволява елементите на това безкрайно множество да бъдат номерирани. (Номерирането на елементите на крайните множества очевидно е винаги възможно.) Не всички безкрайни множества са броими15. Следват две теореми за броимите множества.
(5) Обединението на две броими множества е броимо множество.
Доказателство:
Нека X и Y са броими множества. Можем да приемем, че те нямат общи елементи, защото искаме да покажем, че обединението им не е твърде „голямо“ (така че вече да не е броимо), а ако нямат общи елементи обединението им е „най-голямото възможно“. Ако X и Y са крайни, обединението им също е крайно, и значи е броимо. Нека и двете са безкрайни. Понеже са броими, можем да разглеждаме елементите им като номерирани. Тогава отнасяме произволен елемент a от X∪Y към следното естествено число: ако а е n-тият елемент (броейки от 0) на X, отнасяме а към n-тото четно число, т.е. към 2n. Ако а е n-тия елемент на Y, отнасяме a към n-тото нечетно число, т.е. към 2n+1. По този начин получаваме взаимно еднозначно съответствие (биекция) между елементите на X∪Y и естествените числа, защото, първо, всеки елемент от X∪Y е отнесен към различно естествено число и, второ, няма естествено число, към което да не е отнесен елемент на X∪Y, така че X∪Y е броимо. Ако едното множество е крайно, а другото е безкрайно, това отнасяне на елементи от обединението им към естествени числа ще е такова, че не на всяко естествено число ще отговаря елемент от обединението, но затова пък всеки елемент от обединението ще е номериран с различно (уникално за него) естествено число. Тогава можем да преномерираме елементите на X∪Y по следния начин: на елемента с най-малко число сега отнасяме 0 (то си е 0), на елемента със следващото по големина число сега отнасяме 1, на елемента със следващото по големина число сега отнасяме 2, … и т.н. Ясно е, че по този начин получаваме биекция между естествените числа и X∪Y (всеки елемент на X∪Y е отнесен към различно естествено число и, понеже X∪Y е безкрайно, няма естествено число, към което да не е отнесен елемент на X∪Y), т.е. X∪Y е броимо. Въпросното преномериране показва по принцип, че ако успеем да отнесем всеки елемент от едно безкрайно множество към различно (уникално за него) естествено число (независимо, че не към всяко естествено число е отнесен елемент), то множеството е броимо (ще използваме това по-нататък). Край на доказателството.
(6) Множеството от всички крайни поредици от елементи на едно броимо множество е броимо множество.
Доказателство:
Доказваното положение е очевидна истина, ако множеството е крайно, така че нека X е безкрайно броимо множество и нека Y е множеството от всички крайни поредици от елементи на X. Ще покажем, че всеки елемент на Y може да се отнесе към различно (уникално за него) естествено число. От това ще следва, че Y e броимо (виж края на горното доказателство).
Тъй като X е броимо, съществува биекция f между X и множеството на естествените числа, която номерира елементите на X, като номерът на произволен елемент a от X e f(a). Тогава отнасяме всеки един елемент (а1, …, аn) на Y към следното естествено число:
2f(a1)+1 . 3f(a2)+1 . … . pnf(an)+1
Това е произведение от степени на първите n прости числа (2 е първото просто число, 3 е второто, 5 е третото, …, pn е n-тото). Всеки член на произведението отговаря на елемент от крайната поредица (а1, …, аn). На а1 отговаря 2f(a1)+1, на а2 отговаря 3f(a2)+1, …, на аn отговаря pnf(an)+1. Степента, на която се повдига всяко от простите числа, е номерът на ai, даван му от биекцията f, плюс 1. Добавянето на единица е защото е възможно стойността на f за някое ai да е 0, от което pif(ai) би станало 1 – искаме да изключим тази възможност. В аритметиката съществува теорема, доказана още от Евклид, наречена „Основната теорема на аритметиката“, която гласи, че всяко естествено число по-голямо от 1 е уникално произведение от прости множители16. Тази теорема ни гарантира, че всеки елемент на Y, т.е. всяка крайна поредица (а1, …, аn) от елементи на X, ще получи нейно си, уникално число поради следното. Първо, ако две поредици имат различен брой елементи, в произведението на тази с повечето елементи ще участва просто число, което не участва в другото произведение, и, второ, ако двете поредици са еднакво дълги, щом са различни, някакъв елемент от едната ще е различен от съответния от другата, поради което степента на отговарящото на този елемент просто число ще е различна в двете произведения. (Причината да добавяме единица към степенните показатели е, че ако степента е 0, простото число с тази степен ще изчезне от произведението.) Така всеки елемент на Y ще получи различно произведение от прости числа, а (съгласно Основната теорема на аритметиката) няма две различни произведения от прости числа, които да са равни на едно и също число – значи всеки елемент на Y ще получи различно естествено число. От това следва, че Y (множеството от всички крайни поредици от елементи на X) е броимо. Край на доказателството.
Искаме да покажем, че ако едно множество от твърдения (формули без свободни променливи) Δ е консистентно, то има модел. Δ може и да е безкрайно множество. Твърденията в Δ са част от някакъв език L, чиято лексика включва множество от букви за предикати и множество от константи, като и двете могат да са празни. Лексиката в естествените езици (думите) е крайно множество, но ние няма да налагаме това ограничение върху формалните езици – единственото което ще предпоставим е, че двете множества, от които се състои лексиката на L, са броими. Например, тя би могла да включва безкрайното броимо множество от предикати {F1, F2, …} и безкрайното броимо множество от константи {c1, c2, …}. Тъй като съгласно (5) обединението на две броими множества е броимо множество, в този случай лексиката на L (обединението на множеството на константите и множеството на предикатите) ще е броимо (безкрайно) множество. От (5) също следва, че ако решим да обогатяваме един език, можем да добавяме към лексиката му нови и нови (включително безкрайно много) символи, като лексиката му ще продължи да бъде броимо множество, ако добавените символи са броимо множество.
За разлика от лексиката на един език L, която може и да е крайно множество, самият език L винаги е безкрайно множество от формули. Това е така дори когато лексиката е празна (в езика няма букви за предикати и константи), защото тогава L ще съдържа например твърденията „∀x x=x“, „(∀x x=x) ∧ (∀x x=x)“, „(∀x x=x) ∧ (∀x x=x) ∧ (∀x x=x)“, … и т.н. От (5) и (6) следва, че ако лексиката на L е броимо множество (което ние предпоставяме), то L също ще е броимо множество. Това е така поради следното. Символите, които участват във формулите (правилно образуваните изрази) на L, са броимо (безкрайно) множество, защото освен лексиката тези символи включват още краен брой логически и спомагателни символи („¬“ , „∀“, скобите, … и т.н.) и броимо безкрайно множество от променливи („x1“, „x2“, …). Въз основа на (5) множеството от всички символи в L е броимо, тъй като е обединението на три броими множества (лексиката, логическите символи и променливите). Но щом символите са броимо множество, от (6) следва, че всички възможни крайни поредици от символи образуват броимо множество, и тъй като формулите (правилно-образуваните изрази) са тяхно под-множество (всяка формула е крайна поредица от символи), то L (множеството от всички формули) също ще е броимо множество (аргументът с преномерирането от края на доказателството на (5)).
От това че, ако един език има броима лексика, то той самият е броим, следва, че ако обогатим лексиката му с произволно, броимо множество (включително безкрайно) нови символи, полученият по-богат език ще продължи да бъде броимо множество, тъй като въз основа на (5) лексиката му (която е обединение на две броими множества) ще бъде броимо множество (ще използваме това по-долу).
Ще наричаме едно множество от твърдения от даден език „пълно“ (тази пълнота е нещо различно от пълнотата на една доказателствена процедура), когато за всяко твърдение p от езика, p или ¬p му е елемент. Ще ни интересуват множества от твърдения, които са едновременно консистентни и пълни. Можем да мислим за такива множества като теории, които имат мнение за абсолютно всичко – т.е. съдържат отговор на всеки възможен въпрос, който може да се формулира в езика. В доказателството на теоремата за пълнота ще използваме следното общо положение, което гарантира, че чрез добавяне на твърдения всяко консистентно множество може да стане пълно (продължавайки да бъде консистентно):
(7) (Лема на Линденбаум) Нека Δ е произволно консистентно множество от твърдения от някакъв език L. Тогава Δ може да бъде разширено до множество от твърдения Γ, което е консистентно и пълно (т.е. за всяко твърдение от L важи, че или то, или неговото отрицание е част от Γ).
Доказателство:
Нека Δ е консистентно множество от твърдения от някакъв език L. Тъй като (както предпоставяме) L е броимо множество, то множеството от всички твърдения в L (което е подмножество на L) също е броимо, т.е. можем да подредим тези твърдения в безкрайна редица (отговаряща на редицата на естествените числа): φ1, φ2, …, φn, … . По отношение на тази редица разглеждаме безкрайна редица от разширения на множеството от твърдения Δ: Δ1, Δ2, …, Δn, …, в която всяко разширение се получава от предишното по следния начин. Δ1 се получава от Δ така: ако φ1 e консистентно с Δ, т.е. ако множеството, което се получава като φ1 се добави към Δ, е консистентно, добавяме φ1 към Δ (в случай, че вече не е там). В противен случай, добавяме ¬φ1. Това може да се каже по-кратко така: ако Δ∪{φ1} е консистентно, то Δ1 е Δ∪{φ1}; ако Δ∪{φ1} не е консистентно, то Δ1 е Δ∪{¬φ1}. Δ2 се получава от Δ1 по същия начин, но с оглед на φ2: ако Δ1∪{φ2} е консистентно, то Δ2 е Δ1∪{φ2}; ако Δ1∪{φ2} не е консистентно, то Δ2 е Δ1∪{¬φ2} … и т.н.
Ще покажем, че всяко Δn е консистентно множество от твърдения. Δn се получава от предишното множество от твърдения по един и същи начин, като започваме от консистентното множество Δ. Така че е достатъчно да покажем, че този един и същи начин запазва консистентността на множествата, т.е. да покажем, че ако Δn-1 е консистентно, то и Δn е консистентно. Ако Δn-1∪{φn} е консистентно, то това е всъщност Δn и значи тогава Δn е консистентно. Ако Δn-1∪{φn} не е консистентно, понеже Δn-1 е консистентно, това означава, че φn не е вече елемент на Δn-1 и не може да бъде изведено от Δn-1. От последното и (4) следва, че Δn-1∪{¬φn} е консистентно, но това е Δn. Значи във всички случаи Δn е консистентно (в случай, че Δn-1 е такова).
Нека Γ е обединението на всички тези разширения на Δ, т.е. Γ е ⋃{Δ1, Δ2, …, Δn, …}. Ще покажем, че Γ e консистентно и пълно разширение на Δ (т.е. множеството от твърдения, което търсим). Първо, то съдържа Δ, тъй като съдържа Δ1, което е Δ∪{φ1} или Δ∪{¬φ1}. Второ, Γ е консистентно поради следното. Да допуснем, че не е, т.е. Γ ⊢ p∧¬p за някакво твърдение p. Значи съществува доказателство, което (като всяко доказателство) използва някакво крайно множество от предпоставки от Γ и стига до p∧¬p. Понеже всяко твърдение в Γ или вече е в Δ, или е добавено при конструирането на някое Δn от Δn-1, то можем да вземем такова m (достатъчно голямо), че всички тези краен брой предпоставки, от които се извежда p∧¬p, да са в Δm. Но това би означавало, че Δm е неконсистентно, което е в противоречие с факта, че всяко от разширенията на Δ е консистентно. Значи Γ е консистентно множество от твърдения. Трето, конструкцията на Γ показва, че е пълно множество: отначало подредихме всички твърдения от езика L в редицата φ1, φ2, …, φn, … и за всяко φn или то, или неговото отрицание е в Δn, а всяко Δn е подмножество на Г; значи или φn, или ¬φn е в Γ. Край на доказателството.
Преминаваме към доказателството за пълнота на доказателствената процедура. Ще тръгнем от произволно консистентно множество от твърдения Δ от език L и ще покажем, че Δ има модел. Ще минем през следните главни стъпки. Първо ще добавим към лексиката на L едно изброимо безкрайно множество от нови константи, получавайки по-богатия език L′, след което ще разширим Δ до едно консистентно и пълно в L′ множество Γ, което, разглеждано като теория, имплицира, че всичко което (според тази теория) съществува е обозначено от някоя от добавените нови константи. След това ще конструираме модел на Γ А′, в който, грубо казано, обектите ще са самите константи на L′ (константите ще обозначават самите себе си). Тъй като Δ е подмножество на Γ, А′ ще е модел на Δ. Тогава обедняването А на структурата А′ до езика L17 ще е търсената структура за езика L, която е модел на Δ, защото А′ е модел на Δ, А е обедняване на А′ до езика L, а Δ е от L. Това е идеята на доказателството, сега преминаваме към самото него.
Нека Δ е произволно консистентно множество от твърдения (формули без свободни променливи) от произволен език L. Нека езикът L′ е получен от L, като към лексиката на L е добавено броимо безкрайно множество от нови константи {c1, c2, …, cn, …}. Предвид на казаното по-горе, L′ е броимо множество от формули и значи всяко негово подмножество също е броимо. Това позволява да подредим в безкрайна редица (съответстваща на редицата на естествените числа) всички твърдения в L′ от вида ∃xφ(x) („x“ строи на мястото на която и да е променлива). Нека тази редица е: ∃xφ1(x), ∃xφ2(x), …, ∃xφn(x), …18. По отношение на всяко от тези екзистенциални твърдения конструираме последователно разширения на Δ в езика L′: Δ1, Δ2, …, Δn, … по следния начин. Δ1 се получава от Δ чрез добавянето на ∃xφ1(x)→φ1(ci), където ci е първата константа от {c1, c2, …, cn, …}, която не се среща в φ1 (тъй като φ1 е от L′, в нея може и да участват някои от новите константи), и φ1(ci) е получено от φ1(x) чрез замяната на всички свободни участия на x с ci. (Нека обърнем внимание, че ci не се среща в Δ (предишното множество от твърдения) – това ще се повтаря при следващите разширения.) Съответно, Δ2 се получава от Δ1 чрез добавянето на ∃xφ2(x)→φ2(ci), където ci е първата константа от {c1, c2, …, cn, …}, която не се среща в φ1 и φ2. (Следователно ci не се среща в Δ1, тъй като всички константи от {c1, c2, …, cn, …}, които участват в твърдения от Δ1, участват само в φ1.) … и т.н. Съответно, Δn се получава от Δn-1 чрез добавянето на ∃xφn(x)→φn(ci), където ci е първата константа от {c1, c2, …, cn, …}, която не се среща във φ1, φ2, …, φn. (Константите от {c1, c2, …, cn, …}, които се срещат във φ1, φ2, …, φn, са краен брой, така че можем да говорим за първата, която не се среща в тези твърдения.) Освен това ci не участва в твърденията в Δn-1, тъй като единствените константи от {c1, c2, …, cn, …}, които участват в твърдения от Δn-1, участват само в φ1, φ2, …, φn-1.
Ще покажем, че всяко едно от разширенията на Δ – Δ1, Δ2, …, Δn, … е консистентно множество от твърдения. За целта, понеже всяко се получава от предишното по един и същи начин, като се започва с консистентното множество Δ (за което можем да мислим като Δ0), е достатъчно да покажем, че ако Δn е консистентно, то и Δn+1 e консистентно. С цел противоречие да допуснем противното – че Δn е консистентно, а Δn+1 е неконсистентно. Тъй като неконсистентното множество Δn+1 е всъщност Δn∪{∃xφn+1(x)→φn+1(c)}, то за някакво твърдение p е изпълнено Δn, ∃xφn+1(x)→φn+1(c) ⊢ p∧¬p. Като използваме само предпоставки от Δn, можем да изведем следното:
| 1. ∃xφn+1(x) допускане |
| 2. φn+1(c) 1, EI (в предпоставките от Δn не участва c)19 |
| 3. ¬∃xφn+1(x) ∨ φn+1(c) 2, добавяне и комутация |
| 4. ∃xφn+1(x) → φn+1(c) 3, материална импликация |
| 5. p∧¬p Δn, 4, тъй като Δn, ∃xφn+1(x) → φn+1(c) ⊢ p∧¬p (повтаряме доказателството) |
| 6. ¬∃xφn+1(x) 1-5, reductio ad absurdum |
| 7. ¬∃xφn+1(x) ∨ φn+1(c) 6, добавяне |
| 8. ∃xφn+1(x) → φn+1(c) 7, материална импликация |
| 9. p∧¬p Δn, 8, тъй като Δn, ∃xφn+1(x) → φn+1(c) ⊢ p∧¬p (повтаряме доказателството) |
Получава се, че Δn е неконсистентно, което противоречи на първата част от допускането ни (че Δn е консистентно). Следователно цялото ни допускане (че Δn е консистентно, a Δn+1 не е) е невярно, т.е. ако Δn е консистентно, то Δn+1 също е такова. С това показахме, че всяко от Δ1, Δ2, …, Δn, … е консистентно.
Да разгледаме ⋃{Δ1, Δ2, …, Δn, …} – обединението на всички тези разширения на Δ. Ще покажем, че то също е консистентно. Да допуснем, че не е, т.е. ⋃{Δ1, Δ2, …, Δn, …} ⊢ p∧¬p за някакво твърдение p. С други думи, съществува доказателство в процедурата, която (като всяко такова доказателство) използва някакво крайно множество от предпоставки от ⋃{Δ1, Δ2, …, Δn, …} и стига до p∧¬p. Понеже всяко твърдение в ⋃{Δ1, Δ2, …, Δn, …} или вече е в Δ, или е добавено при конструирането на някое Δn+1 от Δn, то можем да вземем такова m (достатъчно голямо), че всички тези (краен брой) предпоставки, от които се извежда p∧¬p, да са в Δm. Но това би означавало, че Δm е неконсистентно, което противоречи на това, че всяко от разширенията на Δ е консистентно. Значи ⋃{Δ1, Δ2, …, Δn, …} е консистентно множество от твърдения.
Въз основа на (7) съществува пълно и консистентно разширение на ⋃{Δ1, Δ2, …, Δn, …}. Да наречем това съдържащо Δ, консистентно и пълно в L′ множество от твърдения Γ.
Всяко пълно и консистентно множество от твърдения (Γ включително) има следното (много удобно) свойство: ако едно твърдение може да бъде изведено от него, то вече е в него. С други думи от пълните множества не може да бъде изведено нищо, което вече не им е елемент. Това е така поради следното. Да говорим за Γ и да приемем, че за произволно твърдение σ е изпълнено Γ ⊢ σ. От пълнотата на Γ следва, че σ или ¬σ са елементи на Γ, но второто заедно с Γ ⊢ σ би означавало, че Γ е неконсистентно. Значи σ вече е елемент на Γ. По-долу многократно ще използваме това свойство, за да заключаваме, че, понеже някакви твърдения са изводими от Γ, те са негови елементи.
Конструкцията на Γ е такава, че всяко нещо, за което Γ твърди, че съществува, е обозначено от някаква константа от езика L′. Това е така, защото за всяко екзистенциално твърдение ∃xφ(x) от L′, в Γ се съдържа твърдението ∃xφ(x)→φ(c), където c e константа от {c1, c2, …, cn, …}. Γ беше конструирано така, защото предварителната идея е обектите в търсения модел на Γ да са константите от езика на Γ (константи, които обозначават самите себе си). Много е възможно обаче Γ20 да съдържа твърдения, от които да следва, че някакви обекти са обозначени от повече от една константи. Затова обектите на структурата, която ще конструираме за Γ и която (в съответствие с по-горе, когато излагахме основните стъпки на доказателството) ще наречем А′, няма да са константи от L′, а ще са множества от константи от L′. По този начин, ако от Γ следва, че няколко константи обозначават един и същ обект, този обект ще може да бъде множеството от тези константи (това нямаше да е възможно, ако обектите от универсума бяха самите константи – различните константи са различни обекти). За да определим универсума на структурата А′ въвеждаме следното означение:
Ако c е произволна константа от L′, то [c] е множеството от тези и само тези константи d от L′, за които e изпълнено, че твърденията „c=d“ и „d=c“ са елементи на Γ.
Използвайки горното означение, определяме универсума на дискурса на А′ така:
Mножеството от всички [c], където c е константа от L′
Нека видим какво следва от определението на универсума на А′. Първо, за всяка константа c от L′, [c] е един единствен обект – някакво множество от константи от L′. Това е така, защото за всяка константа d от L′ или е изпълнено, че „c=d“ и „d=c“ са елементи на Γ (и тогава d е елемент на [c]), или не е изпълнено (и тогава d не е елемент на [c]). Значи за всяка константа c от L′ има един и само един обект (множество от константи) [c]. В същото време нищо не пречи за някакви константи c1 и c2, [c1] и [c2] да е едно и също множество. Следователно обектите в универсума на А′ не са повече от константите в L′, което значи, че универсумът на А′ е броимо множество, защото константите на L′ са броимо множество.
Второ, за никоя константа c от L′, [c] не е празно множество, защото поне c му е елемент. Това е така, защото въз основа на схемата за извод идентичност със себе си твърдението „c=c“ е изводимо от Γ и значи е елемент на Γ (поради свойството на пълните множества, за което говорихме по-горе), от което въз основа на дефиницията на [c] следва, че c е елемент на [c]. Така че [c] съдържа най-малко c, но може да съдържа и други константи от L′.
Едно друго следствие от определянето на универсума на А′ изисква по-дълго обосноваване, поради което ще го номерираме и докажем като теорема:
(8) Ако c и d са константи от L′, то [c]=[d], ако и само ако „c=d“ е елемент на Γ.
Доказателство:
Едната посока на тази еквивалентност се вижда лесно: ако [c]=[d] (т.е. [c] и [d] са едно и също множество), тъй като d е елемент на [d] (виж първото следствие по-горе), значи d е елемент на [c]. От последното (по дефиниция) следва, че твърдението „c=d“ е елемент на Γ.
За обратната посока (ако „c=d“ е елемент на Γ, то [c]=[d]) ще използваме факта, че следните две твърдения, изразяващи съответно симетричността и транзитивността на релацията на идентичност (за формалните свойства на релациите, виж 3.5 Доказателствена процедура), са изводими в доказателствената ни процедура без предпоставки и значи са изводими и от твърденията в Γ (без да ги използваме). Тъй като Γ е пълно множество от твърдения, щом някакви твърдения са изводими от него, те са в него.
| ∀x∀y(x=y → y=x) (симетричност на идентичността) |
| ∀x∀y∀z[(x=y ∧ y=z) → x=z] (транзитивност на идентичността) |
Доказателства в процедурата за двете:
| 1. ¬∀x∀y(x=y → y=x) допускане |
| 2. ∃x∃y¬(x=y → y=x) връзка между кванторите |
| 3. ¬(a=b → b=a) 2, EI (два пъти) |
| 4. a=b ∧ b≠a 3, материална импликация |
| 5. a=b 4, симплификация |
| 6. b≠a 4, комутация и симплификация |
| 7. b≠b 5, 6, неразличимост на идентичните |
| 8. b=b идентичност със себе си – противоречие с 7 |
| 9. ∀x∀y(x=y → y=x) 1-8, reductio ad absurdum и двойно отрицание |
| 1. ¬∀x∀y∀z[(x=y ∧ y=z) → x=z] допускане |
| 2. ∃x∃y∃z¬[(x=y ∧ y=z) → x=z] връзка между кванторите |
| 3. ¬[(a=b ∧ b=c) → a=c] 2, EI (три пъти) |
| 4. (a=b ∧ b=c) ∧ a≠c 3, материална импликация |
| 5. a=b 4, симплификация (два пъти) |
| 6. b=c 4, симплификация (два пъти) и комутация |
| 7. a=c 6, 5, неразличимост на идентичните |
| 8. a≠c 4, комутация и симплификация – противоречие с 7 |
| 9. ∀x∀y∀z[(x=y ∧ y=z) → x=z] 1-8, reductio ad absurdum и двойно отрицание |
Това, че твърденията за симетричността и транзитивността на идентичността са в Γ, означава, че всички техни спецификации с константи също са в Γ, тъй като последните се изводими от тях с универсална инстанциация. Искаме да покажем, че ако „c=d“ е в Γ, то [c]=[d]. Нека „c=d“ е елемент на Γ. Значи и „d=c“ е елемент на Γ (Γ съдържа твърдението за симетричност на идентичността и значи „c=d → d=c“, от което с модус поненс се извежда „d=c“). По дефиниция, за която и да е константа e от L′ са изпълнени следните две положения:
|
е е елемент на [c]
iff „c=e“ и „e=c“ са елементи на Γ |
|
е е елемент на [d]
iff „d=e“ и „e=d“ са елементи на Γ |
Ако „c=e“ и „e=c“ са елементи на Γ, от това че „d=c“ и c=e“ са елементи на Γ следва, че „d=e“ е елемент на Γ (твърдението за транзитивността на идентичността се съдържа в Γ и значи също и „(d=c ∧ c=e) → d=e“, от което с конюнкция и модус поненс се извежда „d=e“), а от това, че „e=c“ и „c=d“ са елементи на Γ (пак по същия начин от транзитивността на идентичността) следва, че „e=d“ е в Γ. Получава се, че ако „c=e“ и „e=c“ са елементи на Γ, то „d=e“ и „e=d“ са елементи на Γ. Обратното (ако „d=e“ и „e=d“ са елементи на Γ, то „c=e“ и „e=c“ са елементи на Γ) се показва напълно аналогично (двете положения са симетрични). Така получаваме
|
„c=e“ и „e=c“ са елементи на Γ
iff „d=e“ и „e=d“ са елементи на Γ |
Oт трите iff-твърдения получаваме"
|
е е елемент на [c]
iff е е елемент на [d] |
Тъй като e беше произволна константа, всяка константа в L′ е елемент на [c], ако и само ако е елемент на [d], т.е. [c] и [d] са едно и също множество от константи. Получихме, че ако „c=d“ е елемент на Γ, [c]=[d]. Край на доказателството.
Ето и едно друго следствие от определянето на универсума на А′:
(9) Нека X (някакво множества от константи) е обект от универсума на А′. Тогава за всяка константа c от L′ е изпълнено, че c е елемент на X, ако и само ако [c] е X.
Доказателство:
Едната посока на еквивалентността (ако X е [c], то c е елемент на X) следва от факта, че c е елемент на [c] (виж второто следствие по-горе). За другата посока: нека c е елемент на X. От определянето на универсума на А′ следва, че за някаква константа d от L′ е изпълнено, че X е [d]. Значи c е елемент на [d] и (по дефиниция) „c=d“ е елемент на Γ. От (8) следва, че [c]=[d], но X=[d], значи X=[c]. Получава се, че ако c е елемент на X, X е [c]. Край на доказателството.
След като определихме универсума на А′, остава да определим интерпретацията на константите и буквите за предикати от лексиката на L′ в А′. Първо интерпретацията на константите:
Ако c е константа от L′, то cА′ (обектът, който c обозначава в А′) e [c].
Нека обърнем внимание, че от начина, по който определихме универсума на А′, и току що дадената интерпретация на константите на L′ в А′ следва, че всеки обект от универсума на А′ е обозначен в А′ от някаква константа от L′. Това е така, защото универсумът се състои от обектите [c] за всяка константа c в L′, а всяка константа c в L′ обозначава [c] (ще използваме този факт по-долу).
Ето и интерпретацията на буквите за предикати:
Ако F е n-местна буква за предикат от L′, а (X1, X2, …, Xn) е n-торка от обекти от универсума на А′, то (X1, X2, …, Xn) е елемент на FA′ (интерпретацията на F в А′), ако и само ако в Γ e има твърдение от вида „Fd1…dn“, където константата d1 е елемент на множеството X1, d2 е елемент на X2, …, dn е елемент на Xn.
С това структурата А′ е напълно определена. Сега остава да покажем, че тази структура е модел на Γ, т.е. че всички твърдения в Γ са истинни в А′. Съгласно (1) всяко твърдение от езика на една структура е истинно или не в нея, но не и двете. Въз основа на семантичните правила, когато едно твърдение не е истинно в една структура, е истинно неговото отрицание. Следователно за всяко твърдение φ от L′ е изпълнено, че φ или ¬φ е истинно в А′, но не и двете. От друга страна, поради това, че Γ е пълно и консистентно множество от твърдения, за всяко твърдение φ от L′ важи, че φ или ¬φ е елемент на Γ, но не и двете. Следователно, А′ може да е модел на Γ само ако Γ е множеството на всички твърдения, които са истинни в А′. Затова, ще покажем, че А′ е модел на Γ, като покажем, че е вярно привидно по-силното (но всъщност в случая еквивалентно) положение, че за всяко твърдение от езика L′ е изпълнено, че е истинно в А′, ако и само ако е в Γ:
За всяко твърдение φ от L′, А′ ⊨ φ ако и само φ е елемент на Γ.
Ще докажем това с индукция по сложността на твърденията в L′ (за сложността на твърденията виж доказателството на (1)). Първо, разглеждаме случаите, когато φ има сложност 0, т.е. когато е атомарно твърдение.
Случай 1, φ е твърдението d1=d2, където d1 и d2 са константи (не непременно различни). Тогава е изпълнено:
| А′ ⊨ d1=d2 |
|
iff
(по семантичните правила) |
| d1А′=d2А′ |
|
iff
(от интерпретацията на константите в А′) |
| [d1]=[d2] |
|
iff
(от (8)) |
| „d1=d2“ е елемент на Γ |
Получава се, че А′ ⊨ φ, ако и само φ е елемент на Γ.
Случай 2, φ е твърдението Fd1…dn, където F е буква за предикат, а d1, …, dn са константи (не непременно различни). Тогава е изпълнено:
| А′ ⊨ Fd1…dn |
|
iff
(от семантичните правила и интерпретацията на константите) |
| ([d1], …, [dn]) ∈ FA′ |
|
iff
(от интерпретацията на буквите за предикати) |
| В Γ има твърдение „Fе1…еn“, такова че константата е1 е елемент на [d1], …, en е елемент на [dn] |
Нека последното твърдение („В Γ има твърдение …“) е вярно. От (9) и това, че е1 е елемент на [d1], …, е1 е елемент на [dn], следва, че [е1]=[d1], …, [еn]=[dn], от което въз основа на (8) следва, че твърденията „е1=d1“, …, „еn=dn“ са в Γ. Но „Fе1…еn“ също е в Γ. Прилагайки схемата за извод неразличимост на идентичните, можем да изведем твърдението „Fd1…dn“, което следователно също е елемент на Γ. Обратно, нека „Fd1…dn“ е елемент на Γ. Тъй като d1 е елемент на [d1], …, dn е елемент на [dn], в Γ има твърдение „Fе1…еn“, такова че константата е1 е елемент на [dn], …, en е елемент на [dn] (това е самото „Fd1…dn“). С това показахме истинността на следната еквивалентност:
| В Γ има твърдение „Fе1…еn“, такова че константата е1 е елемент на [d1], …, еn е елемент на [dn] |
| iff |
| „Fd1…dn“ е елемент на Γ |
Комбинирайки я с горните еквивалентности, получаваме, че А′ ⊨ Fd1…dn, ако и само ако „Fd1…dn“ е елемент на Γ, което искахме да покажем.
Това бяха двата възможни случая, при които твърдението φ имат сложност 0. Сега приемаме, че когато φ има сложност k, е изпълнено, че А′ ⊨ φ, ако и само ако φ е елемент на Γ, и ще покажем, че същото е изпълнено и когато φ има сложност k+1.
Случай 3: φ има формата на отрицание, т.е. φ е ¬ψ. Тогава е изпълнено:
| А′ ⊨ ¬ψ |
|
iff
(по семантичните правила) |
| А′ ⊭ ψ |
|
iff
(от хипотезата на индукцията, тъй като ψ има сложност k) |
| ψ не е елемент на Γ |
|
iff
(от пълнотата и консистентността на Γ21) |
| ¬ψ е елемент на Γ |
Получаваме, че А′ ⊨ ¬ψ, ако и само ако ¬ψ е елемент на Γ.
Случай 4: φ има формата на конюнкция, т.е. φ е ψ1∧ψ2. Тогава е изпълнено:
| А′ ⊨ ψ1∧ψ2 |
|
iff
(по семантичните правила) |
| А′ ⊨ ψ1 и А′ ⊨ ψ2 |
|
iff
(от хипотезата на индукцията) |
| ψ1 и ψ2 са елементи на Γ |
Нека последното е вярно (ψ1 и ψ2 са елементи на Γ). Използвайки схемата за извод конюнкция, получаваме Γ ⊢ ψ1∧ψ2, от което следва, че ψ1∧ψ2 е елемент на Γ. Обратно, ако ψ1∧ψ2 е елемент на Γ, въз основа на схемата за извод симплификация получаваме, че ψ1 и ψ2 са изводими от Γ, от което следва, че са елементи на Γ. Така че имаме
| ψ1 и ψ2 са елементи на Γ |
| iff |
| ψ1∧ψ2 е елемент на Γ |
Комбинирайки последната еквивалентност с горните две, получаваме, че А′ ⊨ ψ1∧ψ2, ако и само ако ψ1∧ψ2 е елемент на Γ.
Случай 5: φ има формата на дизюнкция, т.е. φ е ψ1∨ψ2. Тогава е изпълнено:
| А′ ⊨ ψ1∨ψ2 |
|
iff
(по семантичните правила) |
| А′ ⊨ ψ1 или А′ ⊨ ψ2 |
|
iff
(от хипотезата на индукцията) |
| ψ1 е елемент на Γ или ψ2 е елемент на Γ |
Нека последното е вярно (ψ1 е елемент на Γ или ψ2 е елемент на Γ). Използвайки схемата за извод добавяне, и в двата случая се получава Γ ⊢ ψ1∨ψ2, от което следва, че ψ1∨ψ2 е елемент на Γ. Обратно, нека ψ1∨ψ2 е елемент на Γ. Допускаме, че нито ψ1, нито ψ2 са елементи на Γ. Тогава (от пълнотата на Γ) ¬ψ1 и ¬ψ2 са елементи на Γ. По схемата за извод конюнкция извеждаме ¬ψ1∧¬ψ2, от което с Де Морган извеждаме ¬(ψ1∨ψ2). Следователно Γ ⊢ ¬(ψ1∨ψ2), от което следва, че ¬(ψ1∨ψ2) е елемент на Γ в противоречие на това, че ψ1∨ψ2 е елемент на Γ (Γ е консистентно). Значи допускането ни е невярно, т.е. ψ1 е елемент на Γ или ψ2 е елемент на Γ. Като цяло се получава, че
| ψ1 е елемент на Γ или ψ2 е елемент на Γ |
| iff |
| ψ1∨ψ2 е елемент на Γ |
Комбинирайки последната еквивалентност с горните две, получаваме, че А′ ⊨ ψ1∨ψ2, ако и само ако ψ1∨ψ2 е елемент на Γ.
Случай 6: φ има формата на импликация, т.е. φ е ψ1→ψ2. Тогава е изпълнено:
| А′ ⊨ ψ1→ψ2 |
|
iff
(по семантичните правила) |
| А′ ⊭ ψ1 или А′ ⊨ ψ2 |
|
iff
(от хипотезата на индукцията) |
| ψ1 не е елемент на Γ или ψ2 е елемент на Γ |
|
iff
(от пълнотата и консистентността на Γ22) |
| ¬ψ1 е елемент на Γ или ψ2 е елемент на Γ |
Нека последното е вярно (¬ψ1 е елемент на Γ или ψ2 е елемент на Γ). Което и от ¬ψ1 или ψ2 да е елемент на Γ, с добавяне извеждаме ¬ψ1∨ψ2, от което с материална импликация извеждаме ψ1→ψ2. Значи ψ1→ψ2 е елемент на Γ. Обратно, нека ψ1→ψ2 е елемент на Γ. Допускаме, че нито ¬ψ1, нито ψ2 са елементи на Γ. Тогава (от пълнотата на Γ) ψ1 и ¬ψ2 са елементи на Γ. По схемата за извод конюнкция извеждаме ψ1∧¬ψ2, от което по материална импликация извеждаме ¬(ψ1→ψ2). Значи ¬(ψ1→ψ2) е елемент на Γ, което заедно с това, че ψ1→ψ2 е елемент на Γ, противоречи на консистентността на Γ. Значи допускането ни е невярно, т.е. ¬ψ1 е елемент на Γ или ψ2 е елемент на Γ. Получихме, че
| ¬ψ1 е елемент на Γ или ψ2 е елемент на Γ |
| iff |
| ψ1→ψ2 е елемент на Γ |
Добавяйки последната еквивалентност към горните три, получаваме, че А′ ⊨ ψ1→ψ2, ако и само ако ψ1→ψ2 е елемент на Γ.
Случай 7: φ има формата на материална еквивалентност, т.е. φ е ψ1↔ψ2. Тогава е изпълнено:
| А′ ⊨ ψ1↔ψ2 |
|
iff
(по семантичните правила) |
| А′ ⊨ ψ1 и А′ ⊨ ψ2, или А′ ⊭ ψ1 и А′ ⊭ ψ2 |
|
iff
(от хипотезата на индукцията) |
| ψ1 и ψ2 са елементи на Γ, или нито ψ1, нито ψ2 са елементи на Γ |
|
iff
(от пълнотата и консистентността на Γ23) |
| ψ1 и ψ2 са елементи на Γ, или ¬ψ1 и ¬ψ2 са елементи на Γ |
Нека последното е вярно (ψ1 и ψ2 са елементи на Γ, или ¬ψ1 и ¬ψ2 са елементи на Γ). Ако ψ1 и ψ2 са елементи на Γ, по конюнкция извеждаме ψ1∧ψ2, от което по добавяне извеждаме (ψ1∧ψ2)∨(¬ψ1∧¬ψ2). Ако ¬ψ1 и ¬ψ2 са елементи на Γ, по същия начин извеждаме (ψ1∧ψ2)∨(¬ψ1∧¬ψ2), така че при всички положения извеждаме последното твърдение. От него по материална еквивалентност извеждаме твърдението ψ1↔ψ2, което значи е елемент на Γ. Обратно, нека ψ1↔ψ2 е елемент на Γ. По материална еквивалентност извеждаме твърдението (ψ1∧ψ2)∨(¬ψ1∧¬ψ2), което значи е в Γ. Допускаме, че нито ψ1∧ψ2, нито ¬ψ1∧¬ψ2 са елементи на Γ. Значи (от пълнотата на Γ) ¬(ψ1∧ψ2) и ¬(¬ψ1∧¬ψ2) са елементи на Γ. По конюнкция и Де Морган от тях извеждаме ¬[(ψ1∧ψ2)∨(¬ψ1∧¬ψ2)], което противоречи на факта, че (ψ1∧ψ2)∨(¬ψ1∧¬ψ2) е в Γ. Значи допускането ни е невярно, т.е. ψ1∧ψ2 е елемент на Γ, или ¬ψ1∧¬ψ2 е елемент на Γ. В първия случай със симплификация извеждаме ψ1 и ψ2, а във втория ¬ψ1 и ¬ψ2. Следователно ψ1 и ψ2 са елементи на Γ, или ¬ψ1 и ¬ψ2 са елементи на Γ. Като цяло получаваме, че
| ψ1 и ψ2 са елементи на Γ, или ¬ψ1 и ¬ψ2 са елементи на Γ |
| iff |
| ψ1↔ψ2 е елемент на Γ |
Добавяйки последната еквивалентност към горните, получаваме, че А′ ⊨ ψ1↔ψ2, ако и само ако ψ1↔ψ2 е елемент на Γ.
Случай 8: φ e екзистенциално твърдение, т.е. φ е ∃xψ(x).
Нека А′ ⊨ ∃xψ(x). Значи (по семантичните правила) за някакъв обект X от А′, А′ ⊨ ψ[X]. Когато определяхме А′, обърнахме внимание, че всеки обект от универсума на А′ е обозначаван от някаква константа от L′. Значи има някаква константа c, която обозначава X в А′. От А′ ⊨ ψ[X] и това, че c обозначава X в А′, следва А′ ⊨ ψ(c). Oт хипотезата на индукцията (сложността на ψ(c) е k) следва, че ψ(c) е елемент на Γ. От ψ(c) можем да изведем ∃xψ(x) така:
| 1. ψ(c) |
| 2. ¬∃xψ(x) допускане |
| 3. ∀¬xψ(x) 2, връзка между кванторите |
| 4. ¬ψ(c) 3, UI – противоречие с 1 |
| 5. ∃xψ(x) 2-4, reductio ad absurdum и двойно отрицание |
Значи ∃xψ(x) е в Γ. Получихме, че ако А′ ⊨ ∃xψ(x), то ∃xψ(x) е елемент на Γ.
Обратно, нека ∃xψ(x) е елемент на Γ. Конструкцията на Γ беше такава, че за всяко екзистенциално твърдение ∃xψ(x) в езика L′, в Γ се съдържа ∃xψ(x)→ψ(c), за някаква константа c от {c1, c2, …, cn, …}. Значи в Γ се съдържат едновременно ∃xψ(x) и ∃xψ(x)→ψ(c), от които по модус поненс се извежда твърдението ψ(c), което значи е в Γ. От последното и хипотезата на индукцията (ψ(c) е със сложност k) следва А′ ⊨ ψ(c). Константата c обозначава някакъв обект X от А′ и значи от А′ ⊨ ψ(c) следва А′ ⊨ ψ[X]. От последното по семантичните правила следва А′ ⊨ ∃xψ(x). Получихме и другата посока (ако ∃xψ(x) е в Γ, то А′ ⊨ ∃xψ(x)). Като цяло, А′ ⊨ ∃xψ(x), ако и само ако ∃xψ(x) е елемент на Γ.
Случай 9: φ e универсално твърдение, т.е. φ е ∀xψ(x).
Нека А′ ⊨ ∀xψ(x). Допускаме, че ∀xψ(x) не е елемент на Γ. Значи ¬∀xψ(x) е елемент на Γ. От ¬∀xψ(x) по връзка между кванторите се извежда ∃x¬ψ(x). Значи ∃x¬ψ(x) е в Γ. От конструкцията на Γ следва, че в Γ присъства твърдението ∃x¬ψ(x)→¬ψ(c) (за някакво c от добавените константи), от което и ∃x¬ψ(x) по модус поненс се извежда ¬ψ(c), което значи е елемент Γ. Тъй като Γ е консистентно, ψ(c) не е в Γ. От хипотезата на индукцията (сложността на ψ(c) е k) А′ ⊭ ψ(c). Следователно за някакъв обект X от А′ важи А′ ⊭ ψ[X], което противоречи на А′ ⊨ ∀xψ(x). Следователно допускането ни е невярно и ∀xψ(x) е елемент на Γ. Получихме, че ако А′ ⊨ ∀xψ(x), то ∀xψ(x) е елемент на Γ.
Обратно, нека ∀xψ(x) е елемент нa Γ. За всяка константа c в L′, от ∀xψ(x) по универсална инстанциация е изводимо твърдението ψ(c), което значи е елемент на Γ. От последното и хипотезата на индукцията следва че, за всяка константа c в L′, важи А′ ⊨ ψ(c). Тъй като в А′ няма обект, който да не е обозначен от константа, за всеки обект X в А′ важи А′ ⊨ ψ[X]. По семантичните правила А′ ⊨ ∀xψ(x). Получихме, и другата посока (ако ∀xψ(x) е в Γ, то А′ ⊨ ∀xψ(x)). Като цяло, А′ ⊨ ∀xψ(x), ако и само ако ∀xψ(x) е елемент на Γ.
С това индукцията е завършена. Показахме, че за всяко твърдение φ в L′ важи: А′ ⊨ φ, ако и само ако φ е елемент на Γ. Следователно, А′ е модел на Γ.
Остава да направим последната стъпка. Δ (консистентното множество от твърдения, от което тръгнахме) е подмножество на Γ и значи А′ е модел на Δ. Но Δ е от езика L, в който липсват константите от {c1, c2, …, cn, …}. Следователно структурата А, която е обедняване на А′ до езика L, ще е модел на Δ. Тъй като Δ беше произволно консистентно множество, това показва, че всяко консистентно множество от твърдения има модел, т.е. доказателствената процедура от 3.5 Доказателствена процедура е пълна.
Самото доказателство показва нещо повече – че всяко консистентно множество има броим модел (универсумът на А беше броимо множество). Като добавим консистентността, която също доказахме, от това следва, че всяко множество от твърдения, което изобщо има модел, има броим модел (защото ако има модел, от коректността, е консистентно, а ако е консистентно, от доказателството за пълнота, има броим модел). Това положение е известно като теорема на Льовенхайм-Сколем и е доказано от (Lowenheim, 1915) и (Skolem, 1920) още преди теоремата за пълнота, доказана (за друга доказателствена процедура) за първи път от Гьодел (Gödel, 1930). Изложеното доказателство за пълнота е на Хенкин (Henkin, 1949) (за друга доказателствена процедура).