To be continued...
Glossary of First-Order Logic, by Peter Suber
Term |
Explanation |
| A | |
| axioms of logic | ML, Section 1.3 |
| atomic formula | ML, Section 1.2 |
| C | |
| classical logic | ML, Section 1.3 |
| clause form / clausal form | ML, Section 5.4 |
| completeness | ML, Section 1.3 |
| Completeness Theorem / classical propositional logic | ML, Section 4.2 |
| Completeness Theorem / classical predicate logic | ML, Section 4.3 |
| Completeness Theorem / constructive propositional logic | ML, Section 4.4 |
| Completeness Theorem / constructive predicate logic | ML, Section 4.5 |
| conjunctive normal form | ML, Section 5.2 |
| consistency | ML, Section 1.3 |
| constructive logic | =intuitionistic logic, ML, Section 1.3 |
| contradiction | ML, Section 1.3 |
| Contraposition Law | ML, Section 2.4 (provable in minimal logic) |
| D | |
| de Morgan Law / First | ML, Section 2.4 (provable in minimal logic) |
| de Morgan Law / Second | ML, Section 2.4 (part provable in minimal logic), ML, Section 2.6 (part provable in classical logic) |
| deduction theorem | ML, Section 1.5 |
| disjunctive normal form | ML, Section 5.2 |
| domain / of interpretation | ML, Section 4.1 |
| Double Negation Law | ML, Section 2.6 (provable in classical logic) |
| E | |
| elementary formula | same as atomic formula, ML, Section 1.2 |
| embedding / constructive | ML, Section 3.5 |
| Equivalence Theorem | see Replacement Theorem |
| Excluded Middle / Law of | ML, Section 1.3 |
| F | |
| first order language | ML, Section 1.2 |
| first order theory | ML, Section 1.3 |
| formal theory | ML, Section 1.1 |
| G | |
| Glivenko's Theorem | ML, Section 2.7 |
| Goedel's Completeness Theorem | see Completeness Theorem / classical predicate logic |
| ground clause | ML, Section 5.6 |
| H | |
| Henkin's Model Existence Theorem | see Model Existence Theorem / Henkin's |
| Herbrand's Theorem / universe | ML, Section 5.6 |
| Horn clauses | ML, Section 5.4 (incomplete) |
| I | |
| independence of axioms | ML, Section 2.8 |
| interpretation | ML, Section 4.1 |
| intuitionistic logic | =constructive logic |
| K | |
| Kripke model / structure | ML, Section 4.4 |
| L | |
| Lindenbaum's Lemma | ML, Section 4.3 |
| logic | ML, Section 1.1 |
| logically valid formula | ML, Section 4.1 |
| M | |
| many sorted logic | Chapter 10. Many-Sorted First Order Logic, by Jean Gallier |
| many valued logic | ML, Section 2.8 |
| material implication / paradoxes of | ML, Section 1.3, Paradoxes of Material Implication, by Peter Suber |
| mgu | most general unifier |
| minimal logic | ML, Section 1.3 |
| Model Existence Theorem / Henkin's | ML, Section 4.3 |
| Modus Ponens | ML, Section 1.3 |
| Modus Tollens | ML, Section 2.4 (provable in minimal logic) |
| most general unifier / mgu | ML, Section 5.7 |
| N | |
| negation as contradiction / absurdity | ML, Section 7.1 |
| P | |
| Peirce's Law | ML, Section 2.6 (provable in classical logic) |
| predicate logic / calculus | ML, Section 1.3 |
| prenex normal form | ML, Section 5.1 |
| prime formula | same as atomic formula, ML, Section 1.2 |
| proof / formal proof | ML, Section 1.3 |
| propositional logic / calculus | ML, Section 1.3 |
| R | |
| Replacement Theorem | ML, Section 3.4 |
| resolution method / propositional logic | ML, Section 5.5 |
| resolution method / predicate logic | ML, Section 5.7 |
| Robinson's resolution method | resolution method |
| Rosser's theorem | GT, Section 5.3, Rossers Theorem |
| S | |
| satisfiability | ML, Section 4.1 |
| Skolem normal form | ML, Section 5.3 |
| Skolem's Paradox | ML, Section 4.3 |
| stable formula | ML, Section 3.5 |
| Substitution Theorem | see Replacement Theorem |
| Syllogism / Law of | ML, Section 2.1 |
| T | |
| tautology | ML, Section 4.2 |
| term / functional expression | ML, Section 1.3 |
| tertium no datur | Excluded Middle / Law of |
| theorem | ML, Section 1.3 |
| true formula | ML, Section 4.1 |
| truth tables / classical | ML, Section 4.2 |
| U | |
| unification / algorithm | ML, Section 5.7 |
| unifier | ML, Section 5.7 |
| V | |
| W | |
| Z |