3
$\begingroup$

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

|cite|improve this question
$\endgroup$
  • $\begingroup$ There's always "define $\vee, \to$ in terms of those, and then use the nice axiomatization you already know". $\endgroup$ – Hurkyl Nov 8 '13 at 21:57
  • 1
    $\begingroup$ @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. $\endgroup$ – Henning Makholm Nov 8 '13 at 22:05
  • $\begingroup$ Who says there's an elegant way to do it? $\endgroup$ – dfeuer Nov 8 '13 at 22:13
  • 1
    $\begingroup$ @dfeuer Nobody, as far as I know. I'm hoping there is an elegant way to do this. $\endgroup$ – Marnix Klooster Nov 8 '13 at 22:17
  • 2
    $\begingroup$ 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. $\endgroup$ – Henning Makholm Nov 8 '13 at 22:23
4
$\begingroup$

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.

|cite|improve this answer
$\endgroup$
  • $\begingroup$ What rules are $\leftrightarrow L$ and $\leftrightarrow R$, exactly? $\endgroup$ – dfeuer Nov 9 '13 at 6:03
  • $\begingroup$ @dfeuer: I've added rule names $\endgroup$ – Henning Makholm Nov 9 '13 at 6:11
  • $\begingroup$ Maybe I'm daft, but how does $\Gamma,P,Q\vdash R$ make sense as a premise? $\endgroup$ – dfeuer Nov 9 '13 at 6:21
  • $\begingroup$ @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. $\endgroup$ – Henning Makholm Nov 9 '13 at 6:23
  • $\begingroup$ 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? $\endgroup$ – dfeuer Nov 10 '13 at 6:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.