这里我们给出定理的证明。 　　设给定一谓词演算公式A。 　　（1） 必有一前束范式E1，且├DE1。 　　（2） 如E1中有自由个体变项⊿1,⊿2,…,⊿m ，则可引用概括规则得 　　E2 = (⊿1)(⊿2)…(⊿m)E1，m≥0。 　　E2和E1可以互推，如E1中无自由个体变项，则E2即是E1。 　　（3） 如E2中只有命题变项而无谓词变项，即是说，E2为一命题演算的公式，则可引用定理 　　├P(x)(F(x)∨F(x)∧P) 　　引入一个处于最前方的存在量词。 　　（4） 如E2为前束范式，则E2即为E。否则E2的形式为 　　(x1)(x2)…(xn)(y)D(x1,…,xn,y)，n≥0。 　　在这里，D(x1,…,xn,y)为一前束范式，其中只有x1,…,xn, y是自由个体变项。E2有两种可能： 　　（a） 全称量词"(y)"之前无存在量词，其后也无存在量词。 　　（b） "(y)"后只有k - 1个全称量词出现于存在量词之前。 　　现在如果能够证明，在上述情形下，必然可以求得一前束范式E3，E3和E2可以互推，并且，如为情况（a），则E3的最前方为一存在量词，也就是说，E3是一个前束范式。如为情况（b），则E3中只有k - 1个全称量词出现于存在量词之前，也就是说，比E2少一个这样的全称量词。在情况（b）下，经过k次这样的转换，就可以得到一前束范式，因此存在定理得证。 　　为了求得E3，可先构造E*如下。 　　(x1)(x2)…(xn){(y)[D(x1,…,xn,y)∧S(x1,…,xn,y)]∨(z)S(x1,…,xn, z) 　　其中S(…)是在D中不出现的谓词变项，z是在D中不出现的个体变项。现在需要 　证明 　　（ⅰ）E2和E*可以互推，（ⅱ）从E*可以得到所需要的E3，E*和E3可以互推。 　　（5） E2和E*可以互推。根据定理 　　├(x)(F(x)→G(x))→((x)F(x)→(x)G(x)) 　　可得 　　├(y)F(y)→(y)(F(y)∧G(y))∨(z)G(z)。 　　在上列公式中，以D(x1,…,xn, ⊿)代F(⊿)，以S(x1,…,xn,⊿)代G(⊿)，可得 　　├(y) D(x1,…,xn,y)→(y)[( D(x1,…,xn,y)∧S(x1,…,xn, y))]∨(z)S(x1,…,xn, z) 　　根据概括规则及定理 　　├(x)(F(x)→G(x))→((x)F(x)→(x)G(x)) 　　可得 　　├(x1)(x2)…(xn)(y)D(x1,…,xn,y) 　　→(x1)(x2)…(xn){(y)[ D(x1,…,xn,y) 　　∧S(x1,…,xn, y)]∨(z)S(x1,…,xn, z)} 　　以上即是├E2→E*。可见从E2可以推出E*。 　　现证从E*可以推出E2。 　　在E*中作代入，以D(x1,…,xn, ⊿)代S(x1,…,xn,⊿) 　　可得 　　(x1)(x2)…(xn){(y) [ D(x1,…,xn,y)∧S(x1,…,xn, y)]∨(z)S(x1,…,xn, z)} 　　消去其中的矛盾式则得 　　(x1)(x2)…(xn)(z)D(x1,…,xn,z)。 　　再用约束变项易字可得E2，即是 　　(x1)(x2)…(xn)(y)D(x1,…,xn,y)。 　　因此，E2和E*可互推得证。 　　（6） 从E*可以推出E3。E*为 　　(x1)(x2)…(xn){(y)[ D(x1,…,xn,y)∧S(x1,…,xn, y)]∨(z)S(x1,…,xn, z)} 　　D(…)为一前束范式，其中只有k - 1个全称量词出现于存在量词之前，设D(…)为 　　Z1Z2…Z1 A*(x1,…,xn, y)，l≥k。 　　其中Z1,…,Z1皆为量词，且约束变项中无z。现将量词(y), Z1,…,Z1等依次前移使其辖域延伸至公式的末端，最后将(z)前移。这样前移的结果即为E3： 　　(x1)(x2)…(xn)(y) Z1Z2…Z1(z){[D(x1,…,xn,y) 　　∧S(x1,…,xn, y)]∨S(x1,…,xn, z)}。 　　由于Z1前的"(y)"已转换为一存在量词"(y)"，同时"(z)"已移至前束词末端，因此（a）如果E2中原无存在量词，E3的第一个量词即为存在量词，所以E3是一个前束范式，（b）如果E2中原有的k个全称量词出现于存在量词之前，在E3中只有k - 1个全称量词在某些存在量词之前，与E3相较已减少一个。 　　E*和E3是等值的，因此也是可以互推的。至此，前束范式的存在定理得证。