証明の形式、骨組み：(スケルトン)
[論理式] proof [証明法] end;
Aが成立する -------------------------------------------------- proof thus A; end;
Q⇒A Qを仮定する ～ Aとなる -------------------------------------------------- Q implies A proof assume Q; ～ thus A; end;
given = assume + consider とする場合 ((∃x)Q[x})⇒A xをQ[x}に与える ～ Aとなる -------------------------------------------------- (ex x st Q[x]) implies A proof given x such that Q[x]; ······ ～ ······ thus A; end;
A⇔B A⇒B and B⇒A -------------------------------------------------- A iff B proof thus A implies B; thus B implies A; end; ================================================== A⇔B これにより Aを仮定 Bとなる Bを仮定 Aとなる -------------------------------------------------- A iff B proof hereby assume A; thus B; end; assume B; thus A; end;
A or B Aでないと仮定 Bとなる --------------------------------------------------- A or B proof assume not A; thus B; end;
A and B Aが成立 Bが成立 --------------------------------------------------- A & B proof thus A; thus B; end;
∀ x ∈集合 ⊆ f(x) x∈集合 f(x)が成立 --------------------------------------------------- for x being set holds f(x) proof let x be set; thus f(x); end;
∃ x ∈集合 ⇒ f(x) あるxとする f(x)が成立 --------------------------------------------------- ex x being set st f(x) proof take a; thus f(a); end;
Pは正しい Pは間違っていると仮定する 矛盾する
Qは間違っている Qは間違っていると仮定する 矛盾しない
A⇒B and B⇒C
A⇒B or A⇒C
consider 変数 型;
変数rを再定義する場合には
reconsider 変数 型;
ラベル付けを行う。(同じラベルの場合には直前のラベルが引用される)
ラベル名:式;
A1: a=b;
that ラベル：式
such that ラベル：式
assume 仮定式