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.

Article Navigation

Comments (27)
Tags: curry-howard kolmogorov_complexity computability ordinal_logic algorithmic_information_theory

Comments (27)

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

Comment author: V_V 20 April 2015 03:59:26PM *  1 point [-]

This is where things get fuzzier. I think that by routing through logic and observing the empirical consequences of ordinal consistency axioms

I'm not sure I understand what you mean here.

Assume we have a formal system and we are using it to predict observations. In classical logic, if the formal system is inconsistent, then ex falso quodlibet, therefore all possible observations will be allowed by it.

Comment author: hairyfigment 20 April 2015 05:29:47PM 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. Though "routing through logic" seems like an incredibly bad way to say that.

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.

Comment author: [deleted] 20 April 2015 09:46:55PM *  -1 points [-]

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.

No. We don't decide an axiom does not produce a contradiction by observing the lack of explosion. We just raise the probability of noncontradiction by observing the lack of explosion.

EDIT: Axiom, not acronym. Holy God I need more sleep.

Though "routing through logic" seems like an incredibly bad way to say that.

-_-. The post itself was a sketch, not a finished, formalized publication. Please refrain from being anal about phrasings or imagining that I've done far more math than I really have. If I want to be precise, I'll just use symbols -- that's what they're for.

Powered by Reddit Powered by Reddit