Θεωρήματα μη πληρότητας του Γκέντελ

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

Υπόβαθρο

Στη μαθηματική λογική, μια θεωρία είναι ένα σύνολο από προτάσεις εκφρασμένες σε μια τυπική γλώσσα. Μερικές δηλώσεις σε μια θεωρία (τα αξιώματα) συμπεριλαμβάνονται χωρίς απόδειξη και άλλες (τα θεωρήματα) συμπεριλαμβάνονται επειδή συνάγονται από τα αξιώματα.
Επειδή οι δηλώσεις μιας τυπικής θεωρίας γράφονται σε συμβολική μορφή, είναι δυνατόν να επαληθευτεί μηχανικά ότι μία τυπική απόδειξη από ένα πεπερασμένο σύνολο από αξιώματα είναι έγκυρη. Αυτή η δουλειά, γνωστή ως αυτοματοποιημένη επαλήθευση αποδείξεων, σχετίζεται στενά με την αυτοματοποιημένη απόδειξη θεωρημάτων. Η διαφορά είναι ότι αντί να κατασκευάσει μια νέα απόδειξη, ο επαληθευτής αποδείξεων απλά ελέγχει αν μια δεδομένη τυπική απόδειξη (ή, σε μερικές περιπτώσεις, οι οδηγίες που μπορεί να ακολουθήσει κανείς για να δημιουργήσει μια τυπική απόδειξη) είναι σωστή. Αυτό δεν είναι απλά και μόνο υποθετικό. Συστήματα όπως το Isabelle χρησιμοποιούνται σήμερα για να τυποποιούν αποδείξεις και μετά να ελέγχουν την εγκυρότητά τους.
Παρ’ όλα αυτά, πολλές θεωρίες που μας ενδιαφέρουν περιλαμβάνουν ένα άπειρο σύνολο από αξιώματα. Για να επαληθευτεί μια τυπική απόδειξη όταν το σύνολο των αξιωμάτων είναι άπειρο, πρέπει να είναι δυνατόν να προσδιορίσουμε αν μία δήλωση η οποία θεωρείται ότι είναι αξίωμα είναι πράγματι αξίωμα. Αυτό το ζήτημα προκύπτει στις πρώτου βαθμού θεωρίες της αριθμητικής, όπως η αριθμητική του Πεάνο, επειδή η αρχή της μαθηματικής επαγωγής εκφράζεται ως ένα άπειρο σύνολο αξιωμάτων (ένα αξιωματικό σχήμα).
Μια τυπική θεωρία λέγεται πως είναι αποτελεσματικά παραχθείσα αν το σύνολο των αξιωμάτων της είναι ένα αναδρομικά απαριθμήσιμο σύνολο. Αυτό σημαίνει ότι υπάρχει ένα πρόγραμμα υπολογιστή που, κατ` αρχήν, θα μπορούσε να απαριθμήσει όλα τα αξιώματα της θεωρίας χωρίς να συμπεριλάβει στη λίστα καμία δήλωση που δεν είναι αξίωμα. Αυτό είναι ισοδύναμο με την ικανότητα να απαριθμήσει όλα τα θεωρήματα της θεωρίας χωρίς να απαριθμήσει καμία δήλωση που δεν είναι θεώρημα. Για παράδειγμα, η θεωρία της αριθμητικής του Πεάνο (η αξιωματική περιγραφή των φυσικών αριθμών) και η θεωρία συνόλων των Τσερμέλο-Φρένκελ έχουν άπειρο αριθμό αξιωμάτων η κάθε μια, και κάθε μια είναι αποτελεσματικά παραχθείσα.
Κατά την επιλογή ενός συνόλου από αξιώματα, ο στόχος είναι με βάση αυτά να μπορεί να αποδείξει κανείς όσο το δυνατόν περισσότερα σωστά αποτελέσματα, χωρίς να μπορεί να αποδείξει κανένα λανθασμένο αποτέλεσμα. Ένα σύνολο από αξιώματα είναι πλήρες αν, για κάθε δήλωση στη γλώσσα των αξιωμάτων, είτε η αυτή δήλωση είτε η άρνησή της μπορεί να αποδειχτεί από τα αξιώματα. Ένα σύνολο αξιωμάτων είναι (απλά) συνεπές αν δεν υπάρχει δήλωση τέτοια ώστε και αυτή και η άρνηση της να μπορούν να αποδειχτούν από τα αξιώματα. Στο πρότυπο σύστημα της λογικής πρώτου βαθμού ένα συνεπές σύνολο αξιωμάτων θα αποδείξει κάθε δήλωση στη γλώσσα της (αυτό μερικές φορές καλείται η αρχή της έκρηξης) και είναι επομένως αυτόματα πλήρες. Ένα σύνολο από αξιώματα που είναι και πλήρες και συνεπές, παρ'όλα αυτά, αποδεικνύει ένα μέγιστο σύνολο από μη-αντιφατικά θεωρήματα. Τα θεωρήματα μη πληρότητας του Γκέντελ δείχνουν ότι σε συγκεκριμένες περιπτώσεις δεν είναι δυνατόν να έχουμε μια αποτελεσματικά παραχθείσα, πλήρη και συνεπή θεωρία.

Περιορισμοί των θεωρημάτων του Γκέντελ

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

Σχέση με την υπολογισιμότητα

Το θεώρημα μη πληρότητας έχει στενή συγγένεια με αρκετά αποτελέσματα σχετικά με τα μη-αποφασίσιμα σύνολα στη θεωρία αναδρομής, η οποία αποτελεί κεντρικό πυλώνα της επιστήμης υπολογιστών.
Ο Στίβεν Κλέινι (Stephen Cole Kleene) (1943) παρουσίασε μία απόδειξη του θεωρήματος μη πληρότητας του Γκέντελ χρησιμοποιώντας βασικά αποτελέσματα της θεωρίας υπολογισμού. Ένα τέτοιο αποτέλεσμα δείχνει ότι το πρόβλημα τερματισμού δεν έχει λύση: δεν υπάρχει πρόγραμμα υπολογιστή που δοθέντος ενός προγράμματος Π ως είσοδο, να μπορεί να αποφασίσει σωστά αν το Π τελικά σταματά όταν τρέξει χωρίς είσοδο. Ο Κλιν έδειξε ότι η ύπαρξη μιας πλήρους, αποτελεσματικής θεωρίας της αριθμητικής με συγκεκριμένες ιδιότητες συνέπειας θα σήμαινε πως το πρόβλημα του τερματισμού είναι αποφασίσιμο (υπολογίσιμο), μια αντίφαση. Η μη-υπολογισιμότητα μπορεί επομένως να περιγραφεί ως συνέπεια της μη πληρότητας του Γκέντελ.