Προτασιακός λογισμός

Ιστορική αναδρομή

Παρ'όλο που η προτασιακή λογική (που συχνά συγχέεται με τον προτασιακό λογισμό) έχει υπαινιχθεί από πρώιμους φιλόσοφους, αναπτύχθηκε σε επίσημη λογική από τον Χρύσιππο τον 3 αιώνα [1] και επεκτάθηκε από τους Στωικούς. Η λογική ήταν εστιασμένη στις προτάσεις. Η ανέλιξη αυτή ήταν διαφορετική από την παραδοσιακή συλλογιστική λογική που εστίαζε στους όρους. Δυστυχώς όμως στην αρχαιότητα τ,η προτασιακή λογική που είχε αναπτυχθεί από τους Στωικούς έπαψε να είναι κατανοητή. Συνεπώς αυτό το σύστημα ιδεών ουσιαστικά ανακαλύφτηκε εκ νέου από τον Πέτρο Αβελάρδο τον 12ο αιώνα.
Η προτασιακή Λογική βελτιώθηκε σταδιακά με την χρήση συμβόλων . Ο φιλόσοφος Γκότφριντ Λάιμπνιτς του 17ου-18ου αιώνα έχει αποτιμηθεί ως ο ιδρυτής της Συμβολικής Λογικής για την δουλειά του. Παρόλο που ήταν ο πρώτος που ασχολήθηκε με αυτό  το  είδος, δεν ήταν γνωστός στην τότε διαδεδομένη κοινότητα που ασχολούνταν με την λογική. Για αυτόν τον λόγο πολλές από τις ανακαλύψεις του, επαναδιατυπώθηκαν από άλλους λογικούς όπως  ο Τζορτζ Μπουλ και ο Αύγουστος ντε Μόργκαν. Όπως ήταν απόλυτα λογικό όμως, όλες οι επαναδιατυπώσεις ήταν απολύτως εξαρτημένες από τις διατυπώσεις και τις ανακαλύψεις του Leibniz.
Όπως η προτασιακή λογική θεωρείται σαν μια εξέλιξη της πρώιμης συλλογιστικής λογικής έτσι και η Κατηγορηματική Λογική του Γκότλομπ Φρέγκε ήταν μια εξέλιξη από την πρώιμη προτασιακή λογική. Ένας συγγραφέας περιγράφει την κατηγορηματική Λογική σαν αντικείμενο που συνδυάζει :  «τα διακριτά χαρακτηριστικά της συλλογιστικής και της προτασιακής λογικής».  Όπως ήταν φυσικό η Κατηγορηματική Λογικά ανήγγειλε μια νέα περιοχή στην ιστορία της Λογικής. Τα επόμενα χρόνια καινούριες ανακαλύψεις προστέθηκαν μετά τον Γκότλομπ Φρέγκε, μερικές από τις οποίες είναι και η Φυσική απαγωγή, τα συντακτικά δέντρα και οι πίνακες αληθείας. Η φυσική απαγωγή ανακαλύφθηκε από τον Gerhard Gentzen και Jan Łukasiewicz. Τα δέντρα αληθείας ανακαλύφτηκαν από τον  Evert Willem Beth.[5] Η ανακάλυψη των  πινάκων αληθείας, όμως παραμένει ως αντικείμενο αντιπαράθεσης ως προς το πρόσωπο που την πρωτοανακάλυψε.

Το κλείσιμο στο πλαίσιο των πράξεων

Η προτασιακή λογική είναι κλειστή  ως προς τους συνδέσμους της συνάρτησης αληθείας. Δηλαδή, για κάθε  πρόταση φ, η ¬φ έιναι  επίσης μια πρόταση. Ομοίως, για τυχόν προτάσεις φ και ψ,η φ ∧ ψ είναι μια πρόταση, και ομοίως για διάζευξη, για υπόθεση και για ισοδυναμία. Αυτό σημαίνει , για παράδειγμα, ότι η φ ∧ ψ όντας μια πρόταση,   μπορεί να είναι συνδεθεί με μια άλλη πρόταση. Για να το παραστήσουμε αυτό, πρέπει να χρησιμοποιήσουμε παρενθέσεις για να δείξουμε ποια πρόταση είναι συνδεδεμένη με ποια. Για παράδειγμα,η πρόταση  P ∧ Q ∧ R δεν είναι μια καλά σχηματισμένη φόρμουλα, γιατί δεν ξέρουμε αν είναι  συνένωση της P ∧ Q με την R ή αν είναι συνένωση της P με την Q ∧ R. Έτσι πρέπει να γράψουμε είτε (P ∧ Q ) ∧ R, για να εκπροσωπεί την πρώτη, ή P ∧ (Q ∧ R) για να εκπροσωπεί την τελευταία αντίστοιχα. Με την αξιολόγηση των συνθηκών αλήθειας, βλέπουμε ότι και οι δύο εκφράσεις έχουν τις ίδιες προϋποθέσεις αλήθειας (θα ισχύουν  στις ίδιες περιπτώσεις), και, επιπλέον, ότι οποιαδήποτε πρόταση που σχηματίζεται από αυθαίρετους συνδέσμους θα έχουν τις ίδιες προϋποθέσεις αλήθειας, ανεξάρτητα από τη θέση των παρενθέσεων. Αυτό σημαίνει ότι η σχέση είναι προσεταιριστική, ωστόσο, δεν θα πρέπει να υποθέσουμε ότι παρενθέσεις δεν εξυπηρετούν ποτέ ένα σκοπό. Για παράδειγμα, η πρόταση P ∧ (Q ∨ R) δεν έχει τις ίδιες προϋποθέσεις αλήθειας με την πρόταση (P ∧ Q) ∨ R, έτσι είναι διαφορετικές προτάσεις που διακρίνονται μόνο από τις παρενθέσεις.Αυτό μπορεί να ελεγθεί με τη μέθοδο του πίνακα αλήθειας που αναφέρεται παραπάνω.
Σημείωση: Για κάθε αυθαίρετο αριθμό  προτασιακών σταθερών, μπορούμε να σχηματίσουμε ένα πεπερασμένο αριθμό  περιπτώσεων στις οποίες παρατίθενται οι πιθανές τιμές αλήθειας τους. Ένας απλός τρόπος για να το δημιουργήσουμε αυτό, είναι οι πίνακες αλήθειας, στους οποίους πρώτα γράφουμε τα P, Q, ..., Z, για οποιαδήποτε λίστα  k προτασιακών σταθερών-δηλαδή, οποιαδήποτε λίστα προτασιακών σταθερών με καταχωρήσεις k και έπειτα γράφουμε 2k σειρές, και κάτω από το P συμπληρώνουμε το πρώτο μισό των σειρών με αληθές (ή Τ) και το δεύτερο μισό με ψευδή (ή F). Κάτω από το Q συμπληρώνουμε το ένα τέταρτο των σειρών με Τ, το επόμενο τέταρτο με F, το επόμενο τέταρτο με το Τ και το τελευταίο τέταρτο με F. Η επόμενη στήλη εναλάσσεται  μεταξύ αληθούς και ψευδούς σε κάθε όγδοη σειρά, στη συνέχεια στην δέκατη έκτη, και ούτω καθεξής, μέχρι την τελευταία προτασιακή σταθερά μεταβάλλεται μεταξύ Τ και F σε κάθε γραμμή. Αυτό θα δώσει μια πλήρη λίστα των περιπτώσεων ή αλλιώς τις πιθανές αναθέσεις τιμών αλήθειας για αυτές τις προτασιακές σταθερές.

Αποδείξεις στον προτασιακό λογισμό

Μία από τις κύριες χρήσεις του προτασιακού λογισμού, όταν
ερμηνεύθηκε για λογικές εφαρμογές, είναι να καθορίσει τις σχέσεις της λογικής
ισοδυναμίας μεταξύ προτασιακών τύπων. Αυτές οι σχέσεις προσδιορίζονται μέσω των
διαθέσιμων κανόνων μετασχηματισμού, οι αλληλουχίες των οποίων ονομάζονται
παράγωγα ή αποδείξεις.
Στη συζήτηση που θα ακολουθήσει, μια απόδειξη παρουσιάζεται
ως μια σειρά αριθμημένων γραμμών, με κάθε γραμμή να αποτελείται από ένα μόνο
τύπο που ακολουθείται από ένα λόγο ή δικαιολογία εισαγωγής του τύπου αυτού.
Κάθε υπόθεση του επιχειρήματος, δηλαδή, μια υπόθεση που εισάγεται ως μια
υπόθεση του επιχειρήματος, αναφέρεται στην αρχή της σειράς και χαρακτηρίζεται
ως "προϋπόθεση" αντί άλλων. Το συμπέρασμα είναι τοποθετημένο στην
τελευταία γραμμή. Μια απόδειξη είναι πλήρης αν κάθε γραμμή προκύπτει από τα
προηγούμενα με την ορθή εφαρμογή του κανόνα μετασχηματισμού. (Για μια αντίθεση
προσέγγιση, βλέπε απόδειξη δέντρα).

Γραφικός λογισμός

Είναι δυνατόν να γενικεύσουμε τον ορισμό μιας τυπικής
γλώσσας από ένα σύνολο  πεπερασμένων
αλληλουχιών σε μια πεπερασμένη βάση που περιλαμβάνει πολλά άλλα σύνολα
μαθηματικών δομών, εφ 'όσον αυτά έχουν κατασκευαστεί με πεπερασμένα μέσα από
πεπερασμένο υλικά. Επιπλέον, πολλές από αυτές τις οικογένειες των τυπικών δομών
είναι ιδιαίτερα καλά προσαρμοσμένες για χρήση στη λογική.
Για παράδειγμα, υπάρχουν πολλές οικογένειες από τα γραφήματα
που είναι αρκετά κοντά αναλογικά σε τυπικές γλώσσες που η έννοια του λογισμού
είναι αρκετά εύκολη και φυσικά εκτείνονται και σε αυτές. Πράγματι, πολλά είδη
γραφημάτων προκύπτουν ως αναλυση γραφημάτων στην συντακτική ανάλυση των
αντίστοιχων οικογενειών των δομών κειμένου. Οι απαιτήσεις της πρακτικής
υπολογισμού της τυπικών γλωσσών συχνά απαιτούν ότι οι συμβολοσειρές κειμένου
πρέπει  να μετατραπούν  σε  δομή δείκτη μεταγλωτιστή γραφημάτων, απλά
στην ουσία ελέγχουν εάν οι χορδές είναι καλά σχηματισμένες ή όχι. Μόλις γίνει
αυτό, υπάρχουν πολλά πλεονεκτήματα που μπορούν να προκύψουν από την ανάπτυξη
των γραφικών ανάλογιών του λογισμού στις χορδές. Η χαρτογράφηση από τα νήματα προς
ανάλυση γραφημάτων ονομάζεται ανάλυση και η αντίστροφη χαρτογράφηση ανάλυση
γραφημάτων σε χορδές επιτυγχάνεται με μια λειτουργία που ονομάζεται
διασχίζοντας τον γράφο.

Εναλλακτικοί Λογισμοί

Θεωρείται εφικτό να ορίσουμε μια διαφορετική έκδοση του προτασιακού λογισμού, η οποία θα καθορίζει τη σύνταξη των λογικών συντελεστών μέσα από τα αξιώματα, και χρησιμοποιεί μόνο ένα συμπέρασμα.

Άλλοι λογισμοί

Ο Προτασιακός λογισμός είναι το απλούστερο είδος λογισμού που χρησιμοποιείται . Μπορεί να επεκταθεί με διάφορους τρόπους. (Αριστοτελική συλλογιστική λογική , η οποία σε μεγάλο βαθμό αντικαταστάθηκε στη σύγχρονη λογική , είναι κατά κάποιο τρόπο πιο απλή - αλλά και σε άλλους τρόπους πιο περίπλοκη – από ότι ο προτασιακός λογισμός . ) Ο πιο άμεσος τρόπος για να αναπτυχθεί μια πιο σύνθετη λογική του λογισμού είναι να καθιερωθούν κανόνες που είναι συνδεδεμένοι  με πιο λεπτομερή στοιχεία πάνω στις προτάσεις που χρησιμοποιούνται .
Λογική πρώτης τάξης ( γνωστή και ως πρώτης τάξης λογική κατηγορήματος ) προκύπτει όταν οι «ατομικές προτάσεις" της προτασιακής λογικής χωρίζονται σε όρους , μεταβλητές , κατηγορήματα , και ποσοδείκτες , τηρώντας τους κανόνες της προτασιακής λογικής μαζί με κάποιους καινούριους. (Για παράδειγμα , από το " Όλα τα σκυλιά είναι θηλαστικά " μπορούμε να συμπεράνουμε « Αν ο Rover είναι ένα σκυλί τότε ο Rover είναι ένα θηλαστικό ».) Με τα εργαλεία της λογικής πρώτης τάξης είναι δυνατόν να διατυπωθεί μια σειρά από θεωρίες , είτε με ρητά αξιώματα, είτε από τους κανόνες του συμπεράσματος ,που μπορούν να αντιμετωπίζονται ως λογική λιθίασης . Η Αριθμητική είναι η πιο γνωστή από αυτές, άλλες περιλαμβάνουν τη θεωρία των συνόλων και mereology. Λογικές δεύτερης τάξης και άλλες λογικές ανώτερης τάξης είναι τυπικές επεκτάσεις της λογικής πρώτης τάξης. Έτσι, σε σύγκριση με αυτές της λογικές αναφερόμαστε στην προτασιακή λογική ως " λογική μηδενικής τάξεως".
Η Τροπική λογική προσφέρει επίσης μια ποικιλία των συμπερασμάτων που δεν μπορούν να σταματούν σε προτασιακού λογισμού. Για παράδειγμα, "κατ 'ανάγκη Χ" μπορούμε να συμπεράνουμε ότι θα ισχύει το Χ. Από Χ μπορούμε να συμπεράνουμε «Είναι πιθανό ότι Χ". Η μετάφραση μεταξύ των τρόπων μεταφοράς λογικής και αλγεβρικής λογικής δημιουργεί την κλασική και ενορατική λογική, αλλά με την εισαγωγή ενός μοναδιαίου τελεστή σε Boolean ή Heyting άλγεβρες, διαφορετικο από ενας Boolean τελεστή, ερμηνεύοντας την τροπικότητα δυνατότητα, και στην περίπτωση της Heyting άλγεβρα ένα δεύτερο φορέα για την ερμηνεία της αναγκαιότητας (στην Boolean άλγεβρα αυτή είναι περιττή αφού η αναγκαιότητα είναι η De Morgan διπλή της δυνατότητας). Ο πρώτος
φορέας διατηρεί το μηδέν και τη διάζευξη, ενώ ο δεύτερος διατηρεί το 1 και τον συνδυασμό
Λογικές πολλαπλής αποτίμησης είναι αυτές που επιτρέπουν οι προτάσεις να έχουν άλλες τιμές εκτός από αλήθεια και ψέμα. (Για παράδειγμα, καμιά από τις δύο είναι "έξτρα τιμές"-η "Λογική συνέχεια" επιτρέπει σε κάθε πρόταση να έχει οποιοδήποτε από έναν άπειρο αριθμό «βαθμών αλήθειας» μεταξύ αληθινού και το ψεύτικου.) Αυτές οι λογικές συχνά απαιτούν υπολογιστικές συσκευές, αρκετά διαφορετικές από του προτασιακού λογισμού. Όταν οι τιμές σχηματίζουν μια Boolean άλγεβρα (η οποία μπορεί να έχει περισσότερες από δύο ή ακόμα και απείρως πολλές τιμές), η λογική πολλαπλής αποτίμησης γίνεται κλασική λογική. Η λογική πολλαπλής αποτίμησης είναι επομένως ανεξάρτητου ενδιαφέροντος, όταν οι τιμές δημιουργούν μια άλγεβρα που δεν είναι Boolean.

Λύτες

Η εξεύρεση λύσεων σε τύπους προτασιακής λογική είναι ένα NP - πλήρες πρόβλημα . Ωστόσο, υπάρχουν πρακτικές μέθοδοι ( π.χ. , ο αλγόριθμος DPLL , 1962 – αλγόριθμος «άχυρο», 2001), που είναι πολύ γρήγορες για πολλές χρήσιμες περιπτώσεις . Πρόσφατες εργασίες έχουν επεκτείνει  τους αλγόριθμους SAT να δουλεύουν με προτάσεις που περιέχουν αριθμητικές εκφράσεις - αυτές είναι οι λύτες SMT .