Ορθότητα και πληρότητα

Δύο ερωτήματα για το σύστημα του κύκλου μαθημάτων

Η ενότητα για την παραγωγή καθόρισε το σύστημα του κύκλου μαθημάτων: τα αξιωματικά σχήματα A1, A2 και A3 του Λουκασέβιτς και δύο κανόνες, τον modus ponens (MP) και την αντικατάσταση της διπλής άρνησης (ΑΔΑ), την οποία το μάθημα για τις τέσσερις τεχνικές παραγωγής πρόσθεσε αφού απέδειξε τη διπλή άρνηση. Μια παραγωγή από ένα σύνολο $\Gamma$ είναι μια πεπερασμένη ακολουθία τύπων στην οποία καθένας είναι αξίωμα, στοιχείο του $\Gamma$, το αποτέλεσμα του modus ponens εφαρμοσμένου σε δύο προηγούμενους τύπους ή το αποτέλεσμα της ΑΔΑ εφαρμοσμένης σε έναν προηγούμενο· το $\Gamma \vdash \varphi$ σημαίνει ότι υπάρχει μια παραγωγή από το $\Gamma$ της οποίας ο τελευταίος τύπος είναι ο $\varphi$. Η ενότητα για τη σημασιολογία, από την πλευρά της, όρισε στο μάθημα για τη σημασιολογική συνέπεια και ισοδυναμία τη σχέση $\Gamma \models \varphi$: κάθε αποτίμηση που ικανοποιεί όλους τους τύπους του $\Gamma$ ικανοποιεί τον $\varphi$. Οι δύο σχέσεις γράφονται με το ίδιο σχέδιο, ένα σύνολο αριστερά και ένας τύπος δεξιά· ωστόσο, η φύση τους είναι αντίθετη. Η πρώτη είναι συντακτική και υπαρξιακή: βεβαιώνει ότι υπάρχει ένα πεπερασμένο αντικείμενο, μια παραγωγή, που μπορεί να ελεγχθεί σύμβολο προς σύμβολο. Η δεύτερη είναι σημασιολογική και καθολική: βεβαιώνει κάτι για όλες τις αποτιμήσεις, που είναι άπειρες, και καθεμία από τις οποίες δίνει τιμή σε άπειρες μεταβλητές.

Δύο ερωτήματα τίθενται, επομένως, για το σύστημα. Το πρώτο: παράγει μόνο ό,τι πρέπει; Λέμε ότι το σύστημα είναι ορθό αν, για κάθε σύνολο $\Gamma$ και κάθε τύπο $\varphi$, το $\Gamma \vdash \varphi$ συνεπάγεται το $\Gamma \models \varphi$: ό,τι παράγεται από κάποιες υποθέσεις είναι αληθές σε κάθε αποτίμηση που κάνει αληθείς τις υποθέσεις. Το δεύτερο: παράγει ό,τι πρέπει; Λέμε ότι το σύστημα είναι πλήρες αν το $\Gamma \models \varphi$ συνεπάγεται το $\Gamma \vdash \varphi$. Η πληρότητα δέχεται τρεις βαθμούς, ανάλογα με τα σύνολα υποθέσεων που καλύπτει:

• ασθενής πληρότητα: αν $\models \varphi$, τότε $\vdash \varphi$· κάθε ταυτολογία είναι θεώρημα·
• πληρότητα για πεπερασμένα σύνολα: αν $\{\gamma_{1}, \ldots, \gamma_{k}\} \models \varphi$, τότε $\{\gamma_{1}, \ldots, \gamma_{k}\} \vdash \varphi$·
• ισχυρή πληρότητα: αν $\Gamma \models \varphi$, τότε $\Gamma \vdash \varphi$, για ένα οποιοδήποτε σύνολο $\Gamma$, και άπειρο.

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

Τι δεν πρέπει να λέγεται

Στα ισπανικά η ορθότητα ονομάζεται μερικές φορές «solvencia», μεταφορά του αγγλικού soundness· ο ισπανικός όρος είναι «corrección», και στα ελληνικά ο κύκλος μαθημάτων λέει «ορθότητα». Ούτε πρέπει να ορίζεται ως η ιδιότητα του συστήματος «να συνάγει μια έκφραση από ένα σύνολο εκφράσεων», που είναι η ίδια η παραγωγιμότητα και όχι μια ιδιότητα του συστήματος. Τα ουσιαστικά λάθη, ωστόσο, είναι δύο άλλα.

Το πρώτο είναι να βεβαιώνεται ότι η ορθότητα και η πληρότητα «μπορούν να συναχθούν η μία από την άλλη». Είναι ανεξάρτητες ιδιότητες: το σύστημα του Λουκασέβιτς, χωρίς τον κανόνα ΑΔΑ, είναι ορθό (η απόδειξη αυτού του μαθήματος το δείχνει, αν παραλειφθεί μία περίπτωση) και δεν είναι πλήρες (το μάθημα για τα τυπικά παραγωγικά συστήματα έδειξε μια ταυτολογία που δεν παράγει)· και ένα σύστημα που θα δεχόταν όλους τους τύπους ως αξιώματα θα ήταν πλήρες χωρίς να είναι ορθό. Το λυμένο πρόβλημα 2 εξετάζει και τα δύο παραδείγματα.

Το δεύτερο λάθος είναι σοβαρότερο, επειδή παρουσιάζει ως απόδειξη της πληρότητας ένα κυκλικό επιχείρημα. Λέει, στην ουσία: αν $\varphi \nvdash \psi$, τότε, από το θεώρημα της απαγωγής, $\nvdash (\varphi \rightarrow \psi)$· «από την ορθότητα», $\not\models (\varphi \rightarrow \psi)$· και από το σημασιολογικό θεώρημα της απαγωγής, $\varphi \not\models \psi$. Ωστόσο, η ορθότητα λέει ότι το παραγώγιμο είναι έγκυρο, και η αντιθετοαντίστροφή της, ότι ό,τι δεν είναι έγκυρο δεν είναι παραγώγιμο:

Το βήμα του επιχειρήματος πηγαίνει προς την άλλη κατεύθυνση, από το $\nvdash \chi$ στο $\not\models \chi$, που είναι η αντιθετοαντίστροφη του $\models \chi \Rightarrow \vdash \chi$, δηλαδή της ασθενούς πληρότητας. Αν αυτό ισχύει, το επιχείρημα προϋποθέτει αυτό που θέλει να αποδείξει. Έπεται ότι η πληρότητα δεν «συνάγεται με απλό τρόπο»: είναι το βαθύτερο αποτέλεσμα του κύκλου μαθημάτων, και η απόδειξή της καταλαμβάνει το μεγαλύτερο μέρος αυτού του μαθήματος. Τέλος, είναι ανακριβές να συνοψίζεται η πληρότητα λέγοντας ότι «όλες οι αληθείς εκφράσεις έχουν απόδειξη»· απόδειξη έχει το έγκυρο, αληθές σε κάθε αποτίμηση, όχι το αληθές σε κάποια: η μεταβλητή $v_{1}$ είναι αληθής σε πολλές αποτιμήσεις, και δεν είναι θεώρημα.