Let’s step through the algorithm. If S proves that A()≠2, then A will immediately return 2. That means S has proved a false statement about the universe. If S doesn’t prove that A()≠2, but proves that A()≠1, then A will immediately return 1, which also means S has proved a false statement about the universe.
So yeah, I guess calling it a violation of consistency was wrong. It’s actually a violation of soundness: all axioms of S must be true statements about the universe. If S is sound, then the above reasoning shows that S cannot prove A()≠a for any a. (Also soundness implies consistency, which might explain why I made the mistake.) Thanks for pointing that out! Edited the post accordingly.
Alright, that makes sense (if my reading of proofs seems uncharitable at times, it is because I know enough about logic to know when a statement doesn’t make sense, but I don’t know enough to tell what the statement wants to be).
Soundness seems like an interesting property to think about for a formal system. I am reminded of the bizarre systems you can get, e.g., by taking PA and adding the axiom “PA is inconsistent”. This, if I recall correctly, is consistent provided PA itself is consistent, but (whether or not it’s consistent) it definitely can’t be sound.
Let’s step through the algorithm. If S proves that A()≠2, then A will immediately return 2. That means S has proved a false statement about the universe. If S doesn’t prove that A()≠2, but proves that A()≠1, then A will immediately return 1, which also means S has proved a false statement about the universe.
So yeah, I guess calling it a violation of consistency was wrong. It’s actually a violation of soundness: all axioms of S must be true statements about the universe. If S is sound, then the above reasoning shows that S cannot prove A()≠a for any a. (Also soundness implies consistency, which might explain why I made the mistake.) Thanks for pointing that out! Edited the post accordingly.
Alright, that makes sense (if my reading of proofs seems uncharitable at times, it is because I know enough about logic to know when a statement doesn’t make sense, but I don’t know enough to tell what the statement wants to be).
Soundness seems like an interesting property to think about for a formal system. I am reminded of the bizarre systems you can get, e.g., by taking PA and adding the axiom “PA is inconsistent”. This, if I recall correctly, is consistent provided PA itself is consistent, but (whether or not it’s consistent) it definitely can’t be sound.
I want people to read my math uncharitably and poke holes in it, otherwise I wouldn’t post :-)
If S was sound-if-consistent, this problem makes it unsound, hence inconsistent.