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. – Henning Makholm Nov 6 '15 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? – konewka Nov 6 '15 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$. – Henning Makholm Nov 6 '15 at 11:19
• I agree with you, this proof system is quite artificial I think – konewka Nov 6 '15 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. – Doug Spoonwood Nov 6 '15 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 – konewka Nov 6 '15 at 11:35
• I don't see how you got the first step, but you can get to what you have there. – Doug Spoonwood Nov 6 '15 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.