V_V comments on A quick sketch on how the Curry-Howard Isomorphism kinda appears to connect Algorithmic Information Theory with ordinal logics

[V_V]

I think the grandparent silently assumes we’ve solved logical uncertainty, and can use this to decide an axiom does not produce a contradiction by observing the lack of explosion.

Wouldn’t that imply having solved undecidability?

[hairyfigment]

I spoke imprecisely, or at least the OP argues that I did. It assumes we have a progressive solution to undecidability/​ logical uncertainty that can take us pretty far, eventually, but does not allow self-knowledge at any time.