Checking logical entailment with truth tables has the merit of being conceptually simple. However, it is not always the most practical method. The number of truth assignments of a language grows exponentially with the number of logical constants. When the number of logical constants in a propositional language is large, it may be impossible to process its truth table.
Proof methods provide an alternative way of checking logical entailment that addresses this problem. In many cases, it is possible to create a proof of a conclusion from a set of premises that is much smaller than the truth table for the language; moreover, it is often possible to find such proofs with less work than is necessary to check the entire truth table.
We begin this lesson by defining some basic concepts - axiom schemas, rules of inference, and direct proofs. We then look at a couple of proof systems, with emphasis on one particular proof system, viz. the Hilbert system. After that, we look at the properties of soundness and completeness - the standards by which proof systems are judged. Finally, we look at hierarchical proofs and some meta-theorems about proofs.
Use the arrow keys to navigate. Press the escape key to toggle all / one.