502 – Propositional logic (2)

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 ${S}$ is a set of formulas, and ${A}$ and ${B}$ are formulas, then ${S\cup\{A\}\vdash B}$ if and only if ${S\vdash A\rightarrow B.}$

Proof: One direction is easy: Given any proof witnessing ${S\vdash A\rightarrow B,}$ one can extend it with ${A,B}$ and the resulting sequence witnesses ${S\cup\{A\}\vdash B:}$ We are allowed to add ${A,}$ since it is in ${S\cup\{A\},}$ and we can then add ${B}$ by MP.

The other direction requires a bit more work. We actually present a procedure that transforms a proof witnessing ${S\cup\{A\}\vdash B,}$ say ${t_1,\dots,t_n,}$ into a proof witnessing ${S\vdash A\rightarrow B.}$ There are three cases for each ${t_i}$ in the sequence:

Case 1: ${t_i}$ is either an axiom or ${t_i\in S.}$ Replace ${t_i}$ with the sequence ${t_i,t_i\rightarrow(A\rightarrow t_i),A\rightarrow t_i,}$ and notice that this is a proof from ${S}$ of ${A\rightarrow t_i.}$ We will frequently use this argument in what follows.

Case 2: ${t_i=A.}$ Replace ${t_i}$ with the proof of ${A\rightarrow A}$ given in Example 9 from last lecture.

Case 3: ${t_i}$ comes from previous ${t_j,t_k}$ by MP. Say ${t_k=t_j\rightarrow t_i.}$ The procedure has so far provided us with a sequence ${t=(t_1',\dots,t_m')}$ that contains a proof of ${A\rightarrow t_j}$ from ${S,}$ and also a proof of ${A\rightarrow (t_j\rightarrow t_i)}$ from ${S.}$ Replace ${t_i}$ with the sequence ${s=\bigl((A\rightarrow(t_j\rightarrow t_i))\rightarrow((A\rightarrow t_j)\rightarrow(A\rightarrow t_i)),(A\rightarrow t_j)\rightarrow(A\rightarrow t_i),A\rightarrow t_i\bigr),}$ and notice that ${t{}^\frown s}$ is a proof of ${A\rightarrow t_i}$ from ${S.}$ $\Box$

Definition 8 A set ${S}$ of formulas is formally inconsistent iff there is some formula ${A}$ such that ${S\vdash A}$ and ${S\vdash\lnot A.}$

Just as in the case of the tree system, an inconsistent set of axioms can prove anything.

Fact 1 If ${S}$ is formally inconsistent, then ${S\vdash B}$ for all ${B.}$

Proof: Let ${A}$ be such that ${S\vdash A,\lnot A.}$ Since ${S\vdash A,}$ the argument of Case 1 from Theorem 7 gives us that ${S\vdash\lnot B\rightarrow A.}$ Similarly, since ${S\vdash\lnot A,}$ then ${S\vdash \lnot B\rightarrow\lnot A.}$ Invoking axiom (3) and using MP twice, we are done. $\Box$

Theorem 9 (Proof by contradiction) ${S\cup\{A\}}$ is formally inconsistent iff ${S\vdash\lnot A.}$

Proof: One direction is clear: If ${S\vdash\lnot A,}$ then ${A\cup\{A\}\vdash A,\lnot A.}$

To prove the converse, we need a lemma:

Lemma 10 ${\lnot\lnot A\vdash A.}$

Proof: Use axiom (3) in the form ${(\lnot A\rightarrow\lnot\lnot A)\rightarrow((\lnot A\rightarrow\lnot A)\rightarrow A).}$ Since ${\lnot\lnot A}$ is given, we then have that ${\lnot A\rightarrow\lnot\lnot A.}$ We also have a proof of ${\lnot A\rightarrow\lnot A.}$ Using MP twice, we conclude ${A.}$ $\Box$

Suppose now that ${S\cup\{A\}}$ is formally inconsistent, say ${S\cup\{A\}\vdash B,\lnot B.}$ Since ${\lnot\lnot A\vdash A,}$ then ${S\cup\{\lnot\lnot A\}\vdash B,\lnot B.}$ By the deduction theorem, ${S\vdash\lnot\lnot A\rightarrow B,\lnot\lnot A\rightarrow\lnot B.}$ Using an appropriate instance of axiom (3) and invoking MP twice, we obtain that ${S\vdash \lnot A,}$ as required. $\Box$

Remark 3 Conversely, ${A\vdash\lnot\lnot A.}$ To see this, simply use proof by contradiction, noticing that ${\{A\}\cup\{\lnot A\}}$ is formally inconsistent.

Remark 4 It is in order to obtain Theorem 9 that we stated axiom ${(3)}$ the way we did. Another natural axiom to consider would have been ${(3)':}$

$\displaystyle ((B\rightarrow\lnot A)\rightarrow((B\rightarrow A)\rightarrow\lnot B)).$

The system one obtains from adopting axioms ${(1),}$ ${(2),}$ and ${(3)',}$ 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 ${(1),}$ ${(2),}$ ${(3)',}$ and ${(4):}$

$\displaystyle A\rightarrow(\lnot A\rightarrow B).$

In this system, one can prove that ${A\rightarrow\lnot\lnot A,}$ but not that ${\lnot\lnot A\rightarrow A.}$ 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) ${S\cup\{A\}\vdash\lnot B}$ iff ${S\cup\{B\}\vdash\lnot A.}$

Proof: By symmetry, it is enough to prove the left-to-right implication. Assume ${S\cup\{A\}\vdash\lnot B.}$ Then ${S\cup\{A\}\cup\{B\}}$ is formally inconsistent. By proof by contradiction, ${S\cup\{B\}\vdash\lnot A.}$ $\Box$

Say that ${S}$ 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 ${S.}$ We will soon show this, but for now we remark that in order to obtain many examples of such sets ${S,}$ it is enough to see that ${\emptyset}$ (i.e., just the set of axioms) is formally consistent.

Lemma 12 Suppose that ${S}$ is formally consistent. Then, for any formula ${A,}$ either ${S\cup\{A\}}$ or ${S\cup\{\lnot A\}}$ is also formally consistent.

Proof: Otherwise, both ${S\cup\{A\}}$ and ${S\cup\{lnot A\}}$ are formally inconsistent. By proof by contradiction, it then follows that ${S\vdash\lnot A,\lnot\lnot A,}$ and therefore ${S}$ itself is formally inconsistent. $\Box$

Say that a set ${S}$ is complete iff for any formula ${A,}$ either ${A\in S}$ or ${\lnot A\in S.}$

The argument below should remind the reader of (part of) the argument of completeness for the tree system.

Corollary 13 Suppose that ${S}$ is formally consistent. Then there is a set ${\hat S\supseteq S}$ 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 ${\{A_0,A_1,\dots\}.}$ Now use Lemma 12 to form a sequence ${S= S_0\supseteq S_1\supseteq\dots}$ where each ${S_n}$ is formally consistent and either ${S_{n+1}=S_n\cup\{A_n\}}$ or ${S_{n+1}=S_n\cup\{\lnot A_n\}.}$

Set ${\hat S=\bigcup_n S_n,}$ and note that ${\hat S}$ extends ${S}$ and is both formally consistent and complete, as required. $\Box$

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 ${S.}$

Definition 14 A truth assignment or valuation is a function ${v}$ from the set of propositional variables into ${\{0,1\}.}$

We identify ${0}$ with false and ${1}$ with true, so ${v(p)=1}$ is our formalization of the statement that ${p}$ is true.

Definition 15 The lifting of a valuation ${v}$ is the function ${v^*}$ extending ${v,}$ defined on the set of all formulas, and given recursively by the following clauses:

${v^*(\lnot A)=1-v^*(A).}$

${v^*(A\rightarrow B)=1-v^*(A)(1-v^*(B)).}$

The common practice (that we follow) is to just write ${v}$ instead of ${v^*}$ unless there is danger of confusion. Note that ${v(A)\in\{0,1\}}$ for all formulas ${A,}$ and that ${v(A\rightarrow B)=0}$ iff ${v(A)=1}$ and ${v(B)=0.}$

(This should probably remind the reader of truth tables.)

There is a slight inconvenience with this definition, in that even if a formula ${A}$ only uses one propositional variable ${p,}$ we need to consider functions defined on infinitely many arguments in order to evaluate the truth or falsity of ${A.}$ The following straightforward observation allows us to avoid this problem.

Definition 16 The support ${{\rm supp}(A)}$ of a formula ${A}$ is the set of propositional variables mentioned in ${A.}$ Recursively, one can define this set by the following clauses:

${{\rm supp}(p)=\{p\}.}$

${{\rm supp}(\lnot A)={\rm supp}(A).}$

${{\rm supp}(A\rightarrow B)={\rm supp}(A)\cup{\rm supp}(B).}$

The following can be easily shown by induction on the length of a parsing sequence.

Fact 2 Let ${A}$ be a formula. Suppose that ${v_1}$ and ${v_2}$ are valuations, and that ${v_1\upharpoonright{\rm supp}(A)=v_2\upharpoonright{\rm supp}(A).}$ Then in fact ${v_1(A)=v_2(A).}$ ${\Box}$

Remark 5 Going through the parsing sequence of a formula provides us with an easy algorithm to evaluate ${v(A)}$ from ${v\upharpoonright{\rm supp}(A).}$

Recall our convention that ${A\lor B}$ is shorthand for ${(\lnot A\rightarrow B).}$ Given a valuation ${v,}$ we then have ${v(A\lor B)=1-(1-v(A))(1-v(B)),}$ and it follows that ${v(A\lor B)=0}$ iff ${v(A)=v(B)=0.}$

Similarly, one can check that ${v(A\land B)=1}$ iff ${v(A)=v(B)=1,}$ and that ${v(A\leftrightarrow B)=1}$ iff ${v(A)=v(B).}$

Our conventions where chosen so that we would recover the usual truth tables of the connectives.

Definition 17 Given a valuation ${v}$ and a formula ${A,}$ say that ${v\models A}$ , “ ${v}$ models ${A}$ ,” or “ ${v}$ satisfies ${A}$ ,” or “ ${v}$ makes ${A}$ true,” iff ${v(A)=1.}$ Otherwise, we write ${v\not\models A.}$

Remark 6 We can easily check that:

${v\models\lnot A}$ iff ${v\not\models A.}$

${v\models A\land B}$ iff ${v\models A}$ and ${v\models B.}$

${v\models A\lor B}$ iff ${v\models A}$ or ${v\models B.}$

${v\models A\rightarrow B}$ iff either ${v\not\models A,}$ or else ${v\models B.}$

${v\models A\leftrightarrow B}$ iff ( ${v\models A}$ iff ${v\models B}$ ). I.e., iff either both ${v\models A}$ and ${v\models B,}$ or else both ${v\not\models A}$ and ${v\not\models B.}$

Definition 18 A formula ${A}$ is said to be valid, or a tautology, iff ${v\models A}$ for all valuations ${v.}$

There are ${|2^{\mathbb N}|=|{\mathbb R}|}$ many valuations, but thanks to Fact 2, only finitely many ( ${2^{|{\rm supp}(A)|}}$ ) valuations need to be considered to determine whether ${A}$ is a tautology or not.

The following are examples of tautologies:

Example 10 The axioms are tautologies. For example, consider ${A\rightarrow(B\rightarrow A).}$ Let ${v}$ be a valuation. Then ${v\not\models A\rightarrow(B\rightarrow A)}$ iff ${v\models A}$ and ${v\not\models B\rightarrow A,}$ i.e., iff ${v\models A}$ and ${v\models B}$ and ${v\not\models A,}$ which of course is impossible.

Similar easy contradictions hold in the other two cases: ${v\not\models(A\rightarrow(B\rightarrow C))\rightarrow((A\rightarrow B)\rightarrow(A\rightarrow C))}$ iff ${v\models A\rightarrow(B\rightarrow C)}$ and ${v\not\models(A\rightarrow B)\rightarrow(A\rightarrow C),}$ iff ${v\models A\rightarrow(B\rightarrow C)}$ and ${v\models A\rightarrow B}$ but ${v\not\models A\rightarrow C.}$ This last clause requires that ${v\models A}$ and ${v\not\models C.}$ The second to last clause requires then that ${v\models B.}$ Hence, ${v\not\models B\rightarrow C}$ but ${v\models A,}$ so ${v\not\models A\rightarrow(B\rightarrow C),}$ against our assumption.

Finally, ${v\not\models(\lnot A\rightarrow\lnot B)\rightarrow(\lnot A\rightarrow B)\rightarrow A)}$ iff ${v\models\lnot A\rightarrow\lnot B}$ and ${v\models \lnot A\rightarrow B}$ and ${v\not\models A.}$ This last clause forces that ${v\models\lnot A,}$ and therefore we must have both ${v\models \lnot B}$ and ${v\models B,}$ which is impossible.

Example 11 ${\lnot\lnot A\leftrightarrow A}$ is a tautology. Whenever ${A\leftrightarrow B}$ is a tautology, we say that ${A}$ and ${B}$ are logically equivalent, ${A\equiv B.}$ One also says that ${A}$ and ${B}$ are semantically indistinguishable. It is straightforward to verify that ${\equiv}$ is an equivalence relation.

Example 12 ${A\rightarrow A}$ is a tautology. This is easily verified directly. Next lecture we will see that, in fact, any theorem (i.e., any ${A}$ such that ${\vdash A}$ ) is a tautology.

Typeset using LaTeX2WP. Here is a printable version of this post.

This entry was posted on Thursday, September 10th, 2009 at 10:28 am and is filed under 502: Logic and set theory. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.

	ปั่นสล็อต on 414/514 The theorems of Rieman…
	Richard Kimberly Hec… on Woodin’s proof of the se…
	Is there a Borel-mea… on 414/514 Examples of Baire clas…
	Simple bijectiveness… on 580 -Some choiceless results…
	Schur’s theore… on 580 -III. Partition calcu…
	Uncountable linearly… on 403/503 – Homework …
	What is a non-constr… on On strong measure zero se…
	function from Nmathb… on Hindsight
	Cauchy Schwarz Inequ… on 275 -Positive polynomials
	What is a Cantor-sty… on 580 -Some choiceless results…
	Question about Gener… on 580 -Some choiceless results…
	Set has Measure Zero… on On strong measure zero se…
	Non-measurable subse… on 580 -Cardinal arithmetic …
	hmeng1 on 414/514 The theorems of Rieman…
	580 -Cardinal arithm… on 580 -Cardinal arithmetic …

A kind of library