1.初始符号 　　A, B, …, X, Y, Z (表示命题) 　　, ∧, ∨,→, (表示联结词) 　　( ) , (圆括号和逗点) 　　α,β,γ,… (表示公式串) 　　2. 形成规则 　　(1) 符号π是合式公式。 (π取值A, B, …) 　　(2) 若A是合式公式, 则A是合式公式。 　　(3) 若A, B是合式公式, 则(A∧B), (A∨B), (A→B), (AB)是合式公式。 　　(4) 只有符号(1) (2) (3)的符号序列才是合式公式。 　　(5) 任何合式公式是公式串, 空符号串也是公式串。 　　(6) 如果α和β是公式串, 则α,β和β,α也是公式串(两者不加区分)。 　　(7) 只有由(5)(6)形成的符号串才是公式串。 　　3. 定义 　　(1) 相继式。如果α和β都是公式串, 则称 　　　　　　　　 　　是相继式。α为前件, β为后件。 　　(2) 规定前件的中的"，"以∧表示, 后件中的"，"以∨表示, 便可将化为α→β。 　　(3) 相继式α→β为真, 便以表示。 　　4. 公理 　　如果公式串α和β中的公式都仅只是命题变项A, B, …(不再有联结词了), 则是公理(为真)的充分必要条件是α和β中至少含有一个相同的命题变项。 　　使用该算法证明定理, 总是把公式串中的各公式使用推理规则化成不再有联结词的形式。如A, B,, D, 这时的两侧有共同变项B, 公理说A, B,, D成立。依3中定义的, A, B,, D等价于 　　A∧B∧C→B∨D 　　为真, 由于B出现在→的两侧, 这蕴涵式必真。 　　5. 变形(推理)规则 　　共有十条, 都是针对联结词的消除(如果反向使用这些规则)而建立的。其中有五条前件规则和五条后件规则。