Θεωρήματα μη-πληρότητας του Γκέντελ
Από τη Βικιπαίδεια, την ελεύθερη εγκυκλοπαίδεια
 |
Αυτό το άρθρο χρειάζεται μετάφραση. Αν θέλετε να συμμετάσχετε, μπορείτε να επεξεργαστείτε το άρθρο μεταφράζοντάς το ή προσθέτοντας δικό σας υλικό και να αφαιρέσετε το {{μετάφραση}} μόλις το ολοκληρώσετε. Είναι πιθανό (και επιθυμητό) το ξενόγλωσσο κείμενο να έχει κρυφτεί σαν σχόλιο με τα <!-- και -->. Πατήστε "επεξεργασία" για να δείτε ολόκληρο το κείμενο. |
Στη μαθηματική λογική, τα θεωρήματα μη-πληρότητας του Γκέντελ, τα οποία αποδείχτηκαν από τον Κουρτ Γκέντελ (Kurt Gödel) το 1931, είναι δύο θεωρήματα που δηλώνουν έμφυτους περιορισμούς στα πιο τετριμμένα μαθηματικού ενδιαφέροντος τυπικά συστήματα για την αριθμητική. Τα θεωρήματα είναι σημαντικής σπουδαιότητας στην φιλοσοφία των μαθηματικών. Θεωρούνται ευρέως ότι έδειξαν πως το πρόγραμμα του Χίλμπερτ να βρεθεί ένα πλήρες και συνεπές σύνολο από αξιώματα για όλα τα μαθηματικά είναι αδύνατο, δίνοντας έτσι αρνητική απάντηση στο δεύτερο πρόβλημα του Χίλμπερτ.
Πίνακας περιεχομένων |
[Επεξεργασία] Υπόβαθρο
Στη μαθηματική λογική, μια θεωρία είναι ένα σύνολο από προτάσεις εκπεφρασμένες σε μια τυπική γλώσσα. Μερικές δηλώσεις σε μια θεωρία συμπεριλαμβάνονται χωρίς απόδειξη (αξιώματα) και άλλες (θεωρήματα) συμπεριλαμβάνονται επειδή συνάγονται από τα αξιώματα.
Επειδή οι δηλώσεις μιας τυπικής θεωρίας γράφονται σε συμβολική μορφή, είναι δυνατόν να επαληθεύσουμε μηχανικά ότι μία τυπική απόδειξη από ένα πεπερασμένο σύνολο από αξιώματα είναι έγκυρη. Αυτή η δουλειά, γνωστή ως αυτοματοποιημένη επαλήθευση αποδείξεων, σχετίζεται στενά με την αυτοματοποιημένη απόδειξη θεωρημάτων. Η διαφορά είναι ότι αντί να κατασκευάσει μια νέα απόδειξη, ο επαληθευτής αποδείξεων απλά ελέγχει αν μια δεδομένη τυπική απόδειξη (ή, σε μερικές περιπτώσεις, οι οδηγίες που μπορούν να ακολουθήσει κανείς για να δημιουργήσει μια τυπική απόδειξη) είναι σωστή. Αυτό δεν είναι απλά και μόνο υποθετικό. Συστήματα όπως η Ισαβέλλα χρησιμοποιούνται σήμερα για να τυπικοποιούν αποδείξεις και μετά να ελέγχουν την εγκυρότητά τους.
Παρόλα αυτά, πολλές θεωρίες ενδιαφέροντος συμπεριλαμβάνουν ένα άπειρο σύνολο από αξιώματα. Για να επαληθευτεί μια τυπική απόδειξη όταν το σύνολο των αξιωμάτων είναι άπειρο, πρέπει να είναι δυνατόν να προσδιορίσουμε αν μία δήλωση η οποία θεωρείται ότι είναι αξίωμα είναι πράγματι αξίωμα. Αυτό το ζήτημα προκύπτει στις πρώτου βαθμού θεωρίες της αριθμητικής, όπως η αριθμητική του Πεάνο, επειδή η αρχή της μαθηματικής επαγωγής εκφράζεται ως ένα άπειρο σύνολο αξιωμάτων (ένα αξιωματικό σχήμα).
Μια τυπική θεωρία λέγεται πως είναι αποτελεσματικά παραχθείσα αν το σύνολο των αξιωμάτων της είναι ένα αναδρομικά απαριθμήσιμο σύνολο. Αυτό σημαίνει ότι υπάρχει ένα πρόγραμμα υπολογιστή που, κατ` αρχήν, θα μπορούσε να απαριθμήσει όλα τα αξιώματα της θεωρίας χωρίς να συμπεριλάβει στη λίστα καμία δήλωση που δεν είναι αξίωμα. Αυτό είναι ισοδύναμο με την ικανότητα να απαριθμήσει όλα τα θεωρήματα της θεωρίας χωρίς να απαριθμήσει καμία δήλωση που δεν είναι θεώρημα. Για παράδειγμα, κάθε μια από τις θεωρίες της αριθμητικής του Πεάνο και της θεωρίας συνόλων των Τσερμέλο-Φρένκελ έχει έναν άπειρο αριθμό αξιωμάτων και κάθε μια είναι αποτελεσματικά παραχθείσα.
Διαλέγοντας ένα σύνολο από αξιώματα, ένα στόχος είναι να μπορεί να αποδείξει όσο το δυνατόν περισσότερα σωστα αποτελέσματα, χωρίς να αποδείξει κανένα λανθασμένο αποτέλεσμα. Ένα σύνολο αξιωμάτων είναι πλήρες αν, για κάθε δήλωση στη γλώσσα των αξιωμάτων, είτε η αυτή δήλωση είτε η άρνησή της μπορεί να αποδειχτεί από τα αξιώματα. Ένα σύνολο αξιωμάτων είναι (απλά) συνεπές αν δεν υπάρχει δήλωση τέτοια ώστε και αυτή και η άρνηση της να μπορούν να αποδειχτούν από τα αξιώματα. Στο πρότυπο σύστημα της λογικής πρώτου βαθμού ένα ασυνεπές σύνολο αξιωμάτων θα αποδείξει κάθε δήλωση στη γλώσσα της (αυτό μερικές φορές καλείται η αρχή της έκρηξης) και είναι έτσι αυτόματα πλήρες. Ένα σύνολο από αξιώματα που είναι και πλήρες και συνεπές, παρόλα αυτά, αποδεικνύει ένα μέγιστο σύνολο από μη-αντιφατικά θεωρήματα. Τα θεωρήματα μη-πληρότητας του Γκέντελ δείχνουν ότι σε συγκεκριμένες περιπτώσεις δεν είναι δυνατόν να εξασφαλίσουμε μια αποτελεσματικά παραχθείσα, πλήρη, συνεπή θεωρία.
[Επεξεργασία] Πρώτο θεώρημα μη-πληρότητας
Το πρώτο θεώρημα μη-πληρότητας του Γκέντελ δηλώνει ότι:
- Καμία αποτελεσματικά παραχθείσα θεωρία ικανή να εκφράσει στοιχειώδη αριθμητική δεν μπορεί να είναι και συνεπής και πλήρης. Συγκεκριμένα, για κάθε συνεπή, αποτελεσματικά παραχθείσα τυπική θεωρία που αποδεικνύει συγκεκριμένες αλήθειες βασικής αριθμητικής, υπάρχει μία αριθμητική δήλωση η οποία είναι αληθής,[1] αλλά δεν μπορεί να αποδειχθεί από τη θεωρία (Kleene 1967, p. 250). -->
Η αληθής δήλωση που δεν μπορεί να αποδειχθεί στην οποία αναφέρεται το θεώρημα συχνά αναφέρεται ως “η πρόταση Γκέντελ” για τη θεωρία. Δεν είναι μοναδική. υπάρχουν άπειρες τέτοιες δηλώσεις στη γλώσσα της θεωρίας οι οποίες μοιράζονται την ιδιότητα του ότι είναι αληθείς και δεν μπορούν να αποδειχθούν.
Για κάθε συνεπή τυπική θεωρία Θ που έχει την απαιτούμενη ποσότητα την θεωρίας αριθμών, η αντίστοιχη πρόταση Γκέντελ G ισχυρίζεται: “Η G δεν μπορεί να αποδειχθεί ότι είναι αληθής μέσα στη θεωρία Θ”. Αν η G μπορούσε να αποδειχθεί μέσω των αξιωμάτων και των κανόνων συμπερασμού της Θ, τότε η Θ θα είχε ένα θεώρημα, το G, το οποίο αντίκειται στον εαυτό του, και έτσι η θεωρία Θ θα ήταν ασυνεπής. Αυτό σημαίνει ότι αν η θεωρία Θ είναι συνεπής τότε η G δεν μπορεί να αποδειχθεί μέσα σ` αυτή. Αυτό σημαίνει ότι η αξίωση της G για την δική της αδυναμία αποδείξεως είναι σωστή. Υπό αυτήν την έννοια η G όχι μόνο δεν μπορεί να αποδειχθεί αλλά είναι και αληθής. Έτσι η δυνατότητα απόδειξης μέσα στη θεωρία Θ δεν είναι ίδια με την αλήθεια. Η θεωρία Θ δεν είναι πλήρης (είναι μη-πλήρης).
Αν η G είναι αληθής τότε η G δεν μπορεί να αποδειχθεί μέσα στη θεωρία, και η θεωρία είναι μη-πλήρης. Αν η G είναι ψευδής τότε η G μπορεί να αποδειχθεί μέσα στη θεωρία, και η θεωρία είναι ασυνεπής μιας και η G και αποδεικνύεται και αντικρούεται από την Θ.
Είναι δυνατόν να ορίσουμε μια μεγαλύτερη θεωρία Θ’ που να περιέχει όλη την Θ, συν την G ως πρόσθετο αξίωμα. Σε αυτήν την περίπτωση, η G είναι πράγματι θεώρημα στην Θ’ (τετριμμένα, μιας και είναι αξίωμα). Παρόλα αυτά, αυτό το θεώρημα μη-πληρότητας τότε εφαρμόζεται στην Θ’. Θα υπάρχει μια νέα πρόταση Γκέντελ G’ για την Θ’, που θα δείχνει ότι η Θ’ είναι επίσης μη-πλήρης. Κάθε θεωρία έχει τη δική της πρόταση Γκέντελ.
Για να αποδείξει το πρώτο θεώρημα μη-πληρότητας, ο Γκέντελ αντιπροσώπησε τις δηλώσεις με αριθμούς. Τότε η εκάστοτε θεωρία, η οποία θεωρείται πως αποδεικνύει συγκεκριμένα γεγονότα για τους αριθμούς, αποδεικνύει επίσης και γεγονότα για τις ίδιες της τις δηλώσεις. Οι ερωτήσεις για την δυνατότητα αποδείξεως των δηλώσεων αντιπροσωπεύονται ως ερωτήσεις για τις ιδιότητες των αριθμών, για τις οποίες θα μπορούσε να αποφασίσει η θεωρία αν ήταν πλήρης. Από αυτήν την άποψη, η πρόταση Γκέντελ δηλώνει ότι δεν υπάρχει φυσικός αριθμός που να έχει μια συγκεκριμένη, παράξενη ιδιότητα. Ένας αριθμός με αυτή την ιδιότητα θα κωδικοποιούσε μια απόδειξη της ασυνέπειας της θεωρίας. Αν υπήρχε ένα τέτοιος αριθμός τότε η θεωρία θα ήταν ασυνεπής, αντίθετα με την υπόθεση ότι είναι συνεπής. Οπότε, υπό την υπόθεση ότι η θεωρία είναι συνεπής, δεν υπάρχει τέτοιος αριθμός.
[Επεξεργασία] Δεύτερο θεώρημα μη-πληρότητας
Το δεύτερο θεώρημα μη-πληρότητας Γκέντελ μπορεί να διατυπωθεί ως εξής:
- Για κάθε τυπική αποτελεσματικά παραχθείσα θεωρία Θ που συμπεριλαμβάνει βασικές αριθμητικές αλήθειες και επίσης συγκεκριμένες αλήθειες για την δυνατότητα τυπικής απόδειξης, η Θ συμπεριλαμβάνει μία δήλωση της ιδίας συνέπειας αν και μόνο αν η Θ είναι ασυνεπής.
Αυτό ενισχύει το πρώτο θεώρημα μη-πληρότητας, επειδή η δήλωση που κατασκευάσαμε στο πρώτο θεώρημα μη-πληρότητας δεν εκφράζει ευθέως την συνέπεια της θεωρίας. Η απόδειξη του δεύτερου θεωρήματος μη-πληρότητας λαμβάνεται, ουσιαστικά, τυπικοποιόντας την απόδειξη του πρώτου θεωρήματος μη-πληρότητας μέσα στην ίδια την θεωρία.
Μια τεχνική λεπτομέρεια στο δεύτερο θεώρημα μη-πληρότητας είναι πως να εκφράσουμε την συνέπεια της Θ ως φόρμουλα στην γλώσσα της Θ. Υπάρχουν πολλοί τρόποι να το κάνουμε, και δεν οδηγούν όλοι στο ίδιο αποτέλεσμα. Συγκεκριμένα, διαφορετικές τυπικοποιήσεις της αξίωσης ότι η Θ είναι συνεπής μπορεί να είναι μην είναι ισοδύναμες στην Θ, και μερικές μπορεί ακόμα και να μπορούν να αποδειχθούν. Για παράδειγμα, η πρώτου βαθμού αριθμητική του Πεάνο (PA: Peano arithmetic) μπορεί να αποδείξει ότι το μεγαλύτερο συνεπές υποσύνολο της PA είναι συνεπές. Αλλά μιας και η PA είναι συνεπής, το μεγαλύτερο συνεπές υποσύνολο της PA είναι απλά η PA, οπότε υπό αυτή την έννοια η PA "αποδεικνύει ότι είναι συνεπής". Αυτό που η PA δεν αποδεικνύει είναι πως το μεγαλύτερο συνεπές υποσύνολο της PA είναι, στην πραγματικότητα, ολόκληρη η PA. (Ο όρος "μεγαλύτερο συνεπές υποσύνολο της PA" είναι μάλλον ασαφής, αλλά αυτό που εννοούμε εδώ είναι το μεγαλύτερο συνεπές αρχικό κομμάτι των αξιωμάτων της PA ταξινομημένο σύμφωνα με κάποια κριτήρια. Για παράδειγμα, με τους "αριθμούς Γκέντελ", τους αριθμούς που κωδικοποιούν τα αξιώματα όπως στο σχήμα που χρησιμοποίησε ο Γκέντελ που αναφέρθηκε παραπάνω).
[Επεξεργασία] Περιορισμοί των θεωρημάτων του Γκέντελ
Τα συμπεράσματα των θεωρημάτων του Γκέντελ ισχύουν μόνο για τις τυπικές θεωρίες που ικανοποιούν τις απαραίτητες υποθέσεις. Δεν ικανοποιούν όλα τα αξιωματικά συστήματα αυτές τις υποθέσεις, ακομά και όταν αυτά τα συστήματα έχουν μοντέλα που συμπεριλαμβάνουν τους φυσικούς αριθμούς ως υποσύνολο. Για παράδειγμα, υπάρχουν πρώτου βαθμού αξιωματικοποιήσεις της Ευκλείδειας γεωμετρίας και των πραγματικών κλειστών πεδίων που δεν ικανοποιούν τις υποθέσεις των θεωρημάτων του Γκέντελ. Το γεγονός κλειδί είναι ότι αυτές οι αξιωματικοποιήσεις δεν είναι αρκετά εκφραστικές ώστε να ορίσουν το σύνολο των φυσικών αριθμών ή να αναπτύξει βασικές ιδιότητες των φυσικών αριθμών.
[Επεξεργασία] Σχέση με την υπολογισιμότητα
Το θεώρημα μη-πληρότητας είναι έχει στενή συγγένεια με αρκετά αποτελέσματα σχετικά με τα μη-αποφασιστέα σύνολα στη θεωρία αναδρομής.
Ο Στήβεν Κόουλ Κλιν (Stephen Cole Kleene) (1943) παρουσίασε μία απόδειξη του θεωρήματος μη-πληρότητας του Γκέντελ χρησιμοποιώντας βασικά αποτελέσματα της θεωρίας υπολογισμού. Ένα τέτοιο αποτέλεσμα δείχνει ότι το πρόβλημα τερματισμού δεν έχει λύση: δεν υπάρχει πρόγραμμα υπολογιστή που να μπορεί να μπορεί να αποφασίσει σωστά, δοθέντος ενός προγράμματος Π ως είσοδο, αν το Π τελικά σταματά όταν τρέξει χωρίς είσοδο. Ο Κλιν έδειξε ότι η ύπαρξη μιας πλήρους αποτελεσματικής θεωρίας της αριθμιτικής με συγκεκριμένες ιδιότητες συνέπειας θα εξανάγκαζε το halting problem να είναι αποφασιστέο, μια αντίφαση.
[Επεξεργασία] Σημειώσεις
- ↑ Η λέξη "αληθής" χρησιμοποιείται ντισκουοτενσιονιστικά εδώ: η πρόταση Γκέντελ είναι αληθής υπό αυτήν την έννοια επειδή "ισχυρίζεται ότι δεν μπορεί να αποδειχθεί και όντως δεν μπορεί" (Smoryński 1977 p. 825. Δείτε επίσης: Franzén 2005 pp. 28–33).
Το άρθρο βασίστηκε αρχικά στο άρθρο Gödel's incompleteness theorems της Αγγλόγλωσσης Βικιπαίδειας, η οποία διανέμεται υπό την GNU FDL και την CC-BY-SA 3.0. (ιστορικό/συντάκτες).
