1
vote
2answers
328 views

Would intuitionistic refutation method imply permutation of premisses?

Dear All In the classical refutation method, one searches for a proof of $\Gamma, \lnot A \vdash \bot$ instead of $\Gamma \vdash A$. The method works, i.e. is complete and correct, since it is for ...
2
votes
1answer
739 views

How establish conversion of cut-free proof into uniform proof?

Dear All Gentzen (*) claimed that through cut-elimination, he can normalize proofs. It is well known that cut-eliminated proofs might still contain some unnecessary noise. I am trying to show that ...