# Axioms based on $\leftrightarrow, \lor, \bot$ for propositional intuitionistic logic?

Propositional intuitionistic logic can be axiomatized based on $\;\to, \land, \lor, \bot\;$, with modus ponens $$\text{from }\; \phi \;\text{ and }\; \phi \to \psi \;\text{ infer }\; \psi$$ as the only inference rule, and a list of axioms like $$\phi \to (\chi \to \phi )$$ See the Wikipedia page on 'Intuitionistic logic' under 'Hilbert-style calculus' for a complete list of axioms.

Now that same page also claims that "{∨, ↔, ⊥} and {∨, ↔, ¬} are complete bases of intuitionistic connectives." And what I am looking for is a list of inference rules and axioms to back up Wikipedia's claim.

Strictly speaking this is of course simple: one can take the $\;\to, \land, \lor, \bot\;$ axioms, and replace every $\;\phi \to \psi\;$ by $\;(\phi \lor \psi) \leftrightarrow \psi\;$, and every $\;\phi \land \psi\;$ by $\;(\phi \lor \psi) \leftrightarrow (\phi \leftrightarrow \psi)\;$. But the result is not very elegant.

I've been puzzling a bit on constructing a nicer axiomatization, and I think it should at least have the inference rule $$\text{from }\; \phi \;\text{ and }\; \phi \leftrightarrow \psi \;\text{ infer }\; \psi$$ and axioms like $$(\phi \leftrightarrow \psi) \;\leftrightarrow\; (\psi \leftrightarrow \phi) \\ (\phi \leftrightarrow (\chi \leftrightarrow \psi)) \;\leftrightarrow\; ((\phi \leftrightarrow \chi) \leftrightarrow \psi)$$

Therefore my question is: What is a complete and elegant axiomatization of propositional intuitionistic logic based on $\;\leftrightarrow, \lor, \bot\;$?

• There's always "define $\vee, \to$ in terms of those, and then use the nice axiomatization you already know".
– user14972
Nov 8, 2013 at 21:57
• @Hurkyl: That seems to be the point of the OP's "Strictly speaking ..." paragraph. I agree that the outcome of that would hardly be elegant. Nov 8, 2013 at 22:05
• @dfeuer Nobody, as far as I know. I'm hoping there is an elegant way to do this. Nov 8, 2013 at 22:17
• Are you sure that $(\phi\land\psi)$ is intuitionistically equivalent to $(\phi\lor\psi)\leftrightarrow(\phi\leftrightarrow\psi)$? It works classically, of course, but I don't see how one can derive $\phi$ from the latter intuitionistically. Nov 8, 2013 at 22:23
• I don't think that "↔" associates in intuitionist logic, does it? Nov 11, 2013 at 0:07

How about a sequent calculus, with standard rules:

$$\frac{\Gamma, P, P\vdash Q}{\Gamma, P\vdash Q}CL \qquad \frac{}{\Gamma,P \vdash P}Ax \qquad \frac{}{\Gamma, \bot \vdash P}{\bot}L$$ $$\frac{\Gamma\vdash Q\quad \Gamma,P\vdash R}{\Gamma,P\leftrightarrow Q\vdash R}{\leftrightarrow}L_1 \quad \frac{\Gamma\vdash P\quad \Gamma,Q\vdash R}{\Gamma,P\leftrightarrow Q\vdash R}{\leftrightarrow}L_2 \quad \frac{\Gamma,P\vdash Q\quad \Gamma,Q\vdash P}{\Gamma\vdash P\leftrightarrow Q}{\leftrightarrow}R$$ $$\frac{\Gamma,P\vdash R \quad \Gamma,Q\vdash R}{\Gamma,P\lor Q\vdash R}{\lor}L \quad \frac{\Gamma\vdash P}{\Gamma\vdash P\lor Q}{\lor}R_1 \quad \frac{\Gamma\vdash Q}{\Gamma\vdash P\lor Q}{\lor}R_2$$ This is complete for the $\{{\leftrightarrow},{\lor},\bot\}$ fragment because the full intuitionistic sequent calculus satisfies cut elimination.

To show that this fragment is complete in expressivity, express $P\to Q$ as $(P\lor Q)\leftrightarrow Q$ -- this equivalence is intuitionistically valid, and the usual left and right rules for $\to$ are easily built as combinations of the above rules.

Similarly, $\neg P$ is of course equivalent to $P\leftrightarrow \bot$.

For conjunction, contrary to speculation in comments, it turns out that $(P\lor Q)\leftrightarrow(P\leftrightarrow Q)$ is indeed intuitionistically equivalent to $P\land Q$. The difficult direction is to see that the usual ${\land}L$ rule is admissible, which can be done as follows in the above sequent calculus:

$$\begin{array}{rll} 0. & \Gamma,~ P,~ Q \vdash R & \text{premise of derived rule} \\ 1. & P\vdash P\lor Q & \text{easy} \\ 2. & P\leftrightarrow Q,~ P \vdash Q & \text{easy} \\ 3. & (P\lor Q)\leftrightarrow(P\leftrightarrow Q),~ P \vdash Q & 1, 2, {\leftrightarrow}L_2 \\ 4. & (P\lor Q)\leftrightarrow(P\leftrightarrow Q),~ Q \vdash P & \text{mutatis mutandis} \\ 5. & (P\lor Q)\leftrightarrow(P\leftrightarrow Q) \vdash P\leftrightarrow Q & 3,4, {\leftrightarrow}R \\ 6. & P\lor Q \vdash P\lor Q & \text{axiom} \\ 7. & \Gamma,~ P\lor Q,~ P\leftrightarrow Q \vdash R & \text{easy consequence of }0 \\ 8. & \Gamma,~ (P\lor Q)\leftrightarrow(P\leftrightarrow Q),~ P\lor Q \vdash R & 6,7, {\leftrightarrow}L_2 \\ 9. & \Gamma,~ (P\lor Q)\leftrightarrow(P\leftrightarrow Q),~ (P\lor Q)\leftrightarrow(P\leftrightarrow Q) \vdash R & 5,8, {\leftrightarrow}L_1 \\ 10. & \Gamma,~ (P\lor Q)\leftrightarrow(P\leftrightarrow Q) \vdash R & 9, CL \end{array}$$

(Proof found by exhaustive search!)

Or, for those that favor the Curry-Howard isomorphism for intuitionistic proofs, the idea in Haskell-like pseudosyntax for the ${\leftrightarrow}{\lor}{\bot}$ fragment is to replace

conj :: (P,Q)
let (x::P,y::Q) = conj
in  <..x..y..>


by

conj :: (Either P Q) <-> (P <-> Q)
let eq1 :: P <-> Q
eq1 (x :: P) = let eq2 :: P <-> Q = conj (Left x) in eq2 x
eq1 (y :: Q) = let eq2 :: P <-> Q = conj (Right y) in eq2 y
disj :: Either P Q = conj eq1
in case disj of
Left(x::P) -> let y::Q = eq1 x in <..x..y..>
Right(y::Q) -> let x::P = eq1 y in <..x..y..>


where P <-> Q is supposed to behave like a function that can be applied to either P or Q and produces an output of the opposite type, and disjunction is represented by the standard Either type.

• What rules are $\leftrightarrow L$ and $\leftrightarrow R$, exactly? Nov 9, 2013 at 6:03
• @dfeuer: I've added rule names Nov 9, 2013 at 6:11
• Maybe I'm daft, but how does $\Gamma,P,Q\vdash R$ make sense as a premise? Nov 9, 2013 at 6:21
• @dfeuer: The goal here is to construct $$\frac{\Gamma, P, Q\vdash R}{\Gamma,~P\land Q\vdash R}{\land}L$$ as a derived rule. If you just want to derive $P\land Q\vdash P$, replace $R$ with $P$ and let $\Gamma$ be empty. Nov 9, 2013 at 6:23
• I've read over it a bit more carefully now. It appears the key steps are really 3–5, with the rest all being build-up and tear-down. Is that about right? Nov 10, 2013 at 6:05