Nitpick(?): His proof was about systems of Peano arithmetic only. He said that he could prove it was true generally, but never did.
Nonetheless, Ultrafilter is correct. If you could prove every statement you could prove a statement and its negation. If you could prove a statement and its negation, then you could prove (using the usual rules of logical inference) every statement.
What Goedel proved is that any axiom system that suffices to define arithmetic cannot be proved complete and consistent. The calculus of simple implication (truth table calculus) is complete and consistent but woefully weak.
By “usual rules”, do you include the law of the excluded middle? It’s my understanding that not everyone accepts that. If the law of the excluded middle is required in order to show <Ultrafilter’s definition> iff <Wikipedia’s definition> then they really aren’t equivalent definitions, are they?
I think he meant first order predicate. I think that’s what most people mean by regular, normal, or usual.
They’re not equivalent in general; as Chronos pointed out, my definition can be used for systems which allow you to prove contradictions. But in the system that 99% of all mathematicians use, they are.
Minor edit : I think you meant our points are now (x,f(x)), and (x+h,f(x+h)). I’m only mentioning because it’s such a great, clear piece that it could be a reference for someone at some point.
You’re right, I goofed. Thanks for the correction.
I think they are equivalent since p & not p ==> False is true even without excluded middle and False ==> q is true in any logic. I suppose you could find a logic sufficiently different that this doesn’t work, but that would be a mighty odd logic.
This(*) is true in any consistent logic (certainly by the Wikipedia definition, since that’s essentially what the Wikipedia definition is). However, we’re looking at what criteria have to be satisfied by a system in order for it to be consistent, so you can’t just make that assumption. If you do, you can show all systems are consistent, even inconsistent ones:
Loop over all possible inconsistent theorems p:
<…show p is true>
<… show (not p) is true>
but p & (not p) is false (by assumption).
end loop
Nope, no inconsistency here…
(*) I have your statement parsed as “(p & not p ==> False) is true, even without excluded middle”. Now, I’m wondering if you meant “(p & not p) ==> (False is true), even without excluded middle”. But in that case, I don’t see how “False is true” follows from “p & not p”.
Ultrafilter when I wrote my original post, I really thought you had just left some words out, and I couldn’t figure out what they were. Now I’m wondering, why even give that definition in the first place, since it’s not always equivalent, it doesn’t match the usual definition of consistent, and it obfuscates the meaning of the term consistent. Is there some reason you prefer that definition to a more typical one?
Because it’s applicable to more general formal systems, and equivalent for the ones with the normal rules. If you think there’s something wrong with that, you should ask about what it means for a function to be continuous.