Dowód metodą Taita-Bussa

Inny dowód eliminacji (Cut) oparty na globalnych przekształceniach dowodu podaje Buss [20]. Jego dowód co do ogólnej strategii oparty jest na dowo-dzie Taita [140], który nie wykorzystuje indukcji po ilości zastosowań (Cut) (jak w dowodzie Gentzena), ale opiera się jedynie na indukcji po długości cut-formuły. Jest to eleganckie rozwiązanie, które pozwala przy okazji podać oszacowanie wielkości zbudowanego w wyniku dokonanych transformacji no-wego dowodu. W przeciwieństwie do Taita w swoim dowodzie Buss nie używa jednak lokalnych przekształceń, ale stosuje globalne transformacje.

5.4. DOWODY GLOBALNE 123 (Cut). Pierwsze ograniczenie jest istotne dla zachowania poprawności do-konywanych transformacji. Drugie nie jest ważne toteż zaprezentujemy tu jego dowód eliminacji, ale dostosowany do multiplikatywnej wersji (Cut), dla łatwiejszego porównania z poprzednimi dowodami (za wyjątkiem dowo-du Smullyana, który też dotyczy addytywnej wersji).

Jak wyżej wspomnieliśmy, charakterystyczne dla ogólnej struktury dowo-du jest też to że, w przeciwieństwie do dowodowo-du Gentzena, nie eliminujemy po kolei najwyższych wystąpień (Cut), ale eliminujemy kolejno maksymalne (co do długości cut-formuły) zastosowania (Cut).

Podstawą dowodu jest poniższy:

Lemat 5.5 Jeżeli D jest dowodem zakończonym (Cut), w którym cut-formuła ϕ ma długość n, a każda inna cut-formuła ma długość mniejszą, to można go zamienić na dowód D⁰, w którym każda cut-formuła ma długość mniejszą od n.

Dowód: Niech Dl oznacza dowód lewej przesłanki ostatniego (Cut), a D_r prawej. Jeżeli któryś z nich nie zawiera zastosowania logicznych reguł, to ma-my do czynienia z uogólnionym aksjomatem i zgodnie z faktem 5.1. to zasto-sowanie (Cut) jest eliminowalne. Zatem przy rozważaniu dalszych przypad-ków zakładamy, że kD_lk i kD_rk są większe od 0. Dowód wymaga rozważenia wszystkich przypadków ϕ.

ϕ jest zmienną. W tym przypadku przekształcamy D_lna D_l⁰w następują-cy sposób: Każdy sekwent Λ ⇒ Θ w D_l zamieniamy na Γ, Π, Λ ⇒ ∆, Σ, Θ_ϕ, gdzie Θ_ϕ oznacza wyrzucenie z Θ wszystkich wystąpień ϕ. W szczególności każdy liść ψ ⇒ ψ w D_lstał się w D⁰_lsekwentem postaci Γ, Π, ψ ⇒ ∆, Σ, ψ gdy ψ jest różne od ϕ lub Γ, Π, ψ ⇒ ∆, Σ, gdy ψ = ϕ. Dzięki kontekstowej nieza-leżności reguł (por. podrozdział 4.5), ani dodanie nowych parametrów ani eli-minacja parametru ϕ nie wpływa na poprawność zastosowanych reguł zatem D0

ljest drzewem dowodowym, które kończy się sekwentem Γ, Π, Γ ⇒ ∆, Σ, ∆. Następnie tworzymy z D⁰_l dowód D⁰ dla Γ, Π ⇒ ∆, Σ w następujący sposób: (a) Sekwent końcowy otrzymujemy z sekwentu końcowego D⁰_l przez kontrak-cję i permutakontrak-cję. (b) Dla każdego liścia postaci Γ, Π, ψ ⇒ ∆, Σ, ψ dodajemy u góry dowód z ψ ⇒ ψ za pomocą (W ) i (P ). (c) Dla każdego liścia po-staci Γ, Π, ϕ ⇒ ∆, Σ dodajemy u góry dowód prawej przesłanki (Cut), czyli ϕ, Π ⇒ Σ z dołączoną dedukcją Γ, Π, ϕ ⇒ ∆, Σ za pomocą (W ) i (P ). Uwaga 5.5: Dowód tego przypadku pokazuje alternatywny (i prostszy) – do dowodu Schüttego – sposób eliminacji atomowych (Cut). Zauważmy, że przeprowadzona transformacja nie wprowadza innych (Cut) na miejsce

eli-minowanego natomiast w D z założenia nie ma powyżej innych zastosowań (Cut), gdyż n = 0 (atom jako cut-formuła).

Przypadek ϕ := ¬ψ. W tym przypadku przekształcamy oba dowody D_l i D_r na dowody D⁰_l i D_r⁰ sekwentów ψ, Γ ⇒ ∆ i Π ⇒ Σ, ψ odpowiednio. Na obu można wykonać (Cut) na ψ. Zatem w rezultacie otrzymujemy dowód D⁰ dla Γ, Π ⇒ ∆, Σ, w którym żadna cut-formuła nie ma długości większej od n − 1. Szczegóły transformacji są następujące: każdy sekwent Λ ⇒ Θ w D_l zastępujemy przez ψ, Λ ⇒ Θ_ϕ a w D_r przez Λ_ϕ ⇒ Θ, ψ. Ponownie dzięki kontekstowej niezależności reguł ani dodanie nowych parametrów ψ ani eliminacja parametru ϕ nie wpływa na poprawność zastosowanych reguł. W szczególności żaden liść nie ma postaci ϕ ⇒ ϕ, z racji ograniczenia do atomów, zatem nie możemy otrzymać liści postaci ψ, ϕ ⇒ lub ⇒ ϕ, ψ. ϕ musiało być zatem wprowadzone przez (W ), a wtedy po prostu zostanie wy-kasowane, lub wprowadzone regułą dla ¬. W tym drugim wypadku fragment dowodu D_l postaci ψ, Λ ⇒ Θ

Λ ⇒ Θ, ¬ψ ^{zostanie zastąpiony przez}

ψ, ψ, Λ ⇒ Θϕ

ψ, Λ ⇒ Θ_ϕ który jest poprawny dzięki kontrakcji; analogicznie w D_r. Zatem D⁰_l i D⁰_r to drzewa dowodowe, które zaczynają się od liści postaci ψ, χ ⇒ χ lub χ ⇒ χ, ψ z χ atomowym. Wystarczy dopisać nad każdym liściem tej postaci aksjomat χ ⇒ χ, aby otrzymać dowód D⁰ dla Γ, Π ⇒ ∆, Σ.

Przypadek ϕ := ψ ∧ χ. W tym przypadku na bazie D_r konstruujemy D_r⁰ dla ψ, χ, Π ⇒ Σ, w którym każdy sekwent Λ ⇒ Θ zastępujemy przez ψ, χ, Λϕ ⇒ Θ. Znów, wszystkie inferencje zachowują poprawność dzięki kon-tekstowej niezależności. W szczególności, jeżeli ϕ było otrzymane w D_rprzez (∧ ⇒), to po przekształceniu na D_r⁰ musimy dodać dwa zastosowania kontr-akcji, aby mieć poprawne przejście od ψ, χ, ψ, χ, Λ_ϕ ⇒ Θ do ψ, χ, Λ_ϕ ⇒ Θ. By otrzymać dowód ψ, χ, Π ⇒ Σ nad każdym liściem postaci ψ, χ, γ ⇒ γ dodajemy aksjomat γ ⇒ γ i dwa zastosowania (W ⇒).

W przypadku D_l konstruujemy w analogiczny sposób dwa dowody: D_ψ⁰ dla Γ ⇒ ∆, ψ i D⁰_χ dla Γ ⇒ ∆, χ. W pierwszej transformacji każdy sekwent Λ ⇒ Θ zastępujemy przez Λ ⇒ Θϕ, ψ, a w drugiej przez Λ ⇒ Θϕ, χ Tym razem jeśli ϕ w D_l było wprowadzone przez (⇒ ∧), to po transformacji na D0

ψ otrzymujemy:

Λ ⇒ Θϕ, ψ, ψ Λ ⇒ Θϕ, χ, ψ Λ ⇒ Θϕ, ψ

z którego można wyrzucić całą prawą przesłankę i prowadzący do niej do-wód gdyż wniosek jest wyprowadzalny z lewej przez (⇒ C). Analogicznie

5.4. DOWODY GLOBALNE 125 postępujemy w D_χ⁰, ponadto w liściach obu drzew dowodowych dodajemy aksjomaty – tak jak w poprzednich przypadkach – otrzymując dowody D_ψ⁰ i D0

χ. Na koniec, budujemy z tych trzech dowodów nowy dowód D⁰ w nastę-pujący sposób. D0 χ Γ ⇒ ∆, χ D0 ψ Γ ⇒ ∆, ψ D⁰_r ψ, χ, Π ⇒ Σ (Cut) χ, Γ, Π ⇒ ∆, Σ (Cut) Γ, Γ, Π ⇒ ∆, ∆, Σ (C) Γ, Π ⇒ ∆, Σ

Oba zastosowania (Cut) są na cut-formułach o długości mniejszej od n. Analogicznie dla innych rodzajów formuł.

Uwaga 5.6: Warto zwrócić uwagę, że transformacja dowodu u Bussa prze-biega inaczej niż u Curry’ego; można wskazać przynajmniej dwie istotne różnice:

1. U Curry’ego mamy do czynienia ze wstawianiem parametrów z dru-giej przesłanki, a tu tylko z zastępowaniem cut-formuły jej podformułami. Bierze się to stąd, że cel transformacji jest zasadniczo inny – u Curry’ego jest to elimnacja (Cut), a u Bussa zmniejszenie długości cut-formuły. Tylko w przypadku formuły atomowej u Bussa występuje podobna transformacja. 2. U Curry’ego tylko te sekwenty są zmieniane, w których występują po-przedniki cut-formuły. U Bussa zasadniczo wszystkie sekwenty ulegają zmia-nie. Faktycznie w dowodzie Bussa w przypadku konstrukcji odpowiadającej dwuprzesłankowym regułom wprowadzającym cut-formułę mamy do czynie-nia z dodaniem ψ lub χ nie do każdego sekwentu, a tylko do tych gdzie wykasowaliśmy poprzedniki ϕ – odpowiada to konstrukcji Φ u Curry’ego. Cały dowód Bussa można w ten sposób przerobić.

Kolejny krok to dowód następującego rezultatu:

Lemat 5.6 Każdy dowód D, w którym każda cut-formuła ma długość nie większą od n można przekształcić na dowód D⁰, w którym każda cut-formuła ma długość mniejszą od n.

Dowód: Po ilości wystąpień takich maksymalnych (Cut). Każdy poddowód D (idąc od góry) kończący się zastosowaniem (Cut) na cut-formule długości n można – zgodnie z lematem 5.5 – zastąpić takiem dowodem, który ma tylko krótsze cut-formuły. Powtarzając tę operację otrzymujemy w końcu dowód z cut-formułami tylko o mniejszej długości.

Twierdzenie o eliminacji (Cut) wynika z obu lematów. Po pierwsze sto-sując tę konstrukcję kolejno na coraz mniejszych wartościach n otrzymujemy w końcu dowód, w którym wszystkie cut-formuły są atomowe. Ale dowód tego przypadku, zanurzony dowodzie lematu 5.5, pokazywał, że eliminacja atomowych cut-formuł prowadzi do konstrukcji dowodu nie zawierającego wogóle (Cut).