I am given the following Hilbert-style system (for intuitionistic propositional logic):

Axiom schemes:

  1. $\phi\vee\phi\rightarrow\phi$
  2. $\phi\rightarrow\phi\wedge\phi$
  3. $\phi\rightarrow\phi\vee\psi$
  4. $\phi\wedge\psi\rightarrow\phi$
  5. $\phi\vee\psi\rightarrow\psi\vee\phi$
  6. $\phi\wedge\psi\rightarrow\psi\vee\phi$
  7. $\bot\rightarrow\phi$

Inference rules:

  1. $\phi$ and $\phi\rightarrow\psi$ imply $\psi$
  2. $\phi\rightarrow\psi$ and $\psi\rightarrow\chi$ imply $\phi\rightarrow \chi$
  3. $\phi\wedge\psi\rightarrow\chi$ implies $\phi\rightarrow(\psi\rightarrow\chi)$
  4. $\phi\rightarrow(\psi\rightarrow\chi)$ implies $\phi\wedge\psi\rightarrow\chi$
  5. $\phi\rightarrow\psi$ implies $\phi\vee\chi\rightarrow\psi\vee\chi$

We define, for a set $\Gamma$ of propositional formulas and a formula $\phi$, we define $\Gamma\vdash_{IL}\phi$ as ''There exists a proof in this Hilbert-style proof system (for intuitionistic logic) of $\phi$ from $\Gamma$.

I am now asked to prove (in essence, the actual question is broader): $$\text{if }\Gamma\vdash_{IL}\psi\text{ and }\Gamma\vdash_{IL}\chi\text{, then }\Gamma\vdash_{IL}\psi\wedge\chi$$ In a proof system like natural deduction, this would be proved by a conjunction introduction, but using above Hilbert-rules, I have not in any way been able to get some kind of conjunction introduction. For instance, using axiom scheme 2 didn't get me anywhere, we could think of substituting $(\psi\wedge\chi)$ for $\phi$, or just substituting $\psi$ for $\phi$, but no inference rule will then get us to the wanted conclusion.

Can the statement be proved using this Hilbert system?

  • $\begingroup$ That's not really a Hilbert-type system. In a Hilbert-type system, modus ponens is the only inference rule, and all the rest of logic is encoded as axioms. $\endgroup$ Nov 6, 2015 at 11:14
  • $\begingroup$ @HenningMakholm okay, this is at least how my professor phrased it. He indeed made the comment that this system was constructed to instruct the idea of a deduction in a Hilbert-style system, but maybe he should not have used the Hilbert part and should have just called it another proof calculus somewhere inbetween natural deduction and Hilbert-style systems. Would it, considering the given rules above, however be possible to prove this statement? $\endgroup$
    – konewka
    Nov 6, 2015 at 11:16
  • $\begingroup$ It looks quite unconventional to me, in fact -- for example, to prove even $\phi\to\phi$ one would need to go via either $\phi\land\phi$ or $\phi\lor\phi$. $\endgroup$ Nov 6, 2015 at 11:19
  • $\begingroup$ I agree with you, this proof system is quite artificial I think $\endgroup$
    – konewka
    Nov 6, 2015 at 11:21
  • 2
    $\begingroup$ @HenningMakholm I disagree. This still does qualify as a "Hilbert"... ahem Frege... type system. A Frege type system gets distinguished by having every step in proofs as either axioms or deductions from previous steps. en.wikipedia.org/wiki/Hilbert_system Nicod's system, for example, qualifies as a Frege type system, but it doesn't use modus ponens. Others have gotten written about in the literature before also. $\endgroup$ Nov 6, 2015 at 18:55

2 Answers 2


You can prove $$\psi\land \chi \to \psi\land\chi$$ by going through $(\psi\land\chi)\land(\psi\land\chi)$. Now apply rule 10 to get $$ \psi \to (\chi\to\psi\land\chi) $$ Then your assumed derivations of $\psi$ and $\chi$, plus modus ponens twice concludes $\psi\land \chi$.

  • $\begingroup$ Oh it indeed does. Thanks for the insight, such proof systems really require more work than one would expect by using some other proof system, even for such elementary statements $\endgroup$
    – konewka
    Nov 6, 2015 at 11:35
  • $\begingroup$ I don't see how you got the first step, but you can get to what you have there. $\endgroup$ Nov 6, 2015 at 18:45

I use Polish notation. The formation rules run:

  1. All lower case letters of the Latin alphabet, and 0 qualify as well-formed formulas (wffs).
  2. If $\alpha$ and $\beta$ qualify as wffs, then so do N$\alpha$, C$\alpha$$\beta$, K$\alpha$$\beta$, and A$\alpha$$\beta$.

The axiom schemes are:

  1. CAppp a law of Clavius
  2. CpKpp a law of K-tautology introduction
  3. CpApq left disjunction introduction
  4. CKpqp left conjunction elimination
  5. CApqAqp A-commutation
  6. CKpqApq conjunction comes as weaker than disjunction
  7. C0p falsum implies any proposition

The inference rules go:

  1. $\alpha$, C$\alpha$$\beta$ $\vdash$ $\beta$ modus ponens

  2. C$\alpha$$\beta$, C$\beta$$\gamma$ $\vdash$ C$\alpha$$\gamma$ hypothetical syllogism

  3. CK$\alpha$$\beta$$\gamma$ $\vdash$ C$\alpha$C$\beta$$\gamma$ exportation

  4. C$\alpha$C$\beta$$\gamma$ $\vdash$ CK$\alpha$$\beta$$\gamma$ importation

  5. C$\alpha$$\beta$ $\vdash$ CA$\alpha$$\gamma$A$\beta$$\gamma$

Now substituting q with p (q/p hereafter) in 3 we obtain

  1. CpApp

Applying hypothetical syllogism to 13 and 1 we thus obtain

  1. Cpp

Substituting p with Kpq in 14 we obtain

  1. CKpqKpq

Now applying exportation to 15 we obtain

  1. CpCqKpq

And I think you can do the rest.


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.