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

Question

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:

8. $\phi$ and $\phi\rightarrow\psi$ imply $\psi$
9. $\phi\rightarrow\psi$ and $\psi\rightarrow\chi$ imply $\phi\rightarrow \chi$
10. $\phi\wedge\psi\rightarrow\chi$ implies $\phi\rightarrow(\psi\rightarrow\chi)$
11. $\phi\rightarrow(\psi\rightarrow\chi)$ implies $\phi\wedge\psi\rightarrow\chi$
12. $\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?

Answer 1

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

Answer 2

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:

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

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

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

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

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

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

13. CpApp

Applying hypothetical syllogism to 13 and 1 we thus obtain

14. Cpp

Substituting p with Kpq in 14 we obtain

15. CKpqKpq

Now applying exportation to 15 we obtain

16. CpCqKpq

And I think you can do the rest.