Cut-free Positive Classical Logic: Excluded Middle for 2-quantifiers formulas.
∀x.(∃y.∀z.P(x,y,z)∨∀y.∃z.¬P(x,y,z))

Cut-free Positive Classical Logic: Stolzengerg Principle (every map f:N→N has infinitely many 0's or infinitely many non-0's).
(   ∀x.∃y.(x≤y∧f(y)=0)    ∨    ∀x.∃y.(x≤y∧¬f(y)=0)   )