Reguła eliminacji (logika)

Te zasady eliminacji z łącznikami (czyli alternatywa The koniunkcja The zaangażowanie The zaprzeczenie , itd.) Są reguły wnioskowania , które znajdują się w naturalnej dedukcji .

Zasady eliminacji po raz pierwszy przedstawił Gentzen w 1934 roku w swoim przełomowym artykule Research on Logical Deduction pod niemiecką nazwą „ Beseitigung ”, co dokładnie oznacza eliminację .

Forma ogólna

Biorąc pod uwagę złącze binarne ★, reguła eliminacji ★ wygląda następująco:

{\ Displaystyle {\ Frac {{\ Frac {\ vdots} {A \ gwiazda B}} ~~~ \ kropki} {C}}}

gdzie C to A lub B , a punkty i reprezentują jeden lub więcej dowodów twierdzeń. $\ vdots$ $\ dots$

Naturalną dedukcję można też przedstawić na podstawie ciągów postaci Γ ⊢ A, gdzie A jest zdaniem, a Γ jest zbiorem zdań, które można odczytać „z wielozbioru zdań Γ wydedukujemy zdanie A ”. Reguła eliminacji binarnych ★ jest następnie prezentowana w postaci reguły wnioskowania:

{\ Displaystyle {\ Frac {\ Delta \ vdash A \ gwiazda B ~~~~ s_ {1} \ kropki s_ {n}} {\ Gamma \ vdash C}}}

gdzie C jest również A lub B i są sekwencjami. Na przykład modus ponens to zasada eliminacji implikacji: ${\ Displaystyle s_ {1} \ kropki s_ {n}}$

{\ Displaystyle {\ Frac {\ Gamma \ vdash A \ Rightarrow B ~~~~~~ \ Gamma \ vdash A} {\ Gamma \ vdash B}}}

Przykłady reguł eliminacji

Eliminacja koniunkcji

Istnieją dwie zasady usuwania koniunkcji:

{\ Displaystyle {\ Frac {A \ klin B} {A}} ~~~~~~~~~~~~~~~~~~~~~~ {\ Frac {A \ klin B} {B }}}

które są zapisane w formie ciągów:

{\ Displaystyle {\ Frac {\ Gamma \ vdash A \ klin B} {\ Gamma \ vdash A}} ~~~~~~~~~~~~~~~~~~~~~~ {\ Frac {\ Gamma \ vdash A \ wedge B} {\ Gamma \ vdash B}}}

Zasady te są uzasadnione następującymi ważnymi konsekwencjami:

{\ Displaystyle (A \ ziemia B) \ Rightarrow A}

{\ Displaystyle (A \ ziemia B) \ Rightarrow B}

Eliminacja dysjunkcji

Istnieje zasada eliminowania dysjunkcji:

{\ Displaystyle {\ Frac {{~ ​​\ atop A \ vee B} ~~~~~ {{[A] \ atop \ vdots} \ atop C} ~~~~~ {{[B] \ atop \ vdots} \ atop C}} {C}}}

który jest napisany w formie sekwencji:

{\ Displaystyle {\ Frac {\ Gamma \ vdash A \ vee B ~~~~~~ \ Gamma, A \ vdash C ~~~~~~ \ Gamma, B \ vdash C} {\ Gamma \ vdash C}} }

Zasada ta jest uzasadniona następującą ważną implikacją:

{\ Displaystyle ((A \ lor B) \ ziemia (A \ Rightarrow C) \ land (B \ Rightarrow C)) \ Rightarrow C.}

Eliminacja zaangażowania

W ponens modus jest zasada eliminacji implikacji.

{\ Displaystyle {\ Frac {A \ Rightarrow B ~~~~~ A} {B}}}

i jego postać w sekwencjach:

{\ Displaystyle {\ Frac {\ Gamma \ vdash A \ Rightarrow B ~~~~~~ \ Gamma \ vdash A} {\ Gamma \ vdash B}}}

Jest to uzasadnione ważnymi wnioskami:

{\ Displaystyle ((A \ Rightarrow B) \ Wedge A) \ Rightarrow B.}

Eliminacja fałszywych

Zasada ex falso quodlibet polega na eliminacji fałszu (⊥):

{\ displaystyle {\ frac {\ bot} {A}}}

gdzie jest jakakolwiek propozycja. Zauważamy, że ⊥ jest tutaj nieważne , to znaczy stała. Jego forma z sekwencjami to: $W$

{\ Displaystyle {\ Frac {\ Gamma \ vdash \ bot} {\ Gamma \ vdash A}}}

Jest to uzasadnione ważnymi wnioskami:

{\ displaystyle \ bot \ Rightarrow A.}

Eliminacja negacji

Jego forma z sekwencjami to:

{\ Displaystyle {\ Frac {\ Gamma \ vdash \ neg A} {\ Gamma, A \ vdash \ bot}}}

Jest to uzasadnione ważnymi wnioskami:

{\ Displaystyle \ neg A \ Rightarrow (A \ Rightarrow \ bot).}

Powiązane artykuły

Bibliografia

Gerhard Gentzen ( tłum. R. Feys i J. Ladrière), Research on logical deduction [„Untersuchungen über das logische schließen”], Presses Universitaires de France,1955, s. 4-5.Przetłumaczone i skomentowane

Bibliografia

René David, Karim Nour, Christophe Raffali, Wprowadzenie do logiki, teoria dowodu 2001, Dunod, ( ISBN 2100067966 ) , rozdz. 5
Stephen Cole Kleene , logika matematyczna , Dover ,1967- Reprint Dover reprint, 2001, ( ISBN 0-486-42533-9 ) . Tłumaczenie francuskie, Logika matematyczna , Armand Colin, 1971 lub Gabay 1987 ( ISBN 2-87647-005-5 ) .
René Lalement, Logika, redukcja, rozdzielczość , Masson,1990