Το μάθημα δίνεται στα πλαίσια του Διαπανεπιστημιακού Μεταπτυχιακού Προγράμματος στη Λογική και Θεωρία Αλγορίθμων και Υπολογισμού (ΜΠΛΑ) στο οποίο συμμετέχει η Σχολή Hλεκτρολόγων Mηχανικών και Mηχανικών Yπολογιστών (ΣHMMY) και ο Tομέας Mαθηματικών της Σχολής Eφαρμοσμένων Mαθηματικών και Φυσικών Eπιστημών (ΣEMΦE) του EMΠ. Επίσης προσφέρεται ως μεταπτυχιακό μάθημα στα πλαίσια του μεταπτυχιακού προγράμματος της ΣΗΜΜΥ (Λογική και Πληροφορική Ι) καθώς και του αντίστοιχου προγράμματος της ΣΕΜΦΕ.
Πρόκειται για εισαγωγικό μάθημα στη Θεωρία Αποδείξεων με έμφαση στη Δομική Θεωρία Aποδείξεων (δομή των μαθηματικών αποδείξεων, απαλοιφή των τομών και κανονικοποίηση) καθώς και τη σύνδεση που έχει με την πληροφορική (λ-λογισμός με τύπους) μέσω της ισοδυναμίας Curry-Howard. Παρουσιάζει μεγάλο ενδιαφέρον για τους Μαθηματικούς και τους θεωρητικούς Πληροφορικούς καθώς η μελέτη της απόδειξης ενός μαθηματικού τύπου μπορεί να θεωρηθεί ως μελέτη του προγράμματος υπολογισμού ενός τύπου δεδομένων. Ενδιαφέρει όμως και τους ασχολούμενους με τα θεμέλια των μαθηματικών και την Επιστημολογία αφού το αρχικό έναυσμα της δημιουργίας της θεωρίας αποδείξεων ήταν η προσπάθεια του Hilbert να θεμελιώσει αυστηρά τα Μαθηματικά προσπαθώντας με περατοκρατικές μεθόδους να αποδείξει τη συνέπειά τους. Θα επιδιωχθεί, με εμβόλιμες σεμιναριακές ώρες, η ανάπτυξη και άλλων ζητημάτων σχετιζομένων με τη Θεωρία Αποδείξεων.

Μικρό ιστορικό: Η ανακάλυψη, πριν από έναν αιώνα, των αντινομιών στη θεωρία συνόλων και η συνακόλουθη αμφιβολία και αβεβαιότητα σε σχέση με τη χρήση αφαιρετικών μεθόδων στα Μαθηματικά οδήγησε τον D. Hilbert στη διατύπωση του περίφημου προγράμματός του: να περισώσει τις μεθόδους που χρησιμοποιούνται στα κλασικά μαθηματικά αποδεικνύοντας τη συνέπεια των μαθηματικών θεωριών με μεθόδους που έχουν στοιχειώδη συνδυαστικό (περατοκρατικό) χαρακτήρα και ως εκ τούτου διαφανείς και ασφαλείς. Παρ' όλο που ο K. Goedel απέδειξε με το θεώρημα της μη πληρότητας ότι το πρόγραμμα του Hilbert δεν μπορεί να πραγματοποιηθεί σύμφωνα με τον αρχικό του σχεδιασμό η ιδέα του Hilbert παρέμεινε η κινούσα δύναμη για την ανάπτυξη της θεωρίας αποδείξεων για πολλά χρόνια. Και επειδή αυτό το πρόγραμμα απαιτούσε την αξιωματικοποίηση-τυποποίηση των διαφόρων μαθηματικών θεωριών αυτό οδήγησε στη μελέτη per se των τυποποιημένων μαθηματικών αποδείξεων. Σήμερα υπάρχουν πολύ περισσότεροι λόγοι για τη μελέτη των αποδείξεων από αυτούς που επιβάλλει το πρόγραμμα Hilbert. Για παράδειγμα, η Aυτόματη Aπόδειξη Θεωρημάτων, μέρος της μελέτης στην Τεχνητή Νοημοσύνη, οδηγεί στη μελέτη των αποδείξεων ως συνδυαστικές δομές. Στο Λογικό Προγραμματισμό οι τυπικές απαγωγές χρησιμοποιούνται στους υπολογισμούς κλπ.

Περιεχόμενα

Αποδεικτικά συστήματα: φυσική απαγωγή, συστήματα Hilbert, συστήματα ακολουθητών του Gentzen.
Η έννοια της τομής, θεωρήματα απαλοιφής των τομών και εφαρμογές.
Κανονικοποίηση και αριθμητικά φράγματα στην απαλοιφή των τομών, δομή των αποδείξεων χωρίς τομές.
Ισοδυναμία Curry-Howard-de Bruijn.
Kανονικοποίηση στη φυσική απαγωγή.
Εισαγωγή στη Γραμμική Λογική.
Αριθμητική του Peano και ανάλυση των αποδείξεων με διατακτικούς αριθμούς.

Βιβλιογραφία, Αναφορές

Basic Proof theory, A.S. Troelstra & H. Schwichtenberg, 2nd ed., Cambridge Univ. Press, 2000.
Structural Proof Theory, Sara Negri & Jan von Plato, Cambridge Univ. Press, 2001.
Proofs and Types, J.-Y. Girard, Cambridge Univ. Press, 1989.
An Introduction to Proof Theory, Samuel R. Buss., in Handbook of Proof Theory, Elsevier, 1998.
Proof Theory and Logical Complexity, J.-Y. Girard, Bibliopolis, 1987.
Λογική και Απόδειξη, Branislav Boricic, Εκδ. Ζήτη, 1995.
The collected papers of G. Gentzen, M.E. Szabo, North Holland, 1969.
Proof Theory and Automated Deduction, Jean Goubault-Larrecq & Ian Mackie, Kluwer Ac. Publ., 1997.