mpla.math.uoa.gr
Font size: Αα Αα Αα hide gadgets
You are here: Courses » 2012-2013 » spring semester » Λ13Ξ. Intuitionistic logic and constructive mathematics (2012-2013, spring semester) Anonymously browsing from 54.81.44.140 at 15:06:36, 24-09-2017. login

Intuitionistic logic and constructive mathematics: 2012-2013, spring semester

For information about this course in general (not just for this specific semester), visit its page: Λ13Ξ. Intuitionistic logic and constructive mathematics.

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.

Taught by: Garyfallia Vafeiadou
Start date: March 5, 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

Tuesday, 05 Mar 2013

Friday, 08 Mar 2013

Monday, 11 Mar 2013

Friday, 15 Mar 2013

Monday, 18 Mar 2013

Friday, 22 Mar 2013

Friday, 29 Mar 2013

Monday, 01 Apr 2013

Friday, 05 Apr 2013

Monday, 08 Apr 2013

Friday, 12 Apr 2013

Monday, 15 Apr 2013

Friday, 19 Apr 2013

Monday, 22 Apr 2013

Friday, 26 Apr 2013

Monday, 13 May 2013

Friday, 17 May 2013

Monday, 20 May 2013

Friday, 24 May 2013

Monday, 27 May 2013

Friday, 31 May 2013

Monday, 03 Jun 2013

Friday, 07 Jun 2013

Monday, 10 Jun 2013

Friday, 14 Jun 2013

Monday, 17 Jun 2013

Comments

You must be logged in to comment.

Reporter

Page updates

No recent updates.

Feeds RSS and Atom feeds

posts
all posts RSS
news RSS
announcements RSS
website news RSS
events
all events RSS
defenses RSS
exams RSS
seminars RSS
graduations RSS
Web standards: XHTML1.0, CSS3.
© 1996 – 2017 MPLA: Graduate program in Logic, Algorithms and Computation.
Contact the webmaster.