It is possible that I wasn’t clear enough (my phrasing could certainly use work). I was thinking of statements such as your remark that “An automated proof-checker can identify some correct proofs—but not all of them” whereas we generally don’t call something an automated proof checker unless it terminates on any proof and returns correctly if that’s a valid proof or not in the axiomatic system. Sometimes we insist that this be a primitively recursive process. Sometimes this is also generalizable in a natural way such that the proofchecker can do this given some specific oracle (there are results about how these sorts of things can behave if they have access to a Halting oracle for example. I don’t fully understand these except in vague generality.)
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.
It is possible that I wasn’t clear enough (my phrasing could certainly use work). I was thinking of statements such as your remark that “An automated proof-checker can identify some correct proofs—but not all of them” whereas we generally don’t call something an automated proof checker unless it terminates on any proof and returns correctly if that’s a valid proof or not in the axiomatic system. Sometimes we insist that this be a primitively recursive process. Sometimes this is also generalizable in a natural way such that the proofchecker can do this given some specific oracle (there are results about how these sorts of things can behave if they have access to a Halting oracle for example. I don’t fully understand these except in vague generality.)
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.