ブロック構造を作る言葉

全称記号の導入

x∈X は任意とする。
 ：
 P(x)
xは任意だったから、
 ∀x.P(x)

含意導入

Pと仮定する。
 ：
 Q
Pを仮定していたから、
 P⇒Q

存在命題からの言い回しが難しい。

∃x.P
 これを満たすxをaとする。
 ：
  Q

例題

• 定義 Even(n) :⇔ ∃p.(n = 2p)
• ターゲット Even(n)∧Even(m) ⇒ Even(n + m)

Even(n)と仮定する。
定義より
 ∃p.(n = 2p) ---(1)
Even(m)と仮定する。
定義より
 ∃q.(m = 2q) ---(2)
$(1)を満たすpを選ぶ。
  n = 2p
$(2)を満たすqを選ぶ。
  m = 2q
計算する。
    n + m
  = 2p + 2q
  = 2(p + q)
したがって
  n + m = 2(p + q)
p + q を事例として
 ∃r.(n + m = 2r)
定義より
  Even(n + m)