WOLFRAM NOTEBOOK

WOLFRAM|DEMONSTRATIONS PROJECT

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.
Wolfram Cloud

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 »

You are using a browser not supported by the Wolfram Cloud. Supported browsers include recent versions of Chrome, Edge, Firefox and Safari.