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. 变形(推理)规则
  共有十条, 都是针对联结词的消除(如果反向使用这些规则)而建立的。其中有五条前件规则和五条后件规则。