mpla.math.uoa.gr
Font size: Αα Αα Αα hide gadgets
You are here: Courses » 2012-2013 » εαρινό εξάμηνο » Λ13Ξ. Ιντουισιονιστική λογική και κατασκευαστικά μαθηματικά (2012-2013, εαρινό εξάμηνο)

Ιντουισιονιστική λογική και κατασκευαστικά μαθηματικά: 2012-2013, εαρινό εξάμηνο

For information about this course in general (not just for this specific semester), visit its page: Λ13Ξ. Ιντουισιονιστική λογική και κατασκευαστικά μαθηματικά.

Η κατασκευαστική άποψη για τα μαθηματικά. Η ερμηνεία BHK των λογικών τελεστών. Συστήματα φυσικής απαγωγής και τύπου Hilbert για την ιντουισιονιστική προτασιακή και πρωτοβάθμια κατηγορηματική λογική. Σημασιολογία Kripke. Πρωτογενής αναδρομική αριθμητική PRA, αριθμητική Heyting HA. Αριθμητική πραγματοποίηση. Εισαγωγή στην κατασκευαστική ανάλυση.

Taught by: Γαρυφαλλιά Βαφειάδου
Start date: 05 Μαρτίου 2013
End date:

Teaching hours

We apologize, but we cannot remember the weekly schedule of this course.

Course information

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

Την Παρασκευή 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.

Enrolled students

Exams

Diary

Τρίτη, 05 Μάρ 2013

Παρασκευή, 08 Μάρ 2013

Δευτέρα, 11 Μάρ 2013

Παρασκευή, 15 Μάρ 2013

Δευτέρα, 18 Μάρ 2013

Παρασκευή, 22 Μάρ 2013

Παρασκευή, 29 Μάρ 2013

Δευτέρα, 01 Απρ 2013

Παρασκευή, 05 Απρ 2013

Δευτέρα, 08 Απρ 2013

Παρασκευή, 12 Απρ 2013

Δευτέρα, 15 Απρ 2013

Παρασκευή, 19 Απρ 2013

Δευτέρα, 22 Απρ 2013

Παρασκευή, 26 Απρ 2013

Δευτέρα, 13 Μάι 2013

Παρασκευή, 17 Μάι 2013

Δευτέρα, 20 Μάι 2013

Παρασκευή, 24 Μάι 2013

Δευτέρα, 27 Μάι 2013

Παρασκευή, 31 Μάι 2013

Δευτέρα, 03 Ιούν 2013

Παρασκευή, 07 Ιούν 2013

Δευτέρα, 10 Ιούν 2013

Παρασκευή, 14 Ιούν 2013

Δευτέρα, 17 Ιούν 2013

Comments

You must be logged in to comment.

Reporter

Web standards: XHTML1.0, CSS3.
© 1996 – 2018 MPLA: Graduate program in Logic, Algorithms and Computation.
Contact the webmaster.