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

Οι συμμετρίες των συνδέσμων

Περίληψη

Το μάθημα αυτό αποδεικνύει ότι η σειρά των ορισμάτων δεν αλλάζει όσα παράγονται από την κοινή άρνηση, τη διάζευξη, τη σύζευξη, τη διπλή συνεπαγωγή και την αποκλειστική διάζευξη. Με τις επίσημες συντομογραφίες του κύκλου μαθημάτων, οι συμμετρίες αυτές δεν είναι προφανείς: η κοινή άρνηση είναι ο πρωταρχικός σύνδεσμος, τα αξιώματα του Λουκασέβιτς μιλούν μόνο για την άρνηση και τη συνεπαγωγή, και ο κανόνας της αντικατάστασης της διπλής άρνησης (ΑΔΑ) μόνο προσθέτει ή αφαιρεί διπλές αρνήσεις. Γι’ αυτό το μάθημα θεμελιώνει πρώτα τρία εργαλεία. Το πρώτο λέει ότι η αποδείξιμη ισοδυναμία συμπεριφέρεται ως ισότητα. Το δεύτερο, το θεμελιώδες λήμμα, μεταφράζει την κοινή άρνηση στη γλώσσα των αξιωμάτων: ο (φ↓ψ)(\varphi \downarrow \psi) ισοδυναμεί με τον ¬(¬φ→ψ)\neg(\neg\varphi \rightarrow \psi), χάρη στον κανόνα ΑΔΑ και στη διπλή άρνηση. Το τρίτο, η αντικατάσταση ισοδυνάμων, την οποία ο κανόνας ΑΔΑ δεν καθιστά περιττή, επιτρέπει να τεθεί στη θέση ενός τύπου οποιοσδήποτε άλλος ισοδύναμός του (και όχι μόνο ο θ\theta στη θέση του ¬¬θ\neg\neg\theta) κάτω από την άρνηση, στις δύο πλευρές της συνεπαγωγής και στις δύο πλευρές της κοινής άρνησης. Με αυτά αποδεικνύονται, ως ισοδυναμίες, οι ισοδύναμες μορφές της διάζευξης και της σύζευξης, που άλλα κείμενα παίρνουν ως ορισμούς, και οι πέντε συμμετρίες, και προς τις δύο κατευθύνσεις και με τη σειρά που επιβάλλουν οι ορισμοί: πρώτα η κοινή άρνηση, και από αυτήν, διαδοχικά, οι υπόλοιπες.

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

  1. Να αναπτύσσει τις επίσημες συντομογραφίες για να κρίνει αν δύο εκφράσεις δηλώνουν τον ίδιο τύπο ή διαφορετικούς τύπους των οποίων η ισοδυναμία απαιτεί παραγωγή.
  2. Να αποδεικνύει το θεμελιώδες λήμμα (φ↓ψ)⊣⊢¬(¬φ→ψ)(\varphi \downarrow \psi) \dashv\vdash \neg(\neg\varphi \rightarrow \psi) με τον κανόνα της αντικατάστασης της διπλής άρνησης (ΑΔΑ) και τη διπλή άρνηση, εντοπίζοντας τις διπλές αρνήσεις που κρύβουν οι συντομογραφίες.
  3. Να εφαρμόζει την αντικατάσταση ισοδυνάμων για να μεταφέρει μια ισοδυναμία στο εσωτερικό μιας άρνησης, μιας συνεπαγωγής ή μιας κοινής άρνησης, να τη διακρίνει από τον κανόνα ΑΔΑ, που μόνο εναλλάσσει τους θ\theta και ¬¬θ\neg\neg\theta, και να χρησιμοποιεί την αποδείξιμη ισοδυναμία ως ισότητα σε αλυσίδες ισοδυναμιών.
  4. Να αποδεικνύει τις ισοδύναμες μορφές της διάζευξης και της σύζευξης και τις πέντε συμμετρίες και προς τις δύο κατευθύνσεις, συνδέοντας αποτελέσματα που έχουν ήδη αποδειχθεί.
  5. Να επεκτείνει την αντικατάσταση ισοδυνάμων σε οποιονδήποτε τύπο μέσω της επαγωγής στην πολυπλοκότητα των τύπων.

Τι χρησιμοποιείται και τι πρέπει να αποδειχθεί

Το μάθημα για τα τυπικά παραγωγικά συστήματα καθόρισε το σύστημα του Λουκασέβιτς: τα αξιώματα A1, A2 και A3 και τον modus ponens. Θεμελίωσε επιπλέον την ανακλαστικότητα (Ανακλ: αν φ∈Γ\varphi \in \Gamma, τότε Γ⊢φ\Gamma \vdash \varphi), τη μονοτονία (Μον), την τομή (Τομή: αν Γ⊢φi\Gamma \vdash \varphi_{i} για κάθε ii και Γ∪{φ1,…,φn}⊢ψ\Gamma \cup \{\varphi_{1}, \ldots, \varphi_{n}\} \vdash \psi, τότε Γ⊢ψ\Gamma \vdash \psi), το θεώρημα της απαγωγής (ΘΑ) και το αντίστροφό του (ΑΘΑ) και την αποδείξιμη ισοδυναμία, φ⊣⊢ψ\varphi \dashv\vdash \psi, που σημαίνει ότι {φ}⊢ψ\{\varphi\} \vdash \psi και {ψ}⊢φ\{\psi\} \vdash \varphi· και έδειξε, με μια σήμανση που τα αξιώματα και ο modus ponens διατηρούν, ότι το σύστημα αυτό δεν παράγει ορισμένους τύπους για την κοινή άρνηση. Το μάθημα για τις τέσσερις τεχνικές παραγωγής πρόσθεσε τον υποθετικό συλλογισμό (ΥΣ: {(φ→ψ),(ψ→χ)}⊢(φ→χ)\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi)), την εναλλαγή υποθέσεων (ΕΥ), τη διπλή άρνηση (ΔΑ: φ⊣⊢¬¬φ\varphi \dashv\vdash \neg\neg\varphi, με τα δύο θεωρήματά της ⊢(¬¬φ→φ)\vdash (\neg\neg\varphi \rightarrow \varphi) και ⊢(φ→¬¬φ)\vdash (\varphi \rightarrow \neg\neg\varphi)) και την αντιθετοαντιστροφή (ΑΑ) στις τρεις μορφές της:

(φ→ψ)⊣⊢(¬ψ→¬φ),(¬φ→ψ)⊣⊢(¬ψ→φ),(φ→¬ψ)⊣⊢(ψ→¬φ)(\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \neg\varphi), \qquad (\neg\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \varphi), \qquad (\varphi \rightarrow \neg\psi) \dashv\vdash (\psi \rightarrow \neg\varphi)

Αφού αποδείχθηκε η διπλή άρνηση, το ίδιο μάθημα συμπλήρωσε το σύστημα του κύκλου μαθημάτων με έναν δεύτερο πρωταρχικό κανόνα, την αντικατάσταση της διπλής άρνησης (ΑΔΑ): αν ο χ′\chi' προκύπτει από τον χ\chi αντικαθιστώντας μία εμφάνιση ενός υποτύπου θ\theta με τον ¬¬θ\neg\neg\theta, ή μία εμφάνιση ενός υποτύπου ¬¬θ\neg\neg\theta με τον θ\theta, τότε από τον χ\chi συνάγεται ο χ′\chi'. Η γραμμή που προκύπτει έτσι από τη γραμμή ii αιτιολογείται με ΑΔΑ(i)(i). Από εκεί και πέρα, το ⊢\vdash αναφέρεται στο σύστημα του κύκλου μαθημάτων (A1 έως A3, ο modus ponens και η ΑΔΑ), στο οποίο εξακολουθούν να ισχύουν η Ανακλ, η Μον, η Τομή, το ΘΑ και το ΑΘΑ. Ο κανόνας δρα στη συμβολοσειρά της βασικής γλώσσας, ώστε φτάνει και στις εμφανίσεις που κρύβει μια συντομογραφία, και σε οποιοδήποτε από τα δύο ορίσματα μιας κοινής άρνησης· ανάμεσα στις άμεσες συνέπειές του είναι οι

(φ↓ψ)⊣⊢(¬¬φ↓ψ),(φ↓ψ)⊣⊢(φ↓¬¬ψ)(\varphi \downarrow \psi) \dashv\vdash (\neg\neg\varphi \downarrow \psi), \qquad (\varphi \downarrow \psi) \dashv\vdash (\varphi \downarrow \neg\neg\psi)

και, γενικά, χ⊣⊢χ′\chi \dashv\vdash \chi' όποτε ο χ′\chi' προκύπτει από τον χ\chi με ΑΔΑ. Μια γραμμή ισοδυναμίας αυτής της μορφής αιτιολογείται με «ΑΔΑ», χωρίς αριθμό γραμμής, όπως μια γραμμή «ΔΑ» ή «ΑΑ» παραπέμπει σε μια ισοδυναμία που έχει ήδη αποδειχθεί. Όπως εκεί, ένα θεώρημα που έχει ήδη αποδειχθεί μπορεί να γραφτεί ως γραμμή μιας παραγωγής, επειδή η δική του παραγωγή μπορεί να παρεμβληθεί σε εκείνη τη θέση· και, με το λήμμα «από το αποτέλεσμα στον κανόνα» εκείνου του μαθήματος, κάθε τεχνική εφαρμόζεται και ως κανόνας κάτω από οποιοδήποτε σύνολο Γ\Gamma υποθέσεων, με παραπομπή στους αριθμούς των γραμμών στις οποίες εφαρμόζεται, όπως ΑΑ(i)(i) ή ΥΣ(i,j)(i, j). Στις παραγωγές για παραγωγές, η «Υπόθεση» δηλώνει μια παραδοχή του κανόνα που αποδεικνύεται.

Οι επίσημες συντομογραφίες, που καθορίστηκαν στο μάθημα για τη γλώσσα της προτασιακής λογικής, είναι οι μόνοι ορισμοί των συνδέσμων:

¬φ:=(φ↓φ),(φ∨ψ):=¬(φ↓ψ),(φ∧ψ):=¬(¬φ∨¬ψ)\neg\varphi := (\varphi \downarrow \varphi), \qquad (\varphi \vee \psi) := \neg(\varphi \downarrow \psi), \qquad (\varphi \wedge \psi) := \neg(\neg\varphi \vee \neg\psi)
(φ→ψ):=(¬φ∨ψ),(φ↔ψ):=((φ→ψ)∧(ψ→φ)),(φ⊻ψ):=¬(φ↔ψ)(\varphi \rightarrow \psi) := (\neg\varphi \vee \psi), \qquad (\varphi \leftrightarrow \psi) := ((\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi)), \qquad (\varphi \veebar \psi) := \neg(\varphi \leftrightarrow \psi)

Μια γραμμή που αιτιολογείται με «Ορ» δεν παράγει τίποτε: γράφει τον ίδιο τύπο με άλλο όνομα, και η σημείωση λέει ποια συντομογραφία αναπτύσσεται ή συμπτύσσεται («Ορ →\rightarrow», «Ορ ∨\vee»). Αξίζει να θυμηθούμε το φαινόμενο που παρατηρήθηκε στο μάθημα για την τυποποίηση της φυσικής γλώσσας: ένας και ο αυτός τύπος δέχεται πολλά ονόματα, ώστε μια σύζευξη είναι επίσης, ως συμβολοσειρά, μια διάζευξη. Για παράδειγμα, αναπτύσσοντας τη συνεπαγωγή με τον ¬φ\neg\varphi στη θέση του φ\varphi, προκύπτει

(¬φ→ψ)=(¬¬φ∨ψ)=¬(¬¬φ↓ψ)(\neg\varphi \rightarrow \psi) = (\neg\neg\varphi \vee \psi) = \neg(\neg\neg\varphi \downarrow \psi)

και η διπλή άρνηση που εμφανίζεται μπροστά από τον φ\varphi, κρυμμένη από τη συντομογραφία, είναι ο λόγος για τον οποίο ο κανόνας ΑΔΑ θα παρεμβαίνει σε όλα όσα ακολουθούν.

Η αποδείξιμη ισοδυναμία ως ισότητα

Οι αποδείξεις αυτού του μαθήματος είναι, σχεδόν όλες, αλυσίδες ισοδυναμιών: φ1⊣⊢φ2\varphi_{1} \dashv\vdash \varphi_{2}, φ2⊣⊢φ3\varphi_{2} \dashv\vdash \varphi_{3}, και ούτω καθεξής. Για να συναχθεί από μια αλυσίδα ότι φ1⊣⊢φn\varphi_{1} \dashv\vdash \varphi_{n}, η αποδείξιμη ισοδυναμία πρέπει να συμπεριφέρεται ως ισότητα, και αυτό θεμελίωσε η πρόταση για τις ιδιότητες της αποδείξιμης ισοδυναμίας του μαθήματος για τα τυπικά παραγωγικά συστήματα: η σχέση είναι ανακλαστική (φ⊣⊢φ\varphi \dashv\vdash \varphi), συμμετρική (αν φ⊣⊢ψ\varphi \dashv\vdash \psi, τότε ψ⊣⊢φ\psi \dashv\vdash \varphi) και μεταβατική (αν φ⊣⊢ψ\varphi \dashv\vdash \psi και ψ⊣⊢χ\psi \dashv\vdash \chi, τότε φ⊣⊢χ\varphi \dashv\vdash \chi), και δύο αποδείξιμα ισοδύναμοι τύποι είναι εναλλάξιμοι ως συμπεράσματα (αν Γ⊢φ\Gamma \vdash \varphi και φ⊣⊢φ′\varphi \dashv\vdash \varphi', τότε Γ⊢φ′\Gamma \vdash \varphi', για κάθε σύνολο Γ\Gamma τύπων). Αξίζει να θυμηθούμε πώς αποδείχθηκαν οι δύο τελευταίες, επειδή ολόκληρο το μάθημα στηρίζεται σε αυτές: από το {φ}⊢φ′\{\varphi\} \vdash \varphi' περνάμε, με μονοτονία, στο Γ∪{φ}⊢φ′\Gamma \cup \{\varphi\} \vdash \varphi', και από αυτό και από το Γ⊢φ\Gamma \vdash \varphi, με τομή, στο Γ⊢φ′\Gamma \vdash \varphi'· η μεταβατικότητα προκύπτει αν εφαρμοστεί αυτό με Γ={φ}\Gamma = \{\varphi\} προς τη μία κατεύθυνση και με Γ={χ}\Gamma = \{\chi\} προς την άλλη.

Στο εξής, το βήμα που συνενώνει μια αλυσίδα ισοδυναμιών σε μία μόνο αιτιολογείται με «Τομή», που είναι το εργαλείο εκείνης της πρότασης. Όμως κάθε κρίκος φi⊣⊢φi+1\varphi_{i} \dashv\vdash \varphi_{i+1} περιέχει τις δύο παραγωγές, του πηγαιμού και της επιστροφής· από όπου μια αλυσίδα ισοδυναμιών αποδεικνύει ταυτόχρονα και τις δύο κατευθύνσεις του συμπεράσματός της, και τίποτε δεν μένει «ως άσκηση».