Independent forall on nat

Stream: maths

[Chris Hughes]

Are there any known independent propositions of the form ∀ x : ℕ, p x , where p is a decidable predicate?

[Kevin Buzzard]

My vague understanding of Friedman's work is that he comes up with statements about finite objects which are independent of ZFC, but they can be typically proved using large cardinal axioms. But are you talking about independence in Lean + the three usual axioms, which I think is a much stronger statement?

[Chris Hughes]

more or less yes. Does independence in ZFC not imply independence in lean?

[Mario Carneiro]

No, of course Con(ZFC) is independent of ZFC and provable in lean

[Mario Carneiro]

But Con(lean) can be expressed as a Pi01 sentence, i.e. as ∀ x : ℕ, p x where p is decidable

[Mario Carneiro]

I don't know if any of the "cheap shot" independent statements like N = Z can be written as arithmetic statements

[Kevin Buzzard]

http://www.ams.org/notices/200604/fea-davis.pdf

[Kevin Buzzard]

This seems to give arguments which prove that p exists without explicitly writing it down, and perhaps it's possible to explicitly write it down but when you've finished it will be pretty horrible

[Mario Carneiro]

There are already lean predicates which will suffice to state this result with an exists

[Mario Carneiro]

specifically, evaln k e 0 in the computability lib will evaluate a partial recursive function e for k steps, so there is some e for which \lam n, (evaln n e 0).is_none satisfies the conditions (using a partial recursive function that searches for a contradiction in lean)

[Kevin Buzzard]

My impression is that this e will be huge though. My impression is that Friedman is actually writing down some precise statements about graphs which are explicit examples of p if independence in ZFC is what you're looking for. See for example the last result in the linked paper. He's quantifying over three variables not one but you just choose a computable bijection between N^3 and N to fix this

[Mario Carneiro]

sure, the encoding isn't optimized for size

[Mario Carneiro]

it's about as complicated as it is to describe a proof system like lean or ZFC+inaccessibles or anything of higher consistency strength

[Kevin Buzzard]

Of course all this assumes lean/ZFC/whatever we're talking about is consistent. I guess you'll have to wait for some Tarski version of Friedman to come along before you can see an explicit and comprehensible p for Lean...

[Mario Carneiro]

I think some of Friedman's work has the consistency strength of some weakly Mahlo cardinals which is more than enough

[Kevin Buzzard]

Oh so maybe there's hope with some weird statement about finite graphs

[Mario Carneiro]

I was somewhat disillusioned with Friedman's claims of "simplicity" when it turned out (in Scott Aaronson's project https://www.scottaaronson.com/blog/?p=2725 to build a TM whose halting is independent of ZFC) that it's cheaper to just build a tiny metamath verifier than to define some of Friedman's combinatorial objects

[Mario Carneiro]

If you are only going for "explicit and comprehensible", not size from scratch, it's not so bad at all. It is certainly easier than defining schemes

[Mario Carneiro]

this e will be huge though

It occurs to me that I don't know what you mean by "huge" here. This number is huge the same way Graham's number is huge: it is numerically very large, but its description is relatively compact. Since you usually aren't working from scratch in lean anyway, but are building up a language as you go, it's perfectly reasonable to get "explicit and comprehensible" by judicious use of sensibly named definitions while still producing a numerically huge result. But I don't see why this should matter to a mathematician

[Kevin Buzzard]

I just mean "irritating to write down explicitly" :-)

[Kevin Buzzard]

@Chris Hughes so the basic trick is to make p n equal to a statement something like "if you write n in base 256 and then interpret the resulting list of numbers as a text file, then this text file is not a proof of X in Lean" where X is carefully chosen. But then you have to build a lean parser etc all within p, and also to get exactly what you ask you need to do some other trickery with computable functions too to actually get this trick to work

[Mario Carneiro]

yikes, that's an extreme solution

[Mario Carneiro]

I was thinking more along the lines of formalizing a syntax for a dependent type theory like lean, not the real lean language which has lots of irrelevant garbage. It would look a lot like formalizing that paper of mine

[Mario Carneiro]

Except easier because there are much simpler languages with the same consistency strength