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

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

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

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

Ιστορία

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

Λογική πρώτου βαθμού

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

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

Το θεώρημα πληρότητας του Γκέντελ (Gödel 1929) θέσπισε την ισοδυναμία μεταξύ σημασιολογικών και συντακτικών ορισμών της λογικής συνέπειας στην πρωτοβάθμια λογική. Δείχνει ότι αν μια συγκεκριμένη πρόταση είναι αληθής σε κάθε μοντέλο που ικανοποιεί ένα συγκεκριμένο σύνολο αξιωμάτων, τότε θα πρέπει να υπάρχει πεπερασμένος συλλογισμός που συμπεραίνει την πρόταση από τα αξιώματα. Το θεώρημα συμπαγείας (compactness theorem) πρώτα εμφανίστηκε ως λήμμα στην απόδειξη του θεωρήματος πληρότητας του Γκέντελ, και χρειάστηκαν αρκετά χρόνια μέχρι να κατανοηθεί η σημασία του και να φτάσει να εφαρμόζεται τακτικά. Αναφέρει ότι ένα σύνολο προτάσεων έχει μοντέλο αν και μόνο αν κάθε πεπερασμένο υποσύνολο έχει μοντέλο, ή με άλλα λόγια ότι ένα ασυνεπές σύνολο από προτάσεις θα πρέπει να έχει κάποιο πεπερασμένο ασυνεπές υποσύνολο. Τα θεωρήματα πληρότητας και συμπαγείας επιτρέπουν εξελιγμένη ανάλυση της λογικής συνέπειας στην πρωτοβάθμια λογική, και την ανάπτυξη της θεωρίας μοντέλων, και αποτελούν βασικό λόγο για την διάδοση της λογικής πρώτου βαθμού στα μαθηματικά.

Τα θεωρήματα μη-πληρότητας του Γκέντελ (Gödel 1931) θεσπίζουν περεταίρω όρια στις πρωτοβάθμιες αξιωματικοποιήσεις. Το πρώτο θεώρημα μη πληρότητας αναφέρει ότι κανένα επαρκώς ισχυρό, αποτελεσματικό λογικό σύστημα δεν μπορεί να αποδείξει την συνέπεια του εαυτού του, παρά μόνο αν δεν είναι στην πραγματικότητα συνεπές. Λέγοντας αποτελεσματικό εννοούμε ότι είναι δυνατό να αποφασιστεί, δεδομένης μιας πρότασης στη γλώσσα του συστήματος, αν αυτή η πρόταση είναι αξίωμα. Όταν εφαρμόζεται στην πρωτοβάθμια λογική, το πρώτο θεώρημα μη πληρότητας συνεπάγεται ότι κάθε πρωτοβάθμια θεωρία που είναι αρκετά ισχυρή, συνεπής, και αποτελεσματική έχει μοντέλα που δεν είναι στοιχειωδώς ισοδύναμα. Αυτό είναι ισχυρότερος περιορισμός από αυτόν που τίθεται λόγω του θεωρήματος Λέβενχάιμ-Σκόλεμ. Το δεύτερο θεώρημα μη-πληρότητας εκφράζει ότι κανένα επαρκώς ισχυρό, συνεπές, αποτελεσματικό αξιωματικό σύστημα για την αριθμητική δεν μπορεί να αποδείξει την συνέπεια του εαυτού του, πράγμα που σημαίνει ότι το πρόγραμμα του Χίλμπερτ δεν γίνεται να υλοποιηθεί.

Θεωρία συνόλων

Η Θεωρία συνόλων είναι η μελέτη των συνόλων, τα οποία είναι αφηρημένες συλλογές από αντικείμενα. Πολλές από τις βασικές έννοιες της θεωρίας συνόλων όπως οι τακτικοί και οι πληθικοί αριθμοί, αναπτύχθηκαν άτυπα από τον Καντόρ πριν αναπτυχθούν τυπικές αξιωματικοποιήσεις της θεωρίας συνόλων. Η πρώτη τέτοια αξιωματικοποίηση, από τον Ζερμέλο (1908), επεκτάθηκε ελαφρώς για να γίνει η θεωρία συνόλων Ζερμέλο-Φράνκελ (ZF), η οποία είναι η πιο διαδεδομένη θεμελιώδης θεωρία για τα μαθηματικά.

Έχουν προταθεί και άλλες τυποποιήσεις της θεωρίας συνόλων, όπως η θεωρία συνόλων φον Νόιμαν-Μπερνάις-Γκέντελ (NBG), η θεωρία συνόλων Μόρς-Κέλλυ (MK) και τα νέα θεμέλια (NF). Από αυτές, οι ZF, NBG και MK είναι παρόμοιες στην περιγραφή μιας συσσωρευτικής ιεραρχίας συνόλων. Τα νέα θεμέλια έχουν διαφορετική προσέγγιση, επιτρέπουν να διατυπωθούν σύνολα όπως το σύνολο όλων των συνόλων, αλλά με αντίτιμο τον περιορισμό στα αξιώματα ύπαρξής τους. Το σύστημα θεωρία συνόλων Κρίπκε-Πλάτεκ είναι στενά σχετιζόμενο με την γενική θεωρία αναδρομής.

Δύο διάσημες προτάσεις στη θεωρία συνόλων είναι το αξίωμα της επιλογής και η υπόθεση του συνεχούς. Το αξίωμα επιλογής, αρχικά διατυπωμένο από τον Ζερμέλο (1904), αποδείχθηκε ανεξάρτητο της θεωρίας ZF από τον Φράνκελ (1922), αλλά είναι πλέον ευρέως αποδεκτό από τους μαθηματικούς. Διατυπώνει ότι δεδομένης μιας συλλογής από μη κενά σύνολα, υπάρχει ένα μοναδικό σύνολο C που περιέχει ακριβώς ένα στοιχείο από κάθε σύνολο στη συλλογή. Το σύνολο C λέγεται ότι «επιλέγει» ένα στοιχείο από κάθε σύνολο στη συλλογή. Αν και η δυνατότητα να γίνει μια τέτοια επιλογή φαίνεται προφανής σε κάποιους, αφού κάθε σύνολο στη συλλογή είναι μη-κενό, η έλλειψη ενός γενικού, συγκεκριμένου κανόνα με βάση τον οποίο γίνεται η επιλογή κάνει το αξίωμα μη κατασκευαστικό. Οι Στέφαν Μπανάχ και Άλφρεντ Τάρσκι (1924) έδειξαν ότι το αξίωμα της επιλογής μπορεί να χρησιμοποιηθεί για να αποσυνθέσει μια στερεή σφαίρα σε πεπερασμένο αριθμό κομματιών, τα οποία μπορούν στη συνέχεια να επαναδιαταχθούν, χωρίς αλλαγή στο μέγεθος, για να σχηματίσουν δύο στερεές σφαίρες του αρχικού μεγέθους. Το θεώρημα αυτό, γνωστό και ως παράδοξο Μπανάχ-Τάρσκι είναι ένα από αρκετά αντιδιαισθητικά αποτελέσματα του αξιώματος επιλογής.

Η υπόθεση του συνεχούς, που αρχικά προτάθηκε ως εικασία από τον Καντόρ, τέθηκε από τον Χίλμπερτ ως ένα από τα 23 του προβλήματα το 1900. Ο Γκέντελ έδειξε ότι η υπόθεση του συνεχούς δεν μπορεί να διαψευσθεί από τα αξιώματα της θεωρίας ZF (με ή χωρίς το αξίωμα επιλογής), αναπτύσσοντας το κατασκευάσιμο σύμπαν της θεωρίας συνόλων, στο οποίο η υπόθεση του συνεχούς πρέπει να ισχύει. Το 1963, ο Πωλ Κοέν έδειξε ότι η υπόθεση του συνεχούς δε μπορεί να αποδειχθεί από τα αξιώματα της θεωρίας συνόλων Ζερμέλο-Φράνκελ (Cohen 1966). Αυτό το αποτέλεσμα ανεξαρτησίας δεν έλυσε τελείως την ερώτηση του Χίλμπερτ, αφού θα μπορούσε νέα αξιώματα για τη θεωρία συνόλων να επιλύσουν την υπόθεση. Πρόσφατη εργασία στο αντικείμενο γίνεται πό τον Χιού Γούντιν, αν και η σημασία της δεν είναι ακόμα ξεκάθαρη (Woodin 2001).

Η σύγχρονη έρευνα στη συνολοθεωρία περιλαμβάνει τη μελέτη των μεγάλων πληθικών και προσδιορισμών. Οι μεγάλοι πληθικοί είναι πληθικοί αριθμοί με συγκεκριμένες ιδιότητες τόσο ισχυρές ώστε η ύπαρξή τους δεν αποδεικνύεται στην ZFC. Η ύπαρξη του μικρότερου δυνατού μεγάλου πληθικού που μελετάται συνήθως, ενός απροσπέλαστου πληθικού, ήδη συνεπάγεται την συνέπεια της ZFC. Παρ'όλο το ότι οι μεγάλοι πληθικοί έχουν υπερβολικά υψηλή πληθικότητα, η ύπαρξή τους έχει πολλές δυσχερείς συνέπειες για τη δομή της γραμμής των πραγματικών. Ο προσδιορισμός (determinacy) αναφέρεται στην πιθανή ύπαρξη επιτυχών στρατηγικών σε συγκεκριμένα παίγνια δύο παικτών (τα παίγνια τότε λέγονται προσδιορισμένα). Η ύπαρξη των στρατηγικών αυτών επηρεάζει δομικές ιδιότητες της γραμμής των πραγματικών και άλλων Πολωνικών χώρων.

Θεωρία μοντέλων

Η Θεωρία μοντέλων μελετά τα μοντέλα διάφορων τυπικών θεωριών. Εδώ θεωρία λέγεται το σύνολο από προτάσεις σε κάποια δεδομένη τυπική λογική και οπλισμό (signature), ενώ ένα μοντέλο είναι μια δομή που δίνει μια συγκεκριμένη ερμηνεία της θεωρίας. Η θεωρία μοντέλων είναι στενά συνδεδεμένη με την καθολική άλγεβρα, και αλγεβρική γεωμετρία, αν και οι μέθοδοι της θεωρίας μοντέλων εστιάζουν περισσότερο σε λογικές ανησυχίες από αυτά τα πεδία.

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

Η μέθοδος απάλειψης ποσοδεικτών μπορεί να χρησιμοποιηθεί για να δείξει ότι ορίσιμα σύνολα σε συγκεκριμένες θεωρίες δεν μπορεί να είναι πολύ περίπλοκα. Ο Τάρσκι (1948) θέσπισε την απαλοιφή ποσοδεικτών για real-closed πεδία, αποτέλεσμα που επίσης δείχνει ότι η θεωρία πεδίων των πραγματικών αριθμών είναι αποκρίσιμο. (Παρατήρησε ακόμα ότι οι μέθοδοί του είναι εξίσου εφαρμόσιμες σε αλγεβρικά κλειστά πεδία με οποιουδήποτε χαρακτηριστικού.) Ένα υποπεδίο που αναπτύχθηκε από αυτό, ασχολείται με ο-ελάχιστες δομές.

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

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

Θεωρία αναδρομής

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

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

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

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

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

Ένα σημαντικό υποπεδίο της θεωρίας αναδρομής μελετά την αλγοριθμική μη επιλυσιμότητα. Ένα πρόβλημα απόφασης είναι αλγοριθμικά άλυτο αν δεν υπάρχει υπολογίσιμη συνάρτηση η οποία, για οποιαδήποτε έκφανση του προβλήματος, επιστρέφει τη σωστή απόφαση. Τα αρχικά αποτελέσματα για την μη επίλυση, ανεπτυγμένα ανεξάρτητα από τους Τσερτς και Τούρινγκ το 1936, έδειξαν ότι το γενικό πρόβλημα απόφασης (Entscheidungsproblem) είναι μη επιλύσιμο αλγοριθμικά. Ο Τούρινγκ το απέδειξε δείχνοντας τη μη επιλυσιμότητα του προβλήματος τερματισμού, αποτέλεσμα που είχε τεράστιες επιπτώσεις τόσο στη θεωρία αναδρομής όσο και στην επιστήμη υπολογιστών

Υπάρχουν πολλά γνωστά παραδείγματα μη αποφασίσιμων προβλημάτων από τα συνήθη μαθηματικά. Το πρόβλημα λέξης για ομάδες αποδείχθηκε μη επιλύσιμο αλγοριθμικά από τον Νόβικοβ το 1955 και ανεξάρτητα από τον Μπουν το 1959. Το πρόβλημα του εργατικού κάστορα, διατυπωμένο από τον Ραντό το 1962, είναι άλλο ένα γνωστό παράδειγμα.

Το δέκατο πρόβλημα του Χίλμπερτ ζητούσε έναν αλγόριθμο που αποφασίζει αν μια πολυμεταβλητή πολυωνυμική εξίσωση με ακέραιους συντελεστές έχει ακέραια λύση. Περιορισμένη πρόοδος σ' αυτό επιτεύχθηκε από την Τζούλια Ρόμπινσον, τον Μάρτιν Ντέιβις και την Χίλαρι Πούτναμ. Η αλγοριθμική μη επιλυσιμότητα του προβλήματος αποδείχθηκε τελικά από τον Γιούρι Ματιγιασέβιτς το 1970.

Θεωρία αποδείξεων και κατασκευαστικά μαθηματικά

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

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

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

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

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

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

Η μελέτη της σημασιολογίας (semantics) γλωσσών προγραμματισμού σχετίζεται με την τροπική λογική (modal logic), όπως και την τυπική επαλήθευση (formal 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, έδειξε ότι δεν είναι δυνατό για οποιοδήποτε πρόγραμμα υπολογιστή να αποφασίσει σωστά αν πολυώνυμα πολλών μεταβλητών με ακέραιους συντελεστές έχουν ακέραιες λύσεις.

Αναφορές

• 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 0-412-80830-7
• 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.

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

• Mathematical Logic around the world
• Polyvalued logic Αρχειοθετήθηκε 2009-06-05 στο Wayback Machine.
• forall x: an introduction to formal logic, by P.D. Magnus, is a free textbook.
• Detlovs, Vilnis, and Podnieks, Karlis (University of Latvia) Introduction to Mathematical Logic. A hyper-textbook.
• Stanford Encyclopedia of Philosophy: Classical Logic -- by Stewart Shapiro.
• Stanford Encyclopedia of Philosophy: First-order Model Theory -- by Wilfred Hodges.