# Hilbert-style proof of $\Gamma\vdash\psi$ and $\Gamma\vdash\chi$ implies $\Gamma\vdash\psi\wedge\chi$

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?

• 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. Nov 6, 2015 at 11:14
• @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? Nov 6, 2015 at 11:16
• 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$. Nov 6, 2015 at 11:19
• I agree with you, this proof system is quite artificial I think Nov 6, 2015 at 11:21
• @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. Nov 6, 2015 at 18:55

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$.

• 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 Nov 6, 2015 at 11:35
• I don't see how you got the first step, but you can get to what you have there. 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\alphaC\beta$$\gamma$ exportation

4. C$\alpha$C$\beta$$\gamma \vdash CK\alpha$$\beta$$\gamma importation 5. C\alpha$$\beta$ $\vdash$ CA$\alpha$$\gammaA\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.