Agler (8.3) Symbolic Logic: Syntax, Semantics, and Proof, 'Sample Proofs', summary

 

by Corry Shores

[Search Blog Here. Index-tags are found on the bottom of the left column.]

 

[Central Entry Directory]

[Logic & Semantics, Entry Directory]

[David Agler, entry directory]

[Agler’s Symbolic Logic, entry directory]

 

[The following is summary. Boldface (except for metavariables) and bracketed commentary are my own. Please forgive my typos, as proofreading is incomplete. I highly recommend Agler’s excellent book. It is one of the best introductions to logic I have come across.]

 

Summary of

 

David W. Agler

 

Symbolic Logic: Syntax, Semantics, and Proof

 

Ch.8: Predicate Logic Derivations

 

8.3 Sample Proofs

 

Brief summary:

Agler illustrates the rules of the derivation system for making proofs in the language of predicate logic with a set of examples.

 

 

Summary

 

Agler will shows us how to use the quantifier rules for making proofs by working through a series of examples.

 

The first one is for:

(∀x)(Ax→Bx), (∃x)¬Bx ⊢ (∃x)¬Ax

(Agler 350)

[We can see that we will probably want to use modus tollens to derive the negation of the antecedent in the first premise. We cannot do this directly. So we will use an existential elimination assumption for premise 2. Then we can use universal elimination to give us the conditional in a form that we can work with. Then we can get a negated antecedent with a constant. This will allow us to use existential introduction to get the goal proposition, which we will move into the main proof using existential elimination.]

 

1	(∀x)(Ax→Bx)	P
2	(∃x)￢Bx	P
3	| ￢Ba	A/∃E
4	| Aa→Ba	1∀E
5	| ￢Aa	3,4MT
6	| (∃x)￢Ax	5∃I
7	(∃x)￢Ax	2,3–6∃E

(Agler 350)

 

Agler then shows another proof for

(∀x)(∀y)(Pxy∧Qxy), (∀z)Pzz→Sb ⊢ (∃x)Sx

(Agler 350)

[For this, we  see that we could use existential introduction on the consequent in premise 2 to get the goal proposition. For that we should obtain the antecedent. We could get that by using universal introduction on a formula of the form Paa. We could obtain such a formula but using universal elimination on the conjunction in the first premise and then using conjunction elimination to extract the first conjunct.]

 

1	(∀x)(∀y)(Pxy∧Qxy)	P
2	(∀z)Pzz→Sb	P/(∃x)Sx
3	(∀y)(Pay∧Qay)	1∀E
4	Paa∧Qaa	3∀E
5	Paa	4∧E
6	(∀z)Pzz	5∀I
7	Sb	2,6→E
8	(∃x)Sx	7∃I

(Agler 350)

 

Agler then has us consider one final example, a theorem.

⊢ (∀x)[¬(Qx→Rx)→¬Px]→(∀x)[¬(Px→Rx)→¬(Px→Qx)]

(Agler 350)

 

[Since we have a conditional, the strategy will be to assume the antecedent and derive the consequent. So first we make that assumption. Next what we should do is build the main consequent of the conclusion first with the same constants and then use universal introduction to get the form we need. So we will want ¬(Pa→Ra)→¬(Pa→Qa). Again we will assume this antecedent and derive the consequent. At this point, in order to derive ¬(Pa→Qa), we will assume the unnegated form and seek a contradiction, and then use negation introduction. Agler will do this through a series of steps that do not come intuitively to me so I will leave the reasoning to be seen in the proof.]

1	| (∀x)[￢(Qx→Rx)→￢Px]    |    |    |	A/(∀x)[￢(Px→Rx)→￢(Px→Qx)]
2	|   | ￢(Pa→Ra)    |   |	A/￢(Pa→Qa)
3	|   |   | Pa→Qa	A/P∧￢P
4	|   |   | ￢(Qa→Ra)→￢Pa	1∀E
5	|   |   | ￢(￢Pa∨Ra)	2IMP
6	|   |   | Pa∧￢Ra	5DEM+DN
7	|   |   | Pa	6∧E
8	|   |   | Qa	3,7→E
9	|   |   | ￢￢Pa	7DN
10	|   |   | Qa→Ra	4,9MT+DN
11	|   |   | Ra	8,10→E
12	|   |   | ￢Ra	6∧E
13	|   | ￢(Pa→Qa)	3–12￢I
14	| ￢(Pa→Ra)→￢(Pa→Qa)	2–13→I
15	| (∀x)[￢(Px→Rx)→￢(Px→Qx)]	14∀I
16	(∀x)[￢(Qx→Rx)→￢Px]→(∀x)[￢(Px→Rx)→￢(Px→Qx)]	1–15→I

(Agler 351)

 

 

 

Agler, David. Symbolic Logic: Syntax, Semantics, and Proof. New York: Rowman & Littlefield, 2013.

 

 

Some changes to the book quotations may have been made, as based on: http://markdfisher.com/wp-content/uploads/2014/02/PHIL_012_ONLINE_SYLLABUS_SP14-3-1.pdf .

 

.