1
$\begingroup$

Could anyone please help me to understand what the question is asking?

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):

enter image description here

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Taroccoesbrocco Feb 9 at 22:29
  • $\begingroup$ 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. $\endgroup$ – Daniel Mak Feb 9 at 22:50
3
$\begingroup$

The Hilbert systems in that book are modular and the axioms are somewhat separable in such a way that you can obtain different systems (and fragments thereof) simply by adding or omitting axioms.

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

$\endgroup$

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.