一句话：提出 falsifier 演算，用 falsifier 规则引入 epsilon 项，使某些一阶定理的无切证明可非初等压缩。
论文研究一阶谓词逻辑中证明大小的非初等压缩。作者在 Hilbert epsilon-演算语言下提出深度推理系统 falsifier 演算，其新规则 falsifier 规则用于引入 epsilon 项，不同于传统 epsilon-演算的 critical axioms，并可视为量词移位规则的推广。作者证明该演算对某些一阶定理给出比相继式演算非初等更短的无切证明，并建立类似 Herbrand 定理的分解定理，引入 falsifier 析取作为新型中间公式。进一步证明某些一阶定理的 falsifier 析取可比 Herbrand 析取非初等地更小。
I introduce the falsifier calculus, a new deep-inference proof system for first-order predicate logic in the language of Hilbert's epsilon-calculus. It uses a new inference rule, the falsifier rule, to introduce epsilon-terms into a proof, distinct from the critical axioms of the traditional epsilon-calculus. The falsifier rule is a generalisation of one of the quantifier-shifts, inference rules for shifting quantifiers inside and outside of formulae. Like the epsilon-calculus and proof systems which include quantifier-shifts, the falsifier calculus admits non-elementarily shorter cut-free proofs of certain first-order theorems than the sequent calculus. Analogous to the way in which Herbrand's Theorem decomposes a proof into a first-order and a propositional part, connected by a Herbrand disjunction as an intermediate formula, I prove a decomposition theorem for the falsifier calculus which gives rise to a new notion of intermediate formula in the epsilon-calculus, falsifier disjunctions. I then prove that certain first-order theorems admit non-elementarily smaller falsifier disjunctions than Herbrand disjunctions.