David W. Agler
Symbolic Logic: Syntax, Semantics, and Proof
7.3 Logical Properties
7.3 Logical Properties
To illustrate what makes a completed open branch, Agler first shows one that looks like it could be an example but in fact is not.Completed open branch: A branch is a completed open branch if and only if (1) all complex propositions that can be decomposed into atomic propositions or negated atomic propositions are decomposed; (2) for all universally quantified propositions ‘(∀x)P’ occurring in the branch, there is a substitution instance ‘P(a/x)’ for each constant that occurs in that branch; and (3) the branch is not a closed branch.Closed tree: A tree is a closed tree if and only if all branches close.Closed branch: A branch is a closed branch if and only if there is a proposition and its literal negation (e.g., ‘P’ and ‘¬P’).(Agler 294)
1

(∀x)(Px→Qx)

P

2

(∃x)(Px∧¬Qx)✔

P

3

Pa→Qa✔

1∀D

4

Pb∧¬Qb✔

2∃D

5

Pb

4∧D

6

¬Qb
/ \
/ \

4∧D

7
 ¬Pa Qa 
3→D

For all universally quantified propositions ‘(∀x)P’ occurring in the branch, there is a substitution instance ‘P(a/x)’ for each constant that occurs in that branch.(294d)
1

(∀x)(Px→Qx)

P

2

(∃x)(Px∧¬Qx)✔

P

3

Pa→Qa✔

1∀D

4

Pb∧¬Qb✔

2∃D

5

Pb

4∧D

6

¬Qb
/ \
/ \

4∧D

7
 ¬Pa Qa 
3→D

8
 Pb→Qb Pb→Qb / \ / \ 
1∀D

9
 ¬Pb Qb ¬Pb Qb X X X X 
8→D

(∀x)(¬Px→¬Rx), (∀x)(Rx→Px)(Agler 295)
1

(∀x)(¬Px→¬Rx)

P

2

(∀x)(Rx→Px)

P

1

(∀x)(¬Px→¬Rx)

P

2

(∀x)(Rx→Px)

P

3

¬Pa→¬Ra

1∀D

1

(∀x)(¬Px→¬Rx)

P

2

(∀x)(Rx→Px)

P

3

¬Pa→¬Ra

1∀D

4

Ra→Pa

2∀D

1

(∀x)(¬Px→¬Rx)

P

2

(∀x)(Rx→Px)

P

3

¬Pa→¬Ra✔

1∀D

4

Ra→Pa✔
/ \

2∀D

5

¬¬Pa ¬Ra
/ \ / \

3→D

6
 ¬Ra Pa ¬Ra Pa O O O O 
4→D

In PL, the basic unit of representation is the proposition, which is assigned a truth value (true or false). In RL, the truth or falsity of a predicate wellformed formula (wff, pronounced ‘woof’) is relative to an interpretation in a model (i.e., relative to a specification of the domain of discourse and an interpretation function). Using the notion of an interpretation, semantic properties can be defined for RL propositions, sets of propositions, and arguments as follows:Tautology: A proposition ‘P’ is a tautology in RL if and only if ‘P’ is true on every interpretation.Contradiction: A proposition ‘P’ is a contradiction in RL if and only if ‘P’ is false on every interpretation.Contingency: A proposition ‘P’ is a contingency in RL if and only if ‘P’ is neither a contradiction nor a tautology.Equivalence Propositions: ‘P’ and ‘Q’ are equivalent in RL if and only if there is no interpretation where the valuation of ‘P’ is different from the valuation of ‘Q.’Consistency: A set of propositions ‘{A, B, C, ..., Z}’ is consistent in RL if and only if there is at least one interpretation such that all of the propositions in the set are true.Validity: An argument ‘P, Q, R, ..., Y⊢Z’ is valid in RL if and only if there is no interpretation such that all of the premises ‘A,’ ‘B,’ ‘C,’ ..., ‘Y’ are true and the conclusion ‘Z’ is false.(Agler 296)
(∀x)Px(∃x)Rx(Agler 296)
to show that ‘{(∀x)Px, (∃x)Rx}’ is consistent in RL involves showing that there is at least one interpretation in a model where v(∀x)Px = T and v(∃x)Rx = T. Here is an example of such a model:D = positive integersP = {x  x is greater than 0}R = {x  x is even}(Agler 296)
1

(∃x)Px

P

2

Pa

P

1

(∃x)Px

P

2

Pa

P

3

Pb

1∃D

1

(∃x)Px

P

2

Pa

P

3

Pb
O

1∃D

we would stipulate a domain of discourse involving two objects, letting ‘a’ stand for an object and ‘b’ stand for an object, and assign the oneplace predicate ‘P’ an extension.D: {John, Fred}Px: x is a person {John, Fred}a: Johnb: Fred(Agler 297)
1

(∀x)Px

P

2

(∃x)Px∨¬(∃x)Px

P

1

(∀x)Px

P

2

(∃x)Px∨¬(∃x)Px
/ \ 
P

3
 (∃x)Px ¬(∃x)Px 
2∨D

1
 (∀x)Px 
P

2
 (∃x)Px∨¬(∃x)Px / \ 
P

3
 (∃x)Px ¬(∃x)Px 
2∨D

4
 Pa  
3∃D

1

(∀x)Px

P

2
 (∃x)Px∨¬(∃x)Px / \ 
P

3
 (∃x)Px ¬(∃x)Px 
2∨D

4
 Pa  
3∃D

5
 Pa  
1∀D

1

(∀x)Px

P

2
 (∃x)Px∨¬(∃x)Px / \ 
P

3
 (∃x)Px ¬(∃x)Px 
2∨D

4
 Pa  
3∃D

5
 Pa  O  1∀D 
1

(∀x)Px

P

2
 (∃x)Px∨¬(∃x)Px / \ 
P

3
 (∃x)Px ¬(∃x)Px 
2∨D

4
 Pa  
3∃D

5
 Pa  O   1∀D 
6
 (∀x)¬Px  3¬∃D 
1

(∀x)Px

P

2
 (∃x)Px∨¬(∃x)Px / \ 
P

3
 (∃x)Px ¬(∃x)Px 
2∨D

4
 Pa  
3∃D

5
 Pa  O  
1∀D

6
 (∀x)¬Px 
3¬∃D

7
 ¬Pa  6∀D 
8
 Pa 
1∀D

1

(∀x)Px

P

2

(∃x)Px∨¬(∃x)Px
/ \ 
P

3

(∃x)Px ¬(∃x)Px 
2∨D

4

Pa  
3∃D

5

Pa  O  
1∀D

6

(∀x)¬Px 
3¬∃D

7

¬Pa  6∀D 
8  Pa O 
1∀D

D: {1}Px: x is a number(Agler 298)
1

(∃x)(∃y)[(Ox∧Ey)∧Gxy]

P

1

(∃x)(∃y)[(Ox∧Ey)∧Gxy]✔

P

2

(∃y)[(Oa∧Ey)∧Gay]

1∃D

1

(∃x)(∃y)[(Ox∧Ey)∧Gxy]✔

P

2

(∃y)[(Oa∧Ey)∧Gay]✔

1∃D

3

(Oa∧Eb)∧Gab

2∃D

1

(∃x)(∃y)[(Ox∧Ey)∧Gxy]✔

P

2

(∃y)[(Oa∧Ey)∧Gay]✔

1∃D

3

(Oa∧Eb)∧Gab✔

2∃D

4

Oa∧Eb✔

3∧D

5

Gab

3∧D

6

Oa

4∧D

7

Eb

4∧D

1

(∃x)(∃y)[(Ox∧Ey)∧Gxy]✔

P

2

(∃y)[(Oa∧Ey)∧Gay]✔

1∃D

3

(Oa∧Eb)∧Gab✔

2∃D

4

Oa∧Eb✔

3∧D

5

Gab

3∧D

6

Oa

4∧D

7

Eb
O

4∧D

there is an interpretation for which the propositions ‘Gab,’ ‘Oa,’ and ‘Eb’ are true, and thus ‘(∃x)(∃y) [(Ox∧Ey)∧Gxy]’ is true. Again, a model can be constructed to reflect this fact:D: {1, 2, 3}Ox: x is an odd numberEx: x is an even numberGxy: x is greater than ya: 3b: 2‘Gab’ is true since it is true that 3 is greater than 2. ‘Oa’ is true since three is an odd number. Lastly, ‘Eb’ is true since 2 is an even number. Thus, the predicate wff ‘(∃x)(∃y)[(Ox∧Ey)∧Gxy],’ which says that there exists an odd number greater than  some existent even number, is also true. In short, the truth tree, along with the model, demonstrates that the set ‘{(∃x)(∃y)[(Ox∧Ey)∧Gxy]}’ is not a contradiction in RL.(Agler 298299)
Consistency: A set of propositions ‘{P, Q, R, ..., Z}’ is shown by the truthtree method to be consistent if and only if a tree of the stack ‘P,’ ‘Q,’ ‘R,’ . . ., ‘Z’ is an open tree; that is, there is at least one completed open branch.
Inconsistency: A set of propositions ‘{P, Q, R, ..., Z}’ is shown by the truthtree method to be inconsistent if and only if a tree of the stack of ‘P,’ ‘Q,’ ‘R,’ . . ., ‘Z’ is a closed tree; that is, all branches close.
(Agler 299)
(∀x)(Px→Rx), ¬(∀x)(¬Rx→¬Px)(Agler 299)
1

(∀x)(Px→Rx)

P

2

¬(∀x)(¬Rx→¬Px)

P

1

(∀x)(Px→Rx)

P

2

¬(∀x)(¬Rx→¬Px)✔

P

3

(∃x)¬(¬Rx→¬Px)

2¬∀D

1

(∀x)(Px→Rx)

P

2

¬(∀x)(¬Rx→¬Px)✔

P

3

(∃x)¬(¬Rx→¬Px)✔

2¬∀D

4

¬(¬Ra→¬Pa)

3∃D

1

(∀x)(Px→Rx)

P

2

¬(∀x)(¬Rx→¬Px)✔
 P 
3

(∃x)¬(¬Rx→¬Px)✔

2¬∀D

4

¬(¬Ra→¬Pa)

3∃D

5

Pa→Ra

1∀D

1

(∀x)(Px→Rx)

P

2

¬(∀x)(¬Rx→¬Px)✔
 P 
3

(∃x)¬(¬Rx→¬Px)✔

2¬∀D

4

¬(¬Ra→¬Pa)

3∃D

5

Pa→Ra✔

1∀D

6

¬Ra

4¬→D

7

¬¬Pa

4¬→D

1

(∀x)(Px→Rx)

P

2

¬(∀x)(¬Rx→¬Px)✔
 P 
3

(∃x)¬(¬Rx→¬Px)✔

2¬∀D

4

¬(¬Ra→¬Pa)

3∃D

5

Pa→Ra✔

1∀D

6

¬Ra

4¬→D

7

¬¬Pa✔

4¬→D

8

Pa

7¬¬D

1

(∀x)(Px→Rx)

P

2

¬(∀x)(¬Rx→¬Px)✔
 P 
3

(∃x)¬(¬Rx→¬Px)✔

2¬∀D

4

¬(¬Ra→¬Pa)

3∃D

5

Pa→Ra✔

1∀D

6

¬Ra

4¬→D

7

¬¬Pa✔

4¬→D

8

Pa
/ \

7¬¬D

9

¬Pa Ra

5→D

1

(∀x)(Px→Rx)

P

2

¬(∀x)(¬Rx→¬Px)✔
 P 
3

(∃x)¬(¬Rx→¬Px)✔

2¬∀D

4

¬(¬Ra→¬Pa)

3∃D

5

Pa→Ra✔

1∀D

6

¬Ra

4¬→D

7

¬¬Pa✔

4¬→D

8

Pa
/ \

7¬¬D

9

¬Pa Ra

5→D

1

(∀x)(Px)→(∀y)(Ry)

P

2

¬(∀y)Ry

P

3

(∃x)¬Px

P

1

(∀x)(Px)→(∀y)(Ry)

P

2

¬(∀y)Ry✔

P

3

(∃x)¬Px

P

4

(∃y)¬Ry

2¬∀D

1

(∀x)(Px)→(∀y)(Ry)

P

2

¬(∀y)Ry✔

P

3

(∃x)¬Px✔

P

4

(∃y)¬Ry✔

2¬∀D

5

¬Ra

4∃D

6

¬Pb

3∃D

1

(∀x)(Px)→(∀y)(Ry)✔

P

2

¬(∀y)Ry✔

P

3

(∃x)¬Px✔

P

4

(∃y)¬Ry✔

2¬∀D

5

¬Ra

4∃D

6

¬Pb
/ \

3∃D

7

¬(∀x)Px (∀y)Ry

1→D

1

(∀x)(Px)→(∀y)(Ry)✔

P

2

¬(∀y)Ry✔

P

3

(∃x)¬Px✔

P

4

(∃y)¬Ry✔

2¬∀D

5

¬Ra

4∃D

6

¬Pb
/ \

3∃D

7

¬(∀x)Px✔ (∀y)Ry

1→D

8

(∃x)¬Px 
 7¬∀D 
1

(∀x)(Px)→(∀y)(Ry)✔

P

2

¬(∀y)Ry✔

P

3

(∃x)¬Px✔

P

4

(∃y)¬Ry✔

2¬∀D

5

¬Ra

4∃D

6

¬Pb
/ \

3∃D

7

¬(∀x)Px✔ (∀y)Ry

1→D

8

(∃x)¬Px✔ 
 7¬∀D 
9

¬Pc 

8∃D

1

(∀x)(Px)→(∀y)(Ry)✔

P

2

¬(∀y)Ry✔

P

3

(∃x)¬Px✔

P

4

(∃y)¬Ry✔

2¬∀D

5

¬Ra

4∃D

6

¬Pb
/ \

3∃D

7

¬(∀x)Px✔ (∀y)Ry

1→D

8

(∃x)¬Px✔ 
 7¬∀D 
9

¬Pc 
O 

8∃D

1

(∀x)(Px)→(∀y)(Ry)✔

P

2

¬(∀y)Ry✔

P

3

(∃x)¬Px✔

P

4

(∃y)¬Ry✔

2¬∀D

5

¬Ra

4∃D

6

¬Pb
/ \

3∃D

7

¬(∀x)Px✔ (∀y)Ry

1→D

8

(∃x)¬Px✔ 
 7¬∀D 
9

¬Pc 
O 

8∃D

10

Ra
 7∀D 
11 
Rb
 7∀D 
1

(∀x)(Px)→(∀y)(Ry)✔

P

2

¬(∀y)Ry✔

P

3

(∃x)¬Px✔

P

4

(∃y)¬Ry✔

2¬∀D

5

¬Ra

4∃D

6

¬Pb
/ \

3∃D

7

¬(∀x)Px✔ (∀y)Ry

1→D

8

(∃x)¬Px✔ 
 7¬∀D 
9

¬Pc 
O 

8∃D

10

Ra
 7∀D 
11 
Rb
X
 7∀D 
1

¬(∀x)(∃y)(Pxy)∧(∀y)¬(∃x)(Rxy)

P

2

¬(∀y)(∀x)(Rxy)

P

3

(Rab∧Rba)∧Pab

P

1

¬(∀x)(∃y)(Pxy)∧(∀y)¬(∃x)(Rxy)

P

2

¬(∀y)(∀x)(Rxy)

P

3

(Rab∧Rba)∧Pab ✔

P

4

Rab∧Rba✔
 3∧D 
5

Pab

3∧D

6

Rab

4∧D

7

Rba

4∧D

1

¬(∀x)(∃y)(Pxy)∧(∀y)¬(∃x)(Rxy)✔

P

2

¬(∀y)(∀x)(Rxy)

P

3

(Rab∧Rba)∧Pab ✔

P

4

Rab∧Rba✔
 3∧D 
5

Pab

3∧D

6

Rab

4∧D

7

Rba

4∧D

8

¬(∀x)(∃y)(Pxy)

1∧D

9

(∀y)¬(∃x)(Rxy)

1∧D

1

¬(∀x)(∃y)(Pxy)∧(∀y)¬(∃x)(Rxy)✔

P

2

¬(∀y)(∀x)(Rxy)✔

P

3

(Rab∧Rba)∧Pab ✔

P

4

Rab∧Rba✔
 3∧D 
5

Pab

3∧D

6

Rab

4∧D

7

Rba

4∧D

8

¬(∀x)(∃y)(Pxy)✔

1∧D

9

(∀y)¬(∃x)(Rxy)

1∧D

10

(∃x)¬(∃y)(Pxy)

8¬∀D

11

(∃y)¬(∀x)(Rxy)

2¬∀D

1

¬(∀x)(∃y)(Pxy)∧(∀y)¬(∃x)(Rxy)✔

P

2

¬(∀y)(∀x)(Rxy)✔

P

3

(Rab∧Rba)∧Pab ✔

P

4

Rab∧Rba✔
 3∧D 
5

Pab

3∧D

6

Rab

4∧D

7

Rba

4∧D

8

¬(∀x)(∃y)(Pxy)✔

1∧D

9

(∀y)¬(∃x)(Rxy)

1∧D

10

(∃x)¬(∃y)(Pxy)✔

8¬∀D

11

(∃y)¬(∀x)(Rxy)

2¬∀D

12

¬(∃y)(Pcy)

10∃D

1

¬(∀x)(∃y)(Pxy)∧(∀y)¬(∃x)(Rxy)✔

P

2

¬(∀y)(∀x)(Rxy)✔

P

3

(Rab∧Rba)∧Pab ✔

P

4

Rab∧Rba✔
 3∧D 
5

Pab

3∧D

6

Rab

4∧D

7

Rba

4∧D

8

¬(∀x)(∃y)(Pxy)✔

1∧D

9

(∀y)¬(∃x)(Rxy)

1∧D

10

(∃x)¬(∃y)(Pxy)✔

8¬∀D

11

(∃y)¬(∀x)(Rxy)

2¬∀D

12

¬(∃y)(Pcy)✔

10∃D

13

(∀y)¬(Pcy)

12¬∃D

1

¬(∀x)(∃y)(Pxy)∧(∀y)¬(∃x)(Rxy)✔

P

2

¬(∀y)(∀x)(Rxy)✔

P

3

(Rab∧Rba)∧Pab ✔

P

4

Rab∧Rba✔
 3∧D 
5

Pab

3∧D

6

Rab

4∧D

7

Rba

4∧D

8

¬(∀x)(∃y)(Pxy)✔

1∧D

9

(∀y)¬(∃x)(Rxy)

1∧D

10

(∃x)¬(∃y)(Pxy)✔

8¬∀D

11

(∃y)¬(∀x)(Rxy)

2¬∀D

12

¬(∃y)(Pcy)✔

10∃D

13

(∀y)¬(Pcy)✔

12¬∃D

14

¬Pca

13∀D

15

¬Pcb

13∀D

16

¬Pcc

13∀D

1

¬(∀x)(∃y)(Pxy)∧(∀y)¬(∃x)(Rxy)✔

P

2

¬(∀y)(∀x)(Rxy)✔

P

3

(Rab∧Rba)∧Pab ✔

P

4

Rab∧Rba✔
 3∧D 
5

Pab

3∧D

6

Rab

4∧D

7

Rba

4∧D

8

¬(∀x)(∃y)(Pxy)✔

1∧D

9

(∀y)¬(∃x)(Rxy)

1∧D

10

(∃x)¬(∃y)(Pxy)✔

8¬∀D

11

(∃y)¬(∀x)(Rxy)✔

2¬∀D

12

¬(∃y)(Pcy)✔

10∃D

13

(∀y)¬(Pcy)✔

12¬∃D

14

¬Pca

13∀D

15

¬Pcb

13∀D

16

¬Pcc

13∀D

17

¬(∀x)(Rxe)

11∃D

1

¬(∀x)(∃y)(Pxy)∧(∀y)¬(∃x)(Rxy)✔

P

2

¬(∀y)(∀x)(Rxy)✔

P

3

(Rab∧Rba)∧Pab ✔

P

4

Rab∧Rba✔
 3∧D 
5

Pab

3∧D

6

Rab

4∧D

7

Rba

4∧D

8

¬(∀x)(∃y)(Pxy)✔

1∧D

9

(∀y)¬(∃x)(Rxy)

1∧D

10

(∃x)¬(∃y)(Pxy)✔

8¬∀D

11

(∃y)¬(∀x)(Rxy)✔

2¬∀D

12

¬(∃y)(Pcy)✔

10∃D

13

(∀y)¬(Pcy)✔

12¬∃D

14

¬Pca

13∀D

15

¬Pcb

13∀D

16

¬Pcc

13∀D

17

¬(∀x)(Rxe)✔

11∃D

18

(∃x)¬(Rxe)

17¬∀D

1

¬(∀x)(∃y)(Pxy)∧(∀y)¬(∃x)(Rxy)✔

P

2

¬(∀y)(∀x)(Rxy)✔

P

3

(Rab∧Rba)∧Pab ✔

P

4

Rab∧Rba✔
 3∧D 
5

Pab

3∧D

6

Rab

4∧D

7

Rba

4∧D

8

¬(∀x)(∃y)(Pxy)✔

1∧D

9

(∀y)¬(∃x)(Rxy)

1∧D

10

(∃x)¬(∃y)(Pxy)✔

8¬∀D

11

(∃y)¬(∀x)(Rxy)✔

2¬∀D

12

¬(∃y)(Pcy)✔

10∃D

13

(∀y)¬(Pcy)✔

12¬∃D

14

¬Pca

13∀D

15

¬Pcb

13∀D

16

¬Pcc

13∀D

17

¬(∀x)(Rxe)✔

11∃D

18

(∃x)¬(Rxe)✔

17¬∀D

19

¬Rfe

18∃D

1

¬(∀x)(∃y)(Pxy)∧(∀y)¬(∃x)(Rxy)✔

P

2

¬(∀y)(∀x)(Rxy)✔

P

3

(Rab∧Rba)∧Pab ✔

P

4

Rab∧Rba✔
 3∧D 
5

Pab

3∧D

6

Rab

4∧D

7

Rba

4∧D

8

¬(∀x)(∃y)(Pxy)✔

1∧D

9

(∀y)¬(∃x)(Rxy)✔

1∧D

10

(∃x)¬(∃y)(Pxy)✔

8¬∀D

11

(∃y)¬(∀x)(Rxy)✔

2¬∀D

12

¬(∃y)(Pcy)✔

10∃D

13

(∀y)¬(Pcy)✔

12¬∃D

14

¬Pca

13∀D

15

¬Pcb

13∀D

16

¬Pcc

13∀D

17

¬(∀x)(Rxe)✔

11∃D

18

(∃x)¬(Rxe)✔

17¬∀D

19

¬Rfe

18∃D

20

¬(∃x)(Rxa)

9∀D

21

¬(∃x)(Rxb)

9∀D

22

¬(∃x)(Rxe)

9∀D

23

¬(∃x)(Rxf)

9∀D

1

¬(∀x)(∃y)(Pxy)∧(∀y)¬(∃x)(Rxy)✔

P

2

¬(∀y)(∀x)(Rxy)✔

P

3

(Rab∧Rba)∧Pab ✔

P

4

Rab∧Rba✔
 3∧D 
5

Pab

3∧D

6

Rab

4∧D

7

Rba

4∧D

8

¬(∀x)(∃y)(Pxy)✔

1∧D

9

(∀y)¬(∃x)(Rxy)✔

1∧D

10

(∃x)¬(∃y)(Pxy)✔

8¬∀D

11

(∃y)¬(∀x)(Rxy)✔

2¬∀D

12

¬(∃y)(Pcy)✔

10∃D

13

(∀y)¬(Pcy)✔

12¬∃D

14

¬Pca

13∀D

15

¬Pcb

13∀D

16

¬Pcc

13∀D

17

¬(∀x)(Rxe)✔

11∃D

18

(∃x)¬(Rxe)✔

17¬∀D

19

¬Rfe

18∃D

20

¬(∃x)(Rxa)✔

9∀D

21

¬(∃x)(Rxb)✔

9∀D

22

¬(∃x)(Rxe)✔

9∀D

23

¬(∃x)(Rxf)✔

9∀D

24

(∀x)¬(Rxa)

20¬∃D

25

(∀x)¬(Rxb)

21¬∃D

26

(∀x)¬(Rxe)

22¬∃D

27
 (∀x)¬(Rxf)  23¬∃D 
1

¬(∀x)(∃y)(Pxy)∧(∀y)¬(∃x)(Rxy)✔

P

2

¬(∀y)(∀x)(Rxy)✔

P

3

(Rab∧Rba)∧Pab ✔

P

4

Rab∧Rba✔
 3∧D 
5

Pab

3∧D

6

Rab

4∧D

7

Rba

4∧D

8

¬(∀x)(∃y)(Pxy)✔

1∧D

9

(∀y)¬(∃x)(Rxy)✔

1∧D

10

(∃x)¬(∃y)(Pxy)✔

8¬∀D

11

(∃y)¬(∀x)(Rxy)✔

2¬∀D

12

¬(∃y)(Pcy)✔

10∃D

13

(∀y)¬(Pcy)✔

12¬∃D

14

¬Pca

13∀D

15

¬Pcb

13∀D

16

¬Pcc

13∀D

17

¬(∀x)(Rxe)✔

11∃D

18

(∃x)¬(Rxe)✔

17¬∀D

19

¬Rfe

18∃D

20

¬(∃x)(Rxa)✔

9∀D

21

¬(∃x)(Rxb)✔

9∀D

22

¬(∃x)(Rxe)✔

9∀D

23

¬(∃x)(Rxf)✔

9∀D

24

(∀x)¬(Rxa)

20¬∃D

25

(∀x)¬(Rxb)

21¬∃D

26

(∀x)¬(Rxe)

22¬∃D

27
 (∀x)¬(Rxf)  23¬∃D 
28

¬Rab

25∀D

Tautology: A proposition ‘P’ is shown by the truthtree method to be a tautology if and only if the tree ‘¬P’ determines a closed tree; that is, all branches close.Contradiction: A proposition ‘P’ is shown by the truthtree method to be a contradiction if and only if the tree ‘P’ determines a closed tree; that is, all branches close.Contingency: A proposition ‘P’ is shown by the truthtree method to be a contingency if and only if ‘P’ is neither a tautology nor a contradiction; that is, the tree of ‘P’ does not determine a closed tree, and the tree of ‘¬P’ does not determine a closed tree.(Agler 305)
“To summarize, the truthtree method can be used to determine whether a proposition ‘P’ is a tautology, contradiction, or contingency. In testing ‘P’ to see if it is a tautology, begin the tree with ‘¬P.’ If the tree closes, you know that it is a tautology. If the tree is open, then ‘P’ is either a contradiction or a contingency. Similarly, in testing ‘P’ to see if it is a contradiction, begin the tree with ‘P.’ If the tree closes, you know that it is a contradiction. If the tree is open, then ‘P’ is either a tautology or a contingency. Lastly, if the truthtree test shows that ‘P’ is neither a contradiction nor a tautology, then ‘P’ is a contingency” (Agler 147). Perhaps another way would be first to test if it is a contingency by seeing if it makes a closed tree. If the tree is closed, then it is a contradiction. If it is not, then we do another test. We negate the proposition and see if it makes a closed tree. If it does, then it is a tautology. If it does not, then it is a contingency.] We will now look at a proposition and see if it is a contradiction, which we do by seeing if all the branches close.
1
 (∃x)¬(∀y)[Px→(Qx∨¬Ry)] 
p

1
 (∃x)¬(∀y)[Px→(Qx∨¬Ry)]✔ 
p

2

¬(∀y)[Pa→(Qa∨¬Ry)]

1∃D

1
 (∃x)¬(∀y)[Px→(Qx∨¬Ry)]✔ 
p

2

¬(∀y)[Pa→(Qa∨¬Ry)]✔

1∃D

3

(∃y)¬[Pa→(Qa∨¬Ry)]

2¬∀D

1
 (∃x)¬(∀y)[Px→(Qx∨¬Ry)]✔ 
p

2

¬(∀y)[Pa→(Qa∨¬Ry)]✔

1∃D

3

(∃y)¬[Pa→(Qa∨¬Ry)]✔

2¬∀D

4

¬[Pa→(Qa∨¬Rb)]
 3∃D 
1
 (∃x)¬(∀y)[Px→(Qx∨¬Ry)]✔ 
p

2

¬(∀y)[Pa→(Qa∨¬Ry)]✔

1∃D

3

(∃y)¬[Pa→(Qa∨¬Ry)]✔

2¬∀D

4

¬[Pa→(Qa∨¬Rb)]✔
 3∃D 
5

Pa

4¬→D

6

¬(Qa∨¬Rb)

4¬→D

1
 (∃x)¬(∀y)[Px→(Qx∨¬Ry)]✔ 
p

2

¬(∀y)[Pa→(Qa∨¬Ry)]✔

1∃D

3

(∃y)¬[Pa→(Qa∨¬Ry)]✔

2¬∀D

4

¬[Pa→(Qa∨¬Rb)]✔
 3∃D 
5

Pa

4¬→D

6

¬(Qa∨¬Rb)✔

4¬→D

7

¬Qa

6¬∨D

8

¬¬Rb

6¬∨D

1

¬(∃x)¬(∀y)[Px→(Qx∨¬Ry)]

P

1

¬(∃x)¬(∀y)[Px→(Qx∨¬Ry)]✔

P

2

(∀x)¬¬(∀y)[Px→(Qx∨¬Ry)]

1¬∃D

1

¬(∃x)¬(∀y)[Px→(Qx∨¬Ry)]✔

P

2

(∀x)¬¬(∀y)[Px→(Qx∨¬Ry)]✔

1¬∃D

3

¬¬(∀y)[Pa→(Qa∨¬Ry)]

2∀D

1

¬(∃x)¬(∀y)[Px→(Qx∨¬Ry)]✔

P

2

(∀x)¬¬(∀y)[Px→(Qx∨¬Ry)]✔

1¬∃D

3

¬¬(∀y)[Pa→(Qa∨¬Ry)]✔

2∀D

4

(∀y)[Pa→(Qa∨¬Ry)]

3¬¬D

1

¬(∃x)¬(∀y)[Px→(Qx∨¬Ry)]✔

P

2

(∀x)¬¬(∀y)[Px→(Qx∨¬Ry)]✔

1¬∃D

3

¬¬(∀y)[Pa→(Qa∨¬Ry)]✔

2∀D

4

(∀y)[Pa→(Qa∨¬Ry)]

3¬¬D

5

Pa→(Qa∨¬Ra)

4∀D

1

¬(∃x)¬(∀y)[Px→(Qx∨¬Ry)]✔

P

2

(∀x)¬¬(∀y)[Px→(Qx∨¬Ry)]✔

1¬∃D

3

¬¬(∀y)[Pa→(Qa∨¬Ry)]✔

2∀D

4

(∀y)[Pa→(Qa∨¬Ry)]

3¬¬D

5

Pa→(Qa∨¬Ra)
/ \

4∀D

6
 ¬Pa Qa∨¬Ra 
5→D

1

¬(∃x)¬(∀y)[Px→(Qx∨¬Ry)]✔

P

2

(∀x)¬¬(∀y)[Px→(Qx∨¬Ry)]✔

1¬∃D

3

¬¬(∀y)[Pa→(Qa∨¬Ry)]✔

2∀D

4

(∀y)[Pa→(Qa∨¬Ry)]

3¬¬D

5

Pa→(Qa∨¬Ra)
/ \

4∀D

6
 ¬Pa Qa∨¬Ra O 
5→D

1

¬(∃x)¬(∀y)[Px→(Qx∨¬Ry)]✔

P

2

(∀x)¬¬(∀y)[Px→(Qx∨¬Ry)]✔

1¬∃D

3

¬¬(∀y)[Pa→(Qa∨¬Ry)]✔

2∀D

4

(∀y)[Pa→(Qa∨¬Ry)]

3¬¬D

5

Pa→(Qa∨¬Ra)
/ \

4∀D

6
 ¬Pa Qa∨¬Ra✔ O / \ 
5→D

7
 Qa ¬Ra 
6∨D

1

¬(∃x)¬(∀y)[Px→(Qx∨¬Ry)]✔

P

2

(∀x)¬¬(∀y)[Px→(Qx∨¬Ry)]✔

1¬∃D

3

¬¬(∀y)[Pa→(Qa∨¬Ry)]✔

2∀D

4

(∀y)[Pa→(Qa∨¬Ry)]

3¬¬D

5

Pa→(Qa∨¬Ra)
/ \

4∀D

6
 ¬Pa Qa∨¬Ra✔ O / \ 
5→D

7
 Qa ¬Ra O O 
6∨D

Agler will perform these tests for the following proposition.
1

(∀x)(Px→Qx)∧(∃x)(Px∧¬Qx)

P

1

(∀x)(Px→Qx)∧(∃x)(Px∧¬Qx)✔

P

2

(∀x)(Px→Qx)

1∧D

3

(∃x)(Px∧¬Qx)

1∧D

1

(∀x)(Px→Qx)∧(∃x)(Px∧¬Qx)✔

P

2

(∀x)(Px→Qx)

1∧D

3

(∃x)(Px∧¬Qx)✔

1∧D

4

Pa∧¬Qa

3∃D

1

(∀x)(Px→Qx)∧(∃x)(Px∧¬Qx)✔

P

2

(∀x)(Px→Qx)

1∧D

3

(∃x)(Px∧¬Qx)✔

1∧D

4

Pa∧¬Qa✔

3∃D

5

Pa
 4∧D 
6

¬Qa

4∧D

1

(∀x)(Px→Qx)∧(∃x)(Px∧¬Qx)✔

P

2

(∀x)(Px→Qx)

1∧D

3

(∃x)(Px∧¬Qx)✔

1∧D

4

Pa∧¬Qa✔

3∃D

5

Pa
 4∧D 
6

¬Qa

4∧D

7
 Pa→Qa 
2∀D

1

(∀x)(Px→Qx)∧(∃x)(Px∧¬Qx)✔

P

2

(∀x)(Px→Qx)

1∧D

3

(∃x)(Px∧¬Qx)✔

1∧D

4

Pa∧¬Qa✔

3∃D

5

Pa
 4∧D 
6

¬Qa

4∧D

7
 Pa→Qa✔ / \ 
2∀D

8

¬Pa Qa

7→D

1

(∀x)(Px→Qx)∧(∃x)(Px∧¬Qx)✔

P

2

(∀x)(Px→Qx)

1∧D

3

(∃x)(Px∧¬Qx)✔

1∧D

4

Pa∧¬Qa✔

3∃D

5

Pa
 4∧D 
6

¬Qa

4∧D

7
 Pa→Qa✔ / \ 
2∀D

8

¬Pa Qa
X X

7→D

(∀x)(Px→Px)∧(∀y)(Qy∨¬Qy)(Agler 307)
1

¬[(∀x)(Px→Px)∧(∀y)(Qy∨¬Qy)]

P

1

¬[(∀x)(Px→Px)∧(∀y)(Qy∨¬Qy)]✔
/ \

P

2

¬(∀x)(Px→Px) ¬(∀y)(Qy∨¬Qy)

1¬∧D

1

¬[(∀x)(Px→Px)∧(∀y)(Qy∨¬Qy)]✔
/ \

P

2

¬(∀x)(Px→Px)✔ ¬(∀y)(Qy∨¬Qy✔

1¬∧D

3

(∃x)¬(Px→Px) (∃y)¬(Qy∨¬Qy)

2¬∀D

1

¬[(∀x)(Px→Px)∧(∀y)(Qy∨¬Qy)]✔
/ \

P

2

¬(∀x)(Px→Px)✔ ¬(∀y)(Qy∨¬Qy✔

1¬∧D

3

(∃x)¬(Px→Px)✔ (∃y)¬(Qy∨¬Qy)✔

2¬∀D

4
 ¬(Pa→Pa) ¬(Qa∨¬Qa) 
3∃D

1

¬[(∀x)(Px→Px)∧(∀y)(Qy∨¬Qy)]✔
/ \

P

2

¬(∀x)(Px→Px)✔ ¬(∀y)(Qy∨¬Qy✔

1¬∧D

3

(∃x)¬(Px→Px)✔ (∃y)¬(Qy∨¬Qy)✔

2¬∀D

4
 ¬(Pa→Pa) ¬(Qa∨¬Qa) 
3∃D

5

Pa 

4¬→D

6

¬Pa 

4¬→D

1

¬[(∀x)(Px→Px)∧(∀y)(Qy∨¬Qy)]✔
/ \

P

2

¬(∀x)(Px→Px)✔ ¬(∀y)(Qy∨¬Qy✔

1¬∧D

3

(∃x)¬(Px→Px)✔ (∃y)¬(Qy∨¬Qy)✔

2¬∀D

4
 ¬(Pa→Pa) ¬(Qa∨¬Qa) 
3∃D

5

Pa 

4¬→D

6

¬Pa 
X 

4¬→D

7

¬Qa

4¬∨D

8

¬¬Qa

4¬∨D

9

Qa
 8¬¬D 
1

¬[(∀x)(Px→Px)∧(∀y)(Qy∨¬Qy)]✔
/ \

P

2

¬(∀x)(Px→Px)✔ ¬(∀y)(Qy∨¬Qy✔

1¬∧D

3

(∃x)¬(Px→Px)✔ (∃y)¬(Qy∨¬Qy)✔

2¬∀D

4
 ¬(Pa→Pa) ¬(Qa∨¬Qa) 
3∃D

5

Pa 

4¬→D

6

¬Pa 
X 

4¬→D

7

¬Qa

4¬∨D

8

¬¬Qa

4¬∨D

9

Qa
X
 8¬¬D 
7.3.4 Logical Equivalence
Equivalence: A pair of propositions ‘P’ and ‘Q’ is shown by the truthtree method to be equivalent if and only if the tree of the stack of ‘¬(P↔Q)’ determines a closed tree; that is, all branches for ‘¬(P↔Q)’ close.(Agler 310)
(∀x)Px¬(∃x)Px(Agler 310)
1

¬[(∀x)Px↔¬(∃x)Px]

P

1

¬[(∀x)Px↔¬(∃x)Px]✔
/ \

P

2

(∀x)Px ¬(∀x)Px

1¬↔D

3

¬¬(∃x)Px ¬(∃x)Px

1¬↔D

1

¬[(∀x)Px↔¬(∃x)Px]✔
/ \

P

2

(∀x)Px ¬(∀x)Px

1¬↔D

3

¬¬(∃x)Px✔ ¬(∃x)Px

1¬↔D

4
 (∃x)Px 
3¬¬D

1

¬[(∀x)Px↔¬(∃x)Px]✔
/ \

P

2

(∀x)Px ¬(∀x)Px

1¬↔D

3

¬¬(∃x)Px✔ ¬(∃x)Px

1¬↔D

4
 (∃x)Px✔ 
3¬¬D

5
 Pa 
4∃D

1

¬[(∀x)Px↔¬(∃x)Px]✔
/ \

P

2

(∀x)Px ¬(∀x)Px

1¬↔D

3

¬¬(∃x)Px✔ ¬(∃x)Px

1¬↔D

4
 (∃x)Px✔ 
3¬¬D

5
 Pa 
4∃D

6
 Pa 
2∀D

1

¬[(∀x)Px↔¬(∃x)Px]✔
/ \

P

2

(∀x)Px ¬(∀x)Px

1¬↔D

3

¬¬(∃x)Px✔ ¬(∃x)Px

1¬↔D

4
 (∃x)Px✔ 
3¬¬D

5
 Pa 
4∃D

6
 Pa O 
2∀D

(∀x)¬(Px∨Gx)(∀y)(¬Py∧¬Gy)(Agler 310)
1

¬{[(∀x)¬(Px∨Gx)]↔[(∀y)(¬Py∧¬Gy)]}

P

1

¬{[(∀x)¬(Px∨Gx)]↔[(∀y)(¬Py∧¬Gy)]}✔
/ \

P

2

(∀x)¬(Px∨Gx) ¬(∀x)¬(Px∨Gx)

1¬↔D

3

¬(∀y)(¬Px∧¬Gx) (∀y)(¬Px∧¬Gx)

1¬↔D

1

¬{[(∀x)¬(Px∨Gx)]↔[(∀y)(¬Py∧¬Gy)]}✔
/ \

P

2

(∀x)¬(Px∨Gx) ¬(∀x)¬(Px∨Gx)

1¬↔D

3

¬(∀y)(¬Px∧¬Gx)✔ (∀y)(¬Px∧¬Gx)

1¬↔D

4

(∃y)¬(¬Px∧¬Gx) 
 3¬∀D 
1

¬{[(∀x)¬(Px∨Gx)]↔[(∀y)(¬Py∧¬Gy)]}✔
/ \

P

2

(∀x)¬(Px∨Gx) ¬(∀x)¬(Px∨Gx)

1¬↔D

3

¬(∀y)(¬Px∧¬Gx)✔ (∀y)(¬Px∧¬Gx)

1¬↔D

4

(∃y)¬(¬Px∧¬Gx)✔ 
 3¬∀D 
5

¬(¬Pa∧¬Ga) 
 4∃D 
1

¬{[(∀x)¬(Px∨Gx)]↔[(∀y)(¬Py∧¬Gy)]}✔
/ \

P

2

(∀x)¬(Px∨Gx) ¬(∀x)¬(Px∨Gx)

1¬↔D

3

¬(∀y)(¬Px∧¬Gx)✔ (∀y)(¬Px∧¬Gx)

1¬↔D

4

(∃y)¬(¬Px∧¬Gx)✔ 
 3¬∀D 
5

¬(¬Pa∧¬Ga)✔ 
/ \ 
 4∃D 
6

¬¬Pa ¬¬Ga 
 5¬∧D 
1

¬{[(∀x)¬(Px∨Gx)]↔[(∀y)(¬Py∧¬Gy)]}✔
/ \

P

2

(∀x)¬(Px∨Gx) ¬(∀x)¬(Px∨Gx)

1¬↔D

3

¬(∀y)(¬Px∧¬Gx)✔ (∀y)(¬Px∧¬Gx)

1¬↔D

4

(∃y)¬(¬Px∧¬Gx)✔ 
 3¬∀D 
5

¬(¬Pa∧¬Ga)✔ 
/ \ 
 4∃D 
6

¬¬Pa✔ ¬¬Ga✔ 
 5¬∧D 
7

Pa Ga 
 6¬¬D 
1

¬{[(∀x)¬(Px∨Gx)]↔[(∀y)(¬Py∧¬Gy)]}✔
/ \

P

2

(∀x)¬(Px∨Gx) ¬(∀x)¬(Px∨Gx)

1¬↔D

3

¬(∀y)(¬Px∧¬Gx)✔ (∀y)(¬Px∧¬Gx)

1¬↔D

4

(∃y)¬(¬Px∧¬Gx)✔ 
 3¬∀D 
5

¬(¬Pa∧¬Ga)✔ 
/ \ 
 4∃D 
6

¬¬Pa✔ ¬¬Ga✔ 
 5¬∧D 
7

Pa Ga 
 6¬¬D 
8

¬(Pa∨Ga) ¬(Pa∨Ga) 
 2∀D 
1

¬{[(∀x)¬(Px∨Gx)]↔[(∀y)(¬Py∧¬Gy)]}✔
/ \

P

2

(∀x)¬(Px∨Gx) ¬(∀x)¬(Px∨Gx)

1¬↔D

3

¬(∀y)(¬Px∧¬Gx)✔ (∀y)(¬Px∧¬Gx)

1¬↔D

4

(∃y)¬(¬Px∧¬Gx)✔ 
 3¬∀D 
5

¬(¬Pa∧¬Ga)✔ 
/ \ 
 4∃D 
6

¬¬Pa✔ ¬¬Ga✔ 
 5¬∧D 
7

Pa Ga 
 6¬¬D 
8

¬(Pa∨Ga) ¬(Pa∨Ga) 
 2∀D 
9

¬Pa ¬Pa 
 8¬∨D 
10

X ¬Ga 
X 
 8¬∨D 
1

¬{[(∀x)¬(Px∨Gx)]↔[(∀y)(¬Py∧¬Gy)]}✔
/ \

P

2

(∀x)¬(Px∨Gx) ¬(∀x)¬(Px∨Gx)

1¬↔D

3

¬(∀y)(¬Px∧¬Gx)✔ (∀y)(¬Px∧¬Gx)

1¬↔D

4

(∃y)¬(¬Px∧¬Gx)✔ 
 3¬∀D 
5

¬(¬Pa∧¬Ga)✔ 
/ \ 
 4∃D 
6

¬¬Pa✔ ¬¬Ga✔ 
 5¬∧D 
7

Pa Ga 
 6¬¬D 
8

¬(Pa∨Ga)✔ ¬(Pa∨Ga)✔ 
 2∀D 
9

¬Pa ¬Pa 
 8¬∨D 
10

X ¬Ga 
X 
 8¬∨D 
11

(∃x)¬¬(Px∨Gx)

2¬∀D

1

¬{[(∀x)¬(Px∨Gx)]↔[(∀y)(¬Py∧¬Gy)]}✔
/ \

P

2

(∀x)¬(Px∨Gx) ¬(∀x)¬(Px∨Gx)

1¬↔D

3

¬(∀y)(¬Px∧¬Gx)✔ (∀y)(¬Px∧¬Gx)

1¬↔D

4

(∃y)¬(¬Px∧¬Gx)✔ 
 3¬∀D 
5

¬(¬Pa∧¬Ga)✔ 
/ \ 
 4∃D 
6

¬¬Pa✔ ¬¬Ga✔ 
 5¬∧D 
7

Pa Ga 
 6¬¬D 
8

¬(Pa∨Ga)✔ ¬(Pa∨Ga)✔ 
 2∀D 
9

¬Pa ¬Pa 
 8¬∨D 
10

X ¬Ga 
X 
 8¬∨D 
11

(∃x)¬¬(Px∨Gx)✔

2¬∀D

12

Pa∨Ga
 11∃D 
1

¬{[(∀x)¬(Px∨Gx)]↔[(∀y)(¬Py∧¬Gy)]}✔
/ \

P

2

(∀x)¬(Px∨Gx) ¬(∀x)¬(Px∨Gx)

1¬↔D

3

¬(∀y)(¬Px∧¬Gx)✔ (∀y)(¬Px∧¬Gx)

1¬↔D

4

(∃y)¬(¬Px∧¬Gx)✔ 
 3¬∀D 
5

¬(¬Pa∧¬Ga)✔ 
/ \ 
 4∃D 
6

¬¬Pa✔ ¬¬Ga✔ 
 5¬∧D 
7

Pa Ga 
 6¬¬D 
8

¬(Pa∨Ga)✔ ¬(Pa∨Ga)✔ 
 2∀D 
9

¬Pa ¬Pa 
 8¬∨D 
10

X ¬Ga 
X 
 8¬∨D 
11

(∃x)¬¬(Px∨Gx)✔

2¬∀D

12

Pa∨Ga✔
/ \
 11∃D 
13

Pa Ga
 12∨D 
1

¬{[(∀x)¬(Px∨Gx)]↔[(∀y)(¬Py∧¬Gy)]}✔
/ \

P

2

(∀x)¬(Px∨Gx) ¬(∀x)¬(Px∨Gx)

1¬↔D

3

¬(∀y)(¬Px∧¬Gx)✔ (∀y)(¬Px∧¬Gx)

1¬↔D

4

(∃y)¬(¬Px∧¬Gx)✔ 
 3¬∀D 
5

¬(¬Pa∧¬Ga)✔ 
/ \ 
 4∃D 
6

¬¬Pa✔ ¬¬Ga✔ 
 5¬∧D 
7

Pa Ga 
 6¬¬D 
8

¬(Pa∨Ga)✔ ¬(Pa∨Ga)✔ 
 2∀D 
9

¬Pa ¬Pa 
 8¬∨D 
10

X ¬Ga 
X 
 8¬∨D 
11

(∃x)¬¬(Px∨Gx)✔

2¬∀D

12

Pa∨Ga✔
/ \
 11∃D 
13

Pa Ga
 12∨D 
14
 ¬Pa∧¬Ga ¬Pa∧¬Ga  3∀D 
1

¬{[(∀x)¬(Px∨Gx)]↔[(∀y)(¬Py∧¬Gy)]}✔
/ \

P

2

(∀x)¬(Px∨Gx) ¬(∀x)¬(Px∨Gx)

1¬↔D

3

¬(∀y)(¬Px∧¬Gx)✔ (∀y)(¬Px∧¬Gx)

1¬↔D

4

(∃y)¬(¬Px∧¬Gx)✔ 
 3¬∀D 
5

¬(¬Pa∧¬Ga)✔ 
/ \ 
 4∃D 
6

¬¬Pa✔ ¬¬Ga✔ 
 5¬∧D 
7

Pa Ga 
 6¬¬D 
8

¬(Pa∨Ga)✔ ¬(Pa∨Ga)✔ 
 2∀D 
9

¬Pa ¬Pa 
 8¬∨D 
10

X ¬Ga 
X 
 8¬∨D 
11

(∃x)¬¬(Px∨Gx)✔

2¬∀D

12

Pa∨Ga✔
/ \
 11∃D 
13

Pa Ga
 12∨D 
14
 ¬Pa∧¬Ga ¬Pa∧¬Ga  3∀D 
15
 ¬Pa ¬Ga X X  14∧D 
Validity: An argument ‘P, Q, R, ..., Y ⊢ Z’ is shown by the truthtree method to be valid in RL if and only if the stack ‘P,’ ‘Q,’ ‘R,’ ..., ‘Y,’ ‘¬Z’ determines a closed tree.Invalidity: An argument ‘P, Q, R, ..., Y ⊢ Z’ is shown by the truthtree method to be invalid in RL if and only if the stack ‘P,’ ‘Q,’ ‘R,’ ..., ‘Y,’ ‘¬Z’ has at least one completed open branch. (Agler 314)
Agler first shows how we do this with a simple argument, namely:
(∀x)Px, Pa ⊢ Pa
(Agler 314)
1

(∀x)Px

P

2

¬Pa

P

1

(∀x)Px

P

2

¬Pa

P

3

Pa
X  1∀D 
(∀x)(Px→Qx), (∃y)(Py) ⊢ (∃x)(Px→Qx)(Agler 314)
1

(∀x)(Px→Qx)

P

2

(∃y)(Py)

P

3

¬(∃x)(Px→Qx)
 P 
1

(∀x)(Px→Qx)

P

2

(∃y)(Py)✔

P

3

¬(∃x)(Px→Qx)
 P 
4

Pa

2∃D

1

(∀x)(Px→Qx)

P

2

(∃y)(Py)✔

P

3

¬(∃x)(Px→Qx)✔
 P 
4

Pa

2∃D

5

(∀x)¬(Px→Qx)

3¬∃D

1

(∀x)(Px→Qx)

P

2

(∃y)(Py)✔

P

3

¬(∃x)(Px→Qx)✔
 P 
4

Pa

2∃D

5

(∀x)¬(Px→Qx)

3¬∃D

6

Pa→Qa
 1∀D 
1

(∀x)(Px→Qx)

P

2

(∃y)(Py)✔

P

3

¬(∃x)(Px→Qx)✔
 P 
4

Pa

2∃D

5

(∀x)¬(Px→Qx)

3¬∃D

6

Pa→Qa

1∀D

7

¬(Pa→Qa)
 5∀D 
1

(∀x)(Px→Qx)

P

2

(∃y)(Py)✔

P

3

¬(∃x)(Px→Qx)✔
 P 
4

Pa

2∃D

5

(∀x)¬(Px→Qx)

3¬∃D

6

Pa→Qa

1∀D

7

¬(Pa→Qa)✔
 5∀D 
8

Pa
 7¬→D 
9

¬Qa

7¬→D

1

(∀x)(Px→Qx)

P

2

(∃y)(Py)✔

P

3

¬(∃x)(Px→Qx)✔
 P 
4

Pa

2∃D

5

(∀x)¬(Px→Qx)

3¬∃D

6

Pa→Qa

1∀D

7

¬(Pa→Qa)✔
 5∀D 
8

Pa
 7¬→D 
9

¬Qa
/ \ 
7¬→D

10

¬Pa Qa
X X  6→D 
Pa∧Qb, (∀x)(∀y)[Px→(Qy→Rx)] ⊢ Ra(Agler 315)
{Pa∧Qb, (∀x)(∀y)[Px→(Qy→Rx)], ¬Ra}(Agler 315)
1

Pa∧Qb

P

2

(∀x)(∀y)[Px→(Qy→Rx)]

P

3

¬Ra

P

1

Pa∧Qb✔

P

2

(∀x)(∀y)[Px→(Qy→Rx)]

P

3

¬Ra

P

4

Pa

1∧D

5

Qb

1∧D

1

Pa∧Qb✔

P

2

(∀x)(∀y)[Px→(Qy→Rx)]

P

3

¬Ra

P

4

Pa

1∧D

5

Qb

1∧D

6

(∀y)[Pa→(Qy→Ra)]

2∀D

7

(∀y)[Pb→(Qy→Rb)]

2∀D

1

Pa∧Qb✔

P

2

(∀x)(∀y)[Px→(Qy→Rx)]

P

3

¬Ra

P

4

Pa

1∧D

5

Qb

1∧D

6

(∀y)[Pa→(Qy→Ra)]

2∀D

7

(∀y)[Pb→(Qy→Rb)]

2∀D

8

Pa→(Qa→Ra)

6∀D

9

Pa→(Qb→Ra)

6∀D

10

Pb→(Qa→Rb)

7∀D

11

Pb→(Qb→Rb)

7∀D

1

Pa∧Qb✔

P

2

(∀x)(∀y)[Px→(Qy→Rx)]

P

3

¬Ra

P

4

Pa

1∧D

5

Qb

1∧D

6

(∀y)[Pa→(Qy→Ra)]

2∀D

7

(∀y)[Pb→(Qy→Rb)]

2∀D

8

Pa→(Qa→Ra)

6∀D

9

Pa→(Qb→Ra)✔

6∀D

10

Pb→(Qa→Rb)

7∀D

11

Pb→(Qb→Rb)
/ \

7∀D

12
 ¬Pa Qb→Ra✔ X / \ 
9→D

13
 ¬Qb Ra X X 
12→D

Pa∧Qb, (∀x)(∀y)[Px→(Qy→Rx)], ¬Rais inconsistent. That furthermore means that the argument
(Agler 316)
Pa∧Qb, (∀x)(∀y)[Px→(Qy→Rx)] ⊢ Ra
.
No comments:
Post a Comment