『構成的数学の体系と実践』

構成的数学はBHK解釈の下で展開される数学

BHK解釈の下で許容される証明は構成的証明

以下の命題は許容されない

LPO(the Limited Principle of Omniscience)

任意の0-1列$ \{a_n\} に対して、$ ∃n(a_n = 1) または$ ∀n(a_n = 0)

WLPO(the Weak Limited Principle of Omniscience)

任意の0-1列$ \{a_n\} に対して、$ ∃n(a_n = 0) または$ \lnot∀n(a_n = 0)

LLPO(the Lesser Limited Principle of Omniscience)

なんもわからん

BHK解釈の下で許容される証明（構成的証明）はアルゴリズムと見なせるもののみ。

排中律は許されない

直観主義数学

– “すべての関数は連続関数”

– LPO, WLPO, LLPOそれぞれの否定が成り立つ。

SIL(safety integrated level、安全度水準)に応じた推奨する開発手法がある

SIL2〜SIL4は形式手法の対象