Η μαθηματική λογική είναι μια βασική περιοχή των μαθηματικών που εξελίχθηκε μέσα από τη συμβολική λογική. Πεδία της μαθηματικής λογικής είναι η θεωρία μοντέλων (model theory), η θεωρία αποδείξεων (proof theory), η θεωρία συνόλων και η θεωρία αναδρομής (recursion theory). Η έρευνα στη μαθηματική λογική συμβάλλει στη μελέτη των θεμελίων των μαθηματικών, αλλά η μαθηματική λογική περιέχει ακόμα πεδία των αμιγή μαθηματικών, που δεν σχετίζονται με θεμελιακές ερωτήσεις.

Η μαθηματική λογική σχετίζεται στενά με την μελέτη της (πολύ παλιότερης) τυπικής λογικής στη φιλοσοφία, που ξεκίνησε με τον Αριστοτέλη. Δίνει έναν ευκολότερο και πιο πλήρη τρόπο για τον έλεγχο της ορθότητας ισχυρισμών από ότι οι κλασσικές Αριστοτελικές μορφές. Η μαθηματική λογική σχετίζεται επίσης στενά με τα μεταμαθηματικά.

Ένα ενοποιητικό θέμα στη μαθηματική λογική είναι η μελέτη της εκφραστικής ισχύος των τυπικών λογικών και των τυπικών συστημάτων αποδείξεων. Η ισχύς αυτή μετράται με το ποιές μαθηματικές έννοιες μπορούν να οριστούν και ποιά θεωρήματα μπορούν να αποδειχθούν σε αυτά τα τυπικά συστήματα.

Ιστορία

Μαθηματική λογική ονομάστηκε από τον Τζουζέπε Πεάνο αυτό που αργότερα ονομάστηκε συμβολική λογική. Στην κλασσική της έκδοση, οι βασικές αρχές θυμίζουν τη λογική του Αριστοτέλη, γραμμένες όμως με συμβολικό τρόπο αντί για φυσική γλώσσα. Ορισμένοι από τους πιό φιλοσοφικούς μαθηματικούς έκαναν προσπάθειες να χειριστούν τις πράξεις της τυπικής λογικής με συμβολικό ή αλγεβρικό τρόπο, όπως ο Λάιμπνιτς και ο Λάμπερτ, αλλά οι προσπάθειές τους έμειναν άγνωστες και απομονομένες. Ήταν ο Τζώρτζ Μπουλ και ο Αυγουστος Ντε Μόργκαν, στο μέσο του 19ου αιώνα που παρουσίασαν ένα συστηματικό τρόπο μελέτης της λογικής. Το παραδοσιακό Αριστοτέλειο δόγμα της λογικής αναμορφώθηκε και συμπληρώθηκε, και από αυτή την εξέλιξη προέκυψε ένα επαρκές εργαλείο για τη μελέτη των θεμελιακών ιδεών των μαθηματικών. Θα ήταν παραπλανητικό να ισχυριστεί κανείς ότι οι θεμελιακές διαμάχες που υπήρχαν την περίοδο 199-1925 έχουν όλες λυθεί, αλλά η φιλοσοφία των μαθηματικών έχει διευκρινίστεί σε μεγάλο βαθμό από τη "νέα" λογική.

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

Κάποιες σημαντικές δημοσιεύσεις στη μαθηματική λογική περιέχουν το Begriffsschrift του Γκότλομπ Φρέγκε, τις Studies in Logic του Τσαρλς Πέιρς την Principia Mathematica του Μπέρτραντ Ράσσελ και του Άλφρεντ Νόρθ Γουάιτχεντ και το On Formally Undecidable Propositions of Principia Mathematica and Related Systems του Κουρτ Γκέντελ.

Τυπική λογική

Στον πυρήνα της, η μαθηματική λογική χειρίζεται μαθηματικές έννοιες που εκφράζονται χρησιμοποιώντας τυπικά συστήματα λογικής. Το σύστημα της λογικής πρώτου βαθμού (first-order logic) έχει μελετηθεί περισσότερο λόγω της εφαρμογής του στα θεμέλια των μαθηματικών και λόγω των επιθυμητών του ιδιοτήτων. Μελετώνται επίσης εκφραστικότερες κλασσικές λογικές όπως η λογική δευτέρου βαθμού (second-order logic) ή η infinitary λογική, αλλά και μη κλασσικές λογικές όπως η ενορατική λογική (intuitionistic logic).

Πεδία της μαθηματικής λογικής

Το βιβλίο "Handbook of Mathematical Logic" (1977) διαχωρίζει τη μαθηματική λογική σε τέσσερα μέρη:

* Θεωρία συνόλων είναι η μελέτων των συνόλων, τα οποία είναι αφηρημένες συλλογές από αντικείμενα. Οι βασικές έννοιες της θεωρίας συνόλων όπως το υποσύνολο και το σχετικό συμπλήρωμα λέγονται συχνά αφελής θεωρία συνόλων. Σύγχρονη έρευνα γίνεται στην περιοχή της αξιωματικής θεωρίας συνόλων, που χρησιμοποιεί λογικές μεθόδους για να μελετήσει ποιές προτάσεις είναι αποδείξιμες σε διάφορες τυπικές θεωρίες όπως η Ζερμέλο-Φράνκελ θεωρία συνόλων (ZFC) ή τα νέα θεμέλια.

* Θεωρία αποδείξεων είναι η μελέτη τυπικών αποδείξεων σε διάφορα συστήματα λογικής αναγωγής. Οι αποδείξεις αυτές αναπαριστώνται σαν τυπικές μαθηματικές οντότητες, διευκολύνοντας την ανάλυσή τους με μαθηματικές τεχνικές. Ο Φρέγκε εργάστηκε πάνω στις μαθηματικές αποδείξεις και τυποποίησε την έννοια της απόδειξης.

* Θεωρία μοντέλων είναι η μελέτη των μοντέλων από διάφορες τυπικές θεωρίες. Το σύνολο όλων τον μοντέλων μιας δεδομένης θεωρίας λέγεται στοιχειώδης κλάση. Η κλασσική θεωρία μοντέλων επιχειρεί να ανακαλύψει τις ιδιότητες των μοντέλων σε κάποια στοιχειώδη κλάση, ή να ανακαλύψει εάν κάποιες κλάσσεις από δομές αποτελούν στοιχειώδεις κλάσσεις. Η μέθοδος απάλειψης ποσοτικών τελεστών χρησιμοποιείται για να δείξει ότι μοντέλα κάποιας θεωρίας δεν μπορεί να είναι υπερβολικά πολύπλοκες.

* Θεωρία αναδρομής, που λέγεται και θεωρία υπολογισιμότητας, μελετά τις ιδιότητες των υπολογίσιμων συναρτήσεων, και τους βαθμούς Τούρινγκ, που διαιρούν τις μη-υπολογίσιμες συναρτήσεις σε σύνολα που έχουν το ίδιο επίπεδο μη-υπολογισιμότητας. Η θεωρία αναδρομής επίσης περιέχει τη μελέτη της γενικής υπολογισιμότητας και ορισιμότητας.

Τα σύνορα μεταξύ των πεδίων αυτών, και ακόμα μεταξύ της μαθηματικής λογικής και άλλων πεδίων των μαθηματικών δεν είναι πάντα καθαρά. Για παράδειγμα, το θεώρημα μη-πληρότητας του Γκέντελ όχι μόνο αποτελεί σταθμό στη θεωρία αναδρομής και τη θεωρία αποδείξεων, αλλά και έχει οδηγήσει στο θεώρημα Λόεμπ, το οποίο είναι σημαντικό στην τροπική λογική. Το μαθηματικό πεδίο της θεωρίας κατηγοριών χρησιμοποιεί πολλές τυπικές αξιωματικές μεθόδους που θυμίζουν αυτές που χρησιμοποιούνται στη μαθηματική λογική, αλλά η θεωρία κατηγοριών δεν θεωρείται συνήθως υποπεδίο της μαθηματικής λογικής.

Σχέση με την επιστήμη υπολογιστών

Υπάρχει μεγάλη σχέση μεταξύ της μαθηματικής λογικής και της επιστήμης υπολογιστών. Αρχικοί πρωτοπόροι της επιστήμης υπολογιστών, όπως ο Άλαν Τούρινγκ, ήταν επίσης μαθηματικοί και λογικοί.

Η μελέτη της θεωρίας υπολογισιμότητας στην επιστήμη υπολογιστών σχετίζεται στενά με τη μελέτη της υπολογισιμότητας στη μαθηματική λογική. Διαφέρουν όμως ως προς την έμφαση. Οι επιστήμονες υπολογιστών συχνά εστιάζουν σε πραγματικές γλώσσες προγραμματισμού και την εφικτή υπολογισιμότητα (feasible computability), ενώ οι ερευνητές στη μαθηματική λογική συχνά εστιάζουν στην υπολογισιμότητα ως θεωρητική έννοια, και στη μη-υπολογισιμότητα.

Η μελέτη της σημασιολογίας (semantics) γλωσσών προγραμματισμού σχετίζεται με την τροπική λογική (modal logic), όπως και την επαλήθευση προγράμματος (program verification), συγκεκριμένα, τον έλεγχο μοντέλων (model checking). Ο ισομορφισμός Κάρρυ-Χάουαρντ μεταξύ αποδείξεων και προγραμμάτων σχετίζεται με τη θεωρία αποδείξεων. Η ενορατική λογική και η γραμμική λογική είναι σημαντικές σ'αυτό. Λογισμοί όπως ο λάμδα λογισμός και η συνδυαστική λογική (combinatory logic) μελετώνται τελευταία ως ιδεατές γλώσσες προγραμματισμού.

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

Σημαντικά αποτελέσματα

* Το θεώρημα Λόβενχαιμ-Σκόλεμ (1919) έδειξε ότι αν ένα σύνολο από προτάσεις σε μια μετρήσημη γλώσσα πρώτου βαθμού έχει ένα άπειρο μοντέλο, τότε έχει τουλάχιστον ένα μοντέλο από κάθε άπειρη πληθικότητα (infinite cardinality).

* Το θεώρημα πληρότητας του Γκέντελ (1929) εδραίωσε την ισοδυναμία μεταξύ συντακτικών και εννοιολογικών ορισμών με λογική σημασία στη λογική πρώτου βαθμού.

* Το θεώρημα μη-πληρότητας του Γκέντελ (1931) έδειξε ότι κανένα αρκετά ισχυρό τυπικό σύστημα δεν μπορεί να αποδείξει την συνέπεια του εαυτού του.

* Η μη ύπαρξη αλγοριθμικής λύσης του προβλήματος απόφασης (Entscheidungsproblem) του Ντάβιντ Χίλμπερτ, που δείχθηκε ανεξάρτητα από τον Άλαν Τούρινγκ και τον Αλόνζο Τσερτς το 1936, έδειξε ότι δεν υπάρχει πρόγραμμα υπολογιστή που μπορεί να αποφασίσει σωστά αν κάποια αυθαίρετη μαθηματική πρόταση είναι αληθής.

* Η λογική ανεξαρτησία της υπόθεσης του συνεχούς (continuum hypothesis) της Ζερμέλο-Φράνκελ θεωρίας συνόλων (ZFC) έδειξε ότι μια στειχειώδεις απόδειξη ή ανταπόδειξη της υπόθεσης αυτής είναι αδύνατη. Το γεγονός ότι η υπόθεση του συνεχούς είναι συνεπής με τη ZFC (αν η ZFC είναι συνεπής απο μόνη της) αποδείχθηκε από τον Κουρτ Γκέντελ το 1940. Το γεγονός ότι η άρνηση της υπόθεσης του συνεχούς είναι συνεπής με τη ZFC (αν η ZFC είναι συνεπής) αποδείχθηκε από τον Πωλ Κοέν το 1963.

* Η μη ύπαρξη αλγοριθμικής λύσης για το δέκατο πρόβλημα του Χίλμπερτ, που δείχθηκε από τον Γιούρι Ματιγιάσεβιτς το 1970, έδειξε ότι δεν είναι δυνατό για οποιοδήποτε πρόγραμμα υπολογιστή να αποφασίσει σωστά αν πολυπαραμετρικά (multivariate) πολυώνυμα με ακέραιους συντελεστές έχουν ακέραιες λύσεις.

Αναφορές

* Andrews, Peter B., 2002. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd ed. Kluwer Academic Publishers.

* Barwise, Jon, ed. (1977) Handbook of Mathematical Logic, Amsterdam: North-Holland. ISBN 0-444-86388-5

* George Boolos, John Burgess, and Richard Jeffrey (2002) Computability and Logic, 4th ed. Cambridge University Press. ISBN 0-521-00758-5.

* Enderton, Herbert (2002) A mathematical introduction to logic, 2nd ed. Academic Press.

* Hamilton, A. G. (1988) Logic for Mathematicians Cambridge University Press.

* Wilfrid Hodges, 1997. A Shorter Model Theory. Cambridge University Press.

* Mendelson, Elliott (1997) Introduction to Mathematical Logic, 4th ed. Chapman & Hall. ISBN 0412808307

* A. S. Troelstra & H. Schwichtenberg (2000) Basic Proof Theory, 2nd. ed. (Cambridge Tracts in Theoretical Computer Science). Cambridge University Press. ISBN 0-521-77911-1.

* John L. Bell & Alan B. Slomson (1969) Models and Ultraproducts: An Introduction, North-Holland (re-printed in 2006 by Dover publications). ISBN 0-486-44979-3.

Εξωτερικοί σύνδεσμοι

Μαθηματικά

Από τη ελληνική Βικιπαίδεια http://el.wikipedia.org . Όλα τα κείμενα είναι διαθέσιμα υπό την GNU Free Documentation License