推理规则列表

引入规则

符号	中文名称	规则描述
^I	合取引入（与引入）	由 x 和 y 推出 x ^ y
->I	蕴涵引入	由“假设 x 推出 y”推出 x -> y
/I	析取引入（或引入）	由 x 推出 x / ? 或 ? / x
~I	否定引入	由“假设原命题推出矛盾”推出其否定
~~I	双重否定引入	由 x 推出 ~~x
FI	矛盾引入	由 x 和 ~x 推出 F
TI	永真引入	由空前提推出 T (这有什么意义呢 😏)
<->I	等值引入	由 x -> y 和 y -> x 推出 x <-> y
existsI	存在量词引入	由 𝝓(x) 推出 ∃a 𝝓(a)
forallI	全称量词引入	由“对任意 c 都能推出 f(c)”推出 ∀x f(x)

消除规则

符号	中文名称	规则描述
^E	合取消除（与消除）	由 x ^ y 推出 x (或 y)
->E	蕴涵消除	由 x -> y 和 x 推出 y
/E	析取消除（或消除）	由 x1 / x2、“假设 x1 推出 y”和“假设 x2 推出 y”推出 y
~E	否定消除	由 x 和 ~x 推出 F (同 FI)
~~E	双重否定消除	由 ~~x 推出 x
FE	矛盾消除	由 F 可推出任意命题
<->E	等值消除	由 x <-> y 和其中一侧推出另一侧
existsE	存在量词消除	由 ∃a 𝝓(a) 和“对某个 c，由 𝝓(c) 推出 x”推出 x
forallE	全称量词消除	由 ∀x f(x) 推出 f[x/c]
forall->E	全称蕴涵消除	由 ∀x f(x) -> g(x) 和 f(c) 推出 g(c)

特殊规则

符号	中文名称	规则描述
LEM	排中律	由空前提推出 p / ~p
MT	拒取式	由 x -> y 和 ~y 推出 ~x
PC	反证法	由“假设 x 推出矛盾”推出 ~x
refl	自反性	由空前提推出 x = x
=sub	等值替换	由 a = b 和 f(a) 推出 f(b)
sym	对称性	由 a = b 推出 b = a
forall I const	全称常量引入	引入一个新的自由变量
given	给定	标记一个给定的命题
premise	前提	标记一个给定的命题 (同 given)
ass	假设	标记一个假设的命题
tick	标记	由 x 推出 x (用于语法标记)

规则详解与用例

引入规则

^I (合取引入)

由 x 和 y 推出 x ^ y

1   x           [...]
2   y           [...]
3   x ^ y       [^I(1,2)]

->I (蕴涵引入)

由“假设 x 推出 y”推出 x -> y

1     x           [ass]
      <中间推导过程>
2     y           [...]
3   x -> y        [->I(1,2)]

/I (析取引入)

由 x 推出 x / ? 或 ? / x

1   x             [...]
2   x / y         [/I(1)]

~I (否定引入)

由“假设原命题推出矛盾”推出其否定

1     x           [ass]
      <中间推导过程>
2     F           [...]
3   ~x            [~I(1,2)]

~~I (双重否定引入)

由 x 推出 ~~x

1   x             [...]
2   ~(~(x))       [~~I(1)]

FI (矛盾引入)

由 x 和 ~x 推出 F

1   x             [...]
2   ~x            [...]
3   F             [FI(1,2)]

TI (永真引入)

由空前提推出 T (这有什么意义呢 😏)

1   T             [TI]

<->I (等值引入)

由 x -> y 和 y -> x 推出 x <-> y

1   x -> y        [...]
2   y -> x        [...]
3   x <-> y       [<->I(1,2)]

existsI (存在量词引入)

由 𝝓(x) 推出 ∃a 𝝓(a)

1   𝝓(x)                [...]
2   exists x. (𝝓(x))    [existsI(1)]

forallI (全称量词引入)

由“对任意 c 都能推出 f(c)”推出 ∀x f(x)

1     c                 [forall I const]
      <中间推导过程>
2     f(c)              [...]
3   forall x. (f(x))    [forallI(1,2)]

消除规则

^E (合取消除)

由 x ^ y 推出 x (或 y)

1   x ^ y       [...]
2   x           [^E(1)]

->E (蕴涵消除)

由 x -> y 和 x 推出 y

1   x           [...]
2   x -> y      [...]
3   y           [->E(1,2)]

/E (析取消除)

由 x1 / x2、“假设 x1 推出 y”和“假设 x2 推出 y”推出 y

1   x1 / x2         [...]
2     x1            [ass]
      <中间推导过程>
3     y             [...]
4     x2            [ass]
      <中间推导过程>
5     y             [...]
6   y               [/E(1,2,3,4,5)]

~E (否定消除)

由 x 和 ~x 推出 F (同 FI)

1   x             [...]
2   ~x            [...]
3   F             [~E(1,2)]

~~E (双重否定消除)

由 ~~x 推出 x

1   ~~x           [...]
2   x             [~~E(1)]

FE (矛盾消除)

由 F 可推出任意命题

1   F             [...]
2   anything      [FE(1)]

<->E (等值消除)

由 x <-> y 和其中一侧推出另一侧

1   x <-> y       [...]
2   y             [...]
3   x             [<->E(1,2)]

existsE (存在量词消除)

由 ∃a 𝝓(a) 和“对某个 c，由 𝝓(c) 推出 x”推出 x

1   exists a. (𝝓(a))    [...]
2     𝝓(c)              [ass]
      <中间推导过程>
3     x                 [...]
4   x                   [existsE(1,2,3)]

forallE (全称量词消除)

由 ∀x f(x) 推出 f[x/c]

1   forall x. (f(x))    [...]
2   f(c)                [forallE(1)]

forall->E (全称蕴涵消除)

由 ∀x f(x) -> g(x) 和 f(c) 推出 g(c)

1   forall x. (f(x) -> g(x))    [...]
2   f(c)                        [...]
3   g(c)                        [forall->E(1,2)]

特殊规则

LEM (排中律)

由空前提推出 p / ~p

1   x / ~x      [LEM]

MT (拒取式)

由 x -> y 和 ~y 推出 ~x

1   x -> y      [...]
2   ~y          [...]
3   ~x          [MT(1,2)]

PC (反证法)

由“假设 x 推出矛盾”推出 ~x

1     x         [ass]
      <中间推导过程>
2     F         [...]
3   ~x          [PC(1,2)]

refl (自反性)

由空前提推出 x = x

1   x = x   [refl]

=sub (等值替换)

由 a = b 和 f(a) 推出 f(b)

1   a = b       [...]
2   f(a)        [...]
3   f(b)        [=sub(2,1)]

sym (对称性)

由 a = b 推出 b = a

1   a = b   [...]
2   b = a   [sym(1)]

forall I const

引入一个新的自由变量

1   c       [forall I const]

given (给定)

标记一个给定的命题

1   x       [given]

premise (前提)

标记一个给定的命题

1   x       [premise]

ass (假设)

标记一个假设的命题

1   x           [...]
2     x -> y    [ass]
3     result    [...]
4   conclusion  [...]

tick (标记)

由 x 推出 x (用于语法标记)。详见 语法注意事项 了解更多。

1   x           [...]
2     y         [...]
3     result1   [...]
4     result1   [tick(3)]   # 必须用 tick 标记，表示当前子证明结束
5     z         [...]
6     result2   [...]
7   conclusion  [...]

重要说明！

• 关于行号...

  • 注释行和空行不计入行号！

  fai           [premise]
  -- 这里写点注释...
  
  -- 可能再多几行...
  foo(x)        [premise]
  
  foo(x)        [tick(2)] -- foo(x) 是证明中的第2行！

  • 此设计是为了方便你在书面证明和 ndpc 可验证的证明之间进行转换。

• 何时使用 tick 规则？

  • 任何时候都可以使用。但如果你要结束一个子证明（即“退出假设框”），而下一行又没有通过减少缩进来明确表示，则必须使用 tick。请看示例：

  有效：通过减少缩进结束子证明

  bar(y)      [premise]
    x         [forall I const]
    -- 中间推导过程...
    foo(x)    [some reason]
  x -> foo(x) [...] -- 有效，因为这里减少了缩进

  无效：缺少明确结束标记

  bar(y)      [premise]
    x         [forall I const]
    -- 中间推导过程...
    foo(x)    [some reason]
  -- 无效！我们直接跳出了缩进块，但没有标记
  x -> foo(x) [...]

  有效：使用 tick 明确结束子证明

  bar(y)      [premise]
    x         [forall I const]
    -- 中间推导过程...
    foo(x)    [some reason]
    foo(x)    [tick(42)] -- 有效！使用了 tick 明确结束子证明
  -- 由于有 tick 标记，子证明已清晰结束
  x -> foo(x) [...]

• 关于双重否定...

  • 为什么不能写成 ~~x 来表示双重否定？
  • 未来版本可能会支持，但目前你必须写成 ~(~(x))。