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

11 [deleted] 19 April 2015 07:35PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Comments (27)

You are viewing a single comment's thread. Show more comments above.

Comment author: V_V 20 April 2015 05:56:36PM 1 point [-]

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?

Comment author: hairyfigment 20 April 2015 08:57:00PM 1 point [-]

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.