I now proceed to present a series of results whose overall goal is to make the handling of formal proofs more efficient and natural. These results formalize different methods of reasoning commonly used in practice. A second goal in presenting these results is in preparing the way for the proof of the completeness theorem.
Theorem 7 (The deduction theorem) If is a set of formulas, and and are formulas, then if and only if
Proof: One direction is easy: Given any proof witnessing one can extend it with and the resulting sequence witnesses We are allowed to add since it is in and we can then add by MP.
The other direction requires a bit more work. We actually present a procedure that transforms a proof witnessing say into a proof witnessing There are three cases for each in the sequence:
Case 1: is either an axiom or Replace with the sequence and notice that this is a proof from of We will frequently use this argument in what follows.
Case 2: Replace with the proof of given in Example 9 from last lecture.
Case 3: comes from previous by MP. Say The procedure has so far provided us with a sequence that contains a proof of from and also a proof of from Replace with the sequence and notice that is a proof of from
Definition 8 A set of formulas is formally inconsistent iff there is some formula such that and
Just as in the case of the tree system, an inconsistent set of axioms can prove anything.
Fact 1 If is formally inconsistent, then for all
Proof: Let be such that Since the argument of Case 1 from Theorem 7 gives us that Similarly, since then Invoking axiom (3) and using MP twice, we are done.
Theorem 9 (Proof by contradiction) is formally inconsistent iff
Proof: One direction is clear: If then
To prove the converse, we need a lemma:
Proof: Use axiom (3) in the form Since is given, we then have that We also have a proof of Using MP twice, we conclude
Suppose now that is formally inconsistent, say Since then By the deduction theorem, Using an appropriate instance of axiom (3) and invoking MP twice, we obtain that as required.
Remark 3 Conversely, To see this, simply use proof by contradiction, noticing that is formally inconsistent.
Remark 4 It is in order to obtain Theorem 9 that we stated axiom the way we did. Another natural axiom to consider would have been
The system one obtains from adopting axioms and is strictly weaker (in several senses; for example, it proves fewer theorems) that the system we are using.
The standard system of propositional intuitionistic logic is obtained by adopting axioms and
In this system, one can prove that but not that The semantics of propositional logic (to be discussed below) is also considerably simpler than the appropriate semantics of its intuitionistic counterpart.
Theorem 11 (Proof by contrapositive) iff
Proof: By symmetry, it is enough to prove the left-to-right implication. Assume Then is formally inconsistent. By proof by contradiction,
Say that is formally consistent precisely when it is not formally inconsistent. It should be clear by now that the main question we need to address is whether there are formally consistent sets We will soon show this, but for now we remark that in order to obtain many examples of such sets it is enough to see that (i.e., just the set of axioms) is formally consistent.
Lemma 12 Suppose that is formally consistent. Then, for any formula either or is also formally consistent.
Proof: Otherwise, both and are formally inconsistent. By proof by contradiction, it then follows that and therefore itself is formally inconsistent.
Say that a set is complete iff for any formula either or
The argument below should remind the reader of (part of) the argument of completeness for the tree system.
Corollary 13 Suppose that is formally consistent. Then there is a set that is both formally consistent and complete.
Proof: First notice that by an easy counting argument there are only countably many formulas, so one can enumerate them as Now use Lemma 12 to form a sequence where each is formally consistent and either or
Set and note that extends and is both formally consistent and complete, as required.
9. Semantics of propositional logic
We now proceed to assign an interpretation to our axioms and rules of deduction. The idea is that we decide “arbitrarily” precisely which propositional variables represent true statements, and from there we can conclude the truth or falsity of any formula. This will allow us, among other things, to verify that there are formally consistent sets
Definition 14 A truth assignment or valuation is a function from the set of propositional variables into
We identify with false and with true, so is our formalization of the statement that is true.
Definition 15 The lifting of a valuation is the function extending defined on the set of all formulas, and given recursively by the following clauses:
The common practice (that we follow) is to just write instead of unless there is danger of confusion. Note that for all formulas and that iff and
(This should probably remind the reader of truth tables.)
There is a slight inconvenience with this definition, in that even if a formula only uses one propositional variable we need to consider functions defined on infinitely many arguments in order to evaluate the truth or falsity of The following straightforward observation allows us to avoid this problem.
Definition 16 The support of a formula is the set of propositional variables mentioned in Recursively, one can define this set by the following clauses:
The following can be easily shown by induction on the length of a parsing sequence.
Fact 2 Let be a formula. Suppose that and are valuations, and that Then in fact
Remark 5 Going through the parsing sequence of a formula provides us with an easy algorithm to evaluate from
Recall our convention that is shorthand for Given a valuation we then have and it follows that iff
Similarly, one can check that iff and that iff
Our conventions where chosen so that we would recover the usual truth tables of the connectives.
Definition 17 Given a valuation and a formula say that , “ models ,” or “ satisfies ,” or “ makes true,” iff Otherwise, we write
Remark 6 We can easily check that:
- iff and
- iff or
- iff either or else
- iff ( iff ). I.e., iff either both and or else both and
Definition 18 A formula is said to be valid, or a tautology, iff for all valuations
There are many valuations, but thanks to Fact 2, only finitely many () valuations need to be considered to determine whether is a tautology or not.
The following are examples of tautologies:
Example 10 The axioms are tautologies. For example, consider Let be a valuation. Then iff and i.e., iff and and which of course is impossible.
Similar easy contradictions hold in the other two cases: iff and iff and but This last clause requires that and The second to last clause requires then that Hence, but so against our assumption.
Finally, iff and and This last clause forces that and therefore we must have both and which is impossible.
Example 11 is a tautology. Whenever is a tautology, we say that and are logically equivalent, One also says that and are semantically indistinguishable. It is straightforward to verify that is an equivalence relation.
Example 12 is a tautology. This is easily verified directly. Next lecture we will see that, in fact, any theorem (i.e., any such that ) is a tautology.
Typeset using LaTeX2WP. Here is a printable version of this post.