Modus ponens
Modus ponens , sau detașare , este o figură de raționament logic în ceea ce privește implicarea . Acesta constă în afirmarea unei implicații („dacă A atunci B ”) și apoi stabilirea antecedentului („sau A ”) pentru a deduce consecința („deci B ”). Termenul modus ponens este o abreviere a latinei modus ponendo ponens, care înseamnă modul care, prin pozare , pune . Provine din faptul că, pozând (afirmând) A , pozăm(afirmă) B ( ponendo este gerunziul verbului ponere care înseamnă a pune , iar ponens este participiul prezent). Silogismul este o formă de aplicare a modus ponens.
Formalizare
Regula modus ponens sau detașarea este o regulă primitivă a raționamentului. Îl scriem formal (în funcție de context):
sau
și putem citi: „din A și A ⇒ B deducem B ”, sau chiar „ A și A ⇒ B deci B ”, adică afirmăm A și A ⇒ B și deducem că putem spune B .
Deși implicația conectorului (în general denotată „⇒” sau „→”) și relația de deducere (notată „⊢”) sunt strâns legate, ele nu sunt de aceeași natură și nu pot fi identificate, această distincție este necesară pentru a formaliza raționamentul. Astfel, tautologia propozițională [ A ∧ ( A ⇒ B )] ⇒ B nu este o regulă și nu poate reprezenta modus ponens, pentru conectorul implicativ desemnat prin „⇒”. Modus ponens poate fi văzut în acest sens ca regula care indică modul de utilizare a unei implicații în timpul unei demonstrații .
Sisteme de deducere
La Hilbert
Este adesea (dar nu neapărat) singura regulă de inferență în calculul propozițiilor , în sistemele de deducție à la Hilbert , deoarece regulile primitive ale celorlalți conectori sunt exprimate din axiome bine alese și din modus ponens. De exemplu regula conjuncției „a A ∧ B deducem A “ este derivat din modus ponens și axioma ( A ∧ B ) ⇒ A . De asemenea, modus ponens face posibil să se ajungă la principiul exploziei sau la raționamentul prin absurditatea logicii clasice .
Această regulă este esențială, în sistemele à la Hilbert : o astfel de reducere nu este posibilă pentru modul în sine, pentru a o deduce de exemplu din [ A ∧ ( A ⇒ B )] ⇒ B , ar fi necesar să se facă alte axiome ... și mai multe aplicații ale modus ponens în sine.
Deducerea naturală
Găsim o formă de modus ponens în sistemele de deducție naturală sub denumirea regulii de eliminare a implicației , unde are neapărat o formă mai generală, în sensul că trebuie să o folosim în prezența ipotezelor. Această generalizare nu este necesară în sistemele à la Hilbert , în care regula simetrică introductivă, „din A ⊢ B deducem A ⇒ B ”, este o regulă derivată, cunoscută sub numele de teorema deducției , care este din nou demonstrată din singura regulă a modus ponens și axiome adecvate, dar într-un mod mai complex, folosind o recurență pe durata deducției (traducerea depinde, așadar, de deducție).
Calculul secvențelor
Calculul sequents , din cauza ca deducerea naturale a Gerhard Gentzen , nu are în mod direct un modus ponens regula. Acest lucru poate fi derivat prin regula de tăiere care este un modus ponens la nivelul deducerii - în esență atunci când avem ⊢ A și A ⊢ B avem ⊢ B aceste deduceri făcându-se într-un anumit context - și implicarea regulii din stânga care poate demonstra secvențial A , A ⇒ B ⊢ B . Gentzen a arătat că regula de tăiere ar putea fi eliminată în calculul secvențelor pentru calculul predicatelor pure (fără egalitate și în afara cadrului unei teorii axiomatice ) și că, în acest context, dovada unei formule ar putea folosi doar sub-formule ale acestuia. Acest lucru nu este posibil într-un sistem à la Hilbert, unde, de îndată ce se apelează la modus ponens, se introduce o formulă mai complexă decât formula care trebuie demonstrată.
Ca o deducție naturală, proprietatea de normalizare, care corespunde eliminării tăieturilor în calculul secvențelor, arată că este posibil (încă în calculul predicatelor pure) să se restricționeze utilizarea modus ponens la sub-formulele din formula de demonstrat.
Proprietatea subformulei pentru aceste două sisteme (deducția naturală și calcularea secvențelor) are ca contrapartidă introducerea unui nivel suplimentar, cel al secvențelor, unde deducerea sistemelor à la Hilbert se ocupă doar de formule.
Articole similare
- Modus tollens
- Raţionament
- Regula de rezolvare (generalizează modus ponens)
- Regula inferenței
- Regula cutoff
- Silogism
- Ce i-a spus țestoasa lui Ahile , dialog de Lewis Carroll expunând un paradox asociat cu modus ponens .
Bibliografie
- René Cori și Daniel Lascar , Logică matematică I. Calcul propozițional, algebre booleene, calcul predicat [ detaliu ediții ]