Θεωρήματα μη πληρότητας του Γκέντελ: Διαφορά μεταξύ των αναθεωρήσεων
Περιεχόμενο που διαγράφηκε Περιεχόμενο που προστέθηκε
μ απόκρυψη |
μδρθ |
||
Γραμμή 4:
Στη [[μαθηματική λογική]], μια [[θεωρία (μαθηματική λογική)|θεωρία]] είναι ένα σύνολο από [[Πρόταση (μαθηματική λογική)|προτάσεις]] εκπεφρασμένες σε μια [[τυπική γλώσσα]]. Μερικές δηλώσεις σε μια θεωρία συμπεριλαμβάνονται χωρίς [[Μαθηματική απόδειξη|απόδειξη]] ([[Αξίωμα|αξιώματα]]) και άλλες (θεωρήματα) συμπεριλαμβάνονται επειδή συνάγονται από τα αξιώματα.
Επειδή οι δηλώσεις μιας τυπικής θεωρίας γράφονται σε συμβολική μορφή, είναι δυνατόν να επαληθεύσουμε μηχανικά ότι μία [[τυπική απόδειξη]] από ένα πεπερασμένο σύνολο από αξιώματα είναι έγκυρη. Αυτή η δουλειά, γνωστή ως αυτοματοποιημένη επαλήθευση αποδείξεων, σχετίζεται στενά με την [[αυτοματοποιημένη απόδειξη θεωρημάτων]]. Η διαφορά είναι ότι αντί να κατασκευάσει μια νέα απόδειξη, ο επαληθευτής αποδείξεων απλά ελέγχει αν μια δεδομένη τυπική απόδειξη (ή, σε μερικές περιπτώσεις, οι οδηγίες που
Παρόλα αυτά, πολλές θεωρίες που μας ενδιαφέρουν περιλαμβάνουν ένα άπειρο σύνολο από αξιώματα. Για να επαληθευτεί μια τυπική απόδειξη όταν το σύνολο των αξιωμάτων είναι άπειρο, πρέπει να είναι δυνατόν να προσδιορίσουμε αν μία δήλωση η οποία θεωρείται ότι είναι αξίωμα είναι πράγματι αξίωμα. Αυτό το ζήτημα προκύπτει στις [[Λογική πρώτου βαθμού|πρώτου βαθμού]] θεωρίες της αριθμητικής, όπως η [[Αριθμητική Πεάνο|αριθμητική του Πεάνο]], επειδή η αρχή της [[Μαθηματική επαγωγή|μαθηματικής επαγωγής]] εκφράζεται ως ένα άπειρο σύνολο αξιωμάτων (ένα [[αξιωματικό σχήμα]]).
| |||