Да предположим, че е дадена една затворена секвенция Γ-:Δ. Някои множества, съставени от по най-много две затворени секвенции, ще наречем редукти на Γ-:Δ, като на всяко от тях ще съпоставим неотрицателно цяло число, наречено ранг. Дефиницията се състои от следните точки, като се подразбира, че Γ-:Δ няма други редукти, освен изрично посочените:
Една затворена секвенция има редукт точно тогава, когато тя не е семантична таблица. И наистина, нека Γ-:Δ е дадена затворена секвенция. Ясно е, че ако Γ-:Δ има някакъв редукт, то Γ-:Δ не е семантична таблица, защото ще бъде нарушено ST-условието, съответно на RD-точката, по която се получава въпросният редукт. Обратно, ако Γ-:Δ не е семантична таблица, то поне едно от ST-условията е нарушено и секвенцията Γ-:Δ ще има редукт съгласно съответната RT-точка (в случая, когато е нарушено условието ST( -: ∀), използуваме, че константите, участващи в Γ-:Δ, са само краен брой, докато всичките константи са безбройно много).
Разбира се, когато секвенцията Γ-:Δ има редукт, измежду нейните редукти ще има поне един с най-малък ранг; такъв редукт на Γ-:Δ ще наричаме неин каноничен редукт.
В следващия пример и в другите по-нататък ще предполагаме, че всички функционални символи са константи.
Пример 1. Да разгледаме секвенцията
Да означим с G0 формалната система, която се получава при ограничаване на системата G чрез използване само на затворени термове, формули и секвенции, чрез отпадане на правилата за дизюнкция и за квантор за съществуване и чрез следното изменение на правилото ( -: ∀): вместо променлива η, която да не е свободна променлива на секвенцията под чертата, се използва константа, която не участва във въпросната секвенция (разбира се субституциите, които заместват променливи с константи и по-общо със затворени термове, са приложими винаги). Лесно се проверява, че и след това изменение прилагането на споменатото правило запазва тъждествената вярност на секвенциите.
От дефиницията на понятието редукт се виждат следните свойства:
Лема 1. Елементите на всеки редукт на дадена затворена секвенция Γ-:Δ са затворени секвенции, строго разширяващи Γ-:Δ.
Лема 2. Всяка затворена секвенция с празен редукт е аксиома на системата G0, а всяка затворена секвенция с непразен редукт може да се получи от неговите елементи по някое от правилата за извод на тази система.
Сега ще пренесем понятията редукт и каноничен редукт върху множества от затворени секвенции. Нека M е множество от затворени секвенции. Редукт на M ще наричаме множество от секвенции, получено като за всяка секвенция от M се избере по един неин редукт и след това се образува обединението на така избраните редукти. Аналогично дефинираме какво е каноничен редукт на M - това е множество от секвенции, получено като за всяка секвенция от M се избере по един неин каноничен редукт и след това се образува обединението на така избраните редукти. Ясно е, че за да има множеството M поне един редукт, необходимо и достатъчно е всяка секвенция от M да има поне един редукт, т.е.никой елемент на M да не е семантична таблица. Оттук следва, че ако M има редукт, то M има и каноничен редукт. Отбелязваме още, че ако M е крайно, то редуктите на M са също крайни.
Като използуваме въведените понятия, ще опишем метода на Бет за изследване на тъждествена вярност на секвенции. Той се състои в следното: когато е дадена една затворена секвенция Γ° -: Δ°, образуваме последователно крайни множества R0, R1, R2, … от затворени секвенции, където R0 е {Γ° -: Δ°}, R1 е каноничен редукт на R0, R2 е каноничен редукт на R1 и т.н., докато евентуално стигнем до такова множество Rn , което е празно или съдържа като елемент някоя семантична таблица. Последователното образуване на множества R0, R1, R2 и т.н. по описания начин ще наричаме редукционен процес за секвенцията Γ° -: Δ°. Ако в хода на този процес се достигне до празно Rn, прави се заключение, че секвенцията Γ° -: Δ° е тъждествено вярна, а ако се достигне до Rn, съдържащо като елемент някоя семантична таблица, прави се заключение, че секвенцията Γ° -: Δ° не е тъждествено вярна. Ако редукционният процес продължава безкрайно без да възникне никой от споменатите два случая, също може да се твърди, че въпросната секвенция не е тъждествено вярна (коректността на такова заключение, както и на заключенията, споменати в предходното изречение, ще бъде доказана по-нататък).
Пример 2. Пример 1 по същество показва как може да се приложи методът на Бет към секвенцията ∀x¬(p(x)&q(x)) -: ¬∀x p(x). Вижда се, че в този случай множествата R1, R2, R3, R4 са едноелементни - техните единствени елементи са съответно споменатата секвенция и следващите четири секвенции в примера. Множеството R5 има за елементи двете последни секвенции от примера. Тъй като едната от тях е семантична таблица, редукционният процес завършва с R5 и заключението е, че дадената секвенция не е тъждествено вярна.
Пример 3. Да приложим метода на Бет към същата секвенция както в горния пример, но с добавена формула ∀x¬q(x) в дясната страна. В този случай редукционният процес може да протече например така:
Пример 4. Да приложим метода на Бет към секвенцията ∀x¬∀y p(x,y) -: ∅. Имаме следното, където α1, α2, α3, … са различни помежду си константи, различни от α:
Не представлява трудност да покажем, че при завършващ редукционен процес заключенията, получени по метода на Бет, са винаги коректни. Първо отбелязваме едно помощно твърдение, което се доказва индуктивно с помощта на лема 1.
Лема 3. Нека Γ° -: Δ° е дадена затворена секвенция и нека R0, R1,R2, … е редицата от множества, която възниква при някое протичане на редукционния процес за тази секвенция. Тогава всяка секвенция, която принадлежи на член на споменатата редица, представлява разширение на секвенцията Γ° -: Δ°.
Теорема за коректност на метода на Бет при завършващ редукционен процес. Нека Γ° -: Δ° е дадена затворена секвенция и нека R0, R1, R2, … е редицата от множества, която възниква при някое протичане на редукционния процес за тази секвенция. Тогава:
а) ако някой член на редицата R0, R1, R2, … е празното множество, то секвенцията Γ° -: Δ° е изводима в системата G0 и следователно е тъждествено вярна;
б) ако някой член на споменатата редица съдържа като елемент семантична таблица, то съществува структура, в която Γ° -: Δ° не е вярна.
Доказателство. Да предположим най-напред, че за дадено n множеството Rn е празно. Тогава n не е 0 и от лема 2 е ясно, че всички секвенции от множеството Rn−1 са аксиоми на G0. Следователно всички секвенции от Rn−1 са изводими в G0. Използвайки същата лема, виждаме, че всеки път, когато за дадено положително цяло число m, по-малко от n, всички секвенции от множеството Rm са изводими в системата G0, в нея са изводими и всички секвенции от множеството Rm−1. Това позволява чрез индукция отгоре надолу да покажем, че при m<n всички секвенции от множеството Rm са изводими в системата G0. Оттук при m=0 получаваме, че секвенцията Γ° -: Δ° е изводима в G0. По такъв начин твърдението а) е доказано.
Да разгледаме сега случая, когато за дадено n множеството Rn съдържа като елемент някоя семантична таблица Γ-:Δ. Според лема 3 секвенцията Γ-:Δ е разширение на Γ° -: Δ°, а според лемата на Бет съществува семантична структура, в която Γ-:Δ не е вярна. Ясно е, че в същата семантична структура ще бъде невярна и секвенцията Γ° -: Δ°. □