FWIW, I was thinking of unprovable truths, (wrt some chosen axioms) that are provable with stronger axioms. There, a proof checker based on a finite axiom set would return “false”, for true and provable statements.
Many statements aren’t simply “true”; if a statement isn’t logically valid, it’s only true in a specific theory, or about a specific structure. A given satisfiable non-valid statement is true about one structure, and false about another, true in one theory, false in another theory, independent in the third one.
That’s irrelevant to a proof-checker. Proof-checkers reside in a specific axiomatic system. It doesn’t matter if there’s an axiomatic system that would give stronger results for the purpose that was under discussion, it just matters if there’s one of a given length in whatever formalism we want.
FWIW, I was thinking of unprovable truths, (wrt some chosen axioms) that are provable with stronger axioms. There, a proof checker based on a finite axiom set would return “false”, for true and provable statements.
Many statements aren’t simply “true”; if a statement isn’t logically valid, it’s only true in a specific theory, or about a specific structure. A given satisfiable non-valid statement is true about one structure, and false about another, true in one theory, false in another theory, independent in the third one.
Sure. In this problem, we at least have a specified problem domain—whether a machine will return “1” or “0″.
That’s irrelevant to a proof-checker. Proof-checkers reside in a specific axiomatic system. It doesn’t matter if there’s an axiomatic system that would give stronger results for the purpose that was under discussion, it just matters if there’s one of a given length in whatever formalism we want.