# The Completeness Theorem of Equivalential Calculus

The Completeness Theorem of Equivalential Calculus

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 . The proof of the formula goes in the opposite direction, and modus ponens is used in this form: follows from and . The first formula in the proof of is a substitution instance of theorem 6, that is, of . 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.

Exx

F

y

Eyx

x

F

Epp