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

Σημασιολογία της προτασιακής λογικής

Περίληψη

Ως εδώ οι τύποι ήταν συμβολοσειρές κύκλων και δίσκων, και οι παραγωγές χειρισμοί συμβολοσειρών: για την αλήθεια τους δεν ειπώθηκε τίποτα. Αυτό το μάθημα τους δίνει σημασία. Μια αποτίμηση αποδίδει σε κάθε μεταβλητή μία από τις δύο τιμές αλήθειας, 11 (αληθές) και 00 (ψευδές), και επεκτείνεται σε όλους τους τύπους με μοναδικό τρόπο, με αναδρομή πάνω στην πολυπλοκότητά τους, με έναν μόνο όρο: ο (φ↓ψ)(\varphi \downarrow \psi) παίρνει την τιμή 11 ακριβώς όταν οι φ\varphi και ψ\psi παίρνουν την τιμή 00. Από αυτόν τον όρο και από τις επίσημες συντομογραφίες υπολογίζονται, χωρίς να οριστεί τίποτε άλλο, οι τιμές της άρνησης, της διάζευξης, της σύζευξης, της συνεπαγωγής, της διπλής συνεπαγωγής και της αποκλειστικής διάζευξης. Το λήμμα σύμπτωσης, που αποδεικνύεται με επαγωγή στην πολυπλοκότητα, εξασφαλίζει ότι η τιμή ενός τύπου εξαρτάται μόνο από τις τιμές των μεταβλητών του· από αυτό έπεται ότι ο πίνακας αληθείας, με 2n2^n γραμμές για nn μεταβλητές, περιέχει ό,τι μπορούν να πουν για τον τύπο οι άπειρες αποτιμήσεις. Με αυτά ορίζονται η ικανοποίηση, η εγκυρότητα, η ικανοποιησιμότητα, η αντίφαση και η ενδεχομενικότητα, καθορίζονται οι τύποι ⊤\top και ⊥\bot, και τίθεται το πρόβλημα της απόφασης για την εγκυρότητα, που οι πίνακες το λύνουν με κόστος που αυξάνεται εκθετικά με το πλήθος των μεταβλητών.

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

  1. Να υπολογίζει την τιμή αλήθειας ενός τύπου κάτω από μια αποτίμηση μέσω της αναδρομικής της επέκτασης, και να εξάγει από τις επίσημες συντομογραφίες την τιμή κάθε παράγωγου συνδέσμου.
  2. Να αποδεικνύει με επαγωγή στην πολυπλοκότητα το λήμμα σύμπτωσης, και να εξηγεί με αυτό γιατί ένας πίνακας αληθείας με 2n2^n γραμμές αρκεί για τη μελέτη ενός τύπου με nn μεταβλητές.
  3. Να κατασκευάζει πίνακες αληθείας στήλη προς στήλη και να ταξινομεί τύπους ως έγκυρους, ενδεχομενικούς ή αντιφάσεις, και σύνολα τύπων ως ικανοποιήσιμα ή μη ικανοποιήσιμα, χωρίς να συγχέει το ⊭φ\not\models \varphi με την αντίφαση.
  4. Να κρίνει την εγκυρότητα ενός τύπου αναζητώντας μια αποτίμηση που τον διαψεύδει, και να εκτιμά το κόστος της μεθόδου των πινάκων ως συνάρτηση του πλήθους των μεταβλητών.

Η σημασία των τύπων

Η ενότητα για τη γλώσσα κατασκεύασε, στο μάθημα για τη γλώσσα της προτασιακής λογικής, ένα σύνολο συμβολοσειρών δύο συμβόλων, και η ενότητα για τον συμπερασμό δίδαξε πώς να παίρνουμε συμβολοσειρές από άλλες με αξιώματα και κανόνες. Καμία από τις δύο δεν μίλησε για αλήθεια: το παραγωγικό σύστημα μετασχηματίζει σύμβολα σύμφωνα με τη μορφή τους, όπως μια μηχανή που δεν καταλαβαίνει τι γράφει. Όμως η γλώσσα κατασκευάστηκε για να παριστάνει αποφάνσεις, και το μάθημα για την τυποποίηση της φυσικής γλώσσας τους απέδωσε άτυπες αναγνώσεις: ο (φ↓ψ)(\varphi \downarrow \psi) είναι αληθής όταν οι φ\varphi και ψ\psi είναι και οι δύο ψευδείς, και οι αναγνώσεις των άλλων συνδέσμων εξήχθησαν από αυτήν. Η σημασιολογία μετατρέπει αυτές τις αναγνώσεις σε μαθηματικούς ορισμούς.

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

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