Μαθηματική λογική

Ιστορία

Μαθηματική λογική ονομάστηκε από τον Τζουζέπε Πεάνο αυτό που αργότερα ονομάστηκε συμβολική λογική. Στην κλασσική της έκδοση, οι βασικές αρχές θυμίζουν τη λογική του Αριστοτέλη, γραμμένες όμως με συμβολικό τρόπο αντί για φυσική γλώσσα. Ορισμένοι από τους πιο φιλοσοφικούς μαθηματικούς έκαναν προσπάθειες να χειριστούν τις πράξεις της τυπικής λογικής με συμβολικό ή αλγεβρικό τρόπο, όπως ο Λάιμπνιτς και ο Λάμπερτ, αλλά οι προσπάθειές τους έμειναν άγνωστες και απομονωμένες. Ήταν ο Τζορτζ Μπουλ και ο Αύγουστος Ντε Μόργκαν, στο μέσο του 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 logic), αλλά και μη κλασσικές λογικές όπως, η διαισθητική λογική (intuitionistic logic).

Αλγοριθμικά μη επιλύσιμα προβλήματα

Ένα σημαντικό υποπεδίο της θεωρίας αναδρομής μελετά την αλγοριθμική μη επιλυσιμότητα.  Ένα πρόβλημα απόφασης είναι αλγοριθμικά άλυτο αν δεν υπάρχει υπολογίσιμη συνάρτηση η οποία, για οποιαδήποτε έκφανση του προβλήματος, επιστρέφει τη σωστή απόφαση.  Τα αρχικά αποτελέσματα για την μη επίλυση, ανεπτυγμένα ανεξάρτητα από τους Τσερτς και Τούρινγκ το 1936, έδειξαν ότι το γενικό πρόβλημα απόφασης (Entscheidungsproblem) είναι μη επιλύσιμο αλγοριθμικά. Ο Τούρινγκ το απέδειξε δείχνοντας τη μη επιλυσιμότητα του προβλήματος τερματισμού, αποτέλεσμα που είχε τεράστιες επιπτώσεις τόσο στη θεωρία αναδρομής όσο και στην επιστήμη υπολογιστών
Υπάρχουν πολλά γνωστά παραδείγματα μη αποφασίσιμων προβλημάτων από τα συνήθη μαθηματικά.  Το πρόβλημα λέξης για ομάδες αποδείχθηκε μη επιλύσιμο αλγοριθμικά από τον Νόβικοβ το 1955 και ανεξάρτητα από τον Μπουν το 1959.  Το πρόβλημα του εργατικού κάστορα, διατυπωμένο από τον Ραντό το 1962, είναι άλλο ένα γνωστό παράδειγμα.
Το δέκατο πρόβλημα του Χίλμπερτ ζητούσε έναν αλγόριθμο που αποφασίζει αν μια πολυμεταβλητή πολυωνυμική εξίσωση με ακέραιους συντελεστές έχει ακέραια λύση.  Περιορισμένη πρόοδος σ' αυτό επιτεύχθηκε από την Τζούλια Ρόμπινσον, τον Μάρτιν Ντέιβις και την Χίλαρι Πούτναμ.  Η αλγοριθμική μη επιλυσιμότητα του προβλήματος αποδείχθηκε τελικά από τον Γιούρι Ματιγιασέβιτς το 1970.

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

Υπάρχει μεγάλη σχέση μεταξύ της μαθηματικής λογικής και της επιστήμης υπολογιστών. Αρχικοί πρωτοπόροι της επιστήμης υπολογιστών, όπως ο Άλαν Τούρινγκ, ήταν επίσης μαθηματικοί και λογικοί.
Η μελέτη της θεωρίας υπολογισιμότητας στην επιστήμη υπολογιστών σχετίζεται στενά με τη μελέτη της υπολογισιμότητας στη μαθηματική λογική. Διαφέρουν όμως ως προς την έμφαση.  Οι επιστήμονες υπολογιστών συχνά εστιάζουν σε πραγματικές γλώσσες προγραμματισμού και την εφικτή υπολογισιμότητα (feasible computability), ενώ οι ερευνητές στη μαθηματική λογική συχνά εστιάζουν στην υπολογισιμότητα ως θεωρητική έννοια, και στη μη-υπολογισιμότητα.
Η μελέτη της σημασιολογίας (semantics) γλωσσών προγραμματισμού σχετίζεται με την τροπική λογική (modal logic), όπως και την τυπική επαλήθευση (formal verification) και πιο συγκεκριμένα τον έλεγχο μοντέλων (model checking). Ο ισομορφισμός Κάρρυ-Χάουαρντ μεταξύ αποδείξεων και προγραμμάτων σχετίζεται με τη θεωρία αποδείξεων. Η ενορατική λογική και η γραμμική λογική είναι σημαντικές σ' αυτό.  Λογισμοί όπως ο λάμδα λογισμός και η συνδυαστική λογική (combinatory logic) μελετώνται τελευταία ως ιδεατές γλώσσες προγραμματισμού.
Η επιστήμη υπολογιστών συμβάλλει ακόμα στα μαθηματικά με την ανάπτυξη τεχνικών για τον αυτόματο έλεγχο ή και εύρεση αποδείξεων, όπως η αυτοματοποιημένη απόδειξη θεωρημάτων (automated theorem proving) και ο λογικός προγραμματισμός.