A Proof-Theoretic Note on the Independence of Intuitionistic Connectives
Ethan Brauer · Studia Logica · 2025
Abstract Prawitz proved that the basic logical connectives $$\wedge ,\vee ,\rightarrow ,\bot $$ ∧ , ∨ , → , ⊥ are not interdefinable in intuitionistic logic. His proof relied essentially on treating negation as a defined connective, and a key lemma fails when $$\lnot $$ ¬ is included as a primitive connective. I provide a new proof of this result that applies when negation is a primitive connective and which also shows that $$\wedge ,\vee ,\rightarrow ,\lnot $$ ∧ , ∨ , → , ¬ are not interdefinable.