Τέσσερις τεχνικές παραγωγής

Τα εργαλεία της αφετηρίας

Στο μάθημα για τα τυπικά παραγωγικά συστήματα ορίστηκε το σύστημα του Λουκασέβιτς. Η γλώσσα του είναι η γλώσσα των κύκλων και των δίσκων, γραμμένη με τις επίσημες συντομογραφίες του μαθήματος για τη γλώσσα της προτασιακής λογικής· αξιώματά του είναι όλα τα στιγμιότυπα των τριών σχημάτων που ακολουθούν, όπου οι $\varphi$, $\psi$ και $\chi$ είναι οποιοιδήποτε τύποι, και μοναδικός κανόνας του είναι ο modus ponens.

• A1: $(\varphi \rightarrow (\psi \rightarrow \varphi))$.
• A2: $((\varphi \rightarrow (\psi \rightarrow \chi)) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \chi)))$.
• A3: $((\neg\psi \rightarrow \neg\varphi) \rightarrow (\varphi \rightarrow \psi))$.
• MP: από τους $\varphi$ και $(\varphi \rightarrow \psi)$ παράγεται ο $\psi$.

Παραγωγή του $\varphi$ από ένα σύνολο $\Gamma$ τύπων είναι μια πεπερασμένη ακολουθία τύπων που τελειώνει στον $\varphi$ και στην οποία κάθε τύπος είναι αξίωμα, στοιχείο του $\Gamma$ ή αποτέλεσμα της εφαρμογής του modus ponens σε δύο προηγούμενους τύπους· αν υπάρχει, γράφουμε $\Gamma \vdash \varphi$, και αν το $\Gamma$ είναι κενό, $\vdash \varphi$, και λέμε ότι ο $\varphi$ είναι θεώρημα. Στο ίδιο μάθημα αποδείχθηκαν τα μεταθεωρήματα που θα χρησιμοποιήσουμε εδώ: η ανακλαστικότητα (Ανακλ: αν $\varphi \in \Gamma$, τότε $\Gamma \vdash \varphi$), η μονοτονία (Μον: αν $\Gamma \subseteq \Delta$ και $\Gamma \vdash \varphi$, τότε $\Delta \vdash \varphi$), ο modus ponens μεταξύ παραγωγών (αν $\Gamma \vdash \varphi$ και $\Gamma \vdash (\varphi \rightarrow \psi)$, τότε $\Gamma \vdash \psi$), ο κανόνας της τομής (Τομή: αν $\Gamma \vdash \varphi_{i}$ για κάθε $i$ από $1$ έως $n$ και $\Gamma \cup \{\varphi_{1}, \ldots, \varphi_{n}\} \vdash \psi$, τότε $\Gamma \vdash \psi$), ο πεπερασμένος χαρακτήρας (αν $\Gamma \vdash \varphi$, αρκεί κάποιο πεπερασμένο υποσύνολο του $\Gamma$), το θεώρημα της απαγωγής (ΘΑ: αν $\Gamma \cup \{\varphi\} \vdash \psi$, τότε $\Gamma \vdash (\varphi \rightarrow \psi)$) και το αντίστροφό του (ΑΘΑ), καθώς και το θεώρημα $\vdash (\varphi \rightarrow \varphi)$, που στις αιτιολογήσεις θα το συντομογραφούμε Ταυτ. Τέλος, η σχέση $\varphi \dashv\vdash \psi$ (αποδείξιμη ισοδυναμία) σημαίνει ότι $\{\varphi\} \vdash \psi$ και $\{\psi\} \vdash \varphi$.

Αξίζει να θυμηθούμε ότι τα $\neg$ και $\rightarrow$ δεν είναι σύμβολα της βασικής γλώσσας, αλλά συντομογραφίες: ο $\neg\varphi$ είναι η συμβολοσειρά $(\varphi \downarrow \varphi)$, και ο $(\varphi \rightarrow \psi)$ είναι ο $(\neg\varphi \vee \psi)$, δηλαδή ο $\neg(\neg\varphi \downarrow \psi)$. Τα τρία αξιώματα μιλούν μόνο για αρνήσεις και για συνεπαγωγές, και το ίδιο μάθημα έδειξε, με μια σήμανση με $0$ και $1$ που αυτά και ο modus ponens διατηρούν, το όριο που απορρέει από αυτό: στο σύστημα του Λουκασέβιτς, από τον $(v_{1} \downarrow v_{2})$ δεν παράγεται ο $(\neg\neg v_{1} \downarrow v_{2})$, και η κοινή άρνηση μένει εν μέρει έξω από την εμβέλειά του. Το μάθημα αυτό προχωρεί, επομένως, σε δύο φάσεις. Μέχρι και τη διπλή άρνηση, το $\vdash$ αναφέρεται στο σύστημα του Λουκασέβιτς, και τίποτε από όσα αποδεικνύονται δεν εξαρτάται από την ανάπτυξη των συντομογραφιών. Αφού αποδειχθεί η διπλή άρνηση, προστίθεται στο σύστημα ένας δεύτερος πρωταρχικός κανόνας, η αντικατάσταση της διπλής άρνησης, που δρα πάνω στην αναπτυγμένη συμβολοσειρά· από εκεί και πέρα, το $\vdash$ αναφέρεται στο σύστημα του κύκλου μαθημάτων, δηλαδή στο σύστημα του Λουκασέβιτς μαζί με αυτόν τον κανόνα. Επειδή κάθε παραγωγή του πρώτου είναι και παραγωγή του δεύτερου, τίποτε από όσα αποδείχθηκαν πριν δεν χάνεται.

Δύο ύφη παραγωγής

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

• Ανακλ: ο τύπος στα δεξιά ανήκει στο σύνολο στα αριστερά.
• A1, A2, A3: ο τύπος στα δεξιά είναι στιγμιότυπο του σχήματος· ένα στιγμιότυπο αξιώματος παράγεται από οποιοδήποτε $\Gamma$ με μια παραγωγή μίας μόνο γραμμής.
• MP$(i, j)$: ο modus ponens μεταξύ παραγωγών, εφαρμοσμένος στη γραμμή $i$, $\Gamma \vdash \varphi$, και στη γραμμή $j$, $\Gamma \vdash (\varphi \rightarrow \psi)$, με το ίδιο $\Gamma$.
• ΘΑ$(i)$ και ΑΘΑ$(i)$: το θεώρημα της απαγωγής ή το αντίστροφό του, εφαρμοσμένο στη γραμμή $i$.
• Το όνομα ενός θεωρήματος που έχει ήδη αποδειχθεί, όπως Ταυτ ή ΔΑ: ο τύπος στα δεξιά είναι στιγμιότυπο αυτού του θεωρήματος, και παράγεται από οποιοδήποτε $\Gamma$ λόγω μονοτονίας, επειδή το κενό σύνολο περιέχεται στο $\Gamma$.
• Υπόθεση, σε μια παραγωγή για παραγωγές: η γραμμή είναι μία από τις παραδοχές του κανόνα που αποδεικνύεται.

Κάθε αποτέλεσμα αυτού του μαθήματος διατυπώνεται με μεταμεταβλητές και ισχύει, επομένως, για οποιουσδήποτε τύπους: η απόδειξή του είναι ένα σχήμα, και αν υποκαταστήσουμε σε αυτήν κάθε μεταμεταβλητή με έναν τύπο προκύπτει μια άλλη απόδειξη, επειδή τα στιγμιότυπα ενός αξιωματικού σχήματος παραμένουν στιγμιότυπα και κάθε modus ponens παραμένει modus ponens (το ίδιο θα ισχύει για κάθε εφαρμογή του νέου κανόνα). Έτσι, από το $\vdash (\varphi \rightarrow \varphi)$ έπεται το $\vdash (\neg\psi \rightarrow \neg\psi)$, με τον $\neg\psi$ στη θέση του $\varphi$. Αυτό το μέσο, η εφαρμογή ενός αποτελέσματος σε έναν τύπο πιο σύνθετο από εκείνον της διατύπωσης, είναι το πιο αποδοτικό σε όσα ακολουθούν.

Από το αποτέλεσμα στον κανόνα

Οι τεχνικές αυτού του μαθήματος αποδεικνύονται από σταθερές υποθέσεις, όπως $\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi)$· χρησιμοποιούνται όμως μέσα σε παραγωγές με άλλες υποθέσεις, όπου οι $(\varphi \rightarrow \psi)$ και $(\psi \rightarrow \chi)$ δεν είναι υποθέσεις, αλλά τύποι που έχουν ήδη παραχθεί. Το λήμμα που ακολουθεί, άμεση συνέπεια της μονοτονίας και της τομής, επιτρέπει αυτή τη χρήση μία για πάντα.

Από αυτό έπεται ότι κάθε τεχνική που αποδεικνύεται από υποθέσεις έχει τρεις παρουσιάσεις: το ίδιο το αποτέλεσμα, το θεώρημα που προκύπτει αποφορτίζοντας τις υποθέσεις του και τον κανόνα που εφαρμόζεται κάτω από οποιοδήποτε $\Gamma$. Σε μια παραγωγή για παραγωγές, ο κανόνας επικαλείται με το όνομα της τεχνικής και τους αριθμούς των γραμμών στις οποίες εφαρμόζεται, όπως ΥΣ$(3, 4)$, και το λήμμα εγγυάται ότι το βήμα είναι θεμιτό.