Τυποποίηση της φυσικής γλώσσας

Από την απόφανση στον τύπο

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

Μια απόφανση, με την έννοια αυτού του μαθήματος, είναι μια διατύπωση που δηλώνει κάτι και που, μέσα στα συμφραζόμενά της, είναι αληθής ή ψευδής: «Το νερό βράζει στους εκατό βαθμούς στο επίπεδο της θάλασσας», «Η Άννα άργησε», «Ο $7$ είναι πρώτος». Οι ερωτήσεις, οι προσταγές και οι ευχές («Άργησε η Άννα;», «Κλείσε την πόρτα», «Μακάρι να βρέξει») δεν είναι αποφάνσεις. Μια απόφανση είναι σύνθετη όταν περιέχει άλλες αποφάνσεις ενωμένες με μόρια όπως «δεν», «και», «ή», «αν… τότε»· είναι ατομική όταν δεν αναλύεται έτσι. Η προτασιακή λογική δεν αναλύει το εσωτερικό των ατομικών αποφάνσεων: γι' αυτήν, η «Η Άννα άργησε» είναι ένα αδιαίρετο κομμάτι, που μπορεί μόνο να είναι αληθές ή ψευδές.

Η σύμβαση των γραμμάτων

Οι τύποι της βασικής γλώσσας είναι συμβολοσειρές από κύκλους και δίσκους· η $n$-οστή μεταβλητή είναι η $v_n = \sigO^{n}\sigI$, δηλαδή $n$ κύκλοι που ακολουθούνται από έναν δίσκο. Το να γράφει κανείς τέτοιες συμβολοσειρές είναι τόσο ασφαλές όσο και κουραστικό, και για την τυποποίηση χρειαζόμαστε σύντομα ονόματα. Υιοθετούμε την εξής σύμβαση, που ισχύει σε αυτό το μάθημα και σε όλο τον υπόλοιπο κύκλο μαθημάτων, εκτός αν δηλωθεί ρητά το αντίθετο:

Αν αυτό ισχύει, τα λατινικά γράμματα $p$, $q$, $r$, $s$ και $t$ είναι ονόματα πέντε καθορισμένων μεταβλητών, όπως ο $7$ είναι το όνομα ενός καθορισμένου αριθμού: η $p$ δεν μεταβάλλεται, αλλά δηλώνει πάντα τη συμβολοσειρά $\sigO\sigI$. Τα ελληνικά γράμματα $\varphi$, $\psi$, $\chi$ και $\theta$, αντίθετα, παραμένουν μεταμεταβλητές, όπως στο μάθημα για τη γλώσσα: δηλώνουν οποιουσδήποτε τύπους, και μια έκφραση γραμμένη με αυτά, όπως ο $(\varphi \downarrow \psi)$, είναι ένα σχήμα που περιλαμβάνει άπειρους τύπους. Από αυτό έπεται μια διαφορά που έχει σημασία: ο $(p \downarrow q)$ είναι ένας μόνο τύπος, η συμβολοσειρά $\sigI\sigO\sigI\sigO\sigO\sigI$· ο $(\varphi \downarrow \psi)$ είναι μια μορφή τύπων, της οποίας οι $(p \downarrow q)$, $(p \downarrow p)$ και $(q \downarrow (p \downarrow r))$ είναι περιπτώσεις. Μερικά κείμενα χρησιμοποιούν τα $p$ και $q$ ως μεταμεταβλητές· εδώ όχι, γιατί στην τυποποίηση χρειαζόμαστε δύο διαφορετικά γράμματα να δηλώνουν με βεβαιότητα διαφορετικές μεταβλητές, και μια μεταμεταβλητή δεν προσφέρει αυτή την εγγύηση: τίποτα δεν εμποδίζει τις $\varphi$ και $\psi$ να δηλώνουν τον ίδιο τύπο.

Το λεξικό μιας τυποποίησης

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