|Description: In the paper "On
Variable Functors of Propositional Arguments",
Lukasiewicz introduced a system that can handle variable connectives.
This was done by introducing a variable, marked with a lowercase delta,
which takes a wff as input. In the system, "delta 𝜑 "
"something is true of 𝜑." "delta 𝜑 "
can be substituted with
¬ 𝜑, 𝜓 ∧ 𝜑, ∀𝑥𝜑, etc.
Later on, Meredith discovered a single axiom, in the form of ( delta
delta ⊥ → delta 𝜑 ).
This represents the shortest theorem
in the extended propositional calculus that cannot be derived as an
instance of a theorem in propositional calculus.
A symmetry with ¬. (Contributed by Anthony