Gödel guarantees that full-blown theorem provers, even with human guidance, cannot prove all true statements about sufficiently rich systems. 'Sufficiently rich' here just means 'includes Peano arithmetic', and you can find tons of tutorials for doing just that (Church encoding) in even the simplest type systems.
(This bit of pure-mathematics wonkery ignores the substance of jarrett's question, though; one doesn't need the full Gödelian power to observe that a priori theorems that must be verified at compile time can never account for data that are provided only after compilation.)
When I write a program, I don't want it to be just correct (true); I want it to be _provably_ correct; I want to be able to be convinced that it is correct, at least in principle, given enough time and whole specification of the system. Programs which are correct, but not provably so, should not pass code review and might as well be lumped together with those which are wrong. It doesn't matter if you are using a full-blown theorem prover or thinking about the code in your head; Gödel's theorems are not really relevant to programming, even when the code uses deep mathematics.
I'm not sure I agree with "theorems that must be verified at compile time can never account for data that are provided only after compilation". At compile time, you prove the assertion "for every x, the program outputs correct answer for x". Now, you don't know that the user will enter say x=5 at runtime, but since you proved a theorem about _every_ x, this includes x=5. You cannot predict the future (the path that will be taken by the program), but once you prepare for all possible futures, you're safe.
The problem with theorem provers like Adga and Coq is they are brittle to refactoring and thus hard to make changes to an app. Something seeming small can ripple through the whole system.
I hear Idris is more reasonable in this regard and has better general purpose programming properties.
>The problem with theorem provers like Adga and Coq is they are brittle to refactoring and thus hard to make changes to an app. Something seeming small can ripple through the whole system.
I hear Idris is more reasonable in this regard and has better general purpose programming properties.
You can say the same for any strongly typed language, but reality is it's the opposite. If your program has a good design, it's easy to refactor.
> can never account for data that are provided only after compilation
It seems to me they could. Suppose my program depends on external input D. That input could be a file it loads, keyboard input, network input, or anything else. Could I declare that I expect D to have properties P? And then, could the language force me to implement a code path for cases where D does not satisfy P? An example of such a code path would be to print an error message and then terminate the program.
Yes, this is a good point. I hope that what I meant was reasonably clear, but a more precise would have been something like "cannot prove certain assertions about data that are provided only after compilation".
>Gödel guarantees that full-blown theorem provers, even with human guidance, cannot prove all true statements about sufficiently rich systems. 'Sufficiently rich' here just means 'includes Peano arithmetic', and you can find tons of tutorials for doing just that (Church encoding) in even the simplest type systems.
They don't prove theorems. You do this by writing a program.
Sure, but, regardless of agency, human or automated, it is still not possible to prove all true theorems. (The human / automated distinction comes in more sharply in the halting problem, where any potential halting decider will choke on some program that proveably terminates.)
I wonder; have mathematicians found something that they know with every fibre of their being is true, but that they can't prove? And do they then try to prove it in another formal system instead?
Or do these unprovable-but-true facts mostly elude them, since they are operating in a formal system that 'hides' them?
There are a couple of statements that have been proven to be unprovable in the standard axiom set (ZF). The provability of the unprovability of unprovable statements is not guaranteed, but happens to be true for many of the more useful axioms.
The most common is the Axiom of Choice, which if true is incredibly convenient. For example, the Axiom of Choice implies that all Vector Spaces have a basis, which makes linear algebra tractable. Mathematicians generally accept it as true because it's useful and intuitively true, but it does have some consequences that are intuitively false, like the Banach-Tarski paradox. We even have a saying: "The Axiom of Choice is obviously true, the Well-Ordering Principle is obviously false, and Zorn's Lemma no one even knows." The implicit punchline being, these three things are logically equivalent because each implies the other.
Other axioms that are independent of ZF include the Continuum Hypothesis and the Axiom of Foundation. The Continuum Hypothesis says that there is no type of infinity that is larger than the cardinality of the Rationals and also smaller than the cardinality of the Reals. It doesn't make a damn lick of sense for such a type of infinity to exist, but it's not technically possible to disprove it. The Axiom of Foundation, in very simple terms, disallows objects like "the set that contains itself." Such sets are not constructable in ZF, and are logically impossible, but they are not technically disallowed.
Using "stronger" axiom sets to investigate the properties and consequences of these unprovable statements is common. Additionally, many automated theorem-provers include several of the more convenient axioms that aren't included in "regular" mathematics.
(Note: ZFC is ZF plus the Axiom of Choice; Choice is so damn convenient that the mathematics establishment usually accepts it by default, although proving that you don't need Choice to prove something is often seen as a worthwhile accomplishment.)
Mathematicians say that formula F is true in system S iff one can find a proof of F in the context S. So truthness is always considered with respect to some system.
Thus, there are no formula which is "true" but that one can't prove, by definition. (That's the kind of smartassery mathematicians like.)
But the Godel's incompleteness theorem states that for all system that includes (Peano's) arithmetic, one can find a formula in this system that has cannot be proved and whose contrary cannot be proved either. And to answer your question, Godel's proof explicitly shows such a formula.
Words in mathematics mean what they are defined to mean, so there's no point arguing about the correctness of definitions. Yours is essentially the constructivist perspective on truth; but it is not the only one. It will declare that certain statements are neither true nor false, which some find distasteful.
A more model-theoretic approach says that a formula is true in a theory (not a system, although the word choice doesn't matter) if it is true in all models of that theory—a statement that can (in principle) be concretely verified simply by testing in each such model. Then it may (and will) be true that a statement is true in "all possible worlds", but that there is no way of proving it from the rules that constrain 'possibility'.
(This bit of pure-mathematics wonkery ignores the substance of jarrett's question, though; one doesn't need the full Gödelian power to observe that a priori theorems that must be verified at compile time can never account for data that are provided only after compilation.)