# Equivalential Calculus

Requires a Wolfram Notebook System

Interact on desktop, mobile and cloud with the free Wolfram CDF Player or other Wolfram Language products.

Requires a Wolfram Notebook System

Edit on desktop, mobile and cloud with any Wolfram Language product.

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.

[more]
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