Συμπερασμός: σύνθεση και προκλήσεις

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

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

Το σύστημα του Λουκασέβιτς και το όριό του

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

Οι τέσσερις τεχνικές και ο νέος κανόνας

Το μάθημα για τις τέσσερις τεχνικές παραγωγής απέδειξε πρώτα το λήμμα «από το αποτέλεσμα στον κανόνα»: αν $\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta$, το ίδιο συμπέρασμα προκύπτει από οποιοδήποτε $\Gamma$ που παράγει τους $\alpha_{i}$, και επιπλέον $\vdash (\alpha_{1} \rightarrow (\alpha_{2} \rightarrow \cdots (\alpha_{n} \rightarrow \beta) \cdots))$. Αυτό το λήμμα επιτρέπει να χρησιμοποιείται κάθε τεχνική σε τρεις παρουσιάσεις (από υποθέσεις, ως θεώρημα και ως κανόνας), και τα μαθήματα για τις συμμετρίες και για τον Ντε Μόργκαν, που συνδέουν αλυσίδες ισοδυναμιών με την τομή, στηρίζονται γι’ αυτό στις ιδιότητες της αποδείξιμης ισοδυναμίας του πρώτου μαθήματος, που είναι η ίδια ιδέα εφαρμοσμένη σε μία μόνο υπόθεση· στην αλυσίδα κάθε αποτέλεσμα εμφανίζεται μία μόνο φορά, εκεί όπου αποδεικνύεται. Με αυτό, το μάθημα παρήγαγε τον υποθετικό συλλογισμό από τα A1 και A2 σε επτά γραμμές, την εναλλαγή υποθέσεων με το θεώρημα της απαγωγής, τη διπλή άρνηση (της οποίας η πρώτη κατεύθυνση εφαρμόζει δύο φορές το A3 σε μια συνεπαγωγή κατασκευασμένη με το A1, και η δεύτερη εφαρμόζει την πρώτη στον $\neg\varphi$ και το A3) και την αντιθετοαντιστροφή στις τρεις μορφές της, που κατανέμουν με τρεις τρόπους τις αρνήσεις μιας συνεπαγωγής· και οι τέσσερις ισχύουν ήδη στο σύστημα του Λουκασέβιτς.

Αφού αποδείχθηκε η διπλή άρνηση, το μάθημα συμπλήρωσε το σύστημα του κύκλου μαθημάτων με έναν δεύτερο πρωταρχικό κανόνα, την αντικατάσταση της διπλής άρνησης (ΑΔΑ): από τον $\chi$ συνάγεται ο $\chi'$ όταν ο $\chi'$ προκύπτει αν αντικατασταθεί στον $\chi$ μία εμφάνιση ενός υποτύπου $\theta$ με τον $\neg\neg\theta$, ή μία εμφάνιση του $\neg\neg\theta$ με τον $\theta$. Ο κανόνας πρέπει να τεθεί ως αίτημα, επειδή η σήμανση $m_{1}$ δίνει $1$ στα θεωρήματα της διπλής άρνησης και ωστόσο ξεχωρίζει τον $(v_{1} \downarrow v_{2})$ από τον $(\neg\neg v_{1} \downarrow v_{2})$· ο ΑΔΑ δεν διατηρεί την $m_{1}$, και γι’ αυτό διευρύνει ό,τι είναι παραγώγιμο, αλλά διατηρεί την τίμια σήμανση, και γι’ αυτό δεν το διευρύνει υπερβολικά. Ο κανόνας δρα πάνω στη συμβολοσειρά της βασικής γλώσσας, όπου μια άρνηση διπλασιάζει το όρισμά της: ο $(\varphi \rightarrow \psi)$ περιέχει δύο φορές τον υποτύπο $\neg\varphi$, και για να τεθεί μια διπλή άρνηση μπροστά στο ηγούμενό του χρειάζονται δύο εφαρμογές. Η ίδια παρατήρηση στηρίζει την επέκταση του θεωρήματος της απαγωγής: αν μια γραμμή προκύπτει με τον κανόνα, η επαγωγική υπόθεση δίνει τη συνεπαγωγή της οποίας το επόμενο είναι η προηγούμενη γραμμή, και δύο εφαρμογές του κανόνα, μία σε κάθε αντίγραφο αυτού του επομένου, δίνουν τη ζητούμενη συνεπαγωγή· οι υπόλοιπες δομικές ιδιότητες ισχύουν με την ίδια απόδειξη. Οι πρώτες συνέπειες είναι ότι ένας τύπος είναι ισοδύναμος με κάθε τύπο που προκύπτει από αυτόν με τον κανόνα, ειδικότερα $(\varphi \downarrow \psi) \dashv\vdash (\neg\neg\varphi \downarrow \psi)$ και $(\varphi \downarrow \psi) \dashv\vdash (\varphi \downarrow \neg\neg\psi)$, και ότι οι αντίστοιχες συνεπαγωγές, που άλλα συστήματα τις παίρνουν ως αξιώματα, είναι εδώ θεωρήματα.

Σύνδεσμοι και αντικατάσταση

Το μάθημα για τις συμμετρίες των συνδέσμων αντιμετώπισε τη δυσκολία που είναι χαρακτηριστική της γλώσσας των κύκλων και των δίσκων: τα αξιώματα του Λουκασέβιτς μιλούν μόνο για αρνήσεις και για συνεπαγωγές, και σχεδόν καμία κοινή άρνηση δεν είναι ούτε το ένα ούτε το άλλο. Το θεμελιώδες λήμμα, $(\varphi \downarrow \psi) \dashv\vdash \neg(\neg\varphi \rightarrow \psi)$, ρίχνει τη γέφυρα: επειδή ο $\neg(\neg\varphi \rightarrow \psi)$ είναι ο $\neg\neg(\neg\neg\varphi \downarrow \psi)$, ο κανόνας ΑΔΑ θέτει την εσωτερική διπλή άρνηση και η διπλή άρνηση την εξωτερική· στην αντίστροφη κατεύθυνση, η διπλή άρνηση και ο κανόνας τις αφαιρούν. Με αυτό, η αντικατάσταση ισοδυνάμων, που αποδείχθηκε πρώτα κάτω από την άρνηση και στις δύο πλευρές της συνεπαγωγής με την αντιθετοαντιστροφή και τον υποθετικό συλλογισμό, επεκτάθηκε και στα δύο ορίσματα της κοινής άρνησης και, από εκεί, στη διάζευξη και στη σύζευξη. Ο κανόνας και η αντικατάσταση δεν καθιστούν ο ένας την άλλη περιττή: ο κανόνας μόνο εναλλάσσει τον $\theta$ και τον $\neg\neg\theta$, ενώ η αντικατάσταση δέχεται οποιουσδήποτε ισοδύναμους· και η αντικατάσταση, που αποδείχθηκε με το θεμελιώδες λήμμα, στηρίζεται με τη σειρά της στον κανόνα. Το μάθημα απέδειξε έπειτα ότι οι μορφές που άλλα κείμενα παίρνουν ως ορισμούς είναι ισοδυναμίες: $(\varphi \vee \psi) \dashv\vdash (\neg\varphi \rightarrow \psi)$, που απαιτεί δύο εφαρμογές του κανόνα, μία σε κάθε αντίγραφο που δημιουργεί η εξωτερική άρνηση, και $(\varphi \wedge \psi) \dashv\vdash (\neg\varphi \downarrow \neg\psi)$, που απαιτεί τη διπλή άρνηση· αντίθετα, ο $(\varphi \wedge \psi)$ και ο $\neg(\varphi \rightarrow \neg\psi)$ είναι η ίδια συμβολοσειρά. Τέλος, απέδειξε τις πέντε συμμετρίες με τη σειρά που επιβάλλουν οι ορισμοί: της κοινής άρνησης με το θεμελιώδες λήμμα και την αντιθετοαντιστροφή, και καθεμιά από τις υπόλοιπες με την προηγούμενη, μεταφερμένη με την αντικατάσταση κάτω από την άρνηση όταν χρειάζεται.

Οι κλασικοί κανόνες και οι νόμοι

Το μάθημα για τις τεχνικές της κλασικής λογικής απέδειξε, όλους με ένα σύνολο υποθέσεων $\Gamma$ που μεταφέρεται από γραμμή σε γραμμή, την εισαγωγή και την απαλοιφή της διάζευξης και της σύζευξης, το αποκλειόμενο τρίτο και τη μη αντίφαση, την έκρηξη, την απαγωγή σε άτοπο στις δύο μορφές της και την απόδειξη κατά περιπτώσεις, με έναν τύπο και την άρνησή του και με μια οποιαδήποτε διάζευξη. Η σειρά των εξαρτήσεων είναι αυστηρή: η έκρηξη στηρίζεται στους κανόνες της διάζευξης· η κλασική απαγωγή σε άτοπο, στην έκρηξη και στο A3· η απόδειξη κατά περιπτώσεις, στην αντιθετοαντιστροφή και στην απαγωγή σε άτοπο. Καμία από αυτές τις αποδείξεις δεν επικαλείται άμεσα τον κανόνα ΑΔΑ: ο κανόνας δρα μέσω των ισοδύναμων μορφών και της αντικατάστασης ισοδυνάμων. Το μάθημα για τους νόμους του Ντε Μόργκαν και τους επιμεριστικούς νόμους έβαλε αυτούς τους κανόνες να δουλέψουν μαζί: ο πρώτος νόμος του Ντε Μόργκαν προκύπτει από τον ορισμό της σύζευξης και από τη διπλή άρνηση· ο δεύτερος απαιτεί να μπει κανείς μέσα στην κοινή άρνηση, όπου ο κανόνας ΑΔΑ παρεμβαίνει δύο φορές, μία σε κάθε όρισμα και χωρίς να χρειαστεί η συμμετρία, και από αυτόν έπεται ότι ο $(\varphi \downarrow \psi)$ είναι ισοδύναμος με τον $(\neg\varphi \wedge \neg\psi)$, την ανάγνωση «ούτε $\varphi$ ούτε $\psi$» που η προηγούμενη ενότητα είχε ορίσει με σύμβαση· στις παραλλαγές περιλαμβάνεται και η $\neg(\varphi \rightarrow \psi) \dashv\vdash (\varphi \wedge \neg\psi)$. Οι δύο επιμεριστικοί νόμοι αποδείχθηκαν και στις δύο κατευθύνσεις τους κατά περιπτώσεις, επιλέγοντας σε καθεμιά τη μορφή της απόδειξης κατά περιπτώσεις που ταιριάζει.

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

Οι συντομογραφίες των αιτιολογήσεων

Οι παραγωγές της ενότητας αιτιολογούν κάθε γραμμή με μια συντομογραφία, την ίδια σε όλα τα μαθήματα. Συγκεντρώνονται εδώ, ταξινομημένες κατά το μάθημα που τις εισάγει. Η «Υπόθεση» δηλώνει μια παραδοχή της εκφώνησης και, στις παραγωγές για παραγωγές, μια παραδοχή του κανόνα που αποδεικνύεται. Οι αριθμοί μέσα σε παρενθέσεις παραπέμπουν στις γραμμές στις οποίες εφαρμόζεται ο κανόνας· μια ισοδυναμία που έχει ήδη αποδειχθεί αναφέρεται χωρίς αριθμό όταν γράφεται ως γραμμή, και με τον αριθμό της γραμμής που μετασχηματίζει όταν εφαρμόζεται σε αυτή τη γραμμή, και σε ένα από τα μέρη της με «Αντ».

• Πρώτο μάθημα: A1, A2 και A3 (τα αξιωματικά σχήματα)· MP$(i, j)$ (modus ponens)· Ορ (ορισμός: ανάπτυξη ή σύμπτυξη μιας συντομογραφίας, με τον σύνδεσμο που αναπτύσσεται: «Ορ $\vee$», «Ορ $\dashv\vdash$»)· Ταυτ (ταυτότητα, το θεώρημα $\vdash (\varphi \rightarrow \varphi)$)· Ανακλ (ανακλαστικότητα: αν $\varphi \in \Gamma$, τότε $\Gamma \vdash \varphi$)· Μον (μονοτονία)· Τομή (κανόνας της τομής: ό,τι έχει παραχθεί μπορεί να χρησιμοποιηθεί ως υπόθεση)· Πεπ (πεπερασμένος χαρακτήρας)· ΘΑ (θεώρημα της απαγωγής) και ΑΘΑ (το αντίστροφό του).
• Δεύτερο μάθημα: ΥΣ (υποθετικός συλλογισμός)· ΕΥ (εναλλαγή υποθέσεων)· ΔΑ (διπλή άρνηση)· ΑΔΑ$(i)$ (αντικατάσταση της διπλής άρνησης στη γραμμή $i$· η ΑΔΑ χωρίς αριθμό παραπέμπει στην ισοδυναμία ανάμεσα σε έναν τύπο και στον τύπο που προκύπτει από αυτόν με τον κανόνα)· ΑΑ (αντιθετοαντιστροφή, σε οποιαδήποτε από τις τρεις μορφές της)· «Λυμένο $n$» (ένα αποτέλεσμα του λυμένου προβλήματος $n$ του ίδιου μαθήματος, γραμμένο ως γραμμή).
• Τρίτο μάθημα: ΘΛ (θεμελιώδες λήμμα, $(\varphi \downarrow \psi) \dashv\vdash \neg(\neg\varphi \rightarrow \psi)$)· Αντ (αντικατάσταση ισοδυνάμων, σε οποιαδήποτε από τις μορφές της, ακολουθούμενη από την ισοδυναμία που εφαρμόζεται: «Αντ, ΝΜ$(i)$»)· Ισ (ισοδύναμες μορφές της διάζευξης και της σύζευξης, $(\varphi \vee \psi) \dashv\vdash (\neg\varphi \rightarrow \psi)$ και $(\varphi \wedge \psi) \dashv\vdash (\neg\varphi \downarrow \neg\psi)$)· Συμ (συμμετρία ενός συνδέσμου).
• Τέταρτο μάθημα: $\vee$Εισ και $\vee$Απ (εισαγωγή και απαλοιφή της διάζευξης)· $\wedge$Εισ και $\wedge$Απ (εισαγωγή και απαλοιφή της σύζευξης)· ΑΤ (αποκλειόμενο τρίτο)· ΜΑ (μη αντίφαση, συντομογραφία που ονομάζει το θεώρημα, αλλά δεν αιτιολογεί καμία γραμμή της ενότητας)· Εκρ (έκρηξη)· Περ$(i, j)$ και Περ$(i, j, k)$ (απόδειξη κατά περιπτώσεις, με έναν τύπο και την άρνησή του ή με μια διάζευξη)· «Περ χωρίς υποθέσεις» (η απόδειξη κατά περιπτώσεις χωρίς σύνολο $\Gamma$, που εμφανίζεται μόνο σε ένα πρόβλημα)· Άτοπο (απαγωγή σε άτοπο, στις δύο μορφές της).
• Πέμπτο μάθημα: ΝΜ (νόμοι του Ντε Μόργκαν)· Επιμ (επιμεριστικότητα)· Προσ (προσεταιριστικότητα της διάζευξης)· Στιγμιότυπο$(i)$ (η γραμμή $i$, που ισχύει για οποιουσδήποτε τύπους, γραμμένη ξανά με άλλους τύπους στη θέση των μεταμεταβλητών της· σημειώνεται η υποκατάσταση).
• Προκλήσεις αυτού του μαθήματος: M3 (το σχήμα που η τρίτη πρόκληση θέτει στη θέση του A3).