命題の例

http://www.chimaira.org/archive/MizarLightForHOLLight_miz.ps.pdf より、

:: The drinker's principle
reserve x for object;

ex x st P x implies for y holds P y
proof
  per cases;
  suppose A0: ex x st not P x;
    consider a such that A1: not P a by A0;
    take a;
    assume A2: P a;
    A3: contradiction by A1,A2;
    thus A4: for y holds P y by A3;
  suppose A5: for x holds P x;
    consider a suah that A6: not contradiction;
    take a;
    thus A7: P a implies for y holds P y by A5;
end;

ちなみにHOLだと、

let DRINKER = prove
(`?x:A. P x ==> !y. P y`,
ASM_CASES_TAC `?x:A. ~P x` THEN
RULE_ASSUM_TAC (REWRITE_RULE[NOT_EXISTS_THM]) THENL
[POP_ASSUM CHOOSE_TAC; ALL_TAC] THEN
EXISTS_TAC `x:A` THEN
ASM_REWRITE_TAC[]);;

キーワードを一部日本語に置換してみる。

:: The drinker's principle
予約 x for object;

∃x.(P x ⇒ (∀y. P y))
証明
  場合分け;
  場合 A0: ∃x. not P x;
    consider a such that A1: not P a 根拠は A0;
    take a;
    assume A2: P a;
    A3: 矛盾 根拠は A1,A2;
    よって A4: ∀y. P y 根拠は A3;
  場合 A5: ∀x. P x;
    consider a such that A6: なんでもいい;
    take a;
    よって A7: P a ⇒ ∀y. P y 根拠は A5;
終り;