>CZF proves "Each total function from R to R is continous"
なんだが。CZF ってのは形式体系でしかない。 構成主義というのは CZF の「可能な解釈の一つ」でしかない。 CZF は ZF の部分体系であるのだから、古典数学も CZF の「可能な解釈の一つ」。 命題 A が形式体系 T で証明可能だということは、 その命題は T のどんな解釈でも正しいことを意味する。 こんなことは論理学の初歩。
よって CZF proves "Each total function from R to R is continous" と書いてあれば CZF の可能な解釈の一つである古典数学でも "Each total function from R to R is continous" が正しいということ。 Sanders本人も>>381も、論理学の初歩が全く身についていない駆け出しだということだ。