Συστήματα Gentzen

Abstract

Το σύστημα των ακολουθιακών (sequent) του Gentzen. Προτασιακή και κατηγορηματική εκδοχή. Απόδειξη της πληρότητας και στις δύο εκδοχές. Η έννοια της τομής και το θεώρημα της κανονικοποίησης (Hauptsatz) του Gentzen. Καθορισμός φραγμάτων στην κανονικοποίηση. Μελέτη (και εξαγωγή συμπερασμάτων) των αποδείξεων χωρίς τομές. Τα συστήματα tableaux του Beth. Προτασιακά και κατηγορηματικά tableaux, σύνολα Hintikka, αποδείξεις πληρότητας για τα tableaux.<br/>Το σύστημα φυσικής απαγωγής και η αντιστοιχία του με το σύστημα των ακολουθιακών. Η έννοια του redex και του contractum και κατά συνέπεια η εισαγωγή ενός στοιχείου υπολογισμού στις λογικές – μαθηματικές αποδείξεις. Κανονικές αποδείξεις και κανονικοποίηση. <br/>Μικρή εισαγωγή στην ιντουισιονιστική λογική. Διαχωρισμός κλασικών και ιντουισιονιστικών αποδείξεων στα συστήματα των ακολουθιακών και της φυσικής απαγωγής. Ισοδυναμίες των συστημάτων με αντίστοιχα συστήματα τύπου Hilbert.

The Sequent Systems of Gentzen. Propositional and predicate versions. Proof of completeness in both versions. The concept of the cut and Gentzen's normalization theorem (Hauptsatz). Establishing bounds in normalization. Study and conclusions from cut-free proofs. Beth's tableaux systems. Propositional and predicate tableaux, Hintikka sets, completeness proofs for tableaux. The natural deduction system and its correspondence with the sequent system. The concepts of redex and contractum, introducing an element of computation into logical-mathematical proofs. Normal proofs and normalization. A brief introduction to intuitionistic logic. Distinguishing classical and intuitionistic proofs in the sequent and natural deduction systems. Equivalences of these systems with corresponding Hilbert-type systems.