Checking a proof in a recursively axiomatizable theory for correctness is decidable. The post topic programs only check proofs up to some length in, say, Peano arithmetic, which is recursively axiomatizable. Tarski’s undefinability theorem is about complete theories of arithmetic.
There is no such thing as a “complete theory of arithmetic”—see Godel’s incompleteness theorems.
The above statement isn’t true. What Godel’s theorem says is that any effectively generatable theory which is strong enough to model PA is either incomplete or inconsistent. Effectively generatable for our purposes can be taken to mean that valid proofs in the system are enumerable and that there’s a primitive recursive procedure to determine whether a given proof is valid.
If one removes the effectively generatable condition then one can easily produce a complete, consistent system. Consider for example the following system: Consider some lexicographic ordering of well-formed statements in the language of PA, and let S(i) be the ith statement in this list. Let P(0) be PA, and generate P(n) by asking whether S(n) or ~S(n) is a theorem in P(n-1). If so, then set P(n) = P(n-1). If not, then let P(n) be P(n-1) with the additional axiom of S(n). Now, consider P(infinity) defined as the union of all P(n). This theory is complete and consistent but it is very much not effectively generatable since we can’t even recursively enumerate the system’s axioms.
It might help for you to take a model theory or logic course since there are a lot of subtle issues here that you seem to be missing.
I suppose there are complete inconsistent theories of arithmetic. However, here the discussion concerns whether a machine returns 1 - or not. Systems of math that are useless, or have infinitely many axioms and so can’t be implemented don’t really enter into the picture.
Tim, you’re making false statements. You’ve now misapplied both Godel’s theorem and Tarski’s theorem.You also seem to be under the impression that proof checking is not generally doable in an axiomatic system, which is also wrong. Let me suggest that you simply don’t have the background expertise to discuss these issues. These are subtle issues. Indeed, even your above reply runs into new issues (For example having infinitely many axioms doesn’t prevent a system of axioms from being effectively generatable. Indeed many well behaved axiomatic systems have axiom schema which do just this.) You may be running into a Dunning-Kruger type problem. I’m a professional mathematician (ok, a grad student but close enough for this purpose), and I find these issues difficult. Vladimir, I and others have pointed out what is wrong with your reasoning but you don’t seem to be following the explanations. Please take a logic course or read a textbook.
Not every possible set. All you need is a primitive recursive procedure to decide whether a given statement is an axiom, and primitive recursive procedures to check whether each rule of inference is correctly followed in going from one step to another.
Right: automated proof checking is not really “generally doable” in an axiomatic system—how hard it is depends entirely on the axiomatic system under discussion.
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.
Checking a proof in a recursively axiomatizable theory for correctness is decidable. The post topic programs only check proofs up to some length in, say, Peano arithmetic, which is recursively axiomatizable. Tarski’s undefinability theorem is about complete theories of arithmetic.
There is no such thing as a “complete theory of arithmetic”—see Godel’s incompleteness theorems.
The post says it is about “programs”—a fairly general class. Where is Peano arithmetic coming into the issue?
Please give up.
The above statement isn’t true. What Godel’s theorem says is that any effectively generatable theory which is strong enough to model PA is either incomplete or inconsistent. Effectively generatable for our purposes can be taken to mean that valid proofs in the system are enumerable and that there’s a primitive recursive procedure to determine whether a given proof is valid.
If one removes the effectively generatable condition then one can easily produce a complete, consistent system. Consider for example the following system: Consider some lexicographic ordering of well-formed statements in the language of PA, and let S(i) be the ith statement in this list. Let P(0) be PA, and generate P(n) by asking whether S(n) or ~S(n) is a theorem in P(n-1). If so, then set P(n) = P(n-1). If not, then let P(n) be P(n-1) with the additional axiom of S(n). Now, consider P(infinity) defined as the union of all P(n). This theory is complete and consistent but it is very much not effectively generatable since we can’t even recursively enumerate the system’s axioms.
It might help for you to take a model theory or logic course since there are a lot of subtle issues here that you seem to be missing.
I suppose there are complete inconsistent theories of arithmetic. However, here the discussion concerns whether a machine returns 1 - or not. Systems of math that are useless, or have infinitely many axioms and so can’t be implemented don’t really enter into the picture.
Tim, you’re making false statements. You’ve now misapplied both Godel’s theorem and Tarski’s theorem.You also seem to be under the impression that proof checking is not generally doable in an axiomatic system, which is also wrong. Let me suggest that you simply don’t have the background expertise to discuss these issues. These are subtle issues. Indeed, even your above reply runs into new issues (For example having infinitely many axioms doesn’t prevent a system of axioms from being effectively generatable. Indeed many well behaved axiomatic systems have axiom schema which do just this.) You may be running into a Dunning-Kruger type problem. I’m a professional mathematician (ok, a grad student but close enough for this purpose), and I find these issues difficult. Vladimir, I and others have pointed out what is wrong with your reasoning but you don’t seem to be following the explanations. Please take a logic course or read a textbook.
Seconded.
Re: “You also seem to be under the impression that proof checking is not generally doable in an axiomatic system, which is also wrong.”
You are claiming that every possible set of axioms allows for easy automation of proof checking?!?
If so, then we do have a genuine disagreement—and I think you are mistaken.
Not every possible set. All you need is a primitive recursive procedure to decide whether a given statement is an axiom, and primitive recursive procedures to check whether each rule of inference is correctly followed in going from one step to another.
Right: automated proof checking is not really “generally doable” in an axiomatic system—how hard it is depends entirely on the axiomatic system under discussion.
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.
You keep talking with confidence about something you clearly don’t understand at all.