One thing that has piqued my interest is something based off of Hilbert's programme, applicable to proof assistants.

Suppose I write a proof assistant in Standard ML. Then I use it to prove some function can be added to the kernel without jeopardizing the soundness of the system. I would like to dynamically extend the running program by compiling this function, and adding it to the program.

Hilbert's programme had something like this (as I understand it, they called it the epsilon substitution method) whereby a theorem stated in "idealized mathematics" which states and proves a claim about "finitary mathematics" can be "imported" back into the finitary metatheory, even if the finitary metatheory cannot prove it directly.

I think John Harrison called such a scheme as I've outlined "computational reflection".

It'd be neat to see a toy model of it.

#proofassistant #standardml #hilbertprogram

So, wait, why isn't total functional programming a viable candidate of Hilbert's finitary methods?

In total functional programming, we see that its "objects that are conceivable in principle" and "processes that can be effectively executed in principle". These are the two criteria laid out in Hilbert and Bernays's "Grundlagen", vol. I, §2(c) ¶69.

Am I missing something more? 🤔

#finitism #Hilbert #HilbertProgram #functional_programming

ゲーデルの不完全性定理によって，ヒルベルトの計画がヒルベルトが思い描いたような形で成就することはあり得ないことが示された，ということは，ヒルベルトの計画自身が無意味であったということを意味するものではないはずですし，ヒルベルト計画が無意味になった，ということも意味するものではないように思えます．

第2節でも既に述べたように，ヒルベルト自身は，ヒルベルトの計画が，彼の思い描いていたような仕方で完結した暁には，数学者たちは，数学の基礎付けの研究を終えて，安心して，従来の数学研究に戻ってゆくことができる，というように考えていたようで，彼の書いた論説の中には，実際にそのような表明も見られます．ゲーデルの不完全性定理が否定したのは，数学者が，この「普通の」数学に戻ってゆくことができる可能性でした．この意味では，数学が健全な科学として発展するためには，未来永劫にわたって，数学の基礎付けや，その研究から派生した数理論理学を，避けて通ることはできない，というのが，この定理の結論のはずなのですが，それを理解できない，あるいは理解することを拒否している数学者があまりに多いことには，驚嘆の念を禁じ得ませんし，本書のような本を書いてしまう人まで出てくることは，開いた口が塞がらない，とでも形容するしかほかないようにも思えます．

https://fuchino.ddo.jp/misc/superlesson.pdf

#HilbertProgram
#IncompletenessTheorems