Ще докажем, че заключението, получено по метода на Бет, е коректно и в случая на незавършващ редукционен процес.
Теорема за коректност на метода на Бет при незавършващ редукционен процес. Нека Γ° -: Δ° е дадена затворена секвенция и нека при някое протичане на редукционния процес за тази секвенция възниква безкрайна редица от множества R0, R1, R2, …, на която никой от членовете не е празен и не съдържа като елемент семантична таблица. Тогава съществува структура, в която секвенцията Γ° -: Δ° не е вярна.
Доказателство. За произволно естествено число k и произволна секвенция Γ-:Δ от Rk да означим с Rk+1(Γ-:Δ) каноничния редукт на Γ-:Δ, използван при построяването на Rk+1. Ще покажем, че в този случай съществува безкрайна редица от секвенции
(1) Γ0 -: Δ0, Γ1 -: Δ1,Γ2 -: Δ2, …,
такава, че Γ0 -: Δ0 е Γ° -: Δ° и за всяко k секвенцията Γk -: Δk принадлежи на множеството Rk, а секвенцията Γk+1 -: Δk+1 - на множеството Rk+1(Γk-:Δk). За тази цел първо отбелязваме, че за всяко естествено число n и всяка секвенция Γ' -: Δ' от множеството Rn съществува n+1-членна редица от секвенции
(2) Γ0 -: Δ0, Γ1 -: Δ1,Γ2 -: Δ2, …,Γn -: Δn,
такава, че Γ0 -: Δ0=Γ° -: Δ°, Γn -: Δn=Γ' -: Δ' и формулираните по-горе условия, отнасящи се до Γk -: Δk и Γk+1 -: Δk+1 са изпълнени за всяко k, по-малко от n (доказателството на това твърдение се извършва чрез индукция относно n). За произволно естествено число m да означим сега с Rm множеството на онези секвенции Γ-:Δ от Rm, които удовлетворяват следното условие: при всеки избор на естественото число n съществува n+1-членна редица (2) от секвенции, такава, че Γ0 -: Δ0 е Γ-:Δ и за всяко k, по-малко от n, секвенцията Γk -: Δk принадлежи на множеството Rm+k, а секвенцията Γk+1 -: Δk+1 - на множеството Rm+k+1(Γk -: Δk). От казаното преди малко е ясно, че секвенцията Γ° -: Δ° принадлежи на множеството R0. Вярно е още и следното: когато за дадено m дадена секвенция Γ-:Δ принадлежи на множеството Rm, то поне един елемент на Rm+1(Γ-:Δ) принадлежи на множеството Rm+1. Това е очевидно в случая, когато редуктът Rm+1(Γ-:Δ) се състои само от една секвенция, а в случай, че той е съставен от две секвенции, твърдението се доказва чрез допускане на противното. Сега вече редицата (1) с формулираните по-горе свойства се строи индуктивно така: полагаме, разбира се, Γ0 -: Δ0=Γ° -: Δ° и по този начин осигуряваме и условието Γ0 -: Δ0∈R0, освен това се уславяме винаги, когато сме дефинирали Γm -: Δm така, че да е изпълнено условието Γm -: Δm∈Rm, в качеството на Γm+1 -: Δm+1 да вземаме секвенция от Rm+1(Γ-:Δ), принадлежаща на Rm+1. Да отбележим, че редуктът Rm+1(Γm-:Δm), със сигурност не е образуван въз основа на точката RD( ), тъй като не е празен.
След като е построена редица (1) със споменатите свойства, отбелязваме, чеΓ0⊆Γ1⊆Γ2⊆…,Δ0⊆Δ1⊆Δ2⊆…и всеки два последователни члена на (1) са различни. Нека Γω е обединението на всички множества Γk, а Δω - обединението на всички множества Δk. Ще покажем, че съществува структура, в която секвенцията Γ° -: Δ° не е вярна, като установим, че съществува структура, в която всички формули от множеството Γω са верни, а всички формули от множеството Δω са неверни. Благодарение на лемата на Бет това ще бъде постигнато, ако успеем да покажем, че наредената двойка (Γω,Δω) е семантична таблица. Сега ще проверим, че седемте ST-условия са удовлетворени, ако в качеството на Γ и Δ вземем съответно Γω и Δω.
Проверката на условието ST( ) е лесна: ако допуснем, че Γω∩Δω≠∅, и използуваме включванията Γ0⊆Γ1⊆Γ2⊆…,Δ0⊆Δ1⊆Δ2⊆…, лесно получаваме, че Γk∩Δk≠∅ за някое k и за това k единствен каноничен редукт на Γk -: Δk би се оказало празното множество, в противоречие с неравенствотоRk+1(Γk-:Δk)≠∅.
За проверката на останалите шест ST-условия ще въведем определен вид обекти, които ще наречем дефекти, и на всеки от тях ще съпоставим естествено число, наречено негов ранг. Дефиницията е следната: за всяко j от множеството {1,2} и всяка неатомарна формула θ, с изключение на случая, когато имамеj=1 и θ=∀ξφ за някоя променлива ξ и някоя формула φ,наредената двойка <j,θ> е дефект с ранг, равен на дължината на думата θ; освен това за всяка променлива ξ, всяка формула φ и всеки терм τ наредената тройка <1,∀ξφ,τ> е дефект с ранг, равен на сбора от дължините на думите ∀ξφ и τ.
Дефинираме също какво значи даден дефект да e налице в една затворена двойка (Γ,Δ) от множества от формули. Дефиницията се състои от следните точки:
Веднага се вижда, че условията ST(¬ -: ), ST( -: ¬), ST(& -: ),ST( -: &),ST(∀ -: ) и ST( -: ∀) в дефиницията за семантична таблица могат да се заменят с изискването в (Γ,Δ) да не е налице никакъв дефект. Дефиницията за редукт също може да се преформулира с помощта на току-що въведените понятия.Например в точка RD(¬ -: ) от тази дефиниция предпоставката може да се замени с изискването дефектът <1,¬φ> да е налице в Γ-:Δ, а думите "дължината на думата ¬φ" - с думите "ранга на дефекта <1,¬φ>". Аналогично преформулиране допускат и следващите точки RD( -: ¬), RD(& -: ), RD( -: &), RD(∀ -: ) иRD( -: ∀), като съответните им дефекти са тези от точки DF(2,¬), DF(1,&), DF(2,&),DF(1,∀) и DF(2,∀).
Отбелязваме също, че ако дефектът <1,¬φ> е налице в дадена затворена секвенция, той не е налице в секвенцията, принадлежаща на нейния редукт,получен чрез съответното прилагане на точка RD(¬ -: ), а също и в никое разширение на въпросната секвенция. Аналогично е положението и с останалите пет вида дефекти. Например ако дефектът <2,φ&ψ> е налице в дадена затворена секвенция, той не е налице в никоя от секвенциите, принадлежащи на нейния редукт, получен чрез съответното прилагане на точка RD( -: &), а също и в никое от техните разширения. Грубо казано, преминаването към шестте вида непразни редукти служи за премахване на дефектите от съответните видове и, веднъж премахнат, никой такъв дефект не се появява отново.
От казаното дотук и от свойствата на редицата (1) се вижда, че за всяко естествено число k съществува дефект Dk, който е налице в секвенциятаΓk -: Δk, има най-малък ранг сред дефектите, които са налице в нея, и не е налице в никой от следващите членове на редицата (1). Ясно е, че при различни стойности на k съответните дефекти Dk ще бъдат различни.
Друго обстоятелство, което ще използуваме, е следното: за всяко дадено естествено число множеството на дефектите с ранг, ненадминаващ това число, е крайно.
Според казаното преди малко, за да завършим доказателството на теоремата,достатъчно е да покажем, че в двойката (Γω,Δω) не е налице никакъв дефект. Допускаме, че даден дефект D е налице в нея. Ще покажем, че той е налице и в Γk -: Δk за всички достатъчно големи стойности на k. За целта разглеждаме поотделно шестте възможни случая, отнасящи се до вида на дефекта D.
Ако D=<1,¬φ> за дадена формула φ, то¬φ∈Γω, но φ∉Δω. Тогава ¬φ принадлежи на всяко Γk с достатъчно голям номер и дефектът D ще е налице в съответната секвенция Γk -: Δk, защото φ не може да принадлежи на Δk.
Съвсем аналогично разсъждаваме, когато D=<2,¬φ> за някоя формула φ.
Ако D=<1,φ&ψ> за дадени формули φ и ψ, то φ&ψ∈Γω, но някоя от формулите φ и ψ не принадлежи на Γω. Тогава φ&ψ принадлежи на всяко Γk с достатъчно голям номер и дефектът D ще е налице в съответната секвенция Γk -: Δk, защото някоя от формулите φ и ψ със сигурност не принадлежи на Γk.
Подобни са и разсъжденията, когато D=<2,φ&ψ> за дадени формули φ и ψ.
Да предположим сега, че D=<1,∀ξφ,τ> за дадена променлива ξ, дадена формула φ и даден терм τ, т.е. ∀ξφ∈Γω и термът τ е допустим за (Γω,Δω), но [ξ/τ]φ∉Γω.Тогава ∀ξφ принадлежи на всяко Γk с достатъчно голям номер, а [ξ/τ]φ не принадлежи на никое Γk. Лесно се вижда, че термът τ е допустим за всички секвенции Γk -: Δk от известно място нататък (това е тривиално, ако в (Γω,Δω) не участва никаква константа, а в останалите случаи използваме, че всяка константа, участваща в τ, участва в някоя формула от Γω∪Δω и че константите, участващи в τ, са крайно много). Ясно е тогава, че дефектът D ще е налице във всяка секвенция Γk -: Δk с достатъчно голям номер.
Ако пък D=<2,∀ξφ> за дадена променлива ξ и дадена формула φ, то ∀ξφ∈Δω, но никой елемент на Δω не е от вида [ξ/τ]φ, където τ е терм, допустим за (Γω,Δω).Тогава ∀ξφ принадлежи на всички Δk от известно място нататък, но никое Δk не притежава елемент от вида [ξ/τ]φ, където τ е терм, допустим за (Γω,Δω). Оттук следва, че при всяко достатъчно голямо k множеството Δk не притежава елемент от вида [τ/ξ]φ, където τ е терм, допустим за Γk -: Δk (това е тривиално, ако в (Γω,Δω) не участва никаква константа, а в останалите случаи използваме, че при всяко достатъчно голямо k съществува константа, участваща в Γk -: Δk, и че всички такива константи участват и в (Γω,Δω)). По такъв начин отново се оказва, че дефектът D е налице във всяка секвенция Γk -: Δk с достатъчно голям номер.
И така, допуснахме, че D е дефект, който е налице в двойката (Γω,Δω), и получихме, че той е налице и във всички секвенции Γk -: Δk с достатъчно голям номер. Но тогава при всички достатъчно големи стойности на k рангът на дефекта Dk ще бъде не по-голям от ранга на дефекта D. Получаваме, че съществуват безбройно много различни дефекти с ранг, ненадминаващ ранга на D, а това, както знаем, не може да бъде вярно. Значи допускането за наличие на дефект в двойката (Γω,Δω) води до противоречие. Следователно в нея не е налице никакъв дефект. □
Като следствие получаваме
Теорема за пълнота на системата G0. Всяка тъждествено вярна затворена секвенция е изводима в системата G0.
Доказателство. Нека Γ° -: Δ° е тъждествени вярна затворена секвенция. Нека R0, R1, R2, … е редицата от множества, която възниква при някое протичане на редукционния процес за тази секвенция. Теоремата за коректност на метода на Бет при незавършващ редукционен процес заедно с твърдението б) от теоремата за коректност при завършващ редукционен процес позволява да твърдим, че споменатата редица е крайна и последният й член не съдържа семантична таблица. Следователно въпросният последен член е празен. При това положение твърдението а) от теоремата за коректност при завършващ редукционен процес дава желаното заключение за изводимостта на Γ° -: Δ° в G0. □
Забележка. Ако вземем произволна (не непременно затворена) секвенция и заместим свободните променливи на нейните формули с различни помежду си константи, неучастващи в дадената секвенция, тъждествената вярност на дадената секвенция е равносилна с тъждествена вярност на така получената. Това позволява системата G0 да се използва като формално средство за получаване и на произволни тъждествено верни секвенции (една друга възможност е замяната на произволни секвенции с еквивалентни на тях затворени секвенции).