2
$\begingroup$

On page 57 of A Short Introduction to Intuitionistic Logic (Mints), the author provides an exercise: prove that the right implication rule is not invertible.

By an invertible rule he means: if the conclusion sequent can be derived, then the premise sequent can be derived.

The right implication rule is as follows (the full rule set is on page 54):

ϕ,Γ ⊢ Δ,ψ
---------
Γ ⊢ Δ,(ϕ→ψ)

My feeling is that the proof has something to do with the fact that the implication in the conclusion of the sequent could be the result of an application of the weaken rule, and that psi does not actually follow from phi. Based on that I'm trying to find a choice of phi,psi,Gamma, and Delta, and so that ϕ,Γ ⊢ Δ,ψ is underivable, but that Γ ⊢ Δ is derivable.

However I'm not sure if I'm on the right track because if Γ ⊢ Δ derivable then we can just weaken on the left and right to obtain ϕ,Γ ⊢ Δ,ψ. So I think my idea won't work. What am I missing here?

Thanks.

Edit: I now realize that I was confused about the right implication rule to point that I wrote it incorrectly here! Sorry about that. This was clearly a large part of my confusion about solving this exercise.

The correct rule is:

ϕ,Γ ⊢ ψ
---------
Γ ⊢ Δ,(ϕ→ψ)

Edit2: After revisiting the problem with respect to the correct implication rule, and the hints, I was able to solve it. Thanks everyone.

$\endgroup$
  • $\begingroup$ This rule is not intuitionistically valid (and it is invertible in the classical case in which it is valid). Are you sure you don't want to get rid of that $\Delta$ on top? $\endgroup$ – spaceisdarkgreen Mar 5 at 6:50
  • $\begingroup$ @spaceisdarkgreen what do you mean by not intuitionistically valid? Mints proves that this rule along with its siblings are sound with respect to intuitionistic semantics (compared to classical sequent calculus, the left implication rule had to be modified). $\endgroup$ – ttbo Mar 5 at 15:45
  • $\begingroup$ @spaceisdarkgreen Yes now I see that you are correct about your statement, and that I had misread the right implication rule (I edited my question to correct the mistake). Thanks. $\endgroup$ – ttbo Mar 5 at 17:01
0
$\begingroup$

However I'm not sure if I'm on the right track because if Γ ⊢ Δ derivable then we can just weaken on the left and right to obtain ϕ,Γ ⊢ Δ,ψ. So I think my idea won't work. What am I missing here?

Hint: Try when $\Delta$ is not derivable from $\Gamma$, but instead only derivable from $\phi$.

You wish to show that something of the form $\Gamma,\phi\vdash\Delta,\psi$ may be acceptable, but $\Gamma\vdash\Delta,\phi\to\psi$ is not in an intuitionistic framework.   Therefore you do not wish to examine cases where $\Gamma\vdash\Delta$.

$\endgroup$
  • $\begingroup$ Thanks for the hint but I'm confused about your statement of my goal. Is my goal not the following? Prove that there exists a choice of Γ,Δ,ϕ,ψ such that Γ ⊢ Δ,(ϕ→ψ) is derivable in intuitionistic sequent calculus, and also that ϕ,Γ ⊢ Δ,ψ is not derivable in intuitionistic sequent calculus. $\endgroup$ – ttbo Mar 5 at 16:10
  • $\begingroup$ Now that I discovered the source of my confusion about the right implication rule, I think my goal should be: Prove that there exists a choice of Γ,Δ,ϕ,ψ such that Γ ⊢ Δ,(ϕ→ψ) is derivable in intuitionistic sequent calculus, and also that ϕ,Γ ⊢ ψ is not derivable in intuitionistic sequent calculus. $\endgroup$ – ttbo Mar 5 at 17:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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