Now that we can express interesting concepts using the quantifiers "∃" ("there exists") and "∀" ("for all"), how can we use them for the problem of determining whether a formula is true? Back in lowly propositional logic, we had three methods:
- truth tables,
- equivalences, and
- formal proofs with inference rules.
How can we adapt these approaches, for first-order logic?
Well, truth tables have no analog approach. With quantifiers, we don't have a finite set of propositions. Furthermore, variables can't refer to specific items in the domain until we try to interpret them. And when we do, the domain may be of any size possibly even infinite. Using a truth table on an infinite domain is clearly infeasible, but the real problem stems from how we want to be able to discuss reasoning without respect to a particular domain.
However, we can add equivalences and inference rules to cope with quantifiers. After showing how to work with quantifiers, we'll come back to examine our newly-augmented systems for those desirable traits, soundness and completeness.
- 1157 reads
