The Completeness Theorem of Equivalential Calculus

length parameter of formula

1

2

3

4

new equivalential formula

show the first 21 theorems

eliminate pairs of equal variables

proof of the formula

show substitution or formula

1. EEpqEErqEpr

2. EEsEErqEprEEpqs

3. EEpqEpq

4. EErEpqEEpqr

5. EEErqEprEpq

6. Epp

7. EEpqEqp

8. EErEqpEEpqr

9. EEEpqrErEqp

10. EErqEEprEpq

11. EEpEpqq

12. EqEpEpq

13. EErqEEpEpqr

14. EEpEqrEEpqr

15. EEEpqrEpEqr

16. EEpEqrEpErq

17. EEEprEqpErq

18. EEEpqrEEqpr

19. EEpEEqrsEpEErqs

20. EEpEEqrsEpEqErs

21. EEpEqErsEpEEqrs

Axiom

1{p  Epq,q  EErqEpr,r  s}, 1

2{s  Epq}, 1

1{p  Epq,q  Epq}, 3

4{r  Epq,p  Erq,q  Epr}, 1

5{r  p,q  p}, 3{q  p}

1{p  q,r  p}, 6{p  q}

1{p  Epq,q  Eqp}, 7

7{p  ErEqp,q  EEpqr}, 8

2{s  EEprEpq,r  p,p  r}, 9{q  r,r  Epq}

5{r  Epq,p  EpEpq}, 10{r  Epq}

7{p  EpEpq}, 11

1{p  EpEpq}, 11

2{s  EEpqr,r  q,q  Eqr}, 13{r  Epq,q  r,p  q}

7{p  EpEqr,q  EEpqr}, 14

9{p  Erq,q  p,r  EpEqr}, 9{p  r,r  p}

16{p  EEprEqp}, 5{r  p,q  r,p  q}

16{p  EEpqr,q  r,r  Eqp}, 9

10{r  EEqrs,q  EErqs}, 18{p  q,q  r,r  s}

10{r  EEqrs,q  EqErs}, 15{p  q,q  r,r  s}

7{p  EpEEqrs,q  EpEqErs}, 20

This Demonstration shows examples of Łukasiewicz's completeness theorem for the equivalential calculus. He first derived 21 theorems. Some of these theorems are associative and commutative rules on different parts of a formula. To show that a formula is a tautology, he eliminated pairs of the same propositional variable, to eventually get a formula of the form

Exx

. The proof of the formula

F

goes in the opposite direction, and modus ponens is used in this form:

y

follows from

Eyx

and

x

. The first formula in the proof of

F

is a substitution instance of theorem 6, that is, of

Epp

. Each following formula follows by modus ponens from the one before it and from one of the 21 numbered theorems on which a substitution is applied.