Constructivism in mathematics. The BHK Interpretation of the logical operators. Natural deduction and Hilbert-type formal systems for intuitionistic propositional and first-order predicate logic. Kripke semantics. Primitive recursive arithmetic PRA, Heyting arithmetic HA. Number realizability. Introduction to constructive analysis.

Συνάντηση για απορίες.

Την Παρασκευή 28 Ιουνίου στις 14:00 στην αίθουσα Γ43 του Μαθηματικού Τμήματος θα γίνει συνάντηση για απορίες και ερωτήματα σχετικά με το μάθημα.

Για το αντικείμενο του μαθήματος

Τα κατασκευαστικά μαθηματικά—σε αντιπαραβολή με τα παραδοσιακά, κλασικά μαθηματικά—χαρακτηρίζονται από την απαίτηση κάθε απόδειξη ύπαρξης ενός μαθηματικού αντικειμένου (που έχει ορισμένες ιδιότητες) να στηρίζεται σε μια (νοερή) κατασκευή του, να μην είναι έμμεση, όπως συμβαίνει όταν χρησιμοποιείται η απαγωγή σε άτοπο.

Η πρώτη συγκροτημένη εμφάνιση της κατασκευαστικής άποψης υπήρξε ο ιντουισιονισμός του L. E. J. Brouwer, ένα από τα συστήματα φιλοσοφίας των μαθηματικών που (όπως ο λογικισμός του Frege και ο φορμαλισμός του Hilbert) προσπάθησαν στα τέλη του 19ου με αρχές του 20ού αιώνα να δώσουν απαντήσεις στα προβλήματα των θεμελίων των μαθηματικών. Η κατασκευαστικότητα, όπως ο Brouwer διέκρινε, επιβάλλει την απόρριψη της λογικής αρχής του αποκλειομένου τρίτου (A είτε όχι A), οδηγώντας στην ιντουισιονιστική λογική, που είναι κομμάτι της συνήθους, κλασικής λογικής και αποτελεί την κοινή λογική βάση ουσιαστικά όλων των προσεγγίσεων του τι είναι κατασκευαστικό.

Εκτός από τις απόψεις για τα θεμέλια, κίνητρο για την κατασκευαστική ανάπτυξη των μαθηματικών αποτελεί το γεγονός ότι κάθε κατασκευαστική απόδειξη έχει υπολογιστικό περιεχόμενο και παρέχει περισσότερη πληροφορία απ' ότι μια μη κατασκευαστική απόδειξη. Παρά τους σοβαρούς περιορισμούς, είναι δυνατόν μεγάλο μέρος των μαθηματικών να αναπτυχθεί κατασκευαστικά, όπως κατόρθωσε ο αναλύστας E. Bishop, υιοθετώντας μάλιστα μια ιδιαίτερα αυστηρή κατασκευαστική οπτική. Ιδιαίτερο ενδιαφέρον έχει η μελέτη των πραγματικών και του συνεχούς, καθώς έχουν αναπτυχθεί διάφορες εναλλακτικές θεωρίες, που αποκλίνουν γενικά από την κλασική.

Η διαμόρφωση της ιντουισιονιστικής λογικής και ιδιαίτερα η τυποποίησή της άνοιξε το δρόμο για τη διασύνδεση της λογικής με την πληροφορική, καθώς επέτρεψε την αντιστοιχία ανάμεσα σε αποδείξεις και προγράμματα μέσω του ισομορφισμού Curry-Howard. Η ιντουισιονιστική θεωρία τύπων του Per Martin-Löf, ο λογισμός των κατασκευών των Cocquand-Huet, η γλώσσα (proof-assistant) Coq είναι μερικά απ' όσα ακολούθησαν. Από μια άλλη πλευρά, σημαντικές δομές από τη θεωρία κατηγοριών όπως οι τόποι, είναι μοντέλα της ιντουισιονιστικής λογικής.

Βιβλιογραφία

1. Troelstra, A. S. and Dalen, D. van: Constructivism in Mathematics: An Introduction, volume 1, North-Holland, Amsterdam, 1988.

2. Moschovakis, Joan Rand: Notes on the Foundations of Constructive Mathematics, in progress (December 2006).

3. Kleene, S. C.: Introduction to Metamathematics, D. Van Nostrand Co., Inc., New York, N. Y., 1952.

4. Kleene, S. C. and Vesley, R. E.: The foundations of intuitionistic mathematics, especially in relation to recursive functions, North-Holland Publishing Co., Amsterdam 1965.

5. Bridges, D. and Richman, F.: Varieties of Constructive Mathematics, Cambridge University Press 1987.