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

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.

Comment author: Sniffnoy 19 April 2015 09:19:15PM *  5 points [-]

The clearest, least mystical, presentation of Goedel's First Incompleteness Theorem is: nonstandard models of first-order arithmetic exist, in which Goedel Sentences are false. The corresponding statement of Goedel's Second Incompleteness Theorem follows: nonstandard models of first-order arithmetic, which are inconsistent, exist. To capture only the consistent standard models of first-order arithmetic, you need to specify the additional axiom "First-order arithmetic is consistent", and so on up the ordinal hierarchy.

This doesn't make sense. A theory is inconsistent if and only if it has no models. I don't know what you mean by an "inconsistent model" here.

Now consider ordinal logic as started in Turing's PhD thesis, which starts with ordinary first-order logic and extends it with axioms saying "First-order logic is consistent", "First-order logic extended with the previous axiom is consistent", all the way up to the limiting countable infinity Omega (and then, I believe but haven't checked, further into the transfinite ordinals).

Actually, it stops at omega+1! Except there's not a unique way of doing omega+1, it depends on how exactly you encoded the omega. (Note: This is not something I have actually taken the time to understand beyond what's written there at all.)

Comment author: [deleted] 20 April 2015 01:43:56AM *  4 points [-]

This doesn't make sense. A theory is inconsistent if and only if it has no models. I don't know what you mean by an "inconsistent model" here.

It straightforwardly means that I don't know very much model theory and interpreted my limited reading in an incorrect way. It appears that I mean a nonstandard model of Peano Arithmetic which is syntactically consistent but which fails to be omega-consistent. Only omega-consistent logics maintain an exact isomorphism between their Goedel Numberings of theorems and actual theorems, AFAIK.

Comment author: hairyfigment 20 April 2015 01:00:39AM 2 points [-]

I think the OP means a model of the assertion that arithmetic is inconsistent. It still seems weirdly written, though. (E.g,I don't know how to interpret, "up to any finite ordinal level, standard models of first-order arithmetic".)