Λογική πρώτου βαθμού
Η λογική πρώτου βαθμού είναι μια τυπική λογική που χρησιμοποιείται στα μαθηματικά, τη φιλοσοφία, τη γλωσσολογία και την επιστήμη υπολογιστών. Συναντάται με διάφορα ονόματα, όπως κατηγορηματικός λογισμός πρώτου βαθμού ή κατηγορηματική λογική. Η πρωτοβάθμια λογική διαφέρει από την προτασιακή λογική στη χρήση ποσοτικών τελεστών: κάθε ερμηνεία της λογικής πρώτου βαθμού περιλαμβάνει ένα πεδίο τιμών όπου κυμαίνονται οι ποσοτικοί τελεστές.
Υπάρχουν πολλά συμπερασματικά συστήματα για την πρωτοβάθμια λογική που είναι συνεπή (παράγουν μόνο σωστά αποτελέσματα) και πλήρη (ικανά να παράγουν οποιαδήποτε ορθή πρόταση). Αν και η σχέση λογικής συνέπειας είναι μόνο ημι-αποφασίσιμη, έχει επιτευχθεί μεγάλη πρόοδος στην αυτόματη απόδειξη θεωρημάτων για τη λογική πρώτου βαθμού. Η λογική πρώτου βαθμού ικανοποιεί επίσης αρκετά θεωρήματα μετα-λογικής που την κάνουν επιδεκτική ανάλυσης στην θεωρία αποδείξεων, όπως το Θεώρημα Λόβενχαϊμ-Σκόλεμ και το θεώρημα συμπαγείας.
Η λογική πρώτου βαθμού έχει μεγάλη σημασία για τα θεμέλια των μαθηματικών, όπου αποτελεί την πρότυπη τυπική λογική για αξιωματικά συστήματα. Έχει ικανή εκφραστική ισχύ ώστε να μπορεί να διατυπώσει δύο σημαντικές μαθηματικές θεωρίες: τη Θεωρία συνόλων Ζερμέλο-Φράνκελ και την (πρωτοβάθμια) αριθμητική Πεάνο. Εντούτοις, κανένα αξιωματικό σύστημα στην πρωτοβάθμια λογική δεν είναι αρκετά ισχυρό ώστε να περιγράψει κατηγορικά άπειρες δομές όπως οι φυσικοί αριθμοί ή η γραμμή των πραγματικών. Κατηγορικά αξιωματικά συστήματα για τέτοιες δομές μπορούν να παραχθούν σε ισχυρότερες λογικές όπως η λογική δευτέρου βαθμού.
Εισαγωγή
[Επεξεργασία | επεξεργασία κώδικα]Ενώ η προτασιακή λογική ασχολείται με απλές δηλωτικές προτάσεις, η λογική πρώτου βαθμού καλύπτει επιπρόσθετα κατηγορήματα και ποσοτικοποιήσεις.
Ένα κατηγόρημα παίρνει μία οντότητα ή οντότητες από το πεδίο τιμών (domain of discourse) ως εισόδους ή εξόδους, είτε Αληθείς είτε Ψευδείς. Θεωρήστε τις δύο προτάσεις "Ο Σωκράτης είναι φιλόσοφος" και "Ο Πλάτωνας είναι φιλόσοφος". Στην προτασιακή λογική, αυτές οι προτάσεις θεωρούνται διαφορετικές μεταξύ τους και συμβολίζονται, για παράδειγμα, ως p και q. Ωστόσο, το κατηγόρημα "είναι φιλόσοφος" εμφανίζεται και στις δύο προτάσεις, οι οποίες έχουν την κοινή δομή "κάποιος είναι φιλόσοφος". Η μεταβλητή κάποιος αρχικοποιείται ως "Σωκράτης" στην πρώτη πρόταση και ως "Πλάτωνας" στη δεύτερη. Η χρήση των κατηγορημάτων, όπως το "είναι φιλόσοφος" σε αυτό το παράδειγμα, διακρίνει τη λογική πρώτου βαθμού από την προτασιακή λογική.
Τα κατηγορήματα μπορούν να συγκριθούν. Σκεφτείτε, για παράδειγμα, τον τύπο πρώτου βαθμού "Εάν κάποιος είναι φιλόσοφος, τότε κάποιος είναι διανοούμενος." Αυτός ο τύπος είναι μία δήλωση υπό όρους, με το "κάποιος είναι φιλόσοφος" να είναι η υπόθεση και το "κάποιος είναι διανοούμενος" ως συμπέρασμα. Η αλήθεια αυτού του τύπου εξαρτάται από το ποιο αντικείμενο δηλώνεται ως κάποιος και από την ερμηνεία των κατηγορημάτων "είναι φιλόσοφος" και "είναι διανοούμενος".
Οι μεταβλητές μπορούν να ποσοτικοποιηθούν. Η μεταβλητή κάποιος στον προηγούμενο τύπο μπορεί να ποσοτικοποιηθεί, για παράδειγμα, στην πρόταση πρώτου βαθμού "Για κάθε κάποιον, εάν κάποιος είναι φιλόσοφος, τότε κάποιος είναι διανοούμενος". Ο παγκόσμιος ποσοδείκτης "Για κάθε" σε αυτή την πρόταση, εκφράζει την ιδέα ότι ο ισχυρισμός "Εάν κάποιος είναι φιλόσοφος, τότε κάποιος είναι διανοούμενος." ισχύει για όλες τις επιλογές του κάποιου.
Η άρνηση της πρότασης "Για κάθε κάποιον, εάν κάποιος είναι φιλόσοφος, τότε ο κάποιος είναι διανοούμενος." είναι λογικά ισοδύναμο με την πρόταση "Υπάρχει κάποιος τέτοιος ώστε κάποιος είναι φιλόσοφος και δεν είναι διανοούμενος." Ο υπαρξιακός ποσοδείκτης "Υπάρχει" εκφράζει την ιδέα ότι ο ισχυρισμός "Κάποιος είναι φιλόσοφος και δεν είναι διανοούμενος" ισχύει για μερικές επιλογές του κάποιου.
Τα κατηγορήματα "είναι φιλόσοφος" και "είναι διανοούμενος" το καθένα έχουν μια μεταβλητή. Τα κατηγορήματα μπορούν να πάρουν αρκετές μεταβλητές. Στην έκφραση πρώτου βαθμού "Ο Σωκράτης είναι ο δάσκαλος του Πλάτωνα", το κατηγόρημα "είναι δάσκαλος του" παίρνει δύο μεταβλητές.
Για να ερμηνεύσει κανείς έναν τύπο πρώτου βαθμού, πρέπει πρώτα να κατανοήσει το κατηγόρημα και τις οντότητες τις οποίες χρησιμοποιούν οι μεταβλητές. Αυτές οι οντότητες είναι από το πεδίο τιμών, το οποίο συνήθως είναι ένα μη κενό σύνολο. Δεδομένου ότι η ερμηνεία με το πεδίο τιμών, που αποτελείται από όλα τα ανθρώπινα όντα και το κατηγόρημα "είναι φιλόσοφος" νοείται ως "έχουν γράψει τη Δημοκρατία", η πρόταση "Υπάρχει κάποιος που είναι φιλόσοφος" είναι αληθής, όπως αποδεικνύεται από τον Πλάτωνα.
Σύνταξη
[Επεξεργασία | επεξεργασία κώδικα]Υπάρχουν δύο βασικά τμήματα της λογικής πρώτου βαθμού. Η σύνταξη καθορίζει ποιες συλλογές των συμβόλων είναι επιτρεπτές εκφράσεις στη λογική πρώτου βαθμού, ενώ η σημασιολογία καθορίζει τις έννοιες πίσω από αυτές τις εκφράσεις.
Αλφάβητο
[Επεξεργασία | επεξεργασία κώδικα]Σε αντίθεση με τις φυσικές γλώσσες, όπως τα αγγλικά, η γλώσσα της λογικής πρώτου βαθμού είναι εντελώς τυπική, έτσι ώστε να μπορεί να προσδιοριστεί μηχανικά κατά πόσον μια δεδομένη έκφραση είναι επιτρεπτή. Υπάρχουν δύο βασικά είδη των επιτρεπτών εκφράσεων: όροι, οι οποίοι αντιπροσωπεύουν διαισθητικά αντικείμενα, και τύπους που διαισθητικά εκφράζουν κατηγορήματα που μπορεί να είναι αληθή ή ψευδή. Οι όροι και οι τύποι της λογικής πρώτου βαθμού είναι σειρές από σύμβολα που σχηματίζουν μαζί το αλφάβητο της γλώσσας. Όπως συμβαίνει με όλες τις τυπικές γλώσσες , η φύση των ίδιων των συμβόλων είναι εκτός του πεδίου εφαρμογής της τυπικής λογική: συχνά θεωρούνται απλώς ως γράμματα και σημεία στίξης.
Συχνά τα σύμβολα του αλφαβήτου διαιρούνται σε λογικά σύμβολα, τα οποία έχουν πάντοτε την ίδια σημασία, και μη λογικά σύμβολα, η σημασία των οποίων ποικίλλει ανάλογα με την ερμηνεία. Για παράδειγμα, το λογικό σύμβολο πάντα αντιπροσωπεύει "και" ποτέ δεν ερμηνεύεται ως "ή". Από την άλλη πλευρά, ένα μη-λογικό σύμβολο κατηγόρημα όπως ο Phil (x) θα μπορούσε να ερμηνευθεί ως "το x είναι ένας φιλόσοφος", "το x είναι ένας άνθρωπος που ονομάζεται Philip", ή οποιοδήποτε άλλο μοναδιαίο κατηγόρημα, ανάλογα με την εκάστοτε ερμηνεία .
Λογικά σύμβολα
[Επεξεργασία | επεξεργασία κώδικα]Υπάρχουν πολλά λογικά σύμβολα στο αλφάβητο, τα οποία μπορεί να διαφέρουν ανάλογα με τον συγγραφέα αλλά συνήθως περιλαμβάνουν:
- Τα σύμβολα ποσοδεικτών και .
- Οι λογικοί σύνδεσμοι: για σύζευξη, για διάζευξη, για συνεπαγωγή, για ισοδυναμία, για άρνηση. Περιστασιακά, χρησιμοποιούνται άλλοι συμβολισμοί για τους λογικούς συνδέσμους. Κάποιοι συγγραφείς χρησιμοποιούν , ή Cpq, αντί για και , ή Epq, αντί για , ειδικά σε περιβάλλοντα όπου χρησιμοποιείται για άλλους λόγους. Επιπλέον, το πέταλο μπορεί να αντικαταστήσει το , το τριπλό ίσον μπορεί να αντικαταστήσει το ,και η περισπωμένη (~), Np ή Fpq μπορούν να αντικαταστήσουν το , , ή Apq αντικαθιστά το , και &, Kpq, ή η μεσαία τελεία, ⋅, μπορούν να αντικαταστήσουν το , ειδικά εάν αυτά τα σύμβολα δεν είναι διαθέσιμα για τεχνικούς λόγους. (Σημείωση: Τα προαναφερθέντα σύμβολα Cpq, Epq, Np, Apq, και Kpq χρησιμοποιούνται στην Πολωνική σημειογραφία.)
- Οι παρενθέσεις, οι αγκύλες και άλλα σημεία της στίξης. Η επιλογή αυτών των συμβόλων ποικίλλει ανάλογα με τα συμφραζόμενα.
- Ένα άπειρο σύνολο μεταβλητών, που συχνά συμβολίζεται από πεζά γράμματα της αλφαβήτου x,y,z,...Οι δείκτες χρησιμοποιούνται συχνά για να ξεχωρίζουν οι μεταβλητές: ,, , ...
- Ένα σύμβολο ισότητας (καμιά φορά και το ταυτοτικό σύμβολο) = , βλέπε παρακάτω την ενότητα για την ισότητα.
Τα σύμβολα αυτά δεν χρειάζονται όλα. Μόνο ένα από τους ποσοδείκτες, την άρνηση και τη σύζευξη, τις μεταβλητές, τις αγκύλες και την ισότητα αρκούν. Υπάρχουν πολλές μικρές παραλλαγές που μπορούν να καθορίσουν πρόσθετα λογικά σύμβολα:
- Μερικές φορές οι σταθερές της αληθείας T, Vpq ή ⊤ για το "αληθές" και F, Opq, ή ⊥, για το "ψευδές" περιλαμβάνονται. Χωρίς κάποιον από τους λογικούς τελεστές του σθένους 0, αυτές οι δύο σταθερές μπορούν να εκφραστούν μόνο χρησιμοποιώντας ποσοδείκτες.
- Κάποιοι επιπλέον λογικοί σύνδεσμοι περιλαμβάνονται, όπως το "Sheffer stroke", Dpq (NAND), και το αποκλειστικό ή, Jpq.
Μη-λογικά σύμβολα
[Επεξεργασία | επεξεργασία κώδικα]Τα μη λογικά σύμβολα αντιπροσωπεύουν κατηγορήματα (σχέσεις), συναρτήσεις και σταθερές σχετικά με τον τομέα του λόγου. Συνήθως χρησιμοποιείται ένα σταθερό, άπειρο σύνολο μη λογικών συμβόλων για όλες τις περιπτώσεις. Μια πιο πρόσφατη πρακτική είναι να χρησιμοποιηθούν διαφορετικά μη λογικά σύμβολα ανάλογα με την εφαρμογή που έχει κανείς στο μυαλό. Ως εκ τούτου, έχει καταστεί αναγκαίο να αναφέρουμε το σύνολο όλων των μη λογικών συμβόλων που χρησιμοποιούνται σε μια συγκεκριμένη εφαρμογή. Η επιλογή γίνεται μέσω της υπογραφής. [1]
Η παραδοσιακή προσέγγιση είναι να υπάρχει μόνο ένα, άπειρο, σύνολο μη-λογικών συμβόλων (μία υπογραφή) για όλες τις εφαρμογές. Κατά συνέπεια, σύμφωνα με την παραδοσιακή προσέγγιση υπάρχει μόνο μία γλώσσα της λογικής πρώτου βαθμού. [2] Η προσέγγιση αυτή εξακολουθεί να χρησιμοποιείται, ειδικά σε φιλοσοφικά βιβλία.
- Για κάθε ακέραιο n ≥ 0 υπάρχει μια συλλογή από n- οστες , ή n - θέσεις, κατηγορηματικών συμβόλων. Επειδή αντιπροσωπεύουν τις σχέσεις μεταξύ των n στοιχείων, καλούνται επίσης σύμβολα σχέσης. Για κάθε τάξη του n έχουμε μια άπειρο πλήθος:
- P n 0, P n 1,P n2 , P n 3, ...
- Για κάθε ακέραιο n ≥ 0 υπάρχουν άπειρα n-οστά σύμβολα συναρτήσεις:
- f n 0, f n 1,f n2 f n 3, ...
Στη σύγχρονη μαθηματική λογική, η υπογραφή ποικίλει ανάλογα με την εφαρμογή. Τυπικά υπογραφές στα μαθηματικά είναι {1, Χ} ή απλά {Χ} για ομάδες , ή {0, 1, +, ×, <} για διατεταγμένα σώματα . Δεν υπάρχουν περιορισμοί σχετικά με τον αριθμό των μη-λογικών συμβόλων. Η υπογραφή μπορεί να είναι κενό , πεπερασμένο ή άπειρο, ακόμα μη μετρήσιμο . Μη μετρήσιμες υπογραφές εμφανίζονται για παράδειγμα σε σύγχρονες αποδείξεις του θεωρήματοςΛόβενχαϊμ-Σκόλεμ.
- Σε αυτή την προσέγγιση, κάθε μη λογικό σύμβολο είναι ένα από τα ακόλουθα:Ένα κατηγορηματικό σύμβολο (ή σύμβολο σχέσης) με κάποια βαρύτητα (σειρά επιχειρημάτων) μεγαλύτερη ή ίση του 0. Αυτά συνήθως συμβολίζονται με κεφαλαία γράμματα P,Q,R,..
- Οι σχέσεις σθένους 0 μπορούν να ταυτιστούν με τις προτασιακές μεταβλητές.
- Για παράδειγμα, το P, μπορεί να είναι δήλωση για οποιαδήποτε πρόταση.Για παράδειγμα,το P(x) είναι μία κατηγορηματική μεταβλητή σθένους 1.Μια πιθανή ερμηνεία είναι "ο χ είναι άνθρωπος".
- Το Q(x,y) είναι μία κατηγορηματική μεταβλητή σθένους 2. Οι πιθανές ερμηνείες του είναι "ο χ είναι μεγαλύτερος από τον y" και "ο χ είναι ο πατέρας του y".
2. Ένα σύμβολο συνάρτηση, με κάποια βαρύτητα μεγαλύτερη ή ίση με μηδέν. Αυτές συχνά συμβολίζονται με πεζά γράμματα f, g, h, ....
- Παραδείγματα: f (x) μπορεί να ερμηνευθούν ως "ο πατέρας του x". Στην αριθμητική , μπορεί να αναπαριστά το "-x". Στη θεωρία των συνόλων , μπορεί να αναπαριστά «το πλήθος συνόλων του x ". Στην αριθμητική, g (x, y) μπορεί αναπαριστά την έκφραση "χ + γ". Στη θεωρία των συνόλων, μπορεί να αναφέρει «την ένωση των x και y".
- Σύμβολα συναρτήσεις βαρύτητας 0 ονομάζονται σύμβολα σταθερές , και συχνά συμβολίζονται με τα πρώτα πεζά γράμματα του αλφαβήτου α, β, γ, .... Το σύμβολο α μπορεί να συμβολίζει τον Σωκράτη. Στην αριθμητική, μπορεί να συμβολίζει το 0. Στη θεωρία των συνόλων, μια τέτοια σταθερά μπορεί να αναφέρεται στο κενό σύνολο.
Η παραδοσιακή προσέγγιση μπορεί να αναχθεί στη σύγχρονη προσέγγιση απλά καθορίζοντας την "δημιουργό" υπογραφή ώστε να αποτελείται από παραδοσιακές ακολουθίες μη λογικών συμβόλων.
Κανόνες σχηματισμού
[Επεξεργασία | επεξεργασία κώδικα]Οι κανόνες σχηματισμού καθορίζουν τους όρους και τους τύπους της λογικής πρώτου βαθμού. Όταν οι όροι και οι τύποι αναπαριστώνται ως ακολουθίες συμβόλων, οι κανόνες αυτοί μπορεί να χρησιμοποιηθούν για να δημιουργηθεί μια τυπική γραμματική για τους όρους και τους τύπους. Αυτοί οι κανόνες είναι γενικά χωρίς συμφραζόμενα (κάθε παραγωγή έχει ένα μόνο σύμβολο στην αριστερή πλευρά), εκτός του ότι το σύνολο των συμβόλων μπορεί να είναι άπειρο και μπορεί να υπάρχουν πολλά σύμβολα έναρξης, για παράδειγμα, οι μεταβλητές στην περίπτωση των όρων .
Όροι
[Επεξεργασία | επεξεργασία κώδικα]Το σύνολο των όρων ορίζεται επαγωγικά από τους παρακάτω κανόνες:
- Μεταβλητές. Κάθε μεταβλητή είναι ένας όρος.
- Συναρτήσεις. Οποιαδήποτε έκφραση f(t1,...,tn) από n επιχειρήματα (όπου κάθε επιχείρημα ti είναι ένας όρος και f είναι ένα συναρτησιακό σύμβολο σθένους n) είναι ένας όρος. Πιο συγκεκριμένα, τα σύμβολα που δηλώνουν μεμονωμένες σταθερές είναι συναρτησιακά σύμβολα βαθμού 0, και άρα είναι όροι.
Μόνο οι εκφράσεις οι οποίες μπορούν να ληφθούν από πολλές εφαργμογές των κανόνων 1 και 2 είναι όροι. Για παράδειγμα, καμία έκφραση που περιέχει κατηγορηματικό σύμβολο είναι όρος.
Τύποι
[Επεξεργασία | επεξεργασία κώδικα]Το σύνολο των τύπων (ονομάζεται επίσης και καλοσχηματισμένοι τύποι[3]) ορίζεται επαγωγικά από τους παρακάτω κανόνες:
- Κατηγορηματικά σύμβολα. Εάν P είναι ένα n-βαθμού κατηγορηματικό σύμβολο και t1, ..., tn είναι όροι, τότε το P(t1,...,tn) είναι τύπος.
- Ισότητα. Εάν το σύμβολο της ισότητας (ίσον) θεωρηθεί μέρος της λογικής, και t1 και t2 είναι όροι, τότε το t1 = t2 είναι τύπος.
- Άρνηση. Εάν το φ είναι τύπος, τότε και το φ είναι τύπος.
- Δυαδικοί σύνδεσμοι. Εάν φ και ψ είναι τύποι, τότε (φ ψ) είναι τύπος, Παρόμοιοι κανόνες ισχύουν και για τους υπόλοιπους δυαδικούς συνδέσμους.
- Ποσοδείκτες. Εάν φ είναι τύπος και χ είναι μία μεταβλητή, τότε x φ και x φ είναι τύποι.
Μόνο οι εκφράσεις οι οποίες μπορούν να ληφθούν από πολλές εφαρμογές των κανόνων 1 και 2 είναι τύποι. Αυτοί που σχηματίζονται από τους δύο πρώτους κανόνες ονομάζονται ατομικοί τύποι.
Για παράδειγμα,
είναι τύπος. Εάν το f είναι ένα μονομελές συναρτησιακό σύμβολο, το P είναι ένα μονομελές κατηγορηματικό σύμβολο και το Q είναι ένα τριαδικό κατηγορηματικό σύμβολο. Από την άλλη μεριά, δεν είναι τύπος, παρόλο που είναι μια σειρά από σύμβολα της αλφαβήτου.
Ο ρόλος των παρενθέσεων στον ορισμό είναι για να διασφαλίσει πως κάθε τύπος μπορεί να κατασκευαστεί με έναν τρόπο ακολουθώντας τον επαγωγικό ορισμό (με άλλα λόγια, υπάρχει μοναδικό συντακτικό δέντρο για κάθε τύπο). Αυτή η ιδιότητα είναι γνωστή ως μοναδική αναγνωσιμότητα των τύπων. Υπάρχουν πολλές συνήθειες για τα σημεία που χρησιμοποιούνται οι παρενθέσεις στους τύπους. Για παράδειγμα, μερικοί συγγραφείς χρησιμοποιούν τελείες αντί για παρενθέσεις ή αλλάζουν τα σημεία που είναι οι παρενθέσεις από την αρχή. Ο κάθε ορισμός του συγγραφέα πρέπει να συνοδεύεται από την απόδειξη της μοναδικής αυτής αναγνωσιμότητας.
Αυτός ο ορισμός του τύπου δεν υποστηρίζει τον καθορισμό της εάν-τότε-αλλιώς συνάρτησης (if-then-else function) ite(c, a, b), όπου το "c" είναι μία κατάσταση που εκφράζεται ως τύπος, η οποία θα επιστρέψει το "a" εάν είναι αληθής και το "b" εάν είναι ψευδής. Αυτό συμβαίνει επειδή και τα κατηγορήματα, και οι συναρτήσεις μπορούν να δεχτούν όρους ως παραμέτρους, αλλά η πρώτη παράμετρος πρέπει να είναι τύπος. Κάποιες γλώσσες έχουν δημιουργηθεί με βάση τη λογική πρώτου βαθμού, όπως η SMT-LIB 2.0.[4]
Συμβατικοί συμβολισμοί
[Επεξεργασία | επεξεργασία κώδικα]Για λόγους ευκολίας, έχουν αναπτυχθεί κάποιες παραδοχές σχετικά με την προτεραιότητα των λογικών τελεστών, για να αποφευχθεί η ανάγκη να γράφουμε παρενθέσεις, σε μερικές περιπτώσεις. Αυτοί οι κανόνες είναι όμοιοι με την σειρά των πράξεων στην αριθμητική. Μια κοινή παραδοχή είναι:
- αξιολογείται πρώτη
- και αξιολογούνται μετά
- Οι ποσοδείκτες στη συνέχεια
- αξιολογείται τελευταία.
Ακόμη, δεν χρειάζονται επιπλέον σημεία στίξης να προστεθούν για να διαβάζεται πιο εύκολα ο τύπος. Έτσι ο τύπος
μπορεί να γραφεί σαν
Σε κάποιους τομείς, συνηθίζεται να χρησιμοποιούνται συμβολισμοί για δυαδικές σχέσεις και συναρτήσεις, αντί για τους προθεματικούς συμβολισμούς που ορίστηκαν πιο πάνω. Για παράδειγμα, στην αριθμητική, κάποιος γράφει συνήθως "2 + 2 = 4" αντί για "=(+(2,2),4)". Ακόμη, πολλές φορές οι συμβολισμοί στους τύπους θεωρούνται ως συντμήσεις για τους αντίστοιχους τύπους σε προθεματικούς συμβολισμούς.
Οι παραπάνω ορισμοί χρησιμοποιούν συμβολισμούς για δυαδικούς συνδέσμους, όπως . Μία λιγότερο συνηθισμένη παραδοχή είναι ο Πολωνικός συμβολισμός, στον οποίο γράφονται , και τα λοιπά μπροστά από τα επιχειρήματα, και όχι ανάμεσα. Αυτή η παραδοχή επιτρέπει όλα τα σημεία στίξης να απορριφθούν. Ο Πολωνικός συμβολισμός είναι συμπαγής και κομψός, αλλά στην πράξη χρησιμοποιείται σπάνια γιατί είναι δύσκολο σε πολλούς να διαβαστεί. Στον Πολωνικό συμβολισμό, ο τύπος
γίνεται "∀x∀y→Pfx¬→ PxQfyxz".
Ελεύθερες και Δεσμευμένες μεταβλητές
[Επεξεργασία | επεξεργασία κώδικα]Σε έναν τύπο, μία μεταβλητή μπορεί να είναι ελεύθερες ή δεσμευμένες. Διαισθητικά, μία μεταβλητή είναι ελεύθερη εάν ο τύπος δεν ποσοτικοποιείται: στο , η μεταβλητή χ είναι ελεύθερη ενώ η y είναι δεσμευμένη. Οι μεταβλητές ενός τύπου καθορίζονται επαγωγικά όπως παρακάτω.
- Ατομικές φόρμουλες. Εάν φ είναι ένας ατομικός τύπος τότε το χ είναι ελεύθερη μεταβλητή στο φ εάν και μόνο εάν το χ εμφανίζεται στο φ. Επιπλέον, δεν υπάρχουν δεσμευμένες μεταβλητές σε ατομικές φόρμουλες
- Άρνηση. Το χ είναι ελεύθερο στο φ αν και μόνο αν το χ είναι ελεύθερο στο φ. Το χ είναι δεσμευμένο στο φ αν και μόνο αν το χ είναι δεσμευμένο στην φ.
- Δυαδικοί σύνδεσμοι. Το χ είναι ελεύθερο στο (φ ψ) αν και μόνο αν το χ είναι ελεύθερο είτε στο φ είτε στο ψ. Το χ είναι δεσμευμένο στο (φ ψ) αν και μόνο αν το χ είναι δεσμευμένο στο φ ή στο ψ. Ο ίδιος κανόνας ισχύει και στους υπόλοιπους δυαδικούς συνδέσμους στη θέση του .
- Ποσοδείκτες. Το χ είναι ελεύθερη μεταβλητή στο y φ αν και μόνο αν το χ είναι ελεύθερο στο φ και το χ είναι διαφορετικό σύμβολο από το y. Ακόμη, το χ είναι δεσμευμένο στο y φ αν και μόνο αν το χ είναι το y ή το χ είναι δεσμευμένο στο φ. Ο ίδιος κανόνας ισχύει και για το στη θέση του .
Για παράδειγμα, στο x y (P(x) Q(x,f(x),z)), x και y 'είναι δεσμευμένες μεταβλητές, το z είναι ελεύθερη μεταβλητή και το w δεν είναι κανένα από τα δύο επειδή δεν υπάρχει στον τύπο.
Η ελευθερία και η δέσμευση, μπορούν επίσης να εξειδικεύονται σε συγκεκριμένα συμβάντα των μεταβλητών στους τύπους. Για παράδειγμα, στο , η πρώτη εμφάνιση του x είναι ελεύθερη μεταβλητή ενώ η δεύτερη είναι δεσμευμένη. Με άλλα λόγια, το x στο P(x) είναι ελεύθερο ενώ το x στο x Q(x) είναι δεσμευμένο.
Μία φόρμουλα (τύπος) στη λογική πρώτου βαθμού χωρίς καμία ελεύθερη μεταβλητή, ονομάζεται πρόταση πρώτου βαθμού. Αυτοί είναι οι τύποι που έχουν καλά-καθορισμένες τιμές αληθείας υπό μια ερμηνεία. Για παράδειγμα, εάν ένας τύπος όπως ο Phil(x) είναι αληθής πρέπει να στηρίζεται σε αυτό που αντιπροσωπεύει το x. Αλλά η πρόταση θα είναι είτε αληθής, είτε ψευδής, ανάλογα με την ερμηνεία.
Παραδείγματα
[Επεξεργασία | επεξεργασία κώδικα]Αβελιανές Ομάδες
[Επεξεργασία | επεξεργασία κώδικα]Στα μαθηματικά η γλώσσα των ταξινομημένων αβελιανών ομάδων έχει ένα σταθερό σύμβολο 0, ένα μονομελές συναρτησιακό σύμβολο −, ένα δυαδικό συναρτησιακό σύμβολο +, και ένα δυαδικό σύμβολο σχέσης ≤. Τότε:
- Οι εκφράσεις +(x, y) και +(x, +(y, −(z))) είναι όροι. Αυτά συνήθως γράφονται ως x + y και x + y − z.
- Οι εκφράσεις +(x, y) = 0 και ≤(+(x, +(y, −(z))), +(x, y)) είναι ατομικές φόρμουλες.
- Αυτά συνήθως γράφονται σαν x + y = 0 και x + y − z ≤ x + y.
- Η έκφραση είναι μία φόρμουλα, η οποία συνήθως γράφεται σαν
Η στοργική σχέση
[Επεξεργασία | επεξεργασία κώδικα]Υπάρχουν 10 διαφορετικοί τύποι με 8 διαφορετικές έννοιες, που χρησιμοποιούν την αγαπητική σχέση LXY ("x αγαπάει y ") και οι ποσοδείκτες ∀ και ∃:
|
Οι λογικοί πίνακες αντιπροσωπεύουν τους τύπους για την περίπτωση που υπάρχουν πέντε άτομα που μπορούν να αγαπήσουν (κάθετος άξονας) και να αγαπηθούν (οριζόντιος άξονας). Εκτός από τις περιπτώσεις 9 και 10, οι άλλοι είναι παραδείγματα. Π.χ. ο πίνακας στην περίπτωση 5 αντιπροσωπεύει το "b αγαπάει τον εαυτό του." ενώ οι πίνακες 7 και 8 το "c αγαπά b." Είναι σημαντικό και διδακτικό να επεξηγηθούν η πρόταση 1, , Και 3, : Σε αμφότερες τις περιπτώσεις, ο καθένας μπορεί να αγαπηθεί, αλλά στην πρώτη περίπτωση ο καθένας αγαπιέται από κάποιον, ενώ στη δεύτερη περίπτωση ο καθένας έχει αγαπηθεί από το ίδιο πρόσωπο.
Μερικές προτάσεις συνεπάγονται η μια την άλλη - π.χ. αν η 3 είναι αλήθεια επίσης η 1 είναι αλήθεια, αλλά όχι το αντίστροφο. (Βλέπε διάγραμμα Hasse)
Σημασιολογία
[Επεξεργασία | επεξεργασία κώδικα]Μια ερμηνεία μιας γλώσσας πρώτου βαθμού εκχωρεί μια ένδειξη σε όλες τις μη λογικές σταθερές σε αυτή τη γλώσσα. Επίσης, καθορίζει ένα πεδίο του λόγου που καθορίζει το εύρος των ποσοδεικτών. Το αποτέλεσμα είναι ότι σε κάθε όρο εκχωρείται ένα αντικείμενο το οποίο αντιπροσωπεύει, και κάθε πρόταση εκχωρείται μια αληθής τιμή . Με τον τρόπο αυτό, η ερμηνεία παρέχει σημασιολογική έννοια με τους όρους και τους τύπους της γλώσσας. Η μελέτη από τις ερμηνείες των τυπικών γλωσσών λέγεται τυπική σημασιολογία . Αυτό που ακολουθεί είναι μια περιγραφή της τυποποιημένης ή σημασιολογίας Τάρσκι για τη λογική πρώτου βαθμού. (Είναι επίσης δυνατόν να καθοριστεί σημασιολογία παιγνίων για τη λογική πρώτου βαθμού , αλλά πέρα από το απαιτούμενο αξίωμα της επιλογής , η σημασιολογία παιγνίων συμφωνεί με την σημασιολογία Τάρσκι για τη λογική πρώτου βαθμού, έτσι η σημασιολογία παιγνίων δεν μπορεί να επεξηγηθεί εδώ.)
Ο τομέας του λόγου D είναι ένα μη κενό σύνολο «αντικειμένων» κάποιου είδους. Διαισθητικά, ένας τύπος πρώτου βαθμού. είναι μια δήλωση σχετικά με αυτά τα αντικείμενα για παράδειγμα, δηλώνει την ύπαρξη ενός αντικειμένου x τέτοιο ώστε το κατηγόρημα P να είναι αληθές όταν αναφέρεται σε αυτό. Ο τομέας του λόγου είναι το σύνολο των θεωρούμενων αντικειμένων . Για παράδειγμα, μπορεί κανείς να λάβει να είναι το σύνολο των ακεραίων αριθμών.
Η ερμηνεία μιας συμβολοσυνάρτησης είναι μια συνάρτηση. Για παράδειγμα, εάν ο τομέας του λόγου αποτελείται από ακέραιους αριθμούς, μια συμβολοσυνάρτηση f τάξης 2 που αποδίδει το άθροισμα των αποτελεσμάτων της. Με άλλα λόγια, το σύμβολο f συνδέεται με τη συνάρτηση I(f) η οποία, σε αυτή την ερμηνεία, είναι η προσθήκη.
Η ερμηνεία ενός σταθερού σύμβολου είναι μια συνάρτηση από το σύνολο ενός στοιχείου D 0 στο D, η οποία μπορεί να προσδιοριστεί απλά με ένα αντικείμενο στο D. Για παράδειγμα, μια ερμηνεία μπορεί να εκχωρήσει την τιμή στο σταθερό σύμβολο .
Η ερμηνεία ενός n-οστού συμβόλου κατηγόρημα είναι ένα σύνολο από n σε πλήθος στοιχεία του τομέα του λόγου. Αυτό σημαίνει ότι, δεδομένης μιας ερμηνείας, ενός συμβόλου κατηγόρημα, και nστοιχείων του τομέα του λόγου, μπορεί κανείς να πει εάν το κατηγόρημα είναι αληθές για τα στοιχεία αυτά, σύμφωνα με τη συγκεκριμένη ερμηνεία. Για παράδειγμα, μια ερμηνεία Ι (Ρ) ενός δυαδικού συμβόλου κατηγόρημα Ρ μπορεί να είναι το σύνολο των ζευγών των ακεραίων τέτοια ώστε το πρώτο να είναι μικρότερο από το δεύτερο. Σύμφωνα με την ερμηνεία αυτή, το κατηγόρημα P θα είναι αληθές αν το πρώτο του επιχείρημα είναι μικρότερο από το δεύτερο.
Δομές πρώτης τάξης
[Επεξεργασία | επεξεργασία κώδικα]Κύριο άρθρο: Δομή (μαθηματική λογική)
Ο πιο συνηθισμένος τρόπος προσδιορισμού μιας ερμηνείας (ιδιαίτερα στα μαθηματικά) είναι να καθορίσουμε μια δομή (επίσης ονομάζεται πρότυπο, Βλ. παρακάτω). Η δομή αποτελείται από ένα μη κενό σύνολο D που αποτελεί το πεδίο του λόγου και μια ερμηνεία Ι των μη λογικών όρων της υπογραφής. Η ερμηνεία αυτή είναι συνάρτηση:
- Κάθε συμβολοσυνάρτηση f τάξης n καθορίζει μια συνάρτηση I(f) από στο . Ειδικότερα, κάθε σταθερό σύμβολο της υπογραφής προσδιορίζει μια μονάδα στον τομέα του λόγου.
- Κάθε σύμβολο κατηγόρημα Ρ τάξης n προσδιορίζει μια σχέση I (P) πάνω ή, ισοδύναμα, μια συνάρτηση από στο . Έτσι, κάθε σύμβολο κατηγόρημα ερμηνεύεται από μια Bool συνάρτηση στο
Αξιολόγηση των τιμών αλήθειας
[Επεξεργασία | επεξεργασία κώδικα]Ένας τύπος εκτιμά το αληθές ή το ψευδές δεδομένης μιας ερμηνείας, και μία εκχώρηση μεταβλητής μ που συνδέει ένα στοιχείο του τομέα του λόγου με κάθε μεταβλητή. Ο λόγος για τον οποίο απαιτείται η εκχώρηση μεταβλητής είναι να δώσει σημασία σε τύπους με ελεύθερες μεταβλητές, όπως . Η τιμή αληθείας του τύπου αυτού αλλάζει ανάλογα με το αν το x και y δηλώνουν το ίδιο μονάδα.
Πρώτα, η εκχώρηση μεταβλητή μ μπορεί να επεκταθεί σε όλους τους όρους της γλώσσας, με αποτέλεσμα ότι κάθε όρος καθορίζει ένα μόνο στοιχείο του τομέα του λόγου. Οι ακόλουθοι κανόνες που χρησιμοποιούνται για να κάνουν αυτή την εργασία:
- Μεταβλητές. Κάθε μεταβλητή x εκτιμάται από το μ (x)
- Συναρτήσεις. Δεδομένου των όρων που έχουν εκτιμηθεί από τα στοιχεία του τομέα του λόγου, και μιας η-οστης τάξης συμβολοσυνάρτηση f, ο όρος εκτιμάται από .
Στη συνέχεια,σε κάθε τύπο αναθέτετε μια αληθής τιμή .Ο επαγωγικός ορισμός που χρησιμοποιείται για να κάνει αυτή την εργασία ονομάζεται T-σχήμα .
- Ατομικοί τύποι (1). Ένας τύπος παίρνει αληθής ή ψευδής τιμή , ανάλογα με το αν , Όπου είναι η εκτίμηση των όρων και είναι η ερμηνεία των , υποθέτοντας ότι είναι ένα υποσύνολο της .
- Ατομικοί τύποι (2). Ένας τύπος παίρνει αληθής τιμή αν και εκτιμόνται από το ίδιο αντικείμενο του τομέα του λόγου (βλ. το τμήμα για την ισότητα παρακάτω).
- Λογικοί σύνδεσμοι. Ένας τύπος με τη μορφή , , Κλπ. εκτιμάται σύμφωνα με τον πίνακα αληθείας για την εν λόγω συνεκκτικότητα όπως στην προτασιακή λογική.
- Υπαρξιακοί ποσοδείκτες. Ένας τύπος είναι αληθής, σύμφωνα με M και αν υπάρχει εκτίμηση των μεταβλητών η οποία διαφέρει μόνο από το ανάλογα με την εκτίμηση των χ και είναι τέτοια ώστε η φ να είναι αληθές σύμφωνα με την εκίμηση Μ και της εκχωρούμενης μεταβλητής . Αυτός ο τυπικός ορισμός υπαγορεύει ότι το οποίο είναι αληθής αν και μόνο αν υπάρχει ένας τρόπος για να επιλέξετε μια τιμή για το x τέτοια ώστε φ (x) να ικανοποιήται
- Οικουμενικοί ποσοδείκτες. Ένας τύπος είναι αληθής, σύμφωνα με M και αν φ (x) είναι αληθής για κάθε ζεύγος που αποτελείται από την ερμηνεία Μ και κάποια εκχωρούμενη μεταβλητή που διαφέρει από μόνο στην τιμή του x. Αυτό υπαγορεύει ότι είναι αληθές αν κάθε πιθανή επιλογή μιας τιμής για το x επαληθεύει το φ (x).
Εάν ο τύπος δεν περιέχει ελεύθερες μεταβλητές, και άρα είναι μία πρόταση, τότε η αρχική εκχώρηση της μεταβλητής δεν επηρεάζει την αξία αληθείας της. Με άλλα λόγια, μία πρόταση είναι αληθής σύμφωνα με το M και το αν και μόνο αν είναι αληθής σύμφωνα με το M και κάθε άλλη εκχωρούμενη μεταβλητή .
Υπάρχει μια δεύτερη κοινή προσέγγιση για τον καθορισμό των αληθών τιμών που δεν βασίζεται σε μεταβλητές συναρτήσεις εκχώρησης. Αντ 'αυτού,δεδομένης μίας ερμηνεία του Μ, μπορεί κάποιος να προσθέσει στην υπογραφή μια συλλογή από σταθερά σύμβολα , ένα για κάθε στοιχείο του τομέα του λόγου στο M. Δηλαδή, για κάθε d στο τομέα το σταθερό σύμβολο cd είναι καθορισμένο . Η ερμηνεία έχει επεκταθεί έτσι ώστε κάθε νέο σταθερό σύμβολο να έχει εκχωρηθεί σε αντίστοιχο στοιχείο του τομέα. Μπορούμε τώρα να αποφανθούμε για το αν είναι αληθείς οι ποσοτικοποιημένοι τύποι ως εξής:
- Υπαρξιακοί ποσοδείκτες (αναπληρωματικό μέλος). Ένας τύπος είναι αληθής, σύμφωνα με το M αν υπάρχει κάποιο d στον τομέα του λόγου, έτσι ώστε να υπάρχει. Εδώ είναι το αποτέλεσμα της αντικατάστασης cd για κάθε περίπτωση του x στην φ.
- Οικουμενική ποσοδείκτες (αναπληρωματικό μέλος). Ένας τύπος είναι αληθής, σύμφωνα με το M αν, για κάθε d στο πεδίο του λόγου, είναι αληθής σύμφωνα με το M.
Αυτή η εναλλακτική προσέγγιση δίνει ακριβώς τις ίδιες τιμές αλήθειας σε όλες τις προτάσεις, όπως η προσέγγιση μέσω αναθέσεις μεταβλητών.
Ισχύς, ικανοποιησιμότητα και λογική συνέπεια
[Επεξεργασία | επεξεργασία κώδικα]Εάν η πρόταση φ θεωρείται αληθής κάτω από τη δοθείσα ερμηνεία M, κάποιος θα μπορούσε να πει ότι το Μ ικανοποιεί τη φ: αυτό συμβολίζεται ως . Μία πρόταση είναι ικανοποιησιμη εάν υπάρχει κάποια ερμηνεία, κάτω από την οποία είναι αληθής.
Η ικανοποιησιμότητα των τύπων μPoε ελεύθερες μεταβλητές είναι πιο περίπλοκη, επειδή μια ερμηνεία από μόνη της δεν καθορίζει το βαθμό αλήθειας ενός τέτοιου τύπου.Το πιο συνηθισμένο είναι ότι ο τύπος με ελεύθερες μεταβλητές να είναι ικανοποιητικός κάτω από μία ερμηνεία εάν ο παραμένει αληθής ανεξάρτητα από ποια άτομα από το πεδίο τιμών θα ανατεθεί στις ελεύθερες μεταβλητές του. Αυτό είναι το ίδιο με το να πούμε πως ο τύπος είναι ικανοποιητικός αν και μόνο αν η γενική κλειστότητά του είναι ικανοποιητική.
Ένας τύπος είναι λογικά έγκυρος (ή απλά ισχύει) εάν είναι αληθής για κάθε ερμηνεία. Αυτοί οι τύποι παίζουν παρόμοιο ρόλο με τις ταυτολογίες στην προτασιακή λογική.
Ένας τύπος φ είναι λογική συνέπεια ενός τύπου ψ εάν κάθε ερμηνεία που καθιστά το ψ αληθές, κάνει και το φ αληθές. Σε αυτή την περίπτωση λέμε ότι το φ συνάγεται λογικά από το ψ.
Αλγεβροποιήσεις
[Επεξεργασία | επεξεργασία κώδικα]Μία εναλλακτική προσέγγιση στη σημασιολογία της λογικής πρώτου βαθμού, πραγματοποιείται μέσω της αφηρημένης άλγεβρας. Αυτή η προσέγγιση γενικεύει τις άλγεβρες Lindenbaum - Τάρσκι της προτασιακής λογικής.
Υπάρχουν τρεις τρόποι για να εξαλειφθούν οι μεταβλητές των ποσοδεικτών από τη λογική πρώτου βαθμού, που δεν περιλαμβάνουν την αντικατάσταση των ποσοδεικτών με άλλους δεσμευμένους τελεστές:
- Κυλινδρική Άλγεβρα, από τον Άλφρεντ Τάρσκι και τους συνεργάτες του
- Πολυαδική Άλγεβρα, από τον Paul Halmos
- Κατηγορηματική Συναρτησιακή Λογική, κυρίως χάρη στον Willard Quine.
Αυτές οι άλγεβρες είναι όλες σύνδεσμοι που επεκτείνουν σωστά την Άλγεβρα Boolean δύο στοιχείων.
Οι Τάρσκι και Givant (1987) έδειξαν ότι το τμήμα της λογικής πρώτου βαθμού δεν έχει ατομικές προτάσεις που βρίσκονται στο πεδίο των ποσοδεικτών που είναι περισσότεροι από τρεις, έχει την ίδια εκφραστική δύναμη με τη άλγεβρα των σχέσεων. Αυτό το τμήμα παρουσιάζει ιδιαίτερο ενδιαφέρον επειδή αρκεί για την αριθμητική Πεάνο και στη θεωρία αξιωματικών συνόλων, συμπεριλαμβανομένου και του κανονικού ZFC. Ακόμη, απέδειξαν πως η λογική πρώτου βαθμού με ένα αρχικό διατεταγμένο ζεύγος είναι ισοδύναμο με την άλγεβρα των σχέσεων με τις προβολικές συναρτήσεις δύο διατεταγμένων ζευγών.
Θεωρίες πρώτου βαθμού, μοντέλα και στοιχειώδεις κλάσεις.
[Επεξεργασία | επεξεργασία κώδικα]Μία θεωρία πρώτου βαθμού μιας συγκεκριμένης υπογραφής είναι ένα σύνολο από αξιώματα, τα οποία είναι προτάσεις που αποτελούνται από σύμβολα αυτής της υπογραφής. Το σύνολο των αξιωμάτων είναι συχνά πεπερασμένο ή αναδρομικά αριθμήσιμο, και σε αυτή την περίπτωση η θεωρία ονομάζεται αποτελεσματική. Μερικοί συγγραφείς απαιτούν, οι θεωρίες αυτές να περιλαμβάνουν και όλα τα λογικά αποτελέσματα των αξιωμάτων. Τα αξιώματα υπάρχουν μέσα στη θεωρία και από αυτά άλλες προτάσεις που τα περιέχουν μπορούν να παραχθούν.
Μια δομή πρώτου βαθμού που ικανοποιεί όλες τις προτάσεις σε δοθείσα θεωρία είναι ένα μοντέλο της θεωρίας αυτής. Μία στοιχειώδης κλάση είναι ένα σύνολο από όλες τις δομές που ικανοποιούν μια συγκεκριμένη θεωρία. Αυτές οι κλάσεις είναι το κύριο θέμα της μελέτης της θεωρίας μοντέλων.
Αρκετές θεωρίες έχουν στοχευμένη ερμηνεία, ένα συγκεκριμένο μοντέλο που έχουμε στο μυαλό μας μελετώντας τη θεωρία. Για παράδειγμα, η στοχευμένη ερμηνεία της αριθμητικής Peano συγκροτείται από τους συνήθεις φυσικούς αριθμούς με τις πράξεις τους. Παρ' όλα αυτά το θεώρημα Λόβενχαϊμ-Σκόλεμ δείχνει ότι οι περισσότερες θεωρίες θα έχουν άλλα, μη τυποποιημένα μοντέλα.
Μία θεωρία είναι συμβιβαστή εάν είναι αδύνατο να αποδειχθεί μία αντίφαση από τα αξιώματά της. Μία θεωρία είναι πλήρης, αν, για κάθε τύπο στην υπογραφή της, είτε αυτός ο τύπος είτε η άρνησή του είναι μία λογική συνέπεια από τα αξιώματα της θεωρίας. Το θεώρημα μη πληρότητας του Γκέντελ δείχνει πως οι αποτελεσματικές θεωρίες πρώτου βαθμού που περιέχουν ένα επαρκές μέρος από τη θεωρία των φυσικών αριθμών δεν μπορεί ποτέ να είναι συμβιβαστή και πλήρης ταυτόχρονα.
Για περισσότερες πληροφορίες σε αυτό το θέμα δείτε τη Λίστα των θεωριών πρώτου βαθμού και τη Θεωρία (Μαθηματική Λογική).
Κενά πεδία
[Επεξεργασία | επεξεργασία κώδικα]Ο παραπάνω ορισμός απαιτεί ότι το πεδίο τιμών οποιασδήποτε ερμηνείας δεν μπορεί να είναι κενό σύνολο. Υπάρχουν ρυθμίσεις, όπως της εγκλειστικής λογικής, όπου τα κενά πεδία απαγορεύονται. Επιπλέον, εάν η κλάση της αλγεβρικής δομής περιλαμβάνει μία κενή δομή (για παράδειγμα, υπάρχει ένα κενό μερικώς διατεταγμένο σύνολο (poset)), αυτή η κλάση είναι στοιχειώδης στην λογική πρώτου βαθμού, αν τα κενά πεδία επιτρέπονται ή η κενή δομή έχει αφαιρεθεί από την κλάση.
Υπάρχουν αρκετές δυσκολίες με τα κενά πεδία, παρ' όλα αυτά:
- Πολλοί συνηθισμένοι κανόνες των συμπερασμάτων ισχύων όταν το πεδίο τιμών δεν πρέπει να είναι κενό. Ένα παράδειγμα είναι ο κανόνας που λέει πως υπονοεί ότι όταν το x δεν είναι ελεύθερη μεταβλητή στο φ. Αυτός ο κανόνας. που συνηθίζεται να μπαίνει στους τύπους σε κανονική μορφή, είναι σωστός σε μη κενά πεδία, αλλά λάθος εάν το κενό πεδίο επιτρέπεται.
- Ο ορισμός της αλήθειας σε μία ερμηνεία που χρησιμοποιεί μία μεταβλητή εντολή συνάρτησης δεν μπορεί να λειτουργήσει με κενά πεδία, επειδή δεν υπάρχουν μεταβλητές εντολές συνάρτησης των οποίων το εύρος είναι κενό. (Παρόμοια, κάποιος δεν μπορεί να εκχωρήσει ερμηνείες σε σταθερά σύμβολα.) Ο ορισμός της αλήθειας απαιτεί ότι κάποιος πρέπει να επιλέξει μια μεταβλητή εκχώρησης συνάρτησης (η προηγούμενη μ) πριν οι τιμές αληθείας, ακόμη και για τις ατομικές φόρμουλες, οριστούν. Τότε, η τιμή της αληθείας μίας πρότασης έχει οριστεί να είναι η τιμή της αλήθειας της κάτω από οποιαδήποτε μεταβλητή εκχώρηση, και έχει αποδειχθεί πως η τιμή της αλήθειας δεν βασίζεται στην εκάστοτε επιλεγμένη εκχώρηση. Αυτή η τεχνική, δεν λειτουργεί εάν δεν υπάρχουν εκχωρήσιμες συναρτήσεις, πρέπει να αλλάξει για να περιέχει κενά πεδία.
Έτσι, όταν το κενό πεδίο επιτρέπεται, συχνά πρέπει να αντιμετωπίζεται σαν μία ειδική περίπτωση. Οι περισσότεροι συγγραφείς, όμως, απλά εξαιρούν το κενό πεδίο εξ' ορισμού.
Συμπερασματικά Συστήματα
[Επεξεργασία | επεξεργασία κώδικα]Ένα συμπερασματικό σύστημα χρησιμοποιείται για να δείξει, αυστηρά σε συντακτική βάση, ότι ο τύπος είναι λογική συνέπεια ενός άλλου τύπου. Υπάρχουν πολλά τέτοια συστήματα για τη λογική πρώτου βαθμού, συμπεριλαμβανομένων και των: συμπερασματικό σύστημα Χίλμπερτ, συστήματα φυσικής παραγωγής, τη μέθοδο tableux και την ανάλυση. Αυτά τα συστήματα έχουν την κοινή ιδιότητα ότι το συμπέρασμα είναι ένα πεπερασμένο συντακτικό αντικείμενο, του οποίου η μορφή και ο τρόπος δόμησής του ποικίλλουν σε μεγάλο βαθμό. Αυτά τα πεπερασμένα συμπεράσματα συχνά καλούνται παράγωγοι στην θεωρία αποδείξεων. Αποκαλούνται επίσης, αποδείξεις, αλλά είναι τελείως διαφορετικά δομημένες από τις συνηθισμένες μαθηματικές αποδείξεις.
Ένα συμπερασματικό σύστημα σώο εάν κάθε τύπος που μπορεί να παραχθεί στο σύστημα, είναι λογικά ισχύον. Αντίθετα, ένα συμπερασματικό σύστημα είναι πλήρες εάν κάθε λογικά ισχύουσα φόρμουλα είναι παραγωγίσιμη. Όλα τα συστήματα τα οποία αναφέρονται σε αυτό το άρθρο είναι και σώα και πλήρη. Η κοινή τους ιδιότητα είναι πως είναι πιθανό να ελέγξει αποτελεσματικά ότι ένα υποτιθέμενα ισχύον συμπέρασμα είναι όντως ένα συμπέρασμα. Τέτοια συστήματα ονομάζονται αποτελεσματικά.
Μία ιδιότητα "κλειδί" των συμπερασματικών συστημάτων είναι πως είναι καθαρά συντακτικά, έτσι οι παράγωγοι μπορούν να επιβεβαιωθούν χωρίς να ληφθεί υπόψη κάποια ερμηνεία. Έτσι, ένα σώο επιχείρημα είναι σωστό με κάθε πιθανή ερμηνεία της γλώσσας, ανεξάρτητα από αν αυτή η ερμηνεία είναι σχετικά με τα μαθηματικά, τα οικονομικά ή οποιοδήποτε άλλο τομέα.
Γενικά, μία λογική συνέπεια στη λογική πρώτου βαθμού είναι μόνο ημικαθοριστική: εάν μία πρόταση Α προϋποθέτει λογικά μία πρόταση Β, τότε αυτό μπορεί να ανακαλυφθεί (για παράδειγμα, αναζητώντας μία απόδειξη μέχρι να βρεθεί, χρησιμοποιώντας αποτελεσματικό, σώο και πλήρες σύστημα απόδειξης). Παρ' όλα αυτά, εάν το Α δεν προϋποθέτει λογικά το Β, αυτό δεν σημαίνει ότι το Α προϋποθέτει λογικά την άρνηση του Β. Δεν υπάρχει μη αποτελεσματική διαδικασία που, δοθέντων των τύπων Α και Β, να αποφασίζει πάντα σωστά εάν το Α προϋποθέτει λογικά το Β.
Κανόνες Συμπεράσματος
[Επεξεργασία | επεξεργασία κώδικα]Ένας κανόνας συμπεράσματος αναφέρει ότι, με δεδομένο κάποιο τύπο (ή ένα σύνολο από αυτούς) με μία συγκεκριμένη ιδιότητα ως υπόθεση, ένας άλλος τύπος (ή ένα σύνολο) μπορεί να παραχθεί σαν συμπέρασμα. Ο κανόνας είναι σώος (ή διατηρεί την αλήθεια) εάν διατηρεί το κύρος με την έννοια ότι οποιαδήποτε άλλη ερμηνεία ικανοποιεί την υπόθεση, τότε η ερμηνεία ικανοποιεί και το συμπέρασμα.
Για παράδειγμα, ένας συνηθισμένος κανόνας συμπεράσματος είναι ο κανόνας της αντικατάστασης. Εάν t είναι ένας όρος και φ ένας τύπος που πιθανότατα περιέχει την μεταβλητή x, τότε το φ[t/x] (που συχνά συμβολίζεται με φ[x/t]) είναι το αποτέλεσμα που προκύπτει εάν αντικαταστήσουμε όλες τις ελεύθερες περιπτώσεις του x με το t στην φ. Ο κανόνας της αντικατάστασης υποστηρίζει πως αν για οποιοδήποτε φ και οποιοδήποτε όρο t, κάποιος θα μπορούσε να συμπεράνει ότι το φ[t/x] από το φ, εφόσον δεν υπάρχει ελεύθερη μεταβλητή t περιορίζεται κατά τη διάρκεια της αντικατάστασης. (Εάν μία ελεύθερη μεταβλητή του t περιορίζεται, τότε για να αντικαταστήσουμε το για το x, πρέπει πρώτα να αλλάξουμε τις δεσμευμένες μεταβλητές του φ να διαφέρουν από τις ελεύθερες μεταβλητές του t.)
Για να δούμε γιατί είναι απαραίτητος ο περιορισμός στις μεταβλητές, ας σκεφτούμε το λογικά ισχύον τύπο φ που δίνεται από , στην υπογραφή του (0,1,+,×,=) της αριθμητικής. Εάν t είναι ο όρο "x + 1", ο τύπος φ[t/y] είναι , το οποίο μπορεί να είναι ψευδές σε πολλές ερμηνείες. Το πρόβλημα είναι πως η ελεύθερη μεταβλητή x του t επειδή δεσμεύεται κατά τη διάρκεια της αντικατάστασης. Η προκειμένη αντικατάσταση μπορεί να γίνει αλλάζοντας το όνομα της δεσμευμένης μεταβλητής x του φ, σε κάτι άλλο, ας πούμε , έτσι ώστε ο τύπος μετά την αντικατάσταση να είναι , το οποίο είναι πάλι λογικά ισχύον.
Ο κανόνας της αντικατάστασης δείχνει αρκετές πλευρές του κανόνα του συμπεράσματος. Είναι εξ' ολοκλήρου συντακτικό, θα μπορούσαμε να πούμε εάν ήταν σωστά εφαρμοσμένο χωρίς προσφυγή σε κάποια ερμηνεία. Έχει (συντακτικά ορισμένους) περιορισμούς σχετικά με το πότε μπορεί να εφαρμοστεί, το οποίο πρέπει να είναι σεβαστό για να διατηρηθεί η ορθότητα των παραγώγων. Επιπλέον, πολλές φορές, αυτοί οι περιορισμοί είναι απαραίτητη λόγω των ερμηνειών μεταξύ ελεύθερων και δεσμευμένων μεταβλητών που λαμβάνουν χώρα κατά τη διάρκεια των συντακτικών αλλαγών των τύπων που περιλαμβάνει ο κανόνας συμπεράσματος.
Συστήματα Hilbert-στυλ και φυσική αφαίρεση
[Επεξεργασία | επεξεργασία κώδικα]Μια αφαίρεση σε ένα συμπερασματικό σύστημα Hilbert στυλ είναι μια λίστα των τύπων, καθένα από τα οποία είναι λογικό αξίωμα , μια υπόθεση που γίνεται πρόχειρα, ή προκύπτει από τις προηγούμενες φόρμουλες μέσω ενός κανόνα του συμπεράσματος. Τα λογικά αξιώματα αποτελούνται από διάφορα συστήματα αξιωμάτων από προφανείς έγκυρους τύπους. Αυτοί καλύπτουν ένα σημαντικό ποσό της προτασιακής λογικής. Οι κανόνες του συμπεράσματος επιτρέπουν τη χειραγώγηση των ποσοτήτων.Τα τυπικά συστήματα Hilbert στυλ έχουν ένα μικρό αριθμό των κανόνων του συμπεράσματος, μαζί με πολλά άπειρα συστήματα των λογικών αξιωμάτων. Είναι κοινό να έχει μόνο προτασιακή λογική και καθολική γενίκευση στους κανόνες του συμπεράσματος.
Τα φυσικά συστήματα αφαίρεσης μοιάζουν με τα συστήματα Hilbert στυλ στο ότι η αφαίρεση είναι ένας ολοκληρωμένος κατάλογος τ τύπων. Ωστόσο, τα φυσικά συστήματα αφαίρεσης δεν έχουν λογικά αξιώματα, αντισταθμίζουν με την προσθήκη επιπλέον κανόνων συμπεράσματος που μπορεί να χρησιμοποιηθεί για να χειραγωγήσουν τους λογικούς συνδέσμους σε τύπους στην απόδειξη.
Ακολούθων λογισμός
[Επεξεργασία | επεξεργασία κώδικα]Περισσότερες πληροφορίες: Ακολούθων λογισμός
Ο ακολούθων λογισμός αναπτύχθηκε για να μελετήσει τις ιδιότητες των φυσικών συστημάτων αφαίρεσης. Αντί να εργάζονται με έναν τύπο σε έναν χρόνο, χρησιμοποιεί ακολουθίες , οι οποίες έχουν εκφράσεις της μορφής :
όπου Α 1 , ..., Α n , Β 1 , ..., Β k είναι τύποι και το σύμβολο περιστροφική πόρτα χρησιμοποιείται ως στίξης για να διαχωρίσει τα δύο μισά. Διαισθητικά, μια ακολουθία εκφράζει την ιδέα που το συνεπάγεται το .
Μέθοδος Tableaux
[Επεξεργασία | επεξεργασία κώδικα]Περισσότερες πληροφορίες: Μέθοδος αναλυτική tableaux
![](http://upload.wikimedia.org/wikipedia/commons/thumb/5/5a/Non-closed_propositional_tableau.svg/220px-Non-closed_propositional_tableau.svg.png)
Σε αντίθεση με τις μεθόδους που μόλις περιγράψαμε, τα παράγωγα στη μέθοδο tableaux δεν είναι κατάλογοι τύπων. Αντ 'αυτού,ένας τύπος είναι ένα δέντρο τύπων. Για να δείξει ότι ένας τύπος Α είναι ευαπόδεικτος , η μέθοδος tableaux επιχειρεί να αποδείξει ότι η άρνηση του Α δεν ικανοποιείται. Το δέντρο παραγωγής έχει στη ρίζα του, κλαδιά δέντρων με έναν τρόπο που αντανακλά την δομή του τύπου. Για παράδειγμα, για να δείξει ότι είναι μη ικανοποιήσιμα πρέπει να δειχθεί ότι το C και το D είναι το καθένα μη ικανοποιήσιμα. Αυτό αντιστοιχεί σε ένα σημείο διακλάδωσης στο δέντρο με γονέα και παιδιά τα C και D.
Ψήφισμα
[Επεξεργασία | επεξεργασία κώδικα]Ο κανόνας ψήφισμα είναι ένας μόνος κανόνας από συμπεράσματα , που ενώνεται με την ενοποίηση, είναι ορθός και πλήρης για τη λογική πρώτου βαθμού. Όπως και με τη μέθοδο tableaux, ένας τύπος αποδεικνύεται δείχνοντας ότι η άρνηση του τύπου είναι μη ικανοποιήσιμη. Η λύση χρησιμοποιείται συνήθως στην αυτοματοποιημένη απόδειξη θεωρήματος.
Η μέθοδος επίλυσης λειτουργεί μόνο με τύπους που είναι διάζευξη ατομικών τύπων, οι αυθαίρετοι τύποι πρέπει πρώτα να μετατραπούν σε αυτή τη μορφή, μέσω Skolemization. Ο κανόνας ψηφίσματος αναφέρει ότι από τις υποθέσεις και , μπορεί να ληφθεί συμπέρασμα .
Αποδείξιμες ταυτότητες
[Επεξεργασία | επεξεργασία κώδικα]Οι παρακάτω προτάσεις μπορούν να ονομαστούν "ταυτότητες", επειδή ο κύριος συνδετικός στον καθένα είναι η συνδετική λογική .
, (όπου το x δεν προκύπτει άμεσα από το P)
, (όπου το x δεν προκύπτει άμεσα από το P)
Ισότητα και αξιώματα
[Επεξεργασία | επεξεργασία κώδικα]Υπάρχουν αρκετές διαφορετικές χρήσεις της ισότητας (ή της ταυτότητας) στη λογική πρώτου βαθμού. Η πιο συνηθισμένη παραδοχή, γνωστή ως λογική πρώτου βαθμού με ισότητα, περιλαμβάνει το ίσον σαν ένα αρχικό λογικό σύμβολο το οποίο ερμηνεύεται πάντα σαν την πραγματική σχέση μεταξύ των μελών του πεδίου τιμών, έτσι ώστε τα "δύο" μέλη που δόθηκαν να είναι ένα και το αυτό. Αυτή η προσέγγιση προσθέτει, επίσης, κάποια αξιώματα σχετικά με τη ισότητα στο συμπερασματικό σύστημα που χρησιμοποιείται. Αυτά τα αξιώματα είναι:
- Ανακλαστικότητα: Για κάθε μεταβλητή x, x = x.
- Αντικατάσταση για συναρτήσεις.Για όλες τις μεταβλητές x και y, και για κάθε συνάρτηση f,
- x = y → f(...,x,...) = f(...,y,...).
- Αντικατάσταση για τύπους.Για οποιεσδήποτε μεταβλητές x και y και για κάθε τύπο φ(x), εάν φ' προκύπτει με αντικατάσταση με οποιοδήποτε αριθμό από τα ελεύθερα γεγονότα του x στην φ με το y, τέτοια ώστε να παραμένουν ελεύθερα γεγονότα του y, τότε
- x = y → (φ → φ').
Αυτά είναι αξιωματικά σχήματα, κάθε ένα από τα οποία ορίζει ένα άπειρο σύνολο από αξιώματα. Το τρίτο σχήμα είναι γνωστό σαν νόμος του Λάιμπνιτς, "η αρχή της αντικατάστασης", ή "η ιδιότητα της αντικατάστασης". Το δεύτερο σχήμα, που περιέχει το συναρτησιακό σύμβολο , είναι (ίσο με) μια ειδική περίπτωση του τρίτου σχήματος, χρησιμοποιώντας τον τύπο
- x = y → (f(...,x,...) = z → f(...,y,...) = z).
Πολλές άλλες ιδιότητες της ισότητας είναι συνέπειες των παραπάνω αξιωμάτων, για παράδειγμα:
- Συμμετρία. Εάν x = y τότε y = x.
- Μεταβατικότητα. Εάν x = y και y = z τότε x = z.
Λογική πρώτου βαθμού χωρίς ισότητα
[Επεξεργασία | επεξεργασία κώδικα]Μία εναλλακτική προσέγγιση μελετάει τη σχέση της ισότητας να είναι ένα μη-λογικό σύμβολο. Αυτή η παραδοχή είναι γνωστή ως λογική πρώτου βαθμού χωρίς ισότητα. Εάν μία σχέση ισότητας υπάρχει στην υπογραφή, τα αξιώματα πρέπει τώρα να προστεθούν στις θεωρίες υπό εξέταση, εάν είναι επιθυμητό, αντί για τους κανόνες της λογικής. Η κυριότερη διαφορά μεταξύ αυτής της μεθόδου και της λογικής πρώτου βαθμού με ισότητα είναι πως μία ερμηνεία μπορεί τώρα να ερμηνεύσει δύο διακριτά άτομα ως "ίσα" (παρ' όλο που, σύμφωνα με το νόμο του Λάιμπνιτς, θα ικανοποιήσουν ακριβώς τους ίδιους τύπους κάτω από οποιαδήποτε ερμηνεία). Αυτό γιατί, η σχέση ισότητας τώρα μπορεί να ερμηνευτεί ως μία αυθαίρετη σχέση ισοδυναμίας στο πεδίο τιμών που είναι μία ισοδυναμία ως προς τις συναρτήσεις και τις σχέσεις της ερμηνείας.
Όταν ακολουθείται η δεύτερη παραδοχή, ο όρος κανονικό μοντέλο χρησιμοποιείται για να αναφερθεί σε μία ερμηνεία όπου τα μη διακριτά άτομα a και b ικανοποιούν την a = b. Στη λογική πρώτου βαθμού με ισότητα, χρησιμοποιούνται μόνο κανονικά μοντέλα, κ έτσι δεν υπάρχει κάποιος όρος για κάποιο άλλο μοντέλο. Στη μελέτη της λογικής πρώτου βαθμού χωρίς ισότητα, είναι απαραίτητο να τροποποιηθούν οι σχετικές καταστάσεις των αποτελεσμάτων, όπως το θεώρημα Λόβενχαϊμ-Σκόλεμ έτσι ώστε να χρησιμοποιούνται μόνο τα κανονικά μοντέλα.
Η λογική πρώτου βαθμού χωρίς ισότητα συχνά αναφέρεται στο πλαίσιο της αριθμητικής δευτέρου βαθμού και σε άλλες υψηλότερου βαθμού θεωρίες της αριθμητικής, όπου η σχέση ισότητας μεταξύ των συνόλων των φυσικών αριθμών συνήθως παραλείπεται.
Παραπομπές
[Επεξεργασία | επεξεργασία κώδικα]- ↑ Η λέξη γλώσσα χρησιμοποιείται κάποιες φορές αντί για την υπογραφή, αλλά αυτό μπορεί να είναι κάπως δύσχρηστο γιατί η "γλώσσα" μπορεί να αναφέρεται και σε ένα σύνολο τύπων.
- ↑ Πιο συγκεκριμένα, υπάρχει μόνο μία γλώσσα για κάθε διαφορετική κατηγορία της λογικής πρώτου βαθμού: με η χωρίς ισότητες, με η χωρίς συναρτήσεις, με η χωρίς προτασιακές μεταβλητές,...
- ↑ Ορισμένοι από τους συγγραφείς που χρησιμοποιούν τον όρο "καλοσχηματισμένοι τύποι" χρησιμοποιούν τον όρο "τύπο" για να δηλώσουν οποιαδήποτε σειρά από σύμβολα της αλφαβήτου. Παρ' όλα αυτά, οι περισσότεροι συγγραφείς στη μαθηματική λογική χρησιμοποιούν τον όρο "τύπο" και εννοούν "καλοσχηματισμένο τύπο" και δεν έχουν κανέναν όρο για τους καλοσχηματισμένους τύπους. Σε κάθε κείμενο, συνήθως μας ενδιαφέρουν μόνο οι καλοσχηματισμένοι τύποι.
- ↑ The SMT-LIB Standard: Version 2.0, by Clark Barrett, Aaron Stump, and Cesare Tinelli. http://goedel.cs.uiowa.edu/smtlib/ Αρχειοθετήθηκε 2012-03-14 στο Wayback Machine.
Βιβλιογραφία
[Επεξεργασία | επεξεργασία κώδικα]- Andrews, Peter B. (2002); An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd ed., Berlin: Kluwer Academic Publishers. Available from Springer.
- Avigad, Jeremy; Donnelly, Kevin; Gray, David; and Raff, Paul (2007); "A formally verified proof of the prime number theorem", ACM Transactions on Computational Logic, vol. 9 no. 1 doi:10.1145/1297658.1297660
- Barwise, Jon (1977); "An Introduction to First-Order Logic", in Barwise, Jon, επιμ. (1982). Handbook of Mathematical Logic. Studies in Logic and the Foundations of Mathematics. Amsterdam, NL: North-Holland. ISBN 978-0-444-86388-1.
- Barwise, Jon; and Etchemendy, John (2000); Language Proof and Logic, Stanford, CA: CSLI Publications (Distributed by the University of Chicago Press)
- Bocheński, Józef Maria (2007); A Précis of Mathematical Logic, Dordrecht, NL: D. Reidel, translated from the French and German editions by Otto Bird
- Ferreirós, José (2001); The Road to Modern Logic — An Interpretation, Bulletin of Symbolic Logic, Volume 7, Issue 4, 2001, pp. 441–484, DOI 10.2307/2687794, JStor
- Gamut, L. T. F. (1991); Logic, Language, and Meaning, Volume 2: Intensional Logic and Logical Grammar, Chicago, IL: University of Chicago Press, ISBN 0-226-28088-8
- Hilbert, David; and Ackermann, Wilhelm (1950); Principles of Mathematical Logic, Chelsea (English translation of Grundzüge der theoretischen Logik, 1928 German first edition)
- Hodges, Wilfrid (2001); "Classical Logic I: First Order Logic", in Goble, Lou (ed.); The Blackwell Guide to Philosophical Logic, Blackwell
- Ebbinghaus, Heinz-Dieter; Flum, Jörg; and Thomas, Wolfgang (1994); Mathematical Logic, Undergraduate Texts in Mathematics, Berlin, DE/New York, NY: Springer-Verlag, Second Edition, ISBN 978-0-387-94258-2
- Rautenberg, Wolfgang (2010), A Concise Introduction to Mathematical Logic (3rd έκδοση), New York, NY: Springer Science+Business Media, doi: , ISBN 978-1-4419-1220-6, http://www.springerlink.com/content/978-1-4419-1220-6/[νεκρός σύνδεσμος]
- Tarski, Alfred; Givant, Steven (1987). «A Formalization of Set Theory without Variables». American Mathematical Society colloquium publications (Providence RI: American Mathematical Society) 41. ISBN 978-0821810415.
Περισσότεροι σύνδεσμοι
[Επεξεργασία | επεξεργασία κώδικα]- Hazewinkel, Michiel, επιμ.. (2001), «Predicate calculus», Encyclopedia of Mathematics, Springer, ISBN 978-1-55608-010-4, http://www.encyclopediaofmath.org/index.php?title=p/p074360
- Stanford Encyclopedia of Philosophy: Shapiro, Stewart; "Classical Logic". Covers syntax, model theory, and metatheory for first-order logic in the natural deduction style.
- Magnus, P. D.; forall x: an introduction to formal logic. Covers formal semantics and proof theory for first-order logic.
- Metamath: an ongoing online project to reconstruct mathematics as a huge first-order theory, using first-order logic and the axiomatic set theory ZFC. Principia Mathematica modernized.
- Podnieks, Karl; Introduction to mathematical logic
- Cambridge Mathematics Tripos Notes (typeset by John Fremlin). These notes cover part of a past Cambridge Mathematics Tripos course taught to undergraduates students (usually) within their third year. The course is entitled "Logic, Computation and Set Theory" and covers Ordinals and cardinals, Posets and Zorn's Lemma, Propositional logic, Predicate logic, Set theory and Consistency issues related to ZFC and other set theories.
- Tree Proof Generator can validate or invalidate formulas of FOL through the semantic tableaux method.