WOLFRAM NOTEBOOK

WOLFRAM|DEMONSTRATIONS PROJECT

The Completeness Theorem of Equivalential Calculus

length parameter of formula

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

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

follows from

Eyx

and

. The first formula in the proof of

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.

You are using a browser not supported by the Wolfram Cloud

Supported browsers include recent versions of Chrome, Edge, Firefox and Safari.

I understand and wish to continue anyway »