Inferensregel
I et logisk system , de reglene slutning er reglene som prosessen med fradrag , derivasjon eller demonstrasjon er basert . Anvendelsen av reglene på aksiomene til systemet gjør det mulig å demonstrere setningene .
Definisjoner og fremstillinger
En slutningsregel er en funksjon som tar en formelformel og returnerer en formel. Argumentformlene kalles " premissene " og den returnerte formelen kalles "konklusjonen". Inferensreglene kan også sees på som relasjoner som forbinder premisser og konklusjoner der en konklusjon sies å være " fradragsberettiget " eller "avledbar" fra premissene. Hvis settet med lokaler er tomt, kalles konklusjonen et " teorem " eller et " aksiom " av logikk.
Inferensregler er generelt gitt i følgende standardform:
Forutsetningen n o en
forutsetning n o 2
...
forutsetningen n o n
Konklusjon
Dette uttrykket sier at hvis man er midt i en logisk avledning, der premissene allerede er oppnådd (dvs. logisk avledet fra aksiomene), så kan man si at konklusjonen er oppnådd. Det formelle språket som brukes til å beskrive premissene og konklusjonen, avhenger av det formelle eller logiske systemet man er plassert i. I det enkleste tilfellet er formlene bare logiske uttrykk; dette er tilfelle for modus ponens :
A → B
A
∴B
Inferensregler kan også formuleres på denne måten:
- en rekke lokaler (kanskje ingen);
- et avledningssymbol som betyr "utleder", "demonstrerer" eller "konkluderer";
- en konklusjon.
Denne formuleringen representerer vanligvis det relasjonelle (i motsetning til funksjonelle) syn på en inferensregel, der avledningssymbolet representerer en påviselig sammenheng som eksisterer mellom premisser og konklusjon.
Inferensens regler blir også noen ganger presentert på samme måte som dette uttrykket for modus ponens , som tydelig uttrykker behovet for at premissene skal være teoremer:
Hvis A → B og A, så B.Inferensregler er generelt formulert som "regelskjemaer", gjennom bruk av universelle variabler. I diagrammene ovenfor kan A og B erstattes av en hvilken som helst velformet formel for proposisjonslogikk (vi noen ganger begrenser oss til en delmengde av formlene til logikk, som proposisjoner ) for å danne et uendelig sett av slutningsregler.
Et demonstrasjonssystem består av et sett med regler som kan lenkes sammen for å danne demonstrasjoner eller avledninger. En avledning har bare en endelig konklusjon, som er det demonstrerte eller avledede uttrykket. Dersom lokalene ikke er fornøyd, så avledning er beviset for en hypotetisk uttrykk: hvis lokalene er fornøyd, så konklusjonen er fornøyd.
Akkurat som aksiomer er regler uten premiss, kan aksiomskjemaer også sees på som regelordninger uten premiss.
Eksempler
Den grunnleggende slutningsregelen for proposisjonslogikk er modus ponens , ved siden av den finner vi modus tollens og regler som beskriver oppførselen til kontakter . For logikken til første ordens predikater , er det slutningsregler som håndterer kvantifiseringsmidler som generaliseringsregelen .
I dag er det mange formelle logikksystemer , hvert med sitt eget språk med velformede formler, sine egne regler for slutning og sin egen semantikk; det er tilfellet med modalogikk som benytter seg av nødvendighetsregelen .
Inferensregler og aksiomer
Inferensregler må skilles fra aksiomer i en teori. Når det gjelder semantikk, er aksiomer gyldige påstander. Aksiomer blir vanligvis sett på som utgangspunkt for anvendelse av inferensregler og generering av sett med konklusjoner. Eller i mindre tekniske termer:
Regler er utsagn om systemet, aksiomer er utsagn som tilhører systemet. For eksempel :
- Regelen som sier at fra p kan vi utlede påviselig (p) er en uttalelse som sier at hvis vi har bevist p , så er p påviselig. Denne regelen gjelder for eksempel i Peano-aritmetikk ;
- Aksiomet p Påviselig (p) vil bety at enhver sann påstand er bevisbar. Denne påstanden er derimot falsk i Peanos aritmetikk (det er karakteriseringen av dens ufullstendighet ).
Eiendommer
Effektivitet
En ønskelig egenskap ved en slutningsregel er at den er effektiv . Det vil si at det er en effektiv prosedyre som bestemmer om en gitt formel kan avledes fra et definert sett med formler. De omega-regel , som er en infinitary regel, er et eksempel på en ikke-effektive regelen. Det er imidlertid mulig å definere bevis med effektive omega-regler, men det er en begrensning som vi legger til, og som ikke kommer fra reglens art, slik det er tilfelle for vanlige proof-systemer.
En slutningsregel bevarer ikke nødvendigvis semantiske egenskaper som sannhet eller validitet. Faktisk har en logikk karakterisert på en rent syntaktisk måte ikke nødvendigvis semantikk. En regel kan for eksempel bevare egenskapen til å være sammenhengen til en underformel av den lengste formelen i settet med lokaler. Imidlertid brukes inferensens regler i mange systemer for å generere (dvs. bevise ) teoremer fra andre teoremer og aksiomer.
Kvalifisering og avledbarhet
I et sett med regler kan en slutningsregel være overflødig i den forstand at den er "tillatt" eller "differensierbar". En avledbar regel er en regel hvis konklusjon kan utledes fra dens premisser ved hjelp av de andre reglene. En tillatt regel er en regel hvis konklusjon er avledet, når premissene er avledede. Alle avledede regler er derfor tillatt, men i noen regelsystemer kan det være tillatte ikke-avledbare regler. For å forstå forskjellen, kan vi vurdere et sett med regler for å definere naturlige tall ( dommen om at det er et naturlig tall):
Den første regelen sier at 0 er et naturlig heltall, den andre sier at s (n) , etterfølgeren til n , er et naturlig heltall hvis n er ett. I dette logiske systemet er følgende regel, som sier at den andre etterfølgeren til et naturlig tall også er et naturlig tall, er avledet:
Dens avledning er ganske enkelt sammensetningen av to bruksområder av arveregelen som er sitert ovenfor. Følgende regel, som hevder eksistensen av en forgjenger for hvert naturlige tall som ikke er null, er bare tillatt:
Faktum er sant for naturlige heltall og kan bevises ved induksjon (for å vise tillatelsen til denne regelen, ville det være nødvendig å anta at premissene er differensierbare, og å få ved induksjon en avledning av ). På den annen side er den ikke avledbar, fordi den avhenger av strukturen til avledningen av premisset. Av denne grunn bevares avledbarhet når et logisk system utvides, mens tillatelse ikke er det. For å se forskjellen, anta at følgende (absurde) regel legges til det logiske systemet:
I dette nye systemet er dobbel-etterfølgerregelen alltid forskjellig. På den annen side er eksistensregelen til en forgjenger ikke lenger tillatt, fordi den er umulig å utlede . Den relative sårbarheten til tillatelse kommer fra måten det demonstreres på: Siden beviset fortsetter ved induksjon på strukturen til avledningen av lokalene, legger utvidelsene til systemet nye tilfeller til dette beviset, som kanskje ikke lenger er gyldig.
De tillatte reglene kan betraktes som teoremer i et logisk system. For eksempel, i beregningen av sequents der eliminering av kutt er gyldig, det kutt regelen er tillatt.
Terminologi
Inferensreglene ble formelt definert av Gerhard Gentzen , som kalte dem figurer eller figurer for deduksjon (Schlußfiguren). I presentasjonen , ... ,, kalles disse matematiske objektene sekvenser eller vurderinger . De blir da kalt forgjengerne eller hypotesene og kalles konsekvensen eller konsekvensen .
Merknader og referanser
- Kirke, 1956.
- Jean-Yves Girard Bevissteori og logisk kompleksitet , kap. 6.
- (fr) Denne artikkelen er delvis eller helt hentet fra den engelske Wikipedia- artikkelen med tittelen " Inferensregel " ( se forfatterlisten ) .