有界深度 Frege

一般 Frege 可以在一行里嵌套长链逻辑结构，有界深度 Frege 只能把信息铺成少数层的宽公式。无界 fan-in 让一层 AND 看见很多输入，却不能建立随 $n$ 增长的层级组合。证明可以有很多行，所以它仍能逐步积累知识；受限的是每个中间断言的内部结构，而不是整个证明共有多少推理轮。

这一区分很重要。一个含百万行、每行深度三的证明仍属于固定深度系统；一份只有十行但其中某行嵌套深度为 $n$ 的证明则不属于。proof DAG 的最长引用链、公式门深度和证明行数是三种不同资源，不能把“bounded depth”误解成常数时间验证或常数轮推理。

一次 resolution 推理

可在浅层 Frege 中由固定永真式

实现。若结论为假，则 $y=z=0$；两个前提分别强迫 $x=1$ 与 $x=0$，矛盾。把 implication 展开成 $\mathrm{\neg }A\vee B$ 后，深度仍是一个与输入规模无关的常数。对一般宽子句，把这里的 $y,z$ 换成相应析取式只需常数条推理和常数深度增量，但符号数仍与两个子句的长度成线性关系；因此逐步模拟的总开销是多项式，而不是把任意宽归结步骤误算成常数大小。

深度参数必须先固定。若对长度为 $n$ 的每个证明都允许另选 $d=\log n$，系统已不是 AC⁰-Frege；若加入 MOD${}_p$ 门，则得到 AC⁰[$p$]-Frege 等不同系统，奇偶与计数能力随之改变。允许 extension variables 又可能把深电路切成浅定义层，产生 extended bounded-depth 系统，不能与这里的纯浅层公式模型混为一谈。

有界深度下界通常针对精心编码的组合原理。把一个深目标公式先转成浅 DNF 可能指数增大，所得下界未必反映原编码。公式深度、扇入约定和目标家族必须同时报告。

随机限制会把浅层小公式简化成低深度决策结构，切换引理公理库Håstad switching lemmaHåstad's switching lemma · Switching lemma说明窄 CNF 或 DNF 在独立随机限制后，以指数高概率退化为浅决策树的结构定理。及其多层版本因此成为分析 AC⁰-Frege 的重要工具。证明下界还会用逼近法、随机结构和有限模型论。与一般 Frege 不同，某些鸽巢与计数原理在有界深度 Frege 中已有超多项式乃至特定参数下的指数下界；这些定理的强度依赖深度、公式基和原理编码。

浅层 Frege 位于电路下界与证明下界的交界：若每条证明行都能被随机限制大幅简化，而受限后的目标原理仍保留全局矛盾，就可排除短证明。这个策略不能直接推广到 unrestricted Frege，因为深公式不会按同一 switching 估计坍缩。已有浅层结果因而是受限系统定理，不是一般 Frege 下界的代名词。