Theorems (or references to analysis) of a particular Hilbert-deductive-system using $\\{\neg, \wedge, \vee, \rightarrow\\}$ as primitive symbols?

Question

Context

The System CL

In section 6.3 of Topoi, Robert Goldblatt describes a Hilbert-style deductive calculus (the only inference law is modus ponens) for the propositional logic of a language with the primitive logical connective symbols $\\{\neg, \wedge, \vee, \rightarrow\\}$, which he calls CL, with following axiom schemata:

1. $\alpha\rightarrow(\alpha\wedge\alpha)$
2. $(\alpha\wedge\beta)\rightarrow(\beta\wedge\alpha)$
3. $(\alpha\rightarrow\beta)\rightarrow((\alpha\wedge\gamma)\rightarrow(\beta\wedge\gamma))$
4. $((\alpha\rightarrow\beta)\wedge(\beta\rightarrow\gamma))\rightarrow(\alpha\rightarrow\gamma)$
5. $\beta\rightarrow(\alpha\rightarrow\beta)$
6. $(\alpha\wedge(\alpha\rightarrow\beta))\rightarrow\beta$
7. $\alpha\rightarrow(\alpha\vee\beta)$
8. $(\alpha\vee\beta)\rightarrow(\beta\vee\alpha)$
9. $((\alpha\rightarrow\gamma)\wedge(\beta\rightarrow\gamma))\rightarrow((\alpha\vee\beta)\rightarrow\gamma))$
10. $\neg\alpha\rightarrow(\alpha\rightarrow\beta)$
11. $((\alpha\rightarrow\beta)\wedge(\alpha\rightarrow\neg\beta))\rightarrow\neg\alpha$
12. $\alpha\vee\neg\alpha$

Some Thoughts

Goldblatt claims that the theorems of this system are the tautologies of classical propositional logic. However, these axioms are different from the ones I'm used to seeing, such as Łukasiewicz's axioms, where in particular $\wedge$ and $\vee$ are defined, rather than primitive, connectives. (I will refer to this system as HS.) Moreover, Goldblatt doesn't provide any examples of this axiom system in action, so it's hard for me to see how it would actually prove simple tautologies, like $(A\wedge A)\rightarrow A$ or $A\rightarrow A$.

Questions

I'm looking for any of the following to help me better understand CL's "engine", so to speak (by analogy with HS, see some proofs or combinatory logic):

• Does anybody have a reference to an analysis of (the propositional fragment of) a Hilbert system with a similar set of axioms--in particular, one with the same set of primitive logical connectives?
• How does a formal proof of $A \rightarrow A$ (or, better yet, $(A\rightarrow(B\rightarrow C))\rightarrow((A\rightarrow B)\rightarrow(A\rightarrow C))$, an axiom of HS), look like in CL?
• How can I prove the conjunction introduction/elimination laws as metatheorems using CL? If I knew how to do this, then I think I could probably figure out how to prove the deduction theorem.
• How would I prove the remaining laws of inference of natural deduction, in particular disjunctive elimination/syllogism, as metatheorems using CL?

Answer 1

Yeah, not a very intuitive system. But I agree, the key is probably to figure out Conjunction Introduction and Conjunction Elimination and from there you can probably get to the Deduction Theorem.

Ok, I found Conjunction Introduction:

$1. \alpha$

$2. \beta$

$3. \alpha \land \alpha (1, Ax. 1)$

$4. \alpha \to \beta (2, Ax.5)$

$5. \beta \land \alpha (3,4.Ax.3)$