Teoria martorilor: Note despre λ-calcul și logică

Titlul original:

Witness Theory: Notes on λ-calculus and Logic

Conținutul cărții:

Această carte se referă la analiza matematică a conceptului de dovadă formală în logica clasică și înregistrează - în esență - un exercițiu mai lung de λ-calcul aplicat.

Urmând limbaje colocviale care se întorc la L. E. J. Brouwer, obiectele de studiu în această întreprindere sunt numite martori. Un martor este menit să reprezinte demonstrația logică a unei formule cu valabilitate clasică, într-un context de demonstrație dat. Formalismele utilizate pentru exprimarea martorilor și a comportamentului lor ecuațional sunt extensii ale λ-calculului "pur tipizat", considerate teorii ecuaționale.

Formal, un martor este generat din variabile martor decorate - sau tipizate' -, care reprezintă ipoteze, și operatori martor, care reprezintă reguli logice de inferență.

Specificațiile ecuaționale servesc la definirea operatorilor martor.

În general, acest lucru se poate face prin ignorarea "tipizării", adică a formulelor logice în sine.

Teoretic, martorii sunt obiecte ale unui model extensional Scott λ-model.

Abordarea - denumită generic "teoria martorilor" - este inspirată din lucrările lui N. G. de Bruijn privind o teorie matematică a demonstrării, efectuate la sfârșitul anilor 1960 și începutul anilor 1970, la Universitatea din Eindhoven (Țările de Jos), și este similară cu abordarea din spatele corespondenței Curry-Howard, cunoscută din logica intuiționistă.

Pentru cazul clasic, decorurile - denumite adesea "tipuri" - sunt formule logice clasice.

La nivelul fără cuantificator, teoria ecuațională de interes este λ-calculul cu "împerechere surjectivă" și unele subsisteme ale acestuia, decorate în mod corespunzător.

Extinderea la cuantificatorii propoziționali, de ordinul întâi și al doilea este simplă.

Cartea constă într-o colecție de note și lucrări scrise și difuzate în ultimii zece ani, ca o continuare a cercetărilor anterioare efectuate de autor în anii optzeci.

Printre altele, ea include o trecere în revistă a originilor teoriei moderne a probelor - de la Frege la Gentzen - din punct de vedere al teoriei martorilor, precum și o aplicație caracteristică a teoriei martorilor la o problemă de logică practică privind axiomatisabilitatea.