g_pepper 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: g_pepper 20 April 2015 05:30:20AM 3 points [-]

However, for purposes of computability theory and algorithmic information theory, such an existence statement is useless.

That is my point - stating that a function that maps a finite domain onto {0,1} is computable is trivially true and (as you said) useless. I was not really trying to be extra Platonist; I was just trying to point out that these sorts of finite mapping functions are not really interesting from a computability theory standpoint.

And I am speaking in a constructive sense of existence, intending to say that we can in fact discover such theories: by learning our way up the ordinal hierarchy, so to speak.

If you can formalize how you will discover such theories (i.e. how the learning our way up the ordinal hierarchy part will work), I'll be interested in seeing what you come up with.

Comment author: [deleted] 20 April 2015 09:47:37PM 4 points [-]

If you can formalize how you will discover such theories (i.e. how the learning our way up the ordinal hierarchy part will work), I'll be interested in seeing what you come up with.

That's the tough bit.