Re:Where do type systems come from? (2017)
by shikoba on Friday October 08, 2021 @04:59AM
(#28797135)
>there are true propositions that cannot be proved
In that case, they're not theorems. Theorem are things that can be proved starting from axioms. And proofs are enumerable, except if the axioms are not enumerable.
enumerable (in fact they are not even countable). See the following article:
https://papers.ssrn.com/abstract=3603021
In a foundational system, there are true propositions that
cannot be proved. For example, is true but unprovable that
an algorithm can enumerate the theorems of an order
abstracted from strings.