Remix.run Logo
griffzhowl 12 hours ago

> Furthermore it's basically proven that these foundations can't even exist,

What are you referring to? The current working foundation is ZFC but there are equivalent type theoretical foundations like what Lean and other proof-checking software uses. I guess you know that, but that's why I don't know what you mean by saying this

alexey-salmin 3 hours ago | parent [-]

I'm referring to the failure of Hilbert's program. All the incompleteness, undefinability and undecidability results arise when and only when some sort of infinite objects are present so I can definitely see the allure of finitism.

ZFC is a working foundation of math but it's unknown whether it's consistent or arithmetically sound and important statements like CH are independent from it. It's a "working foundation" but not a "true foundation" which alas cannot exist.

As mentioned above I'm personally not a finitist and think that math without infinite and uncountable sets is intellectually poorer. I don't mind however developing further a finitist subset of math and see what's provable (and describable) in it, much like there's value in proving theorems in ZF instead of ZFC whenever possible.