Ο ιντουισιονισμός (ή ενδιαισθητισμός, από το intuitionism) είναι φιλοσοφική και μαθηματική σχολή σκέψης που αφορά τη φύση της μαθηματικής αλήθειας και το τι σημαίνει «ύπαρξη» στα μαθηματικά. Ξεκίνησε στις αρχές του 20ού αιώνα με κύριο εκπρόσωπο τον L.E.J. Brouwer (1881–1966).
Μια σύντομη, πρακτική εισαγωγή στη φιλοσοφία που απαιτεί εποικοδομητικές αποδείξεις και ξανασκέφτεται την έννοια της «ύπαρξης».
Σύγκριση με άλλες προσεγγίσεις
| Σχολή | Βασική θέση | Τι σημαίνει «ύπαρξη» |
|---|---|---|
| Πλατωνισμός | Υπάρχει ανεξάρτητος κόσμος μαθηματικών αντικειμένων. | Το «5», τα σύνολα κ.λπ. υπάρχουν αντικειμενικά. |
| Φορμαλισμός (Hilbert) | Τα μαθηματικά είναι σύμβολα/κανόνες· η συνέπεια αρκεί. | «Ύπαρξη» = μη-αντιφατικότητα εντός συστήματος. |
| Ιντουισιονισμός (Brouwer) | Τα μαθηματικά είναι διανοητικές κατασκευές. | «Ύπαρξη» μόνο αν δίνεται κατασκευή (algorithm/proof). |
Τι αλλάζει στην πράξη
- Απόρριψη του Νόμου του Αποκλειομένου Τρίτου (LEM): δεν δεχόμαστε «
P ∨ ¬P» χωρίς εποικοδομητική απόδειξη της μίας πλευράς. - Απόδειξη ύπαρξης = κατασκευή: Ρομαντικές «διά του άτοπου» ύπαρξεις δεν αρκούν.
- Ανάλυση/τοπολογία ξαναδιατυπώνονται: όρια, συνέχεια, συμπάγειες ορίζονται με «υπολογίσιμους»/εποικοδομητικούς όρους.
Παραδείγματα διαφορών
| Ζήτημα | Κλασικά Μαθηματικά | Ιντουισιονιστικά |
|---|---|---|
| Ύπαρξη λύσης | Αρκεί «αν δεν υπήρχε → αντίφαση». | Χρειάζεται ρητή μέθοδος κατασκευής λύσης. |
| Ισότητα πραγματικών | LEM: x = y ή x ≠ y. |
Θέλουμε διαδικασία που αποφασίζει/διακρίνει. |
| Προτάσεις τύπου «είτε/είτε» | Ισχύουν γενικά. | Μόνο με απόδειξη/αλγόριθμο διάκρισης. |
Λογική του Heyting & Πληροφορική
Η ιντουισιονιστική λογική τυποποιείται από τη λογική Heyting (χωρίς LEM). Η αρχή proofs-as-programs (Curry–Howard) συνδέει εποικοδομητικές αποδείξεις με αλγορίθμους και τύπους. Εργαλεία όπως Coq, Agda, Lean ευνοούν ιντουισιονιστικές αποδείξεις.
Με μια φράση
«Αληθινό» σημαίνει «κατασκευάσιμο». Αν δεν μπορώ να το χτίσω (με αυστηρό τρόπο), δεν έχω λόγο να το δέχομαι.
Δεν υπάρχουν σχόλια:
Δημοσίευση σχολίου