We present a streamlined and simplified exponential lower bound on the length of proofs in intuitionistic implicational logic, adapted to Gordeev and Haeusler's dag-like natural deduction.
翻译:我们提出了一个针对直觉主义蕴涵逻辑中证明长度的精简且简化的指数级下界,该下界适用于Gordeev和Haeusler的有向无环图风格的自然演绎。