Logica intuiționistă

Rețeaua Rieger-Nishimura.

Logica intuiționistă (sau intuiționistă ), sau logică constructivă , este logica intuiționismului matematic și a altor forme de constructivism matematic .

Conform perspectivei intuiționiste, logica și matematica sunt aplicațiile metodelor interne coerente pentru realizarea constructelor mentale de complexitate crescândă. Logica intuiționistă este propusă ca o logică matematică riguroasă și formală. Deși nu este clar dacă un calcul logic formal epuizează aspectele mai deschis filosofice ale intuiționismului, acesta prezintă proprietăți care sunt destul de utile în practica științifică .

Logica intuitivă ca paradigmă a raționamentului logic

În logica intuiționistă, pasajele epistemologic inadecvate din probe sunt respinse. În logica clasică, o afirmație A înseamnă că „ A este adevărat”. În intuiționism, o astfel de formulă este considerată adevărată numai dacă poate fi demonstrată . Un exemplu al acestei diferențe este, de exemplu, principiul terțului exclus ( Tertium non datur , vezi și principiul bivalenței : $A\vee \neg A$ ${\ displaystyle A \ vee \ neg A}$ $A \ vee \ neg A$ ); acest principiu este respins de logica intuiționistă deoarece, într-un limbaj care permite o astfel de formulă, este posibil să se concluzioneze că ( $P\vee \neg P$ ${\ displaystyle P \ vee \ neg P}$ ${\ displaystyle P \ vee \ neg P}$ ) fără a fi clar dacă P este adevărat sau fals. În logica intuiționistă, al treilea principiu exclus înseamnă doar că cel puțin unul dintre P și ¬ P poate fi dovedit; o formulare mai puternică decât echivalentul clasic, care consideră adevărată singura disjuncție. Teza fundamentală este că validitatea unui construct mental depinde doar de consistența afirmației în context. Logica intuiționistă înlocuiește noțiunea de adevăr cu cea de justificare în calculul său logic. Prin urmare, o demonstrație corectă nu păstrează validitatea în trecerea de la premise la concluzii, ci justificarea .

Logica intuiționistă a oferit sprijin filozofic mai multor școli filosofice, inclusiv antirealismul lui Michael Dummett .

Logica intuitivă ca calcul formal și logic

În practică, există motive întemeiate să folosim logica intuiționistă. De fapt, în programare , simplele afirmații ale existenței sunt de puțin interes. Un program de calculator este compilat pentru a oferi un răspuns, nu pentru a pretinde că există unul (sau nu există). Într-adevăr, ar fi ciudat ca un sistem să ofere o dovadă pentru ∃ x P ( x ), dar nu ar putea demonstra P ( b ) pentru niciun b care nu este o variabilă liberă.

O formalizare riguroasă a logicii intuiționiste necesită teoria modelelor adecvate și teoria dovezilor. Sintaxa formulelor intuiționiste este similară cu logica propozițională (sau de ordinul întâi). Desigur, multe tautologii ale logicii clasice nu mai pot fi demonstrate în intuiționism; nu numai principiul terțului exclus, ci și legea lui Peirce și una dintre teoremele lui De Morgan .

Un alt exemplu de tautologie clasică respinsă de logica intuiționistă se referă la eliminarea dublei negații . În logica clasică, atât P → ¬¬P, cât și ¬¬P → P sunt teoreme. Logica intuiționistă acceptă doar prima: dubla negație poate fi introdusă, dar nu eliminată. Acest lucru se datorează faptului că noțiunea intuiționistă de negație este diferită de echivalentul său clasic. Dacă logica clasică înțelege ¬P ca „P este falsă”, în logica intuiționistă ¬P afirmă că există o dovadă care dovedește inexistența unei dovezi a lui P. Asimetria dintre cele două implicații este evidentă. Dacă P este demonstrabil, atunci este cu siguranță imposibil să se demonstreze că nu există nici o dovadă a lui P (introducerea dublei negații); dar eliminarea dublei negații este nedurabilă din punct de vedere intuiționist: dacă nu există dovezi că nu există dovezi ale lui P, nu este posibil să se concluzioneze că există o dovadă a lui P. Cu toate acestea, este posibil să se dovedească o versiune mai slabă a eliminarea dublei negații astfel încât ¬¬¬P se termină cu ¬P.

Observând că multe tautologii clasic valabile nu sunt teoreme ale logicii intuiționiste subminează teoria dovedirii logicii clasice. Gerhard Gentzen a obținut o versiune mai slabă a calculului său succesiv (LK), cunoscută sub numele de LJ, care este o teorie susținută din punct de vedere intuiționist.

Semantica intuitivă este mai complicată decât semantica clasică. O teorie model poate fi reprezentată de algebra lui Arend Heyting sau de semantica lui Saul Kripke .