Fitch stil for naturlig deduksjon

I matematisk logikk er Fitchs stil med naturlig deduksjon en variant av naturlig deduksjon . Det ble foreslått av logikeren Frederic Brenton Fitch . Demonstrasjonene presenteres på en lineær måte, og gir avkall på trestrukturen foreslått av Gentzen .

Introduksjon

Reglene angitt i dette avsnittet er de som gjelder beregning av forslag . De gjør det mulig å logisk lenke setningene, det vil si å introdusere nye setninger som logiske konsekvenser av det som er blitt sagt tidligere. Til hver av de grunnleggende logiske operatørene er to fradragsregler knyttet. En av reglene er en innledende regel : den forklarer hvordan man kan bevise et forslag som har operatøren. Den andre regelen er en eliminasjonsregel : den forklarer hvordan man bruker en proposisjon som har operatøren til å fortsette resonnementet.

Introduksjon og eliminering er nødvendig for å kunne demontere og montere formler. Jakten på et logisk trekk består nettopp i å analysere premissene, det vil si i å ta dem fra hverandre, og å sette sammen brikkene igjen for å lage formler som kan logisk knyttes til konklusjonen. Noen ganger antas det at det er veldig vanskelig å bevise matematikk, men i prinsippet er det ikke mye forskjellig fra et byggespill med kuber.

Regler knyttet til involvering

Regelen for å innføre implikasjon eller regelen for å forlate en foreløpig hypotese sier at for å bevise en implikasjon "hvis P da Q", er det tilstrekkelig å gå frem som følger: vi setter P som en foreløpig hypotese, vi trekker deretter trekk fra alt setninger pluss P for å nå Q. Når Q er nådd, kan vi deretter utlede "hvis P så Q". La oss insistere på ett punkt: Q er bevist under hypotesen P, men "hvis P så er Q", avhenger det bare av de tidligere premissene. Hvis vi bruker Fitchs metode, kan vi når som helst introdusere en foreløpig hypotese i et fradrag. Det er tilstrekkelig å flytte det til høyre i forhold til de andre lokalene. Alt som er utledt under en foreløpig antagelse, må være under det eller til høyre, men aldri på venstre side. Innledningsregelen lar oss konkludere med at vi har bevist "hvis P så Q" uten hypotesen P. Vi kan skifte "hvis P så Q" mot venstre med hensyn til P, men ikke med hensyn til de andre premissene som brukes. beviset på Q. Vi vil merke:

{\ displaystyle 1 \ quad \ quad P}

(foreløpig hypotese)

{\ displaystyle 2 \ quad \ quad Q}

(eiendom trukket fra 1)

{\ displaystyle 3 \ quad P \ to Q}

(innføring av implikasjonen mellom de to linjene 1 og 2)

Regelen om eliminering av implikasjon , eller regel om løsrivelse eller modus ponens sier at fra de to setningene "P" og "hvis P så Q" kan vi utlede "Q". Det tillater overføring fra allerede kjente forhold, P, til nye forhold, Q, forutsatt at det er en lov som autoriserer det, "hvis P da Q", som vil bli notert:

{\ displaystyle 1 \ quad P}

{\ displaystyle 2 \ quad P \ to Q}

{\ displaystyle 3 \ quad Q}

(eliminering av implikasjonen mellom linje 1 og 2)

La oss for eksempel vise at vi med disse to reglene kan utlede "hvis P så R" fra de to setningene "hvis P så Q" og "hvis Q så R":

{\ displaystyle 1 \ quad P \ to Q}

(hypotese)

{\ displaystyle 2 \ quad Q \ to R}

(hypotese)

{\ displaystyle 3 \ quad \ quad P}

(foreløpig hypotese)

{\ displaystyle 4 \ quad \ quad Q}

(modus ponens på 3 og 1)

{\ displaystyle 5 \ quad \ quad R}

(modus ponens på 4 og 2)

{\ displaystyle 6 \ quad P \ to R}

(regel for innføring av implikasjon mellom 3 og 5, oppgivelse av den foreløpige hypotesen P).

Reglene knyttet til sammenhengen

For sammenhengen er reglene veldig enkle.

Regelen for innføring av sammenhengen sier at fra de to setningene A og B kan vi utlede setningen (A og B).

{\ displaystyle 1 \ quad A}

{\ displaystyle 2 \ quad B}

{\ displaystyle 3 \ quad A \ land B}

(innføring av sammenhengen mellom 1 og 2)

De forbindelse eliminering regelen sier at, fra setningen (A og B), kan vi utlede to setninger A og B separat.

{\ displaystyle 1 \ quad A \ land B}

{\ displaystyle 2 \ quad A}

(eliminering av konjunksjon 1)

{\ displaystyle 3 \ quad B}

(eliminering av konjunksjon 1)

Disse reglene gjør det mulig å montere eller tvert imot separate påstander som alle anses å være sanne. Det er den logiske formen for fornuftens evne til å analysere verden, det vil si å studere dens deler hver for seg, og å syntetisere den, det vil si å bringe sammen elementene i en studie. I en helhet. Dette er grunnen til at disse reglene også kalles regler for analyse og oppsummering.

Reglene om fratredelse

De to fradragsreglene for disjunksjon er som følger.

Den innledende regel om disjunksjon eller regel om svekkelse av en avhandling sier at fra setningen P kan vi utlede setningen (P eller Q) så vel som setningen (Q eller P), uansett eller setningen Q. Denne regelen kan virker ikke interessant, men det er faktisk veldig viktig. Noen ganger er det fordelaktig å utlede (P eller Q) etter å ha bevist P, fordi vi også kan vite at (P eller Q) har andre konsekvenser.

{\ displaystyle 1 \ quad P}

{\ displaystyle 2 \ quad P \ lor Q}

(innføring av disjunksjon fra 1)

og det samme

{\ displaystyle 1 \ quad Q}

{\ displaystyle 2 \ quad P \ lor Q}

(innføring av disjunksjon fra 1)

Den motsetninger eliminering regelen eller hypotese motsetninger regel eller fall skilles regel, følger at hvis vi har vist seg (P eller Q), og vi har også vist seg (dersom P er R), så vel som (hvis Q, så er R), da vi har vist seg R. Denne regelen er nyttig når vi undersøker flere mulige tilfeller som fører til den samme konklusjonen.

{\ displaystyle 1 \ quad P \ lor Q}

{\ displaystyle 2 \ quad \ quad P}

(foreløpig hypotese)

{\ displaystyle 3 \ quad \ quad R}

(eiendom trukket fra 2)

{\ displaystyle 4 \ quad P \ to R}

(innføring av implikasjonen mellom 2 og 3)

{\ displaystyle 5 \ quad \ quad Q}

(foreløpig hypotese)

{\ displaystyle 6 \ quad \ quad R}

(eiendom trukket fra 5)

{\ displaystyle 7 \ quad Q \ to R}

(innføring av implikasjoner mellom 5 og 6)

{\ displaystyle 8 \ quad R}

(eliminering av skillet mellom 1, 4, 7)

Reglene om negasjon

Regelen for å innføre negasjonen sier at hvis vi viser en motsetning fra en hypotese P, er sistnevnte nødvendigvis falsk, og derfor er negasjonen dens sant. Således, hvis vi i et fradrag under den foreløpige hypotesen P, har funnet en motsigelse (Q og ikke Q), også bemerket , kan vi utlede nonP fra alle de tidligere premissene unntatt P. Med Fitchs metode skifter vi derfor (ikke P ) til venstre med hensyn til P, som er representert som følger: $\ bot$

{\ displaystyle 1 \ quad \ quad \ quad P}

{\ displaystyle 2 \ quad \ quad \ quad \ bot}

{\ displaystyle 3 \ quad \ lnot P}

(innføring av negasjon mellom 1 og 2)

Regelen om eliminering av negasjon eller regel om eliminering av dobbelnegasjon eller resonnement fra absurd sier at fra (nonP) kan vi utlede P. Dette er faktisk resonnement fra absurd fordi i en slik resonnement, for å bevise P, vi antar (ikke P) og vi søker å oppnå en motsetning. Hvis dette er tilfelle, har vi bevist (ikke P) i henhold til regelen om innføring av negasjonen, og det er faktisk regelen om eliminering av dobbeltnegasjonen som gjør det mulig å konkludere ved P:

{\ displaystyle 1 \ quad \ lnot \ lnot P}

{\ displaystyle 2 \ quad P}

(eliminering av dobbel negasjon 1)

eller

{\ displaystyle 1 \ quad \ quad \ lnot P}

(foreløpig hypotese [resonnering av det absurde])

{\ displaystyle 2 \ quad \ quad \ bot}

{\ displaystyle 3 \ quad \ lnot \ lnot P}

(innføring av negasjon mellom 1 og 2)

{\ displaystyle 4 \ quad P}

(eliminering av dobbel negasjon 3)

Når vi vurderer at hver setning nødvendigvis er enten sant eller usant, er gyldigheten av denne siste regelen åpenbar. Det er karakteristisk for klassisk logikk , som presenteres her og brukes av de aller fleste forskere. Noen ganger blir det bestridt på grunn av et viktig problem, bevis for eksistens av det absurde. Noen ganger kan du bevise at et problem har en løsning uten å kunne finne den. For det er det nok å bevise at fraværet av løsning fører til en motsetning. Begrunnelsen fra det absurde gjør det da mulig å konkludere med at det ikke er sant at problemet ikke har en løsning: nei nei (problemet har en løsning). I klassisk logikk fjerner vi den dobbelte negasjonen for å konkludere med at problemet har en løsning. Imidlertid gir fremgangsmåten som følges ikke noen konstruktiv prosess for den søkt løsning. Denne innvendingen ble reist av visse matematikere og logikere, inkludert Brouwer , som bestred denne metoden og motarbeidet Hilbert som forsvarte den. Konstruktivistiske eller intuisjonistiske matematikere anser at et bevis på tilværelsen er meningsløst hvis det ikke også gir en konstruktiv prosess for det aktuelle objektet. Også sistnevnte avviser regelen om undertrykkelse av den dobbelte negasjonen for å erstatte den med følgende regel: fra P og (ikke P) kan man utlede en motsetning, og fra denne motsetningen ethvert forslag Q (prinsippet om ex falso quodlibet ).

{\ displaystyle 1 \ quad P}

{\ displaystyle 2 \ quad \ lnot P}

{\ displaystyle 3 \ quad \ bot}

{\ displaystyle 4 \ quad Q}

(eliminering av negasjon 2 i intuisjonistisk logikk)

I eksemplene vil vi bruke denne andre eliminasjonsregelen når det er mulig å gjøre uten den dobbeltnegative eliminasjonsregelen.

Vi kan introdusere andre regler for de andre boolske operatørene, spesielt ekvivalensoperatøren, men dette er ikke nødvendig, fordi disse operatørene kan defineres fra de forrige, og deres fradragsregler kan deretter trekkes fra de tidligere reglene. (P tilsvarer Q) er definert av ((hvis P deretter Q) og (hvis Q så P)).

Eksempler

Vi gir nedenfor noen eksempler på bruk av naturlig fradrag. I den første delen vil vi ikke bruke regelen for å eliminere dobbel negasjon. I den andre delen vil vi bruke denne regelen. Formlene utledet i denne andre delen anerkjennes ikke som gyldige av intuisjonistiske matematikere . Vi bruker følgende symboler: for hvis ... så ... , for eller , for og , for nei . Symbolet angir en motsetning, det vil si en falsk proposisjon. $\ til$ $\ lor$ $\ land$ $\ ikke$ $\ bot$

Eksempler som ikke bruker dobbel negasjon eliminering

Eksempel 1 : ${\ displaystyle (\ lnot A \ land \ lnot B) \ to \ lnot (A \ lor B)}$

{\ displaystyle 01 \ quad \ quad \ lnot A \ land \ lnot B}

(foreløpig hypotese)

{\ displaystyle 02 \ quad \ quad \ lnot A}

(eliminering av konjunksjon 01)

{\ displaystyle 03 \ quad \ quad \ lnot B}

(eliminering av konjunksjon 01)

{\ displaystyle 04 \ quad \ quad \ quad A \ lor B}

(foreløpig hypotese)

{\ displaystyle 05 \ quad \ quad \ quad \ quad A}

(foreløpig hypotese)

{\ displaystyle 06 \ quad \ quad \ quad \ quad \ bot}

motsetning mellom 02 og 05

{\ displaystyle 07 \ quad \ quad \ quad A \ to \ bot}

(innføring av implikasjonen mellom 05 og 06)

{\ displaystyle 08 \ quad \ quad \ quad \ quad B}

(foreløpig hypotese)

{\ displaystyle 09 \ quad \ quad \ quad \ quad \ bot}

motsetning mellom 03 og 08

{\ displaystyle 10 \ quad \ quad \ quad B \ to \ bot}

(innføring av implikasjonen mellom 08 og 09)

{\ displaystyle 11 \ quad \ quad \ quad \ bot}

(eliminering av skillet mellom 04, 07, 10)

{\ displaystyle 12 \ quad \ quad \ lnot (A \ lor B)}

(innføring av negasjonen mellom 04 og 11)

{\ displaystyle 13 \ quad (\ lnot A \ land \ lnot B) \ to \ lnot (A \ lor B)}

(innføring av implikasjonen mellom 01 og 12 og slutten av fradraget)

Vi viser at det omvendte også er gyldig. Vi viser også at , men for gjensidighet av denne siste eiendommen, bruker vi eliminering av den dobbelte negasjonen. ${\ displaystyle \ lnot (A \ lor B) \ to (\ lnot A \ land \ lnot B)}$ ${\ displaystyle (\ lnot A \ lor \ lnot B) \ to \ lnot (A \ land B)}$

Eksempel 2 : ${\ displaystyle A \ to \ lnot \ lnot A}$

{\ displaystyle 01 \ quad \ quad A}

(foreløpig hypotese)

{\ displaystyle 02 \ quad \ quad \ quad \ lnot A}

(foreløpig hypotese)

{\ displaystyle 03 \ quad \ quad \ quad \ bot}

(eliminering av negasjon mellom 01 og 02)

{\ displaystyle 04 \ quad \ quad \ lnot \ lnot A}

(innføring av negasjonen mellom 02 og 03)

{\ displaystyle 05 \ quad A \ to \ lnot \ lnot A}

(innføring av implikasjonen mellom 01 og 04, slutten av fradraget)

Det omvendte følger direkte fra eliminering av dobbel negasjon og blir avvist av intuisjonister. Men merkelig nok er det ikke det samme med hvem som viser seg uten denne hypotesen, og som på sin side blir akseptert av intuisjonister. ${\ displaystyle \ lnot \ lnot A \ til A}$ ${\ displaystyle \ lnot \ lnot \ lnot A \ to \ lnot A}$

Eksempel 3 : ${\ displaystyle \ lnot \ lnot \ lnot A \ to \ lnot A}$

{\ displaystyle 01 \ quad \ quad \ lnot \ lnot \ lnot A}

(foreløpig hypotese)

{\ displaystyle 02 \ quad \ quad \ quad A}

(foreløpig hypotese)

{\ displaystyle 03 \ quad \ quad \ quad A \ to \ lnot \ lnot A}

(setning i eksempel 2)

{\ displaystyle 04 \ quad \ quad \ quad \ lnot \ lnot A}

(eliminering av involvering eller modus ponens mellom 02 og 03)

{\ displaystyle 05 \ quad \ quad \ quad \ bot}

(eliminering av negasjon mellom 01 og 04)

{\ displaystyle 06 \ quad \ quad \ lnot A}

(innføring av negasjonen mellom 02 og 05)

{\ displaystyle 07 \ quad \ lnot \ lnot \ lnot A \ to \ lnot A}

(innføring av implikasjonen mellom 01 og 06, slutten av fradraget)

Eksempler som bruker eliminering av dobbel negasjon

Følgende eksempler bruker eliminering av dobbel negasjon. Det kan vises at denne bruken er nødvendig. De aksepteres derfor ikke i intuisjonistisk logikk .

Eksempel 4 : ${\ displaystyle \ lnot (A \ land B) \ to (\ lnot A \ lor \ lnot B)}$

{\ displaystyle 01 \ quad \ quad \ lnot (A \ land B)}

(foreløpig hypotese [resonnering av det absurde])

{\ displaystyle 02 \ quad \ quad \ quad \ lnot (\ lnot A \ lor \ lnot B)}

(foreløpig hypotese)

{\ displaystyle 03 \ quad \ quad \ quad \ lnot (\ lnot A \ lor \ lnot B) \ to (\ lnot \ lnot A \ land \ lnot \ lnot B)}

(setning, gjensidig fra eksempel 1)

{\ displaystyle 04 \ quad \ quad \ quad \ lnot \ lnot A \ land \ lnot \ lnot B}

(eliminering av involvering eller modus ponens mellom 02 og 03)

{\ displaystyle 05 \ quad \ quad \ quad A \ land B}

(eliminering av dobbel negasjon i 04)

{\ displaystyle 06 \ quad \ quad \ quad \ bot}

(eliminering av negasjon mellom 01 og 05)

{\ displaystyle 07 \ quad \ quad \ lnot \ lnot (\ lnot A \ lor \ lnot B)}

(innføring av negasjonen mellom 02 og 06)

{\ displaystyle 08 \ quad \ quad \ lnot A \ lor \ lnot B}

(eliminering av dobbel negasjon i 07)

{\ displaystyle 09 \ quad \ lnot (A \ land B) \ to (\ lnot A \ lor \ lnot B)}

(innføring av implikasjonen mellom 01 og 08)

Eksempel 5 : Hvis det ikke kreves eliminering av den dobbelte negasjonen, er denne nødvendig for å bevise det omvendte . ${\ displaystyle (A \ til B) \ til (\ lnot B \ til \ lnot A)}$ ${\ displaystyle (\ lnot B \ til \ lnot A) \ til (A \ til B)}$

Eksempel 6 : Det kan vi vise . Faktisk hvis vi og , har vi (falske) og derfor har vi det . ${\ displaystyle \ lnot A \ to (A \ til B)}$ $\ A ikke$ $PÅ$ $\ bot$ $B$

Eksempel 7 : På samme måte bruker beviset på gyldigheten til den utelukkede tredjedelen eliminering av den dobbelte negasjonen. Forutsatt at vi utleder (gjensidig av eksempel 1), derav en motsetning og gyldigheten av . $A \ lor \ lnot A$ ${\ displaystyle \ lnot (A \ lor \ lnot A)}$ ${\ displaystyle \ lnot A \ land \ lnot \ lnot A}$ ${\ displaystyle \ lnot \ lnot (A \ lor \ lnot A)}$

Hvis intuisjonister avviser det ekskluderte, aksepterer de selvfølgelig prinsippet om ikke-motsigelse . Antagelsen er faktisk en motsetning. Vi har dermed ved innføring av negasjonen. $\ lnot (A \ land \ lnot A)$ ${\ displaystyle A \ land \ lnot A}$ $\ lnot (A \ land \ lnot A)$

Eksempel 7 kjent under navnet lov Peirce : . Merkelig nok, selv om det ikke inneholder en negasjon, krever fradraget av denne loven eliminering av den dobbelte negasjonen, for eksempel ved bruk av den ekskluderte tredje. Vi antar at vi har det . I følge den ekskluderte tredje: ${\ displaystyle ((A \ til B) \ til A) \ til A}$ ${\ displaystyle ((A \ til B) \ til A)}$

eller vi har , $PÅ$

eller vi har og derfor har vi (eksempel 6) og siden vi har med modus ponens, har vi det . $\ A ikke$ ${\ displaystyle A \ til B}$ ${\ displaystyle ((A \ til B) \ til A)}$ $PÅ$

Trekkreglene for kvantifiserere

Bruk av variabelnavn i førsteordens teorier

Fradragsreglene for universelle og eksistensielle operatører styrer bruken av variabelnavn. Denne bruken gir en teori generalitetens kraft, det vil si muligheten for å kjenne ikke hvert individ tatt isolert, men alle individer av samme kjønn, i en enkelt setning.

Reglene for bruk av variabler spesifiserer betingelsene under hvilke variabelnavn kan introduseres og hva som deretter kan sies om dem. Disse reglene er naturlige, men det er noen tekniske vanskeligheter med begrepene begrep, fri eller koblet forekomst av en variabel, erstatning av et begrep for forekomster av en variabel og erstatning av en variabel for forekomster. Av et begrep.

For at en teori skal kunne bruke førsteordenslogikk, er det nødvendig å ha definert et domene av objekter, og det er nødvendig at predikatene som teorien tillegger objektene ikke i seg selv er gjenstander for teorien.

Betydningen av et objektvariabelsnavn er å representere ethvert objekt i teorien: la x være et tall. Ofte introduserer vi et variabelt navn i lokaler som bestemmer generelle forhold for dette objektet. x er ethvert objekt i teorien, forutsatt at den oppfyller disse betingelsene: la x være et primtall ... En teori inneholder vanligvis navn på objektene. Hele tallteorien inneholder for eksempel navn på alle tall: 0, 1, 2, ..., -1, -2, ...

Vilkår kan være enkle eller sammensatte. Dette er objektnavnene, objektvariabelnavnene og alle sammensatte uttrykk som kan dannes ut fra dem ved å bruke teoriens objektoperatører. For eksempel er 1, x, x + 1 og (x + x) +1 termer fra tallteori.

La oss først huske det veldig viktige skillet mellom variablene koblet av en operatør og de andre, de frie variablene. Forekomsten av et variabelnavn i en setning er alle stedene der navnet vises. En hendelse kan være gratis eller koblet. Når en eksistensiell eller universell operator i x blir brukt på en kompleks setning, blir alle forekomster av x koblet av denne operatoren. Alle hendelser som ikke er knyttet sammen er gratis.

Hvis en setning inneholder flere eksistensielle og universelle operatorer, er det ønskelig at disse operatorene alle forholder seg til forskjellige variabelnavn. Denne regelen er ikke viktig. Det blir ikke respektert når vi setter beregningen av predikater i form av en sylindrisk algebra (en sylindrisk algebra er en boolsk algebra fullført av lover som er spesifikke for universelle og eksistensielle operatører). Men det blir alltid respektert i praksis fordi det hjelper til å unngå forvirring.

En setning erholdes fra en annen ved å erstatte forekomsten av en variabel x når alle ledige forekomster av x er erstattet av t. For eksempel (far til x er menneske og far til x er ærlig) oppnås ved å erstatte begrepet far til x for variabelen y i formelen (y er menneskelig og y er ærlig).

Disse forberedelsene gjør det mulig å formulere fradragsregler for universelle og eksistensielle operatører.

Reglene knyttet til den universelle kvantifisereren

Innledningsregelen til den universelle kvantifiserings- eller generaliseringsregelen sier at fra P (x) kan vi utlede (for alle x, P (x)) forutsatt at variabelnavnet x aldri vises i hypotesene som P (x) avhenger av.

{\ displaystyle 1 \ quad P (x)}

{\ displaystyle 2 \ quad \ forall x \; P (x)}

(introduksjon av hva som helst , der x ikke er gratis i lokalene til P)

Ofte introduseres variabler i foreløpige forutsetninger. Vi resonnerer om dem som om de var gjenstander. Deretter kan vi trekke generelle lover, fordi det vi har utledet, er sant for alle objektene som tilfredsstiller de samme hypotesene. Det er reglene for å forlate en foreløpig hypotese og for generalisering som tillater oss å konkludere.

Den universelle kvantifiseringseliminasjonsregelen eller singulariseringsregelen sier at, fra en setning av formen (for alle x) P (x), kan vi utlede P (t), for ethvert begrep t som variablene ikke er relatert til i P (x ). P (x) betegner enhver setning som inneholder x som en fri variabel, P (t) betegner setningen som er oppnådd fra P (x) ved å erstatte t for alle frie forekomster av x. Singulariseringsregelen er ganske enkelt å anvende en universell lov på en sak.

{\ displaystyle 1 \ quad \ forall x \; P (x)}

{\ displaystyle 2 \ quad P (t)}

(eliminering av hva som helst )

Regler knyttet til den eksistensielle kvantifisereren

Innledningsregelen til den eksistensielle kvantifisereren , eller regelen om direkte bevis for eksistens, sier at fra setningen P (t) kan vi utlede at det eksisterer en x slik at P (x) for enhver variabel x som ikke vises i P (t) og for ethvert begrep t hvis variabelnavn ikke er relatert i P (x).

P (t) betegner en setning som inneholder begrepet t minst en gang. P (x) oppnås fra P (t) ved å erstatte x med t ved en eller flere av dens forekomster. I denne regelen er det ikke nødvendig å erstatte x for alle forekomster av t.

{\ displaystyle 1 \ quad P (t)}

{\ displaystyle 2 \ quad \ eksisterer x \; P (x)}

(introduksjon av det eksisterer )

Regelen om eliminering av den eksistensielle kvantifisereren eller regelen om konsekvensene av eksistens tillater, fra en proposisjon (det eksisterer x, P (x)), å introdusere en ny foreløpig hypotese P (y) der y er et variabelt navn som aldri har blitt brukt før og hvor P (y) erholdes fra P (x) ved å erstatte y for alle forekomster av x. Vi kan da resonnere under denne hypotesen. Regelen om konsekvensene av tilværelsen gjør det da mulig å konkludere som følger: fra setningen (det er en x slik at P (x)) kan vi utlede R når R er utledet under den eneste ekstra foreløpige hypotesen P ( y) og at y ikke vises i lokalene før P (y) og heller ikke i R. y er en slags hypotetisk vesen. Det fungerer bare som mellomledd i et fradrag, men det vises ikke i sine lokaler eller i konklusjonen.

{\ displaystyle 1 \ quad \ eksisterer x \; P (x)}

(hypotese)

{\ displaystyle 2 \ quad \ quad P (y)}

( y ny variabel)

{\ displaystyle 3 \ quad \ quad R}

(trekk fra 2, R ikke involverer y )

{\ displaystyle 4 \ quad R}

(eliminering av det finnes i 1 og 3)

Eksempler

Eksempel 1 ${\ displaystyle (\ eksisterer x \; \ lnot A (x)) \ til (\ lnot \ forall x \; A (x))}$

{\ displaystyle 1 \ quad \ quad \ eksisterer x \; \ lnot A (x)}

(foreløpig hypotese)

{\ displaystyle 2 \ quad \ quad \ quad \ forall x \; A (x)}

(foreløpig hypotese)

{\ displaystyle 3 \ quad \ quad \ quad \ quad \ lnot A (y)}

( y ny variabel fra 1)

{\ displaystyle 4 \ quad \ quad \ quad \ quad A (y)}

(eliminering av hva som helst i 2)

{\ displaystyle 5 \ quad \ quad \ quad \ quad \ bot}

(eliminering av negasjon 3, 4)

{\ displaystyle 6 \ quad \ quad \ quad \ bot}

(eliminering av det er mellom 1 og 5)

{\ displaystyle 7 \ quad \ quad \ lnot (\ forall x \; A (x))}

(innføring av negasjon mellom 2 og 6)

{\ displaystyle 8 \ quad (\ exist x \; \ lnot A (x)) \ to (\ lnot \ forall x \; A (x))}

(innføring av implikasjon 1, 7)

Eksempel 2 : vi har også , men beviset krever en eliminering av den dobbelte negasjonen, og denne teoremet om klassisk logikk aksepteres ikke i intuisjonistisk logikk. ${\ displaystyle \ lnot (\ forall x \; A (x)) \ to \ eksisterer x (\ lnot A (x))}$

Hvordan sjekker riktigheten av en resonnement?

Til disse tolv reglene, eller fjorten, hvis vi teller at regelen om eliminering av konjunktjonen faktisk er en dobbel regel, og den samme for regelen om innføring av disjunksjonen, må vi legge til en femtende, veldig enkel, repetisjonsregelen : du kan alltid gjenta en tidligere avhandling, med mindre det avhenger av en hypotese som har blitt forlatt. Vi kan derfor gjenta alle tesene så lenge vi ikke forskyver dem til venstre. Denne regelen er nødvendig når man ønsker å gjenta en premiss i en konklusjon eller når man trenger en tidligere avhandling i kroppen av et fradrag under foreløpig hypotese for å anvende en regel.

Listen over de foregående femten reglene er fullstendig i den forstand at det er tilstrekkelig å gjøre alle riktige fradrag. Kurt Gödel beviste, ( fullstendighetsteorem ) for et annet logisk system, men tilsvarende det som nettopp ble presentert, at det er tilstrekkelig å formalisere alle de riktige fradragene for beregningen av første ordens predikater .

De riktige fradragene er først og fremst de som strengt respekterer disse grunnleggende reglene. Alle setninger må være enten aksiomer, eller foreløpige hypoteser, eller konsekvenser av setningene som går foran dem i kraft av en av de femten reglene. For hastighets skyld kan du også bruke avledede regler (for eksempel fremover av ). En avledet regel er riktig når det kan vises at alt som kan utledes med det, også kan utledes uten det med bare grunnreglene. ${\ displaystyle \ lnot (A \ lor B)}$ ${\ displaystyle (\ lnot A \ land \ lnot B}$

Så lenge fradragene er formalisert, er det alltid mulig å gjenkjenne, inkludert et program, hvis et fradrag er riktig fordi fradragsreglene er endelige i antall, og det er alltid mulig å kontrollere på en endelig tid om en formel er konsekvensen av en eller flere andre under en av disse reglene. Denne tilnærmingen utfører en del av programmet som noen ganger kalles finitaire foreslått av David Hilbert for å løse problemene med grunnlaget for matematikk. Hilbert lette etter en effektiv metode som gjør det mulig å bestemme hvilken som helst matematisk uttalelse om det er en teorem, det vil si en matematisk sannhet. Beregningen av predikatene gjorde det mulig å redusere problemet til spørsmålet om å vite om en formel er en logisk lov eller ikke.

Men selv om det er mulig å verifisere gyldigheten av et fradrag som fører til en formel, kan omvendt ikke spørsmålet om en gitt formel er en logisk lov eller ikke løses generelt. Det er faktisk ingen universell metode som tillater å si om en formel er en logisk lov eller ikke. Denne ueksistensen trekkes ut fra Gödel's ufullstendighetssetning . Det sies at spørsmålet om en formel er en logisk lov er ubestemmelig.

Det er vanskeligere å kontrollere riktigheten av fradrag i det aktuelle språket. Det er først nødvendig å oversette de kjente setningene til et formalisert språk i predikatens kalkulator. Dette trinnet utgjør noen ganger et problem hvis du er i tvil om nøyaktigheten av oversettelsen. Men den største vanskeligheten kommer av det faktum at nåværende fradrag generelt gir et stort sted for det implisitte. Selv forholdet mellom avhengighet av en hypotese blir ikke alltid gjort eksplisitt. Tvert imot, formelle fradrag etterlater ingenting i mørket. De som er foreslått her ligner veldig på gjeldende fradrag bortsett fra at de forklarer alt. For å sertifisere det vanlige resonnementet og demonstrasjonene riktig, må alt som er implisitt forklares. Dette er grunnen til at du ofte må studere mye og vite alt det implisitte før du vet om en resonnement er riktig.

Bibliografi

Jon Barwise og John Etchemendy , Språkbestandig og logisk , Seven Bridges Press og CSLI, 1999.
Pelletier, Jeff, " A History of Natural Deduction and Elementary Logic Textbooks. "