証明の形式、骨組み:(スケルトン)

[論理式] 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 仮定式