Equivalential Calculus

Requires a Wolfram Notebook System
Interact on desktop, mobile and cloud with the free Wolfram Player or other Wolfram Language products.
The equivalential calculus is a subsystem of propositional calculus with equivalence (≡) as the only connective. Two equivalential tautologies are and
. In Polish notation, discovered by Łukasiewicz, these formulas are written as
and
. This Demonstration shows the derivation of 21 theorems of the equivalential calculus based on one axiom,
, and the rules of substitution and modus ponens.
Contributed by: Izidor Hafner (November 2013)
Open content licensed under CC BY-NC-SA
Snapshots
Details
In 1929, Leśniewski recognized that the equivalential calculus could be axiomatized. He used two axioms and the rules of detachment and substitution. He also observed that a formula of propositional calculus in which equivalence was the only propositional function was a tautology if and only if each propositional letter occurs an even number of times. In 1932, Wajsberg showed that the calculus can be based on a single axiom. In 1933, Łukasiewicz found the shortest axiom and gave a simple completeness proof.
This axiomatization of the equivalential calculus was presented in [1]. These 21 theorems were derived on pages 98–99.
Reference
[1] J. Łukasiewicz, "The Equivalential Calculus," in Polish Logic 1920–1939 (S. McCall, ed.), Oxford: Clarendon Press, 1967 pp. 88–115.
Permanent Citation