-(∀z)(∃y)Tzy ⊢ (∃z)(∀y)-Tzy

Using Lande, (AI,EI,AE,EE,->E,->I,-I,--E,^I,^E,vI,vE) I cannot figure out the proof on this sequent.

  • I think such questions are off-topic here and belong to mathoverflow.net
    – tkruse
    Dec 5, 2021 at 2:58
  • Is "-" meant to be negation? If so, why not start with an easier problem Ax[Px] -> ~Ex[~Px]? Where "Ax" is forall, "Ex" is exists, and "~" is negation
    – Ten O'Four
    Dec 5, 2021 at 6:54
  • I’m voting to close this question because this is not a homework forum Dec 6, 2021 at 5:49

1 Answer 1


-(∀z)(∃y)Tzy ⊢ (∃z)(∀y)-Tzy

quantifier negation to z: (∃z)~(∃y)Tzy

quantifier negation to y


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .