Exactly. For a more familiar example, the independence of the continuum hypothesis from ZFC means that we’ll never stumble across a set of intermediate cardinality while doing an analysis problem (otherwise, we’d have a disproof), and so the CH is valid in a practical sense even though formally undecidable.
Generally speaking, if a statement is undecidable and claims the existence of something which could be effectively verified if it were found, then for practical purposes you can assume it’s false.
EDIT: Oops- see paulfchristiano’s comment on why P vs. NP isn’t a case of this principle. I think the general principle is still OK, I just forgot about the whole “ability to effectively verify” bit in this case.
See paulfchristiano’s comments. The mistake in DanielLC’s comment is that, even though any polynomial algorithm can be “stated in ZFC”, the proof that it runs in polynomial time doesn’t necessarily lie within ZFC, or ZFC+Con(ZFC), or any other system you can name in advance.
Exactly. For a more familiar example, the independence of the continuum hypothesis from ZFC means that we’ll never stumble across a set of intermediate cardinality while doing an analysis problem (otherwise, we’d have a disproof), and so the CH is valid in a practical sense even though formally undecidable.
Generally speaking, if a statement is undecidable and claims the existence of something which could be effectively verified if it were found, then for practical purposes you can assume it’s false.
EDIT: Oops- see paulfchristiano’s comment on why P vs. NP isn’t a case of this principle. I think the general principle is still OK, I just forgot about the whole “ability to effectively verify” bit in this case.
See paulfchristiano’s comments. The mistake in DanielLC’s comment is that, even though any polynomial algorithm can be “stated in ZFC”, the proof that it runs in polynomial time doesn’t necessarily lie within ZFC, or ZFC+Con(ZFC), or any other system you can name in advance.
Ah, thanks.