Μετάβαση στο περιεχόμενο
Topos Uranos
Ελληνικά

Μεταθεωρία: σύνθεση και προκλήσεις

Περίληψη

Το μάθημα αυτό κλείνει την ενότητα που είναι αφιερωμένη στη μεταθεωρία και, μαζί της, το περιεχόμενο του κύκλου μαθημάτων. Ανασυνθέτει την παραγωγική αλυσίδα που οδηγεί από την εγκυρότητα των αξιωμάτων στην ορθότητα του συστήματος· από τα δύο λήμματα της κοινής άρνησης στο λήμμα του Καλμάρ και στην πληρότητα για πεπερασμένες υποθέσεις· από το λήμμα των δύο μαρτύρων στο θεώρημα της συμπάγειας και, μέσω αυτού, στην ισχυρή πληρότητα· και από τη μορφή φράσεων στην ορθότητα και στην πληρότητα διάψευσης της μεθόδου της επίλυσης, δείχνοντας σε κάθε κρίκο ποια αποτελέσματα χρησιμοποιεί και σε ποιο μάθημα αποδεικνύεται. Δείχνει πώς συγκλίνουν στη σύμπτωση του ⊢\vdash και του ⊨\models τα τρία προηγούμενα μέρη του κύκλου μαθημάτων, η γλώσσα, η παραγωγή και η σημασιολογία, και τι συνεισφέρει καθένα σε αυτή τη σύμπτωση· διακρίνει όσα απέδειξε ο κύκλος μαθημάτων από όσα δέχθηκε και από όσα αφήνει ανοιχτά. Επαναλαμβάνει στην τελική αξιολόγησή του τις δεξιότητες της αρχικής αξιολόγησης και κλείνει με έξι προκλήσεις, μεγαλύτερης δυσκολίας από τα προβλήματα των μαθημάτων, που απαιτούν να συνδυαστούν τα εργαλεία πολλών από αυτά.

Μαθησιακοί στόχοι

  1. Να ανασυντίθεται η λογική σειρά των αποτελεσμάτων της ενότητας, με τον εντοπισμό των προηγούμενων αποτελεσμάτων στα οποία στηρίζεται καθένα και του μαθήματος στο οποίο αποδεικνύεται, και να αιτιολογείται η σειρά της συμπάγειας και της ισχυρής πληρότητας.
  2. Να εξηγείται πώς συγκλίνουν η γλώσσα, η παραγωγή και η σημασιολογία στη σύμπτωση του ⊢\vdash και του ⊨\models, και ποιο αποτέλεσμα κάθε ενότητας του κύκλου μαθημάτων είναι απαραίτητο γι’ αυτήν.
  3. Να διακρίνεται ό,τι απέδειξε ο κύκλος μαθημάτων από ό,τι δέχθηκε (τα αξιωματικά σχήματα, τους πρωταρχικούς κανόνες και την επαγωγή) και από ό,τι αφήνει ανοιχτό (το κόστος της απόφασης για την ικανοποιησιμότητα και τη λογική με ποσοδείκτες).
  4. Να λύνονται προβλήματα που συνδυάζουν τις σημάνσεις, το λήμμα του Καλμάρ, την ομοιόμορφη υποκατάσταση, τη συμπάγεια και την επίλυση, με χρήση σε κάθε περίπτωση της εύκολης πλευράς της σύμπτωσης.

Όσα πέτυχε η ενότητα

Η ενότητα έθεσε ως σκοπό να συγκρίνει τις δύο σχέσεις που είχαν κατασκευάσει οι προηγούμενες ενότητες πάνω στην ίδια γλώσσα, την παραγωγιμότητα Γ⊢φ\Gamma \vdash \varphi και τη σημασιολογική συνέπεια Γ⊨φ\Gamma \models \varphi, και να αποδείξει ότι συμπίπτουν. Ο σκοπός εκπληρώθηκε χωρίς επιφυλάξεις στις διατυπώσεις: οι δύο σχέσεις είναι η ίδια για κάθε σύνολο υποθέσεων, πεπερασμένο ή άπειρο, και η επίλυση προσφέρει έναν τρίτο τρόπο, εξίσου ορθό και πλήρη, για την απόφαση της συνέπειας. Οι επιφυλάξεις βρίσκονται στις μεθόδους, και καθεμία δηλώθηκε στη θέση της: η πληρότητα του πρώτου μαθήματος είναι κατασκευαστική αλλά όχι πρακτική, επειδή παράγει παραγωγές τόσο μακριές όσο ο πίνακας· η συμπάγεια εξασφαλίζει ότι υπάρχει μια αποτίμηση, αλλά δεν διδάσκει πώς να βρεθεί· και η επίλυση αποφασίζει, αλλά το κόστος της στη χειρότερη περίπτωση είναι ανοιχτό ερώτημα. Με αυτές τις επιφυλάξεις, ο δρόμος που διανύθηκε μπορεί να διαβαστεί ως μία ενιαία παραγωγική αλυσίδα σε τέσσερα τμήματα.

Η ορθότητα

Το μάθημα για την ορθότητα και την πληρότητα ξεκίνησε καθορίζοντας το λεξιλόγιο: το σύστημα είναι ορθό αν Γ⊢φ⇒Γ⊨φ\Gamma \vdash \varphi \Rightarrow \Gamma \models \varphi, και πλήρες αν ισχύει το αντίστροφο, σε τρεις βαθμούς (ασθενής, για πεπερασμένα σύνολα και ισχυρή). Αποδόμησε ένα κυκλικό επιχείρημα που επιχειρεί να αποκτήσει την πληρότητα «από την ορθότητα» περνώντας από το ⊬χ\nvdash \chi στο ⊭χ\not\models \chi, βήμα που είναι η αντιθετοαντίστροφή της ασθενούς πληρότητας, και έδειξε ότι οι δύο ιδιότητες είναι ανεξάρτητες. Απέδειξε έπειτα ότι κάθε στιγμιότυπο των A1, A2 και A3 είναι έγκυρο, υποθέτοντας μια αποτίμηση που θα το διέψευδε και φθάνοντας, μέσω της ψευδούς γραμμής της συνεπαγωγής, σε αδύνατες τιμές· και, με ισχυρή επαγωγή στο πλήθος των γραμμών, την ορθότητα, με μία περίπτωση για τα αξιώματα, μία για τις υποθέσεις, τον σημασιολογικό modus ponens και, για τον κανόνα της αντικατάστασης της διπλής άρνησης, την ισοδυναμία θ≡¬¬θ\theta \eqsem \neg\neg\theta μαζί με το θεώρημα σημασιολογικής αντικατάστασης. Η ιδιότητα που μεταδίδεται από γραμμή σε γραμμή δεν είναι η εγκυρότητα, αλλά η ικανοποίηση από μια σταθερή αποτίμηση που ικανοποιεί τις υποθέσεις, και γι’ αυτό η ορθότητα ισχύει με υποθέσεις, ακόμη και άπειρες. Από αυτήν προέκυψαν η μη αντιφατικότητα κάθε ικανοποιήσιμου συνόλου, ιδίως εκείνη του συστήματος, και η μέθοδος που δεν είχε η ενότητα της παραγωγής: ένα αντιμοντέλο αποδεικνύει ότι μια παραγωγή δεν υπάρχει.

Ο Καλμάρ και η πεπερασμένη πληρότητα

Το ίδιο μάθημα απέδειξε το αντίστροφο σε δύο βήματα. Το πρώτο είναι το λήμμα του Καλμάρ: αν οι μεταβλητές του φ\varphi βρίσκονται ανάμεσα στις u1,…,unu_{1}, \ldots, u_{n}, τότε {u1v,…,unv}⊢φv\{u_{1}^{v}, \ldots, u_{n}^{v}\} \vdash \varphi^{v} για κάθε αποτίμηση vv, όπου ο ψv\psi^{v} είναι ο ψ\psi αν v(ψ)=1v(\psi) = 1 και ο ¬ψ\neg\psi αλλιώς· το σύστημα παράγει από κάθε γραμμή ό,τι λέει η γραμμή για τον τύπο. Η επαγωγή του στην πολυπλοκότητα έχει μία μόνο σύνθετη περίπτωση, την (α↓β)(\alpha \downarrow \beta), επειδή η κοινή άρνηση είναι ο μόνος πρωταρχικός σύνδεσμος, και σε αυτήν τρεις υποπεριπτώσεις, που απαιτούν δύο λήμματα του συστήματος, το δεύτερο σε δύο μορφές: το ⊢(¬α→(¬β→(α↓β)))\vdash (\neg\alpha \rightarrow (\neg\beta \rightarrow (\alpha \downarrow \beta))), που παράγεται με την εισαγωγή της σύζευξης, τη διπλή άρνηση και δύο εφαρμογές του κανόνα ΑΔΑ, και τα ⊢(α→¬(α↓β))\vdash (\alpha \rightarrow \neg(\alpha \downarrow \beta)) και ⊢(β→¬(α↓β))\vdash (\beta \rightarrow \neg(\alpha \downarrow \beta)), που παράγονται με την εισαγωγή της διάζευξης. Το δεύτερο βήμα απαλείφει τις υποθέσεις: αν ο φ\varphi είναι ταυτολογία, παράγεται από τις υποθέσεις των 2n2^{n} γραμμών, και η απόδειξη κατά περιπτώσεις απαλείφει το λεκτικό της τελευταίας μεταβλητής, έπειτα της προτελευταίας, μέχρι να φθάσει στο ⊢φ\vdash \varphi, την ασθενή πληρότητα. Με το σημασιολογικό θεώρημα της απαγωγής και το αντίστροφο του συντακτικού, η πληρότητα επεκτάθηκε σε πεπερασμένα σύνολα υποθέσεων· από όπου, για πεπερασμένες υποθέσεις, η παραγωγή και η συνέπεια συμπίπτουν, η αποδείξιμη ισοδυναμία συμπίπτει με τη σημασιολογική και η παραγωγιμότητα είναι αποκρίσιμη, επειδή ο πίνακας απαντά γι’ αυτήν.

Συμπάγεια και ισχυρή πληρότητα

Το μάθημα για το θεώρημα της συμπάγειας αντιμετώπισε την άπειρη περίπτωση, την οποία το λήμμα του Καλμάρ δεν φθάνει, επειδή άπειρες υποθέσεις δεν εκφορτώνονται σε μια συνεπαγωγή. Απέδειξε, χωρίς να αναφέρει καμία παραγωγή, ότι ένα σύνολο είναι ικανοποιήσιμο αν και μόνο αν είναι ικανοποιήσιμο καθένα από τα πεπερασμένα υποσύνολά του. Μια ακολουθία τιμών για τις v1,…,vnv_{1}, \ldots, v_{n} είναι καλή αν κάθε πεπερασμένο υποσύνολο του συνόλου ικανοποιείται από κάποια αποτίμηση που την επεκτείνει· το λήμμα των δύο μαρτύρων εξασφαλίζει ότι μια καλή ακολουθία επεκτείνεται σε μια καλή, επειδή, αν καμία από τις δύο επεκτάσεις δεν ήταν καλή, η ένωση των δύο πεπερασμένων μαρτύρων θα αντέφασκε στο ότι η ακολουθία είναι καλή· και η αποτίμηση που προκύπτει αν προτιμάται πάντοτε το 11 όταν είναι δυνατό ικανοποιεί κάθε τύπο, χάρη στο λήμμα σύμπτωσης, επειδή κάθε τύπος έχει πεπερασμένο πλήθος μεταβλητών. Η κατασκευή δεν χρειάζεται το αξίωμα της επιλογής, επειδή οι μεταβλητές είναι αριθμημένες και κάθε βήμα έχει έναν κανόνα. Από τη συμπάγεια προέκυψαν οι ισοδύναμες μορφές της, η μορφή της μη ικανοποιησιμότητας και η μορφή της συνέπειας· από τη δεύτερη, από την πληρότητα για πεπερασμένες υποθέσεις και από τη μονοτονία, η ισχυρή πληρότητα· και από αυτήν και από την ορθότητα, η πλήρης σύμπτωση: Γ⊢φ⇔Γ⊨φ\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi για κάθε Γ\Gamma, και ένα σύνολο είναι συνεπές αν και μόνο αν είναι ικανοποιήσιμο. Το μάθημα προειδοποίησε ότι αυτή η σειρά δεν είναι θέμα προτίμησης: η απόκτηση της συμπάγειας από μια ισχυρή πληρότητα που δεν έχουμε ακόμη θα ήταν κυκλική. Έκλεισε με τον χρωματισμό αριθμήσιμων γραφημάτων, που μεταφράζει ένα άπειρο πρόβλημα σε ένα σύνολο τύπων του οποίου τα πεπερασμένα μέρη είναι ικανοποιήσιμα, και με τα όρια όσων μπορεί να εκφράσει ένα σύνολο τύπων.

Η επίλυση

Το μάθημα για τη μέθοδο της επίλυσης αντικατέστησε τα σύνολα τύπων με σύνολα φράσεων, καθεμία ένα πεπερασμένο σύνολο λεκτικών, με δύο αναπαραστάσεις: τη μορφή φράσεων, που έχει τα ίδια μοντέλα, και την ορισμική μορφή, που εισάγει μια νέα μεταβλητή για κάθε σύνθετη επιμέρους γραφή, διατηρεί μόνο την ικανοποιησιμότητα και αυξάνεται όπως ο τύπος, όχι όπως μια δύναμη του δύο. Πάνω στις φράσεις δρα ένας μόνο κανόνας: από τις CC και DD, με ℓ∈C\ell \in C και ℓ∗∈D\ell^{*} \in D, συνάγεται η (C∖{ℓ})∪(D∖{ℓ∗})(C \setminus \{\ell\}) \cup (D \setminus \{\ell^{*}\}), και μια διάψευση είναι μια συναγωγή που φθάνει στη □\Box. Η ορθότητα αποδείχθηκε όπως εκείνη του συστήματος, με επαγωγή στη συναγωγή και με την επιλύουσα ως συνέπεια των υποθέσεών της· η πληρότητα διάψευσης, με επαγωγή στο πλήθος των μεταβλητών, με την απαλοιφή μιας μεταβλητής, που διατηρεί την ικανοποιησιμότητα και της οποίας η απόδειξη κατασκευάζει ένα μοντέλο· και για άπειρα σύνολα, πάλι με τη συμπάγεια. Από αυτό προέκυψε ότι Γ⊨φ\Gamma \models \varphi αν και μόνο αν μια μορφή φράσεων του Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} έχει διάψευση, και ότι ο κορεσμός, πεπερασμένος επειδή με nn μεταβλητές δεν υπάρχουν περισσότερες από 4n4^{n} φράσεις, αποφασίζει την ικανοποιησιμότητα χωρίς πίνακες. Το μάθημα παρουσίασε το πρόβλημα της ικανοποιησιμότητας, του οποίου το κόστος στη χειρότερη περίπτωση κανείς δεν γνωρίζει, και δύο περιπτώσεις που αποφασίζονται γρήγορα, τις φράσεις Horn και τις φράσεις δύο λεκτικών.

Η εικόνα που ακολουθεί συγκεντρώνει τα τέσσερα τμήματα σε μία ενιαία αλυσίδα. Κάθε κόμβος της στήλης είναι ένα αποτέλεσμα, αριθμημένο σύμφωνα με τη λογική σειρά και ενωμένο με ένα τόξο με τους προηγούμενους κρίκους που χρησιμοποιεί η απόδειξή του· γύρω της αιωρούνται τα στηρίγματα, δηλαδή οι αρχές και τα εργαλεία στα οποία η αλυσίδα καταφεύγει ξανά και ξανά, καθένα ενωμένο με συνεχή γραμμή με τους κρίκους που στηρίζονται σε αυτό και με διακεκομμένη με τον κρίκο όπου θεμελιώνεται, εκτός από όσα προέρχονται από τις προηγούμενες ενότητες, που σχεδιάζονται ως δακτύλιοι. Όταν πατηθεί ένα στήριγμα, τονίζονται όλοι οι κρίκοι που το χρησιμοποιούν, και κάθε κρίκος παραπέμπει στο μάθημα όπου αποδεικνύεται. Ας σημειωθεί ότι η ορθότητα και η συμπάγεια, που θεμελιώθηκαν η μία στο πρώτο τμήμα και η άλλη στο τρίτο, επανεμφανίζονται στα επόμενα τμήματα, και ότι το πιο πολυσύχναστο στήριγμα της ενότητας είναι οι αποτιμήσεις και η σύμπτωση, και ακολουθεί η επαγωγή, στις τρεις μορφές της: στις γραμμές μιας παραγωγής, στην πολυπλοκότητα ενός τύπου και στο πλήθος των μεταβλητών ενός συνόλου φράσεων.

Στηρίγματα της αλυσίδας

  • AΕπαγωγή και αναδρομή. Ισχυρή επαγωγή στους φυσικούς, επαγωγή στην πολυπλοκότητα των τύπων, με μοναδική σύνθετη περίπτωση την (α↓β)(\alpha \downarrow \beta), και ορισμός με αναδρομή. Αποδείχθηκαν στην πρώτη ενότητα. Γίνεται δεκτό χωρίς απόδειξη σε αυτή την ενότητα.
  • BΤο σύστημα του κύκλου μαθημάτων. A1, A2 και A3, ο modus ponens και ο κανόνας ΑΔΑ· ανακλαστικότητα, μονοτονία, modus ponens μεταξύ παραγωγών, πεπερασμένος χαρακτήρας και Γ∪{φ}⊢ψ⇔Γ⊢(φ→ψ)\Gamma \cup \{\varphi\} \vdash \psi \Leftrightarrow \Gamma \vdash (\varphi \rightarrow \psi). Καθορίστηκαν στη δεύτερη ενότητα. Γίνεται δεκτό χωρίς απόδειξη σε αυτή την ενότητα.
  • CΠαράγωγες τεχνικές. Διπλή άρνηση, από το μάθημα για τις τέσσερις τεχνικές· εισαγωγή της σύζευξης και της διάζευξης και απόδειξη κατά περιπτώσεις (αν Γ∪{ψ}⊢χ\Gamma \cup \{\psi\} \vdash \chi και Γ∪{¬ψ}⊢χ\Gamma \cup \{\neg\psi\} \vdash \chi, τότε Γ⊢χ\Gamma \vdash \chi), από το μάθημα για τις τεχνικές της κλασικής λογικής. Αποδείχθηκαν στη δεύτερη ενότητα. Γίνεται δεκτό χωρίς απόδειξη σε αυτή την ενότητα.
  • DΑποτιμήσεις και σύμπτωση. v((α↓β))=(1−v(α))(1−v(β))v((\alpha \downarrow \beta)) = (1 - v(\alpha))(1 - v(\beta))· αν δύο αποτιμήσεις συμπίπτουν στο V(φ)V(\varphi), δίνουν στον φ\varphi την ίδια τιμή· η εγκυρότητα αποφασίζεται με 2n2^{n} γραμμές. Αποδείχθηκαν στην τρίτη ενότητα. Γίνεται δεκτό χωρίς απόδειξη σε αυτή την ενότητα.
  • EΣημασιολογική συνέπεια. Ψευδής γραμμή της συνεπαγωγής, μονοτονία, Γ∪{φ}⊨ψ⇔Γ⊨(φ→ψ)\Gamma \cup \{\varphi\} \models \psi \Leftrightarrow \Gamma \models (\varphi \rightarrow \psi), Γ⊨φ\Gamma \models \varphi αν και μόνο αν το Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} είναι μη ικανοποιήσιμο, και το θεώρημα σημασιολογικής αντικατάστασης. Αποδείχθηκαν στην τρίτη ενότητα. Γίνεται δεκτό χωρίς απόδειξη σε αυτή την ενότητα.
  • FΣυζευκτικές μορφές. Λήμμα της τιμής· κάθε τύπος είναι ισοδύναμος με μια συζευκτική κανονική μορφή, που μπορεί να χρειαστεί 2n2^{n} φράσεις· μια διάζευξη λεκτικών είναι έγκυρη αν και μόνο αν περιέχει ένα συμπληρωματικό ζεύγος. Αποδείχθηκαν στην τρίτη ενότητα. Γίνεται δεκτό χωρίς απόδειξη σε αυτή την ενότητα.
  • GΟρθότητα. Αν Γ⊢φ\Gamma \vdash \varphi, τότε Γ⊨φ\Gamma \models \varphi, για κάθε σύνολο Γ\Gamma· ένα αντιμοντέλο αποδεικνύει ότι μια παραγωγή δεν υπάρχει. Θεμελιώνεται στον κρίκο: 2. Ορθότητα.
  • HΣυμπάγεια. Ένα σύνολο τύπων είναι ικανοποιήσιμο αν και μόνο αν κάθε πεπερασμένο υποσύνολό του είναι ικανοποιήσιμο· από όπου ό,τι είναι μη ικανοποιήσιμο είναι ήδη μη ικανοποιήσιμο σε ένα πεπερασμένο μέρος του. Θεμελιώνεται στον κρίκο: 11. Θεώρημα της συμπάγειας.

  1. Τμήμα 1 Η ορθότητα

    • Να ελέγχεται ότι κάθε στιγμιότυπο των σχημάτων είναι έγκυρο χωρίς να κατασκευάζεται ο πίνακάς του.
    • Να αποδεικνύεται η ορθότητα με ισχυρή επαγωγή στο πλήθος των γραμμών, με την περίπτωση του κανόνα της αντικατάστασης της διπλής άρνησης.
    • Να αποδεικνύεται με ένα αντιμοντέλο ότι ένας τύπος δεν παράγεται, και να εξάγεται από την ορθότητα η μη αντιφατικότητα.

    1. Εγκυρότητα των αξιωμάτων. Κάθε στιγμιότυπο των A1, A2 και A3 είναι έγκυρο: μια αποτίμηση που θα το διέψευδε θα απαιτούσε, μέσω της ψευδούς γραμμής της συνεπαγωγής, αδύνατες τιμές.

      Στηρίζεται σε: E (Σημασιολογική συνέπεια). Αποδεικνύεται στη διάλεξη: Ορθότητα και πληρότητα.

    2. Ορθότητα. Αν Γ⊢φ\Gamma \vdash \varphi, τότε Γ⊨φ\Gamma \models \varphi, για κάθε Γ\Gamma: με ισχυρή επαγωγή στο πλήθος των γραμμών, με μία περίπτωση για τα αξιώματα, μία για τις υποθέσεις, τον σημασιολογικό modus ponens και, για τον κανόνα ΑΔΑ, την θ≡¬¬θ\theta \eqsem \neg\neg\theta μαζί με τη σημασιολογική αντικατάσταση.

      Χρησιμοποιεί: 1. Εγκυρότητα των αξιωμάτων. Στηρίζεται σε: A (Επαγωγή και αναδρομή), B (Το σύστημα του κύκλου μαθημάτων), E (Σημασιολογική συνέπεια). Αποδεικνύεται στη διάλεξη: Ορθότητα και πληρότητα.

    3. Μη αντιφατικότητα και αντιμοντέλα. Κάθε ικανοποιήσιμο σύνολο είναι συνεπές· το σύστημα είναι συνεπές και ⊬v1\nvdash v_{1}· αν μια αποτίμηση ικανοποιεί το Γ\Gamma και διαψεύδει τον φ\varphi, τότε Γ⊬φ\Gamma \nvdash \varphi, και ο πίνακας πιστοποιεί ότι ό,τι δεν είναι έγκυρο δεν είναι θεώρημα.

      Στηρίζεται σε: G (Ορθότητα), D (Αποτιμήσεις και σύμπτωση). Αποδεικνύεται στη διάλεξη: Ορθότητα και πληρότητα.

  2. Τμήμα 2 Ο Καλμάρ και η πεπερασμένη πληρότητα

    • Να παράγονται στο σύστημα τα δύο λήμματα της κοινής άρνησης, με τον κανόνα της αντικατάστασης της διπλής άρνησης όπου χρειάζεται.
    • Να αποδεικνύεται το λήμμα του Καλμάρ με επαγωγή στην πολυπλοκότητα, με μία μόνο σύνθετη περίπτωση.
    • Να απαλείφονται με την απόδειξη κατά περιπτώσεις οι υποθέσεις των γραμμών, και να εκφορτώνονται πεπερασμένες υποθέσεις με τα δύο θεωρήματα της απαγωγής.
    • Να αποφασίζονται με τον πίνακα η παραγωγιμότητα, η αποδείξιμη ισοδυναμία και η μη αντιφατικότητα από πεπερασμένες υποθέσεις.

    1. Εισαγωγή της κοινής άρνησης. {¬α,¬β}⊢(α↓β)\{\neg\alpha, \neg\beta\} \vdash (\alpha \downarrow \beta) και ⊢(¬α→(¬β→(α↓β)))\vdash (\neg\alpha \rightarrow (\neg\beta \rightarrow (\alpha \downarrow \beta))): η σύζευξη των αρνήσεων είναι η ¬¬(¬¬α↓¬¬β)\neg\neg(\neg\neg\alpha \downarrow \neg\neg\beta)· η διπλή άρνηση αφαιρεί την εξωτερική, και ο κανόνας ΑΔΑ τις δύο εσωτερικές.

      Στηρίζεται σε: B (Το σύστημα του κύκλου μαθημάτων), C (Παράγωγες τεχνικές). Αποδεικνύεται στη διάλεξη: Ορθότητα και πληρότητα.

    2. Άρνηση της κοινής άρνησης. ⊢(α→¬(α↓β))\vdash (\alpha \rightarrow \neg(\alpha \downarrow \beta)) και ⊢(β→¬(α↓β))\vdash (\beta \rightarrow \neg(\alpha \downarrow \beta)), επειδή η ¬(α↓β)\neg(\alpha \downarrow \beta) είναι η (α∨β)(\alpha \vee \beta) και αρκεί η εισαγωγή της διάζευξης.

      Στηρίζεται σε: B (Το σύστημα του κύκλου μαθημάτων), C (Παράγωγες τεχνικές). Αποδεικνύεται στη διάλεξη: Ορθότητα και πληρότητα.

    3. Λήμμα του Καλμάρ. Αν V(φ)⊆{u1,…,un}V(\varphi) \subseteq \{u_{1}, \ldots, u_{n}\}, τότε {u1v,…,unv}⊢φv\{u_{1}^{v}, \ldots, u_{n}^{v}\} \vdash \varphi^{v} για κάθε αποτίμηση vv· το επαγωγικό βήμα έχει μία μόνο περίπτωση, την (α↓β)(\alpha \downarrow \beta), με τρεις υποπεριπτώσεις ανάλογα με τις τιμές του α\alpha και του β\beta.

      Χρησιμοποιεί: 4. Εισαγωγή της κοινής άρνησης, 5. Άρνηση της κοινής άρνησης. Στηρίζεται σε: A (Επαγωγή και αναδρομή), D (Αποτιμήσεις και σύμπτωση), B (Το σύστημα του κύκλου μαθημάτων). Αποδεικνύεται στη διάλεξη: Ορθότητα και πληρότητα.

    4. Ασθενής πληρότητα. Αν ⊨φ\models \varphi, τότε ⊢φ\vdash \varphi: το λήμμα του Καλμάρ παράγει τον φ\varphi από κάθε γραμμή, και η απόδειξη κατά περιπτώσεις απαλείφει τα λεκτικά από την τελευταία μεταβλητή ως την πρώτη, με 2n2^{n} χρήσεις του λήμματος και 2n−12^{n} - 1 της απόδειξης κατά περιπτώσεις.

      Χρησιμοποιεί: 6. Λήμμα του Καλμάρ. Στηρίζεται σε: C (Παράγωγες τεχνικές). Αποδεικνύεται στη διάλεξη: Ορθότητα και πληρότητα.

    5. Πληρότητα για πεπερασμένες υποθέσεις. {γ1,…,γk}⊨φ⇒{γ1,…,γk}⊢φ\{\gamma_{1}, \ldots, \gamma_{k}\} \models \varphi \Rightarrow \{\gamma_{1}, \ldots, \gamma_{k}\} \vdash \varphi: το σημασιολογικό θεώρημα της απαγωγής οδηγεί σε μια ταυτολογία, η ασθενής πληρότητα την παράγει και το αντίστροφο του θεωρήματος της απαγωγής επαναφέρει τις υποθέσεις.

      Χρησιμοποιεί: 7. Ασθενής πληρότητα. Στηρίζεται σε: E (Σημασιολογική συνέπεια), B (Το σύστημα του κύκλου μαθημάτων). Αποδεικνύεται στη διάλεξη: Ορθότητα και πληρότητα.

    6. Πεπερασμένη σύμπτωση και απόφαση. Για πεπερασμένο Γ\Gamma, Γ⊢φ⇔Γ⊨φ\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi, και φ⊣⊢ψ⇔φ≡ψ\varphi \dashv\vdash \psi \Leftrightarrow \varphi \eqsem \psi· από όπου η παραγωγιμότητα από πεπερασμένες υποθέσεις είναι αποκρίσιμη, μέσω του πίνακα.

      Χρησιμοποιεί: 8. Πληρότητα για πεπερασμένες υποθέσεις. Στηρίζεται σε: G (Ορθότητα), D (Αποτιμήσεις και σύμπτωση). Αποδεικνύεται στη διάλεξη: Ορθότητα και πληρότητα.

  3. Τμήμα 3 Συμπάγεια και ισχυρή πληρότητα

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

    1. Λήμμα των δύο μαρτύρων. Αν η ακολουθία ss των καθορισμένων τιμών είναι καλή (κάθε πεπερασμένο υποσύνολο του συνόλου ικανοποιείται από μια αποτίμηση που την επεκτείνει), είναι καλή η (s,1)(s, 1) ή η (s,0)(s, 0): αν καμία δεν ήταν, η ένωση των δύο πεπερασμένων μαρτύρων θα αντέφασκε στο ότι η ss είναι καλή.

      Στηρίζεται σε: D (Αποτιμήσεις και σύμπτωση). Αποδεικνύεται στη διάλεξη: Το θεώρημα της συμπάγειας.

    2. Θεώρημα της συμπάγειας. Το Γ\Gamma είναι ικανοποιήσιμο αν και μόνο αν κάθε πεπερασμένο υποσύνολο είναι ικανοποιήσιμο: η vn+1v_{n + 1} τίθεται ίση με 11 αν η (sn,1)(s_{n}, 1) είναι καλή και ίση με 00 αλλιώς, και η αποτίμηση που προκύπτει ικανοποιεί κάθε τύπο χάρη στο λήμμα σύμπτωσης. Δεν χρειάζεται το αξίωμα της επιλογής, επειδή οι μεταβλητές είναι αριθμημένες.

      Χρησιμοποιεί: 10. Λήμμα των δύο μαρτύρων. Στηρίζεται σε: A (Επαγωγή και αναδρομή), D (Αποτιμήσεις και σύμπτωση). Αποδεικνύεται στη διάλεξη: Το θεώρημα της συμπάγειας.

    3. Ισοδύναμες μορφές. Το Γ\Gamma είναι μη ικανοποιήσιμο αν και μόνο αν κάποιο πεπερασμένο μέρος του είναι· Γ⊨φ\Gamma \models \varphi αν και μόνο αν Γ0⊨φ\Gamma_{0} \models \varphi για κάποιο πεπερασμένο Γ0⊆Γ\Gamma_{0} \subseteq \Gamma· και αυτή η τελευταία μορφή συνεπάγεται με τη σειρά της το θεώρημα.

      Χρησιμοποιεί: 11. Θεώρημα της συμπάγειας. Στηρίζεται σε: E (Σημασιολογική συνέπεια). Αποδεικνύεται στη διάλεξη: Το θεώρημα της συμπάγειας.

    4. Ισχυρή πληρότητα. Αν Γ⊨φ\Gamma \models \varphi, τότε Γ⊢φ\Gamma \vdash \varphi, για κάθε Γ\Gamma: η μορφή της συνέπειας δίνει ένα πεπερασμένο Γ0\Gamma_{0}, η πληρότητα για πεπερασμένες υποθέσεις δίνει Γ0⊢φ\Gamma_{0} \vdash \varphi, και η μονοτονία Γ⊢φ\Gamma \vdash \varphi.

      Χρησιμοποιεί: 8. Πληρότητα για πεπερασμένες υποθέσεις, 12. Ισοδύναμες μορφές. Στηρίζεται σε: B (Το σύστημα του κύκλου μαθημάτων). Αποδεικνύεται στη διάλεξη: Το θεώρημα της συμπάγειας.

    5. Η παραγωγή είναι η συνέπεια. Γ⊢φ⇔Γ⊨φ\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi για κάθε Γ\Gamma· τα θεωρήματα είναι ακριβώς οι ταυτολογίες, και ένα σύνολο είναι συνεπές αν και μόνο αν είναι ικανοποιήσιμο.

      Χρησιμοποιεί: 13. Ισχυρή πληρότητα. Στηρίζεται σε: G (Ορθότητα). Αποδεικνύεται στη διάλεξη: Το θεώρημα της συμπάγειας.

    6. Χρωματισμός αριθμήσιμων γραφημάτων. Με μια μεταβλητή xi,cx_{i,c} για κάθε κορυφή και χρώμα, και τύπους που λένε ότι κάθε κορυφή έχει ένα χρώμα και μόνο ένα και ότι οι γειτονικές διαφέρουν, ένα αριθμήσιμο γράφημα δέχεται χρωματισμό με kk χρώματα αν τον δέχεται κάθε πεπερασμένο υπογράφημά του.

      Στηρίζεται σε: H (Συμπάγεια), F (Συζευκτικές μορφές). Αποδεικνύεται στη διάλεξη: Το θεώρημα της συμπάγειας.

  4. Τμήμα 4 Η επίλυση

    • Να αναπαρίσταται ένα σύνολο τύπων ως σύνολο φράσεων, μέσω της συζευκτικής ή της ορισμικής μορφής.
    • Να κατασκευάζονται διαψεύσεις χωρίς να απαλείφονται δύο συμπληρωματικά ζεύγη σε ένα βήμα.
    • Να αποδεικνύονται η ορθότητα και η πληρότητα διάψευσης της επίλυσης, για πεπερασμένα σύνολα και, με τη συμπάγεια, για οποιαδήποτε.
    • Να αποφασίζονται συνέπειες με κορεσμό και να αναγνωρίζονται οι περιπτώσεις που αποφασίζονται γρήγορα.

    1. Μορφή φράσεων. Μια φράση είναι ένα πεπερασμένο σύνολο λεκτικών, που ικανοποιείται αν κάποιο παίρνει την τιμή 11, και η □\Box είναι μη ικανοποιήσιμη· μια μορφή φράσεων του Γ\Gamma έχει τα ίδια μοντέλα με αυτό, και Γ⊨φ\Gamma \models \varphi αν και μόνο αν μια μορφή φράσεων του Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} είναι μη ικανοποιήσιμη.

      Στηρίζεται σε: F (Συζευκτικές μορφές), E (Σημασιολογική συνέπεια). Αποδεικνύεται στη διάλεξη: Η μέθοδος της επίλυσης.

    2. Ορισμική μορφή φράσεων. Με μια νέα μεταβλητή για κάθε επιμέρους γραφή και τις φράσεις ορισμού της, η T(φ)T(\varphi) είναι ισοϊκανοποιήσιμη με τον φ\varphi και έχει το πολύ 4k+14k + 1 φράσεις, το πολύ τριών λεκτικών η καθεμία· οι ορισμικές μορφές αποφασίζουν τη συνέπεια από πεπερασμένες υποθέσεις.

      Χρησιμοποιεί: 16. Μορφή φράσεων. Στηρίζεται σε: A (Επαγωγή και αναδρομή), D (Αποτιμήσεις και σύμπτωση). Αποδεικνύεται στη διάλεξη: Η μέθοδος της επίλυσης.

    3. Ορθότητα της επίλυσης. {C,D}⊨Rℓ(C,D)\{C, D\} \models R_{\ell}(C, D), κατά περιπτώσεις ως προς την τιμή του ℓ\ell· με ισχυρή επαγωγή στη συναγωγή, S⊨CS \models C για κάθε φράση CC που συνάγεται από το SS, και αν το SS έχει διάψευση, είναι μη ικανοποιήσιμο.

      Χρησιμοποιεί: 16. Μορφή φράσεων. Στηρίζεται σε: A (Επαγωγή και αναδρομή). Αποδεικνύεται στη διάλεξη: Η μέθοδος της επίλυσης.

    4. Απαλοιφή μιας μεταβλητής. Το Ep(S)E_{p}(S), που διατηρεί τις φράσεις χωρίς pp ούτε ¬p\neg p και προσθέτει τις επιλύουσες ως προς pp, δεν περιέχει το pp και είναι ισοϊκανοποιήσιμο με το SS· από ένα μοντέλο του προκύπτει ένα μοντέλο του SS με την επιλογή της τιμής της pp.

      Χρησιμοποιεί: 18. Ορθότητα της επίλυσης. Στηρίζεται σε: D (Αποτιμήσεις και σύμπτωση). Αποδεικνύεται στη διάλεξη: Η μέθοδος της επίλυσης.

    5. Πεπερασμένη πληρότητα διάψευσης. Κάθε πεπερασμένο και μη ικανοποιήσιμο σύνολο φράσεων έχει διάψευση, με επαγωγή στο πλήθος των μεταβλητών: απαλείφεται η τελευταία και παρεμβάλλονται οι υποθέσεις κάθε επιλύουσας.

      Χρησιμοποιεί: 19. Απαλοιφή μιας μεταβλητής. Στηρίζεται σε: A (Επαγωγή και αναδρομή). Αποδεικνύεται στη διάλεξη: Η μέθοδος της επίλυσης.

    6. Πληρότητα διάψευσης. Ένα σύνολο φράσεων, πεπερασμένο ή άπειρο, είναι μη ικανοποιήσιμο αν και μόνο αν έχει διάψευση· από όπου Γ⊨φ\Gamma \models \varphi αν και μόνο αν μια μορφή φράσεων του Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} έχει διάψευση.

      Χρησιμοποιεί: 16. Μορφή φράσεων, 18. Ορθότητα της επίλυσης, 20. Πεπερασμένη πληρότητα διάψευσης. Στηρίζεται σε: H (Συμπάγεια). Αποδεικνύεται στη διάλεξη: Η μέθοδος της επίλυσης.

    7. Ο κορεσμός αποφασίζει. Με nn μεταβλητές, το σύνολο των φράσεων που συνάγονται έχει το πολύ 4n4^{n} στοιχεία· ο κορεσμός τερματίζει και αποφασίζει την ικανοποιησιμότητα χωρίς πίνακες, αν και όχι πάντα ταχύτερα από αυτούς.

      Χρησιμοποιεί: 18. Ορθότητα της επίλυσης, 20. Πεπερασμένη πληρότητα διάψευσης. Αποδεικνύεται στη διάλεξη: Η μέθοδος της επίλυσης.

Το τέλος του κύκλου μαθημάτων. Η αλυσίδα τελειώνει εκεί όπου οι δύο όψεις του κύκλου μαθημάτων αναγνωρίζονται ως μία ενιαία σχέση και υπάρχει μια μέθοδος για να αποφασίζεται. Ό,τι μένει ανοιχτό δεν είναι πια ερώτημα για την προτασιακή λογική, αλλά για το κόστος της και για την επέκτασή της στους ποσοδείκτες.