Η μέθοδος της επίλυσης

Το μάθημα για τη σημασιολογία της προτασιακής λογικής έδειξε ότι η εγκυρότητα και η ικανοποιησιμότητα είναι αποκρίσιμες μέσω του πίνακα αληθείας, με κόστος που διπλασιάζεται με κάθε μεταβλητή, και προανήγγειλε μεθόδους που δεν θα απαιτούσαν να τον διατρέξουμε. Το μάθημα για τη σημασιολογική συνέπεια και ισοδυναμία ανήγαγε κάθε συνέπεια σε μη ικανοποιησιμότητα: $\Gamma \models \varphi$ αν και μόνο αν το $\Gamma \cup \{\neg\varphi\}$ είναι μη ικανοποιήσιμο. Τα μαθήματα για τις κανονικές μορφές και για τον αλγόριθμό τους έδωσαν σε κάθε τύπο μια συζευκτική μορφή, της οποίας η εγκυρότητα φαίνεται με μια ματιά, αλλά η ικανοποιησιμότητα δεν φαίνεται. Αν αυτό ισχύει, λείπει μια διαδικασία που να αποφασίζει τη μη ικανοποιησιμότητα μιας σύζευξης φράσεων δρώντας πάνω στις ίδιες τις φράσεις. Αυτή η διαδικασία είναι η επίλυση, που πρότεινε ο John Alan Robinson το 1965 πάνω σε ιδέες των Martin Davis και Hilary Putnam (1960)· είναι ο πυρήνας των προγραμμάτων που σήμερα αποφασίζουν την ικανοποιησιμότητα τύπων με εκατομμύρια μεταβλητές. Σε αντίθεση με το σύστημα της ενότητας του συμπερασμού, του οποίου τις σχέσεις με τη σημασιολογία μελετούν τα μαθήματα για την ορθότητα και την πληρότητα και για το θεώρημα της συμπάγειας, η επίλυση δεν παράγει συμπεράσματα: διαψεύδει σύνολα. Αυτό το μάθημα αποδεικνύει ότι το κάνει με τρόπο ορθό και πλήρη.

Όπως στα προηγούμενα μαθήματα, τα $p$, $q$, $r$, $s$ και $t$ ονομάζουν τις μεταβλητές $v_1$ έως $v_5$· το γράμμα $v$ χωρίς δείκτη, και επίσης το $w$, δηλώνουν αποτιμήσεις· και το $V(\varphi)$ είναι το σύνολο των μεταβλητών του $\varphi$.

Φράσεις και σύνολα φράσεων

Υπενθυμίζεται από το μάθημα για τις κανονικές μορφές ότι ένα λεκτικό είναι μια μεταβλητή ή η άρνηση μιας μεταβλητής, και ότι το αντίθετο ενός λεκτικού $\ell$, που γράφεται $\ell^{*}$, είναι το λεκτικό της ίδιας μεταβλητής με το άλλο πρόσημο· δύο αντίθετα λεκτικά σχηματίζουν ένα συμπληρωματικό ζεύγος. Από το λήμμα της άρνησης ενός λεκτικού, $v(\ell^{*}) = 1 - v(\ell)$ για κάθε αποτίμηση $v$. Εκεί μια φράση ήταν μια διάζευξη λεκτικών· εδώ συμφέρει να ξεχάσουμε τη σειρά και τις επαναλήψεις, που δεν αλλάζουν την τιμή, και να κρατήσουμε το σύνολο.

Μια φράση είναι ένα πεπερασμένο σύνολο λεκτικών. Η φράση χωρίς λεκτικά λέγεται κενή φράση και γράφεται $\Box$. Μια αποτίμηση $v$ ικανοποιεί μια φράση $C$, και γράφεται $v \models C$, αν κάποιο λεκτικό της $C$ έχει τιμή $1$ στην $v$· σε αντίθετη περίπτωση, η $v$ τη διαψεύδει. Μια φράση με ένα μόνο λεκτικό λέγεται μοναδιαία. Οι μεταβλητές μιας φράσης σχηματίζουν το σύνολο $V(C)$· οι μεταβλητές ενός συνόλου $S$ φράσεων, το σύνολο $V(S)$, ένωση των προηγούμενων. Μια αποτίμηση ικανοποιεί ένα σύνολο $S$ φράσεων, $v \models S$, αν ικανοποιεί καθεμία από τις φράσεις του· το $S$ είναι ικανοποιήσιμο αν κάποια αποτίμηση το ικανοποιεί, και μη ικανοποιήσιμο σε αντίθετη περίπτωση. Τέλος, αν το $S$ είναι ένα σύνολο φράσεων και η $C$ μια φράση, το $S \models C$ σημαίνει ότι κάθε αποτίμηση που ικανοποιεί το $S$ ικανοποιεί την $C$.

Δύο ακραίες περιπτώσεις έπονται από τον ορισμό και αξίζει να τις σημειώσουμε. Η κενή φράση δεν έχει λεκτικά· επομένως, κανένα λεκτικό της δεν έχει τιμή $1$, και καμία αποτίμηση δεν την ικανοποιεί: η $\Box$ είναι μη ικανοποιήσιμη, και κάθε σύνολο που την περιέχει επίσης. Το κενό σύνολο φράσεων, αντίθετα, δεν έχει φράσεις προς ικανοποίηση, και κάθε αποτίμηση το ικανοποιεί. Δεν πρέπει να συγχέονται: το $\{\Box\}$ είναι μη ικανοποιήσιμο και το $\emptyset$ ικανοποιείται από όλες τις αποτιμήσεις.

Μια φράση που περιέχει ένα συμπληρωματικό ζεύγος λέγεται ταυτολογική: δεν επιβάλλει καμία συνθήκη, και μπορεί να αφαιρεθεί από οποιοδήποτε σύνολο χωρίς να αλλάξουν τα μοντέλα του. Το να γράφουμε τις φράσεις ως σύνολα δεν είναι ιδιοτροπία του συμβολισμού. Αν από τις $(p \vee q)$ και $(p \vee \neg q)$ θέλουμε να πάρουμε το $p$, η διάζευξη δίνει $(p \vee p)$, που είναι ισοδύναμος με τον $p$ αλλά δεν είναι ο ίδιος τύπος· με σύνολα, $\{p\} \cup \{p\} = \{p\}$, και η συγχώνευση των επαναλαμβανόμενων λεκτικών γίνεται από μόνη της.