# Provide sequent calculus proofs of the axioms of the $\{→,∀,⊥\}$-fragment of the Hilbert system $H_c$

Theorem: G1$$_i$$ + Cut $$\vdash \Gamma \Rightarrow A$$ iff H$$_i$$ $$\vdash \Gamma \Rightarrow A$$

1) Prove equivalence of G1$$_i$$ with the Hilbert system H$$_i$$ directly, that is to say, not via the equivalence of G1$$_i$$ with natural deduction.

2) Provide sequent calculus proofs of the axioms of the $$\{→,∀,⊥\}$$-fragment of the Hilbert system $$H_c$$.

1) is the question in the textbook, and 2) is the one that my lecturer is asking specifically (that is based on 1).

For 1) it is fairly clear what I need to do: do an induction on length of proof so that the 2nd proof system can prove all the rules that the 1st has, vice versa.

But the bit about fragment in 2) confuses me: I imagine 2) is asking me to prove that whatever one can prove in $$H_c$$, one can also prove in G1$$_i$$ (hence the 'provide sequent calculus proof').

But in a $$H_c$$ system, one has a bunch of axioms and 2 inference rules - that's it. And none of them even involves $$⊥$$. So what am I actually supposed to prove here?

Here is the $$H_c$$ system as depicted in my textbook (Troelstra and Schwictenberg's Basic Proof Theory):

• What have you tried so far? You are asking for so many derivations! Some of them are trivial. Some others are more tricky. Please, ask a precise question for a single axiom that you don't manage to prove. – Taroccoesbrocco Feb 9 at 22:29
• No I am not asking for an actual proof; I actually don't even fully understand what the question is asking for - that's what I am trying to find out. Specifically, the 'of the {→,∀,⊥}-fragment' bit is what confuses me: I don't understand what that means. – Daniel Mak Feb 9 at 22:50

For instance, in order to obtain the pure implication fragment of minimal logic Hm, you would consider only the axioms: $$A\to(B\to{A})$$ and $$(A\to{(B\to{C})})\to{((A\to{B})\to{(A\to{C})})}$$. For a fragment $$\{\to{},\vee\}$$ of Hm containing implication and disjunction, you would add the axioms containg disjunction on the second and third line of the list (and so on and so forth).
So, the second question is asking you to provide a sequent calculus derivation for the axioms on implication above, plus the axioms for the universal quantifier (first axiom on fifth line and the axiom on the sixth line), plus $$\bot\to{A}$$ and $$\lnot\lnot{A}\to{A}$$ (in order to obtain a classical system from the minimal one). Remember that negation is defined as $$\lnot{A}\equiv{A\to{\bot}}$$.
P.S. Your claim that $$\bot$$ does not occur among the axioms for Hc is incorrect: "Hi has in addition the axiom $$\bot\to{A}$$ and Hc is Hi plus an additional axiom schema $$\lnot\lnot{A}\to{A}$$".