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

Τυπικά παραγωγικά συστήματα

Περίληψη

Το μάθημα αυτό μετατρέπει τη γλώσσα της προηγούμενης ενότητας σε όργανο απόδειξης. Ορίζει τι είναι ένα τυπικό παραγωγικό σύστημα (μια γλώσσα, ορισμένα αξιωματικά σχήματα και ορισμένοι κανόνες συμπερασμού) και παρουσιάζει το πρώτο από τα δύο συστήματα με τα οποία εργάζεται ο κύκλος μαθημάτων, το σύστημα του Λουκασέβιτς: τρία αξιωματικά σχήματα και τον modus ponens ως μοναδικό κανόνα. Ορίζει με ακρίβεια την παραγωγή από ένα σύνολο υποθέσεων, το θεώρημα και τη σχέση Γ⊢φ\Gamma \vdash \varphi, παράγει το ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi) σε πέντε γραμμές και αποδεικνύει τις δομικές ιδιότητες της παραγωγής: ανακλαστικότητα, μονοτονία, modus ponens μεταξύ παραγωγών, τομή και πεπερασμένο χαρακτήρα. Αποδεικνύει έπειτα, με ισχυρή επαγωγή στον αριθμό των γραμμών, το θεώρημα της απαγωγής και το αντίστροφό του, που επιτρέπουν να συλλογιζόμαστε με παραγωγές για παραγωγές, και ορίζει την αποδείξιμη ισοδυναμία. Τέλος, θεμελιώνει χωρίς προσφυγή στις τιμές αληθείας το όριο αυτού του συστήματος σε μια γλώσσα της οποίας ο μόνος σύνδεσμος είναι η κοινή άρνηση: μια σήμανση με τιμές 00 και 11, υπολογισμένη με αναδρομή πάνω στους τύπους, την οποία διατηρούν τα αξιώματα του Λουκασέβιτς και ο modus ponens, αποδεικνύει ότι ορισμένοι τύποι που θα έπρεπε να παράγονται δεν παράγονται, και ότι δεν περνά κανείς ούτε καν από τον (v1↓v2)(v_{1} \downarrow v_{2}) στον (¬¬v1↓v2)(\neg\neg v_{1} \downarrow v_{2}). Από αυτό έπεται η ανάγκη ενός δεύτερου κανόνα, της αντικατάστασης της διπλής άρνησης, με τον οποίο το επόμενο μάθημα συμπληρώνει το σύστημα.

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

  1. Να αναγνωρίζει τα στιγμιότυπα των σχημάτων A1, A2 και A3 και να κρίνει αν μια ακολουθία τύπων είναι παραγωγή από ένα σύνολο υποθέσεων.
  2. Να κατασκευάζει παραγωγές στο σύστημα του Λουκασέβιτς, με αξιώματα, υποθέσεις και modus ponens, και παραγωγές για παραγωγές με ανακλαστικότητα, μονοτονία, τομή, το θεώρημα της απαγωγής και το αντίστροφό του.
  3. Να αποδεικνύει τις δομικές ιδιότητες της παραγωγής και το θεώρημα της απαγωγής με ισχυρή επαγωγή στον αριθμό των γραμμών.
  4. Να θεμελιώνει αποδείξιμες ισοδυναμίες και να χρησιμοποιεί ότι η αποδείξιμη ισοδυναμία είναι ανακλαστική, συμμετρική και μεταβατική.
  5. Να αποδεικνύει ότι ένας τύπος δεν είναι παραγώγιμος μέσω μιας σήμανσης που διατηρούν τα αξιώματα και ο modus ponens, και να εξηγεί με αυτήν το όριο του συστήματος του Λουκασέβιτς στη γλώσσα με έναν μόνο σύνδεσμο και γιατί χρειάζεται ένας δεύτερος κανόνας.

Τι είναι ένα τυπικό παραγωγικό σύστημα

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

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

Αξιωματικά σχήματα και στιγμιότυπα

Τα συστήματα της προτασιακής λογικής δεν διατυπώνουν τα αξιώματά τους ένα προς ένα, επειδή είναι άπειρα, αλλά μέσω σχημάτων: εκφράσεων της μεταγλώσσας γραμμένων με μεταμεταβλητές, όπως το (φ→(ψ→φ))(\varphi \rightarrow (\psi \rightarrow \varphi)). Ένα σχήμα δεν είναι τύπος· είναι καλούπι. Ένα στιγμιότυπο του σχήματος είναι ο τύπος που προκύπτει όταν κάθε μεταμεταβλητή υποκατασταθεί από έναν τύπο με ομοιόμορφο τρόπο: όλες οι εμφανίσεις της ίδιας μεταμεταβλητής υποκαθίστανται από τον ίδιο τύπο, ενώ διαφορετικές μεταμεταβλητές μπορούν να λάβουν τον ίδιο τύπο ή διαφορετικούς τύπους.

ΠαράδειγμαΣτιγμιότυπα ενός σχήματος

Με φ:=v1\varphi := v_{1} και ψ:=¬v2\psi := \neg v_{2}, το σχήμα (φ→(ψ→φ))(\varphi \rightarrow (\psi \rightarrow \varphi)) δίνει το στιγμιότυπο (v1→(¬v2→v1))(v_{1} \rightarrow (\neg v_{2} \rightarrow v_{1}))· με φ:=(v1↓v2)\varphi := (v_{1} \downarrow v_{2}) και ψ:=(v1↓v2)\psi := (v_{1} \downarrow v_{2}), δίνει τον ((v1↓v2)→((v1↓v2)→(v1↓v2)))((v_{1} \downarrow v_{2}) \rightarrow ((v_{1} \downarrow v_{2}) \rightarrow (v_{1} \downarrow v_{2}))), επειδή τίποτε δεν εμποδίζει δύο μεταμεταβλητές να λάβουν τον ίδιο τύπο. Αντίθετα, ο (v1→(v2→v3))(v_{1} \rightarrow (v_{2} \rightarrow v_{3})) δεν είναι στιγμιότυπο αυτού του σχήματος: η πρώτη και η τελευταία εμφάνιση του φ\varphi θα λάμβαναν διαφορετικούς τύπους, και η υποκατάσταση δεν θα ήταν ομοιόμορφη. Κάθε στιγμιότυπο, όταν αναπτυχθούν οι συντομογραφίες, είναι μια συμβολοσειρά από κύκλους και δίσκους· το σχήμα, αντίθετα, ζει μόνο στη μεταγλώσσα.