WOLFRAM|DEMONSTRATIONS PROJECT

Equivalential Calculus

​
all theorems
explain individual step
part of original
step
2
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
The equivalential calculus is a subsystem of propositional calculus with equivalence (≡) as the only connective. Two equivalential tautologies are
p≡p
and
(p≡q)≡(q≡p)
. In Polish notation, discovered by Łukasiewicz, these formulas are written as
Epp
and
EEpqEqp
. This Demonstration shows the derivation of 21 theorems of the equivalential calculus based on one axiom,
EEpqEErqEpr
, and the rules of substitution and modus ponens.
Here is an example of substitution. The substitution
{pEpq,qEEpqs}
means that the propositional variable
p
is replaced by
Epq
and that
q
is replaced by
EEpqs
. So applying that substitution to the formula
EpEpq
gives
EEpqEEpqEEpqs
.
Modus ponens is a derivation of
y
from
x
and
Exy
.
To be a theorem of the equivalential calculus, its formula must follow from already proven theorems. The first theorem is the axiom, but the rest of the numbered formulas need explanation.
1.
EEpqEErqEpr
Axiom
2.
EEsEErqEprEEpqs
1{pEpq,qEErqEpr,rs},1
The second line means that the formula
EEsEErqEprEEpqs
follows by modus ponens from formula 1 (the axiom), to which the substitution
S={pEpq,qEErqErp,rs}
is applied, and from the formula 1, which is the axiom.
So
1S
gives
EE(Epq)(EErqEpr)EEs(EErqEpr)E(Epq)s
, which is
EEpqEErqEpr≡EEsEErqEprEEpqs
.
The formula
EEsEErqEprEEpqs
in step 2 follows from the last two by modus ponens.