Hilbert

有限の立場

Hilbertは数学における普遍妥当な論理式を機械的に導出可能とする公理系と推論法則を言語内部に構築し、実数学の諸概念を離散世界の抽象物に飛ばす機構を目指した言語です.

Hilbertで前提でされているものは自然演繹と恒真（トートロジー）のみです. この貧しさこそが豊かさなのです.

Hilbertでは実解析に関わる公理系を標準で添付しており、仮定をすればまるで紙の上で数式を撫でる感覚で実解析を行なう事出来ます.