Θεωρήματα μη πληρότητας του Γκέντελ: Διαφορά μεταξύ των αναθεωρήσεων

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

 

 

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