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