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

Question

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\;$?

Answer 1

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.