Godel's Incompleteness Theorems vs Justified True Belief
I'm working from a very limited understanding of both math and philosophy so kindly bear with me.
[quote=Wikipedia]The first Godel incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an effective procedure (i.e., an algorithm) is capable of proving all truths about the arithmetic of natural numbers. For any such consistent formal system, there will always be statements about natural numbers that are true, but that are unprovable within the system. The second incompleteness theorem, an extension of the first, shows that the system cannot demonstrate its own consistency.[/quote]
Please note the highlighted section in the above quote: "true, but that are unprovable".
Justified True Belief (JTB) : Knowledge of proposition P = P is true, P is justified and you believe P.
The part of the JTB I want to draw your attention to is justification. If we are to say a proposition P is true then it has to be justified. Justification becomes rigorous in deductive logic, mathematics is entirely deductive in character, and is then called proof.
In mathematics if a proposition P can't be proven then P is neither true nor false. I guess this agrees with the philosophical JTB principle too.
How is it then that a statement like (refer highlighted section of quote above): "true, but that are unprovable" occur in Godel's incompleteness theorem.
To clarify, suppose it's the mathematical proposition T that's true but unprovable in a given mathematical axiomatic system. If it's unprovable then it's truth value is neither true nor false. How can it be that T is true then?
Isn't true but unprovable a contradiction?
Comments...
[quote=Wikipedia]The first Godel incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an effective procedure (i.e., an algorithm) is capable of proving all truths about the arithmetic of natural numbers. For any such consistent formal system, there will always be statements about natural numbers that are true, but that are unprovable within the system. The second incompleteness theorem, an extension of the first, shows that the system cannot demonstrate its own consistency.[/quote]
Please note the highlighted section in the above quote: "true, but that are unprovable".
Justified True Belief (JTB) : Knowledge of proposition P = P is true, P is justified and you believe P.
The part of the JTB I want to draw your attention to is justification. If we are to say a proposition P is true then it has to be justified. Justification becomes rigorous in deductive logic, mathematics is entirely deductive in character, and is then called proof.
In mathematics if a proposition P can't be proven then P is neither true nor false. I guess this agrees with the philosophical JTB principle too.
How is it then that a statement like (refer highlighted section of quote above): "true, but that are unprovable" occur in Godel's incompleteness theorem.
To clarify, suppose it's the mathematical proposition T that's true but unprovable in a given mathematical axiomatic system. If it's unprovable then it's truth value is neither true nor false. How can it be that T is true then?
Isn't true but unprovable a contradiction?
Comments...
Comments (182)
If no counter-examples are found, and no proof is presented, then the justification is not perfect, but accepted as true.
For instance, if you substract a positive number from a larger positive number, you get a positive number. There is no proof for this, despite it ensuing from mathematical axioms. No proof, but then again, nobody can find a counter-example for it, either.
a > b > 0
a > b
a - b > b - b
a - b > 0
Anyway
You made an interesting point here viz. but I want to ask you a question:
How do you know that a proposition P is true?
You need to justify P i.e. provide a logical argument to show that P is true.
How else are you doing philosophy or math or science or even just living?
This is at odds with Godel's claim that there exist propositions in math, say P, that are true but unprovable. How do you know P is true when you didn't prove it to be true? That's my question.
You provided a route out of what I think is a problem viz. that there are no counterexamples. As attractive and comforting as this sounds it's not the way I see mathematical theorems being proved. At best a theorem that doesn't have a counterexample is considered a conjecture that is likely to be true. It seems your method is central to scientific thinking (falsificationism) and you already know that scientific "truths" are provisional - assumed to be true but not for certain. However, math is different. I've never heard of theorems that are provisionally true and I'm reasonably sure that Godel's theorems are deductive in character and so excludes such a method as yours.
If nothing else, we'll die our hair when we get old enough. (-:
Truth or something being true can be accepted as such, even if not proven, if no counter-examples are given. In the above example, no counter-example is given to your being alive. Yet you know you will not live forever. Despite the lack of proof, and despite the lack of counter-examples. (Others' deaths are not yours; they are only people or things SIMILAR to you, but not quite you, so dead people's examples are, strictly speaking, not counter examples to your immortality.)
Nice proof, by the way, of my "theorem". Haha. You finished me off in a flash. But as a mathematician, using Google, you can surely find examples of stuff on the Internet where a theorem is not proven, but true... the only reason being for accepting it as true, is the lack of counter-examples that prove it wrong.
I can't say much else about this... you insist that for truth, the only valid criteria is a proof, esp. in mathematics. Some others think differently, and that's something I can't force you to accept, to think like them... or like us, since I am with "them" (whoever "they" are). And that, for the umpteenth time, is, that lack of counter-examples constitute a reason believe that something is true, or justified in belief.
I'm familiar with the term, counterexample, in the context of logic. It's used as a method to prove invalidity of arguments. Another area where counterexamples show up is in science - the disconfirming observation.
I must agree with you that counterexamples are used in math too but do notice the word itself - counterexample - indicating that it's an instance/example that opposes a claim or theorem/proposition.
So, given the meaning of the word, counterexamples obviously disprove some claim. I mean it's primary use is as a method of disproof and not proof. Although using counterexamples, specifically an absence of them, to prove a proposition, like you're claiming, looks quite attractive, I don't think it's the standard approach to mathematical proofs. If you disagree still, kindly furnish a counterexample that disproves that.
I think there's a solid reason why counterexamples aren't used in proofs. Consider a proposition P. P can either be true or false. Suppose no one has found a proof for P being true. Also suppose that P has no counterexample. The logical conclusion should be that P hasn't been proved either true or false - yes there is this option which you're missing. To assume P as true, which you're claiming should be done. would be committing the fallacy of argument from ignorance - P hasn't been disproved. Ergo, mistakenly, claiming P is true.
Please note that the counterexample method is used in science where all claims are provisional, subject to change/deletion as soon as a counterexample occurs. However, don't forget that in science we need confirmatory evidence too. For example the theory of relativity is true not just because there are no counterexamples but also because it's been confirmed by many other observations. As you can see counterexamples are used mainly for disproving and not proving.
Thanks for your valuable comments.
Quoting TheMadFool
An important condition to incompleteness theorem is the axiomatic system is strong enough to do arithmetic.
The concept of complete is that every true statement that can be expressed in the system can be provable. The concept of consistent is simply that there are no contradictions.
The axiom of P = P forms a system of a single axiom where the only statement understandable to the system is P = P which doesn't contradict P = P, so it's complete and consistent.
Incompleteness theorem doesn't create doubts about things like P = P, and even adding a few more rules about P doesn't necessarily run into incompleteness theorem.
Enough rules to do arithmatic are needed.
Once arithmatic is possible, statements understandable to the system can also be statements about the system.
How this is possible is because all statements can be encoded as a number and rules about arithmatic describe numbers and what can be done with them.
Armed with this, it's then possible (in a completely proper mathematical way, not just conceptually) to make statements such as "This theorem is unprovable" and then show we can't prove that theorem with the axiom. But it's a true statements!!! We know it's true because we proved that it's unprovable, there's just no axiomatic way to prove it.
Without getting technical, I hope this gives some key intuitions as to what's going on.
Why this theorem was so important, is because before incompleteness theorem, mathematicians were looking for the "one true system", a system of rules about numbers from which all true statements about numbers can be proven and no contradictions arise.
The "no system of arithmetic can prove it's own consistency" part is, for me anyways, much more abstract relevance, I'm not sure there's some key intuitions about it.
Quoting alcontali
Indeed. I sensed that there wasn't the required level of correspondence between Godel's incompleteness theorems (GIT) and the justified true belief (JTB) of philosophy. The shared characteristic between the two I was hoping to emphasize was the need for proof to establish truth. As you can see I'm under the impression that the only way to claim truth in mathematics is by proof. Hence my puzzlement when "true, but unprovable" cropped up in GIT.
Can you tell me more about Quoting alcontali?
My logic:
If a proposition P is true then necessarily that a proof must exist for P being true.
Mx = x is a mathematical proposition
Px = x has a proof
t = mathematical proposition that Godel says is true BUT not provable.
Mt = t is a mathematical theorem
~Pt = not the case that t has a proof
1. Ax(Mx > Px)....premise
2. Mt.......premise
3. ~Pt......premise
4. Mt > Pt.......1 UI
5. Pt...........2, 4 MP
6. Pt & ~Pt....contradiction
As you can see I have to reject one or all of the three propositions 1, 2, or 3.
This is the premise you need to abandon.
There can be true statements that have no proof. Incompleteness shows us an example.
There can also be just "true facts" about numbers and arithmetic that are true and there's simply no proof possible.
For instance, the Collatz conjecture we may simply never be able to prove is true, false, or even undecidable, it just stays unknown (beyond what we can check through computer calculation, which wikipedia says we've done to 87 * 2^60 which seems impressible is minuscule compared to "all numbers"). I.e. it can be "true" but also true that no proof nor proving it's undecidable is possible; some things that "resist refutation" can potentially just stay a big question mark indefinitely. The halting problem is a related concept.
Thanks a lot. I remember quite vaguely that self-reference or the liar paradox has something to do with Godel's theorem.
Please note the underlined part of your quote.
If "this theorem T is unprovable" is proof, as you say, then doesn't that mean it's provable after all and that too within the axiomatic system?
How do you go from "this theorem is unprovable" to "this theorem is true but unprovable"?
How did Godel know that "this" theorem was true?
Yes (that's a good question) and why the phrases "inside and outside the system" come up.
"Inside the system" the theorem isn't provable, there's no problem; the axioms are content to just leave it at that. It's only us outside the system that we realize that if the system can't deal with that statement, then that statement is actually true.
It's basically the liar paradox but there are two different systems to evaluate the theorem, whereas the liar paradox is fully "in our minds" and we can't look at it "outside the system it's expressed in".
So, "within the system" we can follow Godels axioms and statements to arrive at a completely proper conclusion. We need to use reasoning "outside the system" (that are not based on the axioms of the system) to arrive at the conclusion the statement is actually true. We can't do this with the liar paradox and so cannot do a similar thing to conclude it's actually true, as if it's true then it's false; incompleteness is a version of this idea that somehow works out due to these nuances of building it in a system that is smaller and weaker than our own minds and these nuances of "unprovable" doesn't necessarily mean "false"; so saying that statement is "actually true" doesn't make a contradiction with the truth value within the system which just says "unknown (as far as these axioms are concerned)"; i.e. if I say "I don't know if it's raining outside" isn't contradicted by you coming and saying "it's raining".
True things without justification.
Kinda the same thing.
I watched a video on Godel's theorem. A very simple argument and I think you're on the right track with your explanation.
Basically, every new theorem "proved" by Godel's method may be added to the original axioms creating a new axiomatic system. This new system itself is susceptible to the same problem and we have an infinite regress.
In the Godel statement "This statement is true but unprovable what does "this" refer to? To me "this" looks like a placeholder for theorems that satisfy the Godel condition of true but unprovable or is it that "this" refers to the statment "this statement is true but unprovable"?
If "this" refers to a particular theorem T then we get "Theorem T is true but unprovabl" which is a proof and still inside the axiomatic system that generated the statement.
IF "this" refers to the statement itself: "this statement is true but unprovable" then it doesn't make sense because "this statement is true but unprovable" is NOT a mathematical proposition.
Thanks again.
I'll have to delve deeper to understand Godel. Thanks for good advice :rofl:
Proof does not establish truth, it establishes justification. However, since mathematics is the science of drawing necessary conclusions about hypothetical states of affairs (Peirce), there is a sense in which mathematical justification is equivalent to mathematical truth. A sentence is "true" within a consistent formal system as long as it does not contradict the underlying assumptions (axioms). A sentence is "undecidable" within that same system if it can neither be proved nor disproved on the basis of those particular axioms.
What Gödel proved is that it is possible to formulate an "undecidable" sentence within any sufficiently powerful formal system. However, there are still many formal systems--include standard first-order propositional and predicate logic--that are both consistent and complete, such that it is not possible to formulate an "undecidable" sentence within them.
As I have pointed out in other threads, classical logic does not require proof to establish truth, which is why "proof" by contradiction (reductio ad absurdum) is allowed. By contrast, constructive systems such as intuitionistic logic do require positive proof, such that the Law of Excluded Middle (every proposition is either true or false) does not apply.
So it stands to be proven or to find counter-examples that prove it wrong.
Therefore your objection or criticism (how can you know what's not proven) hinges upon the truth of Godel's theorem, which FIRST needs to be proven or else counter examples need to be found to disprove it, BEFORE your criticism could find validation.
"I can't prove this, but you can accept it as truth, that things can be accepted as truth without a supporting proof."
There, you have it. If you accept it, you accept all similarly stated truths; if you don't accept it, then it is self-evident that it isn't true. But acceptance and non- both depend on an individual's autonomous choice, as the theorem is still a theorem, no proof or counter-example has been presented yet.
No, it is called a theorem because Gödel provided a proof; otherwise, it would be called a hypothesis or conjecture. Fermat's conjecture came to be known as a theorem because he claimed to have a proof, which no one ever found; Andrew Wiles finally came up with one in 1994.
Oops, I screwed up big time. I was sure theorems were unproven theories. My ignorance. Totally.
But now I KNOW the meaning of the expression "Theorem".
Thanks, @aletheist.
By-the-by: what does your moniker mean?
Thanks for asking. The Greek word for "truth" is transliterated aletheia, so I call myself "aletheist" because I believe that there is such a thing as (absolute) truth.
Noble conviction you have.
Now, go out and find it!!!
(Hehehe)
Transliterated from the actual Greek work ???????.
Quoting god must be atheist
Thanks; but then, the denial that there is such a thing as (absolute) truth is self-refuting.
Funny thing is humans first envisioned they have the truth about the material world, but solipsism and many of its sub branches destroyed that hypothesis. So the first one we took for granted was the first one we took as unprovable.
The second thing we envisioned as being true are tautisms, logical proofs, math proofs. Then we realized they rest on axioms and have nothing to do with the physical world, despite math's and logic's original uses, that made the physical world be understood better.
Then came quantum mechanics that destroyed by stating counter examples to them, our faith in the tenets of intuitive logic.
So now we are here, not trusting our senses, not trusting our sensibilities, not trusting our intuition.
Whew! What a relief. Thanks. You have a nice n superb command of English. And you know how to use a computer for more things than the mainstream. I mean, to get to the Greek keyboard and type actual words is a bit more complex than sending cute cat pictures on the Internet (by females) or sending magnificent pictures of people's own genitals (by males).
aletheist claims that proofs are sufficient but not necessary for truth.
god must be atheist claims that that truth can be based on the absence of counterexamples.
Where do the two of you stand on each other's claims? Thanks.
I would say it's the toes.
But seriously speaking, other things are necessary than just the lack of known counterexamples. So I say this is a false assessement of my stand, please disregard the quote by @TheMadFool that attributes this to me.
Now I am not confident that @aletheist claim is properly written, either.
So I refuse to make a statement on a potential Strawman.
You are still conflating justification with truth, and consequently ascribing views to both of us that we did not state and do not hold.
Quoting aletheist
Proofs are sufficient, but not necessary, for justification.
Quoting god must be atheist
Justification can be based on the absence of counterexamples.
I tentatively agree with aletheist on what he said in this last post above this one of mine.
Excellent, and I agree with you that justification can be based on the absence of counterexamples. It is what Charles Sanders Peirce called "crude induction," describing it as the "weakest kind of inductive reasoning" and "the only kind of induction that is capable of inferring the truth of what, in logic, is termed a universal proposition." Its chief virtue is that it is readily self-correcting, because it only takes one counterexample. The paradigm case is "all swans are white," which was a justified belief of Europeans for centuries, but turned out not to be true.
Do you think justification is necessary for truth?
Sorry. Thanks.
You say that if a claim doesn't have a counterexample it can be taken as proof.
That's the fallacy of the argument from ignorance. There's a third option between true and false which is "I don't know".
No, justification is about why someone believes a proposition, while truth is about whether that proposition represents reality. Besides, if justification were necessary for truth, then only justified beliefs could be true, which is not the case.
Quoting TheMadFool
No, he did not say that, either. He said that an absence of counterexamples can be taken as justification for a belief; proof is a stronger form of justification.
Can you name one unjustified truth?
Lots of people believe things without justification that happen to be true. That is why the standard modern definition of knowledge is justified true belief, not merely true belief.
Basically, what we thought we "knew" turns out to be just part of a spectrum or continuum. Spectrums are not thin lines but more like a solid cheese with textures. Nuancing science is what mostly happens, rather than "revolutions" or even "falsifying" (unless the proposition had been very narrow).
So, knowing and believing are not as dodgy as we might fear, provided we are respectful of their complexity.
I think the subtlety and slight but not excessive looseness in all this is refreshingly hard-nosed. I've always intuited this, I think the family and my teachers always accepted something like this.
It's tragic how often the "great" and the "good" deny that the middle needn't be excluded when it doesn't contradict the law of non-contradiction.
I read in Knowles that Anselm (and I type from memory) translated "necessarius" as "admissible" and not "compelling". (However he spoiled everything by attempting a so-called "ontological proof" which I am told Descartes swallowed.)
This is truly a great observation although I was hoping the theories themselves constituted subtleties that are missed by the novice like me. However, you meant something else - the progress of science and how it's made of small drifts rather than major shifts. Am I correct? Kindly clarify.
Quoting Fine Doubter
Did Anselm use "necessarius" in a logical context? Did he make a mistake?
:up: :ok: Thanks
1 - I am sure all theories contain subtleties which however are not beyond our faculties to contemplate as we help each other along. The other thing is, "falsification" and "revolutions" in the rather weak sense might not happen for several generations. It looks silly for some people to crow that they have "ruled out" something that was the all-the-rage hypothesis a few years ago, when in 200 years time they will have arrived at a far more compendious halfway house. (I except the so called "many worlds" which in fact didn't make sense, all along, so I am not really excepting it - a thread of its own.)
2 - I haven't been reading Anselm, this was alluded to in passing by Knowles, 'The evolution of medieval thought'. But I don't think Anselm made a mistake - although some of his contemporaries perhaps gave it a little stronger meaning - and perhaps not much stronger (again my feeling from secondary sources). I think it is very important for us moderns to realise when we don't need to be quite so categorically categorical. I think of reality as one of those old ships that flexes and creaks - and sails. Not as a Titanic that cracks up (without us noticing). Principles are there for the apply-ing. Perhaps "necessarius" means "the rule" and a word for contingent would mean something like occasional and quasi-random. The two are of course on a continuum and might even sometimes coincide, in my opinion. I think it is vital to remember that there are two kinds of probability - both occurrences, and our knowledge of them. I think of reality as being on the non-approximate side of approximation.
3 - An interesting thing about Gödel indeed is that what he describes as "proof" can reputedly sometimes occur without help from an outside system, however it rather often does require input from outside. I really adore ifs and I really adore buts - I think they are so firm and reliable.
Me too. :joke:
There is something very syntactic about the proof. The starting point is the diagonal lemma, which says:
Lemma:
For each formula F with one free variable in the theory T, there exists a sentence ? such that:
? ? F(°#(?))
is provable in T.
If we now look at the provability function B(x) which accepts the encoding of any sentence and returns yes/no if it is provable, we can see that it has a strange "corner case". By choosing F(x)=~B(x), we obtain the following proposition:
? ? ~B(°#(?)) is provable in T
The sentence ? is not provable in T, because that is exactly what the expression says. So, this "corner case" sentence is true. This issue is caused by the diagonal lemma, which insists that each one-variable formula in the theory must have a fixed point.
The proof for the diagonal lemma itself is also purely syntactic. It is the result of just symbol manipulation. The final result may give a semantic impression, but Gödel's theorem is also purely syntactic.
Like "Colorless green ideas sleep furiously"? No meaning? I though proofs need to be meaningful.
The justification has to be purely syntactic. I am currently still looking into what it means for alternative functions F(x):
? ? F(°#(?)) is provable in T
Since it should work for any function F(x), I think that the secret to a proper interpretation of this lemma can be found by looking at alternative choices for F(x). The following stackexchange question also asks for alternative examples, but I find the answers not particularly satisfactory. Maybe there are better links for this?
That a proposition is true means you have a proof that demonstrates that proposition to be true and unprovable means you don't have a proof. :confused: :chin:
No. Consider Goldbach's conjecture(GC):Every even integer greater than 2 can be expressed as the sum of two primes.
GC may be true even if it cannot be proven true. If true, and unprovable, it is unknowable.
Important clause.
There's a difference between "can be true" and "is true". Godel statements are not of the "can be true" type, they're of the "is true" type. The transition from "can be true" to "is true" is done via justification aka proof. That's the usual procedure anyway.
A fairly decent layman's guide I think, if anyone is interested.
The problem is this: if I can't prove a proposition in a given system x, that proposition can't belong to that system. Proof of a proposition is a precondition for inclusion in a system. Ergo, no Godel sentence for system x, since it can't be proved in x, can be part of the system x. For instance I can't prove anything about quantum physics in the system of theism, so, how can anything about quantum physics be part of theism?
I can form the grammatically correct sentence "the uncertainty principle is true" with words that occur in theism in statements like " it is true there's no uncertainty regarding god's existence", "god commands us to live by the moral principles he laid out". The uncertainty principle is a fact in quantum physics, a totally different system to theism and insofar as theism is concerned, the sentence "the uncertainty principle is true" is meaningless.
Could all Godel sentences be of such kind, syntactically sound but semantically empty? If yes then Godel's incompleteness is "harmless" to mathematics because Godel sentences are meaningless gibberish spoken with perfect grammar.
That's not true.Goldbach's Conjecture is not "semantically empty": all the terms and relations are well defined (prime number, even number, sum). If true and unprovable, it is because the formal system of peano arithmetic is incomplete. That's what Godel's incompleteness theorem is all about: incompleteness = there are unprovable true statements in the formal system.
Quoting TheMadFool
Godel's Incompleteness theorem is about formal mathematical systems. It has no metaphysical implications. Similary, the uncertainty principle of Quantum Mechanics has no relation to the uncertainty various metaphysical claims.
I must confess that I didn't understand the proof in the link but one thing stood out: the proof in the link made the following contradictory claims:
[quote=Quanta article]The mapping works because no two formulas will ever end up with the same Gödel number.[/quote]
and
[quote=Quanta article]“The formula with Gödel number sub(y, y, 17) cannot be proved” — is sure to translate into a formula with a unique Gödel number. Let’s call it n.
Now, one last round of substitution: Gödel creates a new formula by substituting the number n anywhere there’s a y in the previous formula. His new formula reads, “The formula with Gödel number sub(n, n, 17) cannot be proved.” Let’s call this new formula G.
Naturally, G has a Gödel number. What’s its value? Lo and behold, it must be sub(n, n, 17). By definition, sub(n, n, 17) is the Gödel number of the formula that results from taking the formula with Gödel number n and substituting n anywhere there’s a symbol with Gödel number 17. And G is exactly this formula! Because of the uniqueness of prime factorization, we now see that the formula G is talking about is none other than G itself.[/quote]
1. There's a formula with Godel number sub(n, n, 17)
AND
2. The Godel number for "the formula with Godel number sub(n, n, 17) cannot be proved" is also sub(n, n, 17)
It's like the Godel number critical to the proof is ambiguous and, from the rudimentary math I know, Godel numbering is then not a function. How this impacts Godel's proof? I have no idea.
:chin:
One choice leads to understanding. The other, to psychoceramics.
Quoting tim wood
The issue is simple: Godel claims any given axiomatic mathematical system is incomplete because there's always going to be a mathematical proposition that's both
1. true
AND
2. unprovable in the system.
I want to know how a proposition can be true sans any justification. The normal, standard procedure when it comes to assigning truth values is to offer proof but Godel is quite clear on the unprovable nature of Godel sentences.
Then tim wood said: Quoting tim wood
This, however, is incorrect. All articles on Godel's theorems only mention adding Godel sentences as axioms to the axiomatic system they render incomplete. Nowhere is it mentioned that they're "provable outside the system".
:chin:
Sure; you can't see how the argument works.
My question is, what do you do next? Do you re-read and study and find alternate presentations, until you see how the argument works; or do you conclude that all the mathematicians and logicians up to you are wrong?
Quoting Banno
I'm asking a simple question and no satisfactory answer has been offered by forum members.
I hope this dogged persistence on my part is only a minor irritation to you all.
First, let's get the facts straight:
Kinds of mathematical truths:
1. Axioms (assumed)
2. Theorems (proven from the axioms)
Godel sentences, if you don't know what they are, are sentences like "this mathematical statement is true but unprovable in a given axiomatic system".
As you can see, Godel sentences are neither axioms nor theorems which leads me to believe they aren't mathematical truths at all unless...there's a third category of mathematical truth. If yes what is this third kind of mathematical truth?
Last but not least, Godel admits that his method of proof has a connection with the Liar Paradox which, to me, should set the alarm bells ringing.
The answer was given back here:
You missed it or misunderstood it.
SO, again, what will you conclude?
It is not easy to wrap your head around this. I sort of understand it, but still struggle with it.
I can recommend two sources which might help you.
First, get a hold of Godel, Escher and Bach by Douglas Hofstadter. it's a great read in of itself with all sorts of very cool insights.
Next, you might want to check this out: https://www.youtube.com/watch?v=GbtNQ7yzo9Y&feature=youtu.be
The example here is analogous to Godel - well sort of.
@tim wood @EricH
Simply put, there appears to be a contradiction in Godel's proof.
Try using the phrase "true BUT unprovable" in any other topic of discussion, and don't forget philosophical discourse, and see what response you get from your audience.
For instance if I say the proposition "God exists" is "true BUT unprovable" you would think I'm an idiot or insane or both or something even worse for the simple reason that truth of propositions mandates proofs; I can't say a proposition P is true without a proof, no? To understand what I mean you need look no further than Godel himself; after all, he did prove his incompleteness theorems didn't he? How come then that when Godel slips in a claim that contradicts the very principle that he assumes by attempting to prove his theorem viz. making the statement "true but not provable", everyone seems to ignore it?
And again, what will you conclude?
That's a different issue. Of course, the chances are next to zero that the entire mathematical community is wrong about the truth of Godel's theorems.
Nevertheless, I'd like to know their reactions to the following make-believe conversation between lowly me and the great Kurt Godel:
Me: Godel's incompleteness thoerems are false. There exists a mathematical axiomatic system that's both complete and consistent. Let's call this last statement of mine S.
Godel: Prove it.
Me: Just like Godel sentences that state things like "this mathematical proposition is true but unprovable" are, well, true but unprovable, my statement S is also true but unprovable.
Godel: But I proved the existence of Godel sentences
Me: So, proof is necessary to establish truth?
Godel: Yes
Me: Then explain how, in a Godel sentence that claims "this mathematical proposition is true but unprovable", the mathematical proposition being considered is true.
Godel:
Explain this statement.
Quoting boethius
I've argued as much elsewhere. Being true is not the same as being proven, justified, or believed
Let me ask you another question... can "This statement is not proven" be false?
Start by assuming that it has been proven...
Then consider what happens when it is assume to be false.
Proof is both necessary and sufficient for truth unless we're talking about postulates/axioms. Godel's theorems are missing the proof that is both necessary and sufficient to prove Godel sentences.
Yes, "this statement is not proven" can be false. Ok, I assumed that it has been proven. Now I consider what happens if it is assumed to be false. We'll arrive at a contradiction. So?
So, you don't mind if I say that it's true that you're the robber that carried out the bank heist last Wednesday but that that's not provable?
So, you are right, and mathematics is wrong.
Then your name is most apt.
...then there is a proof, and it is true.
The only option is to conclude that it is true and hence not proven.
Hence, being proven and being true are not the very same.
Being true is not the same as being proven, justified or believed.
No, I'm not claiming that I'm right. What I'm bothered by is the contradiction that takes the following form in Godel's theorems:
1. Godel deems proofs necessary to establish truth because he puts forth a "proof" for his theorems
2. Godel sentences are of the form "this statement is true but unprovable" which implies that proofs are not necessary to establish truth because "this statement" is true but unprovable
1 & 2 = Proofs are necessary & Proofs are unnecessary
Godel is contradicting himself.
This is only a side issue though. The main problem is the statement "true but unprovable". This is self-contradictory
This is partially correct but only in the domain of induction, not deduction and math is completely deductive - if the premises are true and the argument is valid, it's impossible for the conclusion to be false. Ergo, being proven in math implies and is implied by truth.
So there it stands, you have the issue, the solution and the choice.
Quoting TheMadFool
Please, reconsider. It can only be true.
In deductive logic, that includes math, true if and only if proven.
OK, let's try something a little bit more complex. informally:
"this statement is not proven" can be provided with and equivalent well-formed formula in the system that Godel constructed.
It cannot be proven within that system
But if you peruse it again, you will see that it cannot be false.
Here's the proof: If it is false, then there is a proof and it must be true, which would be a contradiction. IF it is true, there is no contradiction Hence, it is true.
Now that proof lies outside of the system constructed by Godel.
How's that?
Edit: you have your proof that "this statement is not proven" is true; and a proof that any system of sufficient complexity is either incomplete or inconsistent.
Things are beginning to clear up for me. Thanks.
Your argument above according to me is:
G (Godel sentence) = this mathematical statement (Godel number xyz) is not provable. For the moment let's forget the truth claim.
Now assume P = there's a proof of G. Then...
1. If P then G
2. if G then ~P [because G claims it can't be proven]
3. If P then ~P......1, 2 HS
4. P.......assume for reductio ad absurdum
5. ~P....3, 4 MP
6. P & ~P.....4, 5 Conj
7.~P.....4 to 6 reductio ad absurdum
~P = there's no proof for G and so G is true and G states that there's a mathematical statement (Godel number xyz) that's not provable: Godel's first incompleteness theorem there. Is this correct?
:ok: Thanks
P = there's a proof of G
G (Godel sentence) = the mathematical statement with Godel number xyz is unprovable
1. ~G > P (if G is false then P is true)
2. P > G (if P is true then G is true)
3. G > ~P (if G is true then P is false)
4. ~G....assume for reductio ad absurdum
5. P......1, 4 MP
6. ~G > G.....1, 2 HS
7. ~G > ~P....3, 6 HS
8. ~P........4, 7 MP
9. P & ~P....5, 8 Conj
10. G.....4 to 9 reductio ad absurdum
No need to acknowledge this post unless you see errors.
s
Suppose G = the mathematical statement with Godel number xyz is unprovable. Notice that the mathematical statement with Godel number xyz is essentially a free variable and ALL mathematical statements that have a Godel number, and that includes all of mathematics, can be assigned to it. Basically G = the X is unprovable, and X can take on values from the entirety of mathematics. That mean your argument "proves" all mathematical statements that can be reduced to a Godel number, and that's all of mathematics, are unprovable.
There has to be another constraint on the proof that restricts the variable X to those mathematical statements that actually are true but unprovable within a given axiomatic statement.
All this is on the fly so, bear with me. I'm hoping to stagger through this like a drunk and hopefully bump into the truth. If you have the patience, indulge me.
Quoting TheMadFool
I ignored this error before, for the sake of getting to the main point. Each and every statement in mathematics has a Godel number. What you are calling a Godel statement is equivalent to one particular such number - to to all of them.
Yet it isn't equivalent to Liar Paradox or perhaps in this case to Russell's paradox. This is something that some writers erroneously think. The self refence doens't fall into a vicious circle (as Russell put it), even if there's a statement / Gödel number referring to a Gödel number.
It might have gotten lost in the shuffle, so I'll repeat my suggestions
First, get a hold of Godel, Escher and Bach by Douglas Hofstadter. Besides giving (in my opinion) one of the best explanations of Godel, it's a very entertaining read in of itself with all sorts of very cool insights.
Next, you might want to check this out: https://www.youtube.com/watch?v=GbtNQ7yzo9Y&feature=youtu.be
This explains the technique behind Godel in totally non-mathematical terms.
1. There is a God
2. String theory
Things that are true but aren't provable: { } or not?
A simple scenario:
It's true that this roller coaster, the one you want to ride on, is safe but it's my duty as the one in charge of this roller coaster to inform you that no one has ever proved that this ride is, in fact, safe.
Would you ride this roller coaster?
Did the esteemed Kurt Godel prove the statement: this [mathematical] statement is true but unprovable?
(1) We say that a theory is recursively axiomatized if there is an algorithm which tells us whether or not a given formula is an axiom of the theory, i.e. you input a formula and the algorithm prints YES or NO if the formula is an axiom or is not an axiom, respectively. By a long, tedious process of coding, Gödel was able to show that in the case of such theories, whether or not a sequence of formulas is a proof is also checkable by an algorithm. This implies that all there is another algorithm which prints all the theorems of the theory in a sequence, i.e. there is an algorithm that enumerates the theorems of the theory (the algorithm in question is horrid, by the way). In other words, the theorems of such a theory are computably enumerable. Now, there is another theorem that roughly shows that computably enumerable predicates are definable in PA by a formula with just one existential quantifier. So, in particular, the predicate "x is a theorem of T" is definable in PA for any recursively axiomatized theory T.
(2) But Tarski also showed that being a true formula of PA is not definable in PA by any formula, let alone one with just one existential quantifier. The idea is very roughly as follows: if truth were definable in PA, since PA allows for self-referential predicates, a version of the liar paradox would be replicated inside PA. But then PA would be inconsistent. So truth is not so definable.
Putting these together, we obtain the following: (1) Being provable is definable in PA, but (2) being true is not definable in PA. On the other hand, we have (3) if something is provable, then it is true. Hence, since, by (1) and (2), being provable and being true are different, and, by (3), everything that is provable is true, we have that there must be something that is true without being provable. In other words, PA is incomplete.
This version is better than the one originally presented by Gödel because it deals directly with intrinsic properties of the predicates of being a theorem and being a true formula, i.e. properties that are not relative to any system (this stems from the rather astonishing fact that the notion of algorithm is system-independent). So it avoids retorts of the sort "but we just prove [whatever] in a higher system".
It's not an interesting retort anyway, because if a formula is true but not provable, we can just make it an axiom in a higher system, so it would be trivially provable.
Thanks.
But, in deductive logic, math included, proof guarantees truth. Ergo, being true doesn't need to be defined separately - it's redundant. Also, proof of a proposition is necessary to claim that that proposition is true. In other words a proposition is true IFF that proposition has a proof unless the proposition is an axiom.
You keep saying this as if it was self-evident. Now, if you'd never before encountered this problematic, never had anyone contradict you, it wouldn't be unreasonable to say this. But after ten months and four pages of discussion a thinking person would begin to suspect that the question might not be so straightforward...
Does this observation apply exclusively to TheMadFool or does it also range over others?
Also, no one answered my rollercoaster question.
Does it matter? Do you hold your intelligence contintgent on the intelligence of people you are arguing with?
Ok. It shouldn't matter but I feel bad when people accuse me of something which they themselves are guilty of.
All the time!
The rules of math were designed by human beings, so don't we design the proof and the truth if we are the designers of the system? What is the proof and truth of how to spell the word, "cat"? Humans didn't design the universe therefore truth and proof of some state of the universe will be difficult to come by however humans did design the means to represent and communicate our experiences of the universe, so any truth or proof would be inherent in the rules we've dictated.
Unfortunately, from the fact that provability is sufficient for truth, it does not follow that it is necessary for truth (in general, being a sufficient condition is not, well, sufficient for being a necessary condition). But truth would be redundant only if provability were sufficient and necessary for truth. Gödel's theorem, in the particular form I mentioned in my previous post, shows, however, that provability is not necessary for truth. So you must revise your position (note that the form I mentioned in my previous post does not exhibit any particular sentence, and therefore avoids your roller-coaster dilemma).
Incidentally, the idea that truth is simply redundant, at least in its naive form, is untenable. We already know that simply adding a predicate T to PA with the axioms T(x) iff x is the code of a true sentence results in inconsistency, which is already surprising to a redundant theorist, since it shows that adding a truth predicate with this simple property already goes much beyond the original theory (indeed, the simple property is so powerful that it results in inconsistency! In a sense, it is too powerful). But even more surprisingly, suppressing that axiom and adding weaker ones invariably result in non-conservative extensions of the base theories, i.e. theories that are more powerful than the original (both Friedman-Sheard and Kripke-Feferman have this property, for instance). So truth cannot be redundant.
The lesson here is that truth is an exceedingly difficult subject. As Timothy Williamson puts it in "Must Do Better":
Hence why we need formalization, as Williamson himself defends later in the essay:
I think the ideas that truth is provability or that truth is redundant, at least in the naive forms presented here, are precisely of the type that "differ subtly from provably incorrect claims" and "do not withstand even that very elementary scrutiny, because the attempt to construct a non-trivial model reveals a hidden structural incoherence in the idea itself".
Godel sentences do not support the colloquial interpretation they receive, that is to say "G is true because G is unprovable, assuming Peano Arithmetic is consistent". This is because
i) Firstly, the hypothesis that PA is consistent is potentially falsifiable, but it can never be verified. Therefore it is irrational for logicians and philosophers to assume or even talk about PA's 'infinitely complete' hypothetical consistency. Instead, they should only talk about PA's consistency within a limited finite scope of derivations.
ii) PA cannot talk about what isn't provable in PA, which is the central conclusion of Godel's first incompleteness theorem, and corresponds to both the Halting Problem and Tarski's undefinability of truth within PA. In general, for any sentence S of PA we have
a) PA |-- S <---> PA |-- Prov('S')
e.g. PA derives S if and only if PA derives Prov('S')
b) PA |-- G <--> ~Prov('G') For any Godel sentence G.
Therefore b substituted into a leads to the conclusion
c) PA |-- ~Prov('G') <--> Prov('G')
In other words,
PA |-- ~Prov('S') does not imply that PA does not derive S .
i.e. Peano arithmetic cannot enumerate the formulas that PA cannot derive (duh).
Therefore G does not say that "G isn't provable"
iii) The arithmetical theorems that PA cannot derive, e.g. Goodstein's Theorem, aren't constructively acceptable in any case, due to them appealing to the Axiom of Choice. These theorems cannot be computationally or otherwise empirically verified in principle without begging the question. Therefore they should not be considered as having a truth value.
In conclusion, an undecidable proposition of PA cannot be said to have a truth value, unless it is added as an additional axiom, in which case it is vacuously true due to now being provable as an axiom.
Unfortunately, Classical Logic and it's accomplice Model Theory, give this illusion that arithmetic is a meta-language for defining the truth of PA or vice versa from 'outside the system'. This isn't the case, due to the very ability of each system to encode each other. They are therefore one and the same theory, for formal purposes and are as equally undecided as each other.
Let us suppose that everything you say is true. This still does nothing to address two facts: (1) the set of true formulas is not arithmetically definable, but the set of provable formulas is, whence the two must be distinct; (2) truth is not conservative over PA, whence it can't be redundant. I sketched that argument in my first post here precisely so we did not get entangled in fruitless discussions about how we can know that G is true or about the Kirby-Paris theorem.
Obviously, that particular argument assumes the soundness of PA, which you have disputed (this is a minority position, but one that I respect, if only because in the case of Nelson it generated some interesting mathematics). But this is not necessary for the argument to go through: one can start with Q and argue that any recursively axiomatized theory that extends Q will fall into the same problem, namely truth will be arithmetically undefinable and theoremhood will be arithmetically definable. Since no one that I know of doubts the soundness of Q (not even Nelson), the argument should go through.
By the way, if your ii.c) is correct, then PA is inconsistent. In any case, that is not a valid substitution instance of ii.a): ii.a) says merely that (assuming soundness) PA |- S iff PA |- Prov('S'), not that PA |- S <-> Prov('S') (the latter is a reflection principle and is actually not provable in PA).
Correct me if i'm wrong, but aren't we both referring to the fact that the negation of PA's provability predicate doesn't actually enumerate what isn't derivable in PA?
Quoting Nagase
If by truth not being redundant, you are merely referring to the difference between
PA |-\- S (i.e. the event that PA doesn't derive S) versus PA |-- ~Prov('S')
then I think we're in agreement. But in this event, the notion of truth is redundant in the sense that it doesn't transcend the notion of derivability within PA, which is what I took the OP's point to be.
As for G's "truth" value, I can only recognise it as having undefined truth value, both in the sense of it's unknown status as a derivable theorem of PA, and also in the sense of it's decoded arithmetical interpretation pertaining to the undecidable solutions of Diophantine equations. As an aside, i don't recognize the truth of Goodstein's Theorem, due to it's proof relying on non-constructive notions pertaining to transfinite induction.
Quoting Nagase
I'm not so much of the view that PA will turn out to be inconsistent within my life time, but rather of the view that talk of the consistency of PA is meaningless in both demanding infinite evidence and also in being logically inexpressible, as demonstrated formally by Godel's second incompleteness theorem.
Quoting Nagase
ii a) doesn't express soundness in the sense of begging an external notion of arithmetic truth, rather it expresses the ability of Prov to enumerate what is derivable within PA:
PA |-- S <---> PA |-- Prov('S')
this is a provable equivalence, because Prov(''S') merely enumerates what can be derived in PA and it doesn't lead to false derivations, because it directly encodes PA's axioms and rules of inference.
ii c): By itself ii c doesn't imply inconsistency, because it is specifically stated with reference to the Godel sentence G that diagonalizes the negative provability predicate:
PA |-- ~Prov('G') <--> Prov('G')
Only if PA |-- G is derivable does ii c lead to inconsistency.
ii c) is equivalent to Tarksi's undefineability of truth applied to PA, in which PA's derivability predicate, Prov, is taken to be it's "truth predicate" . It also implies the constructive content of Godel's first incompleteness theorem, namely that ~Prov is a misnomer in not being able to enumerate what PA cannot derive.
That's why i said i agreed with Mad fool, for reasons you hinted at. Truth, as far as mathematical logic is concerned, IS derivability , for mathematical logic cannot be partitioned into a metalanguage talking about an independent object language, for both languages are isomorphic to one another and suffer from the same undecidability.
So you would call the cops if someone accused me of a felony crime but didn't have a shred of evidence against me?
By the way, justified true belief (JTB) theory of knowledge, in stating truth as a separate condition, lends support to your claim that proving a proposition and the truth of that proposition are two different things but, in my humble opinion, this proof-truth gap exists only in inductive logic as opposed to deductive logic where a sound argument gaurantees the truth of the conclusion and mathematics is exclusively deductive in character. That's why I think truth is redundant.
Just to inquire, did Godel prove the Godel sentence "this mathematical statement is true but unprovable"?
Let me put it this way. Suppose truth were equal to provability (or even just extensionally equivalent). Then any algorithm for enumerating all the theorems would ipso facto enumerate all the truths. But, in fact, we have an algorithm for enumerating all the theorems (they are computably enumerable) and none for enumerating all the truths (truth is not even arithmetically definable, let alone definable by a Sigma_1 formula). Therefore, they truth is not equal to provability.
So no, I'm not merely claiming that theoremhood is not fully capturable in PA. I'm claiming that whereas theoremhood is weakly capturable, truth is not capturable at all, and therefore these are different concepts.
As for the supposed redundancy of truth, again, I'm not referring just to the fact that theoremhood is only weakly capturable in PA. Rather, I'm referring to the fact that (i) if truth were redundant, the addition of a truth predicate to PA would result in a conservative extension of PA and (ii) the addition of a truth predicate to PA does not result in a conservative expression of PA. Hence, truth is not redundant.
As for your ii.c), you're saying that PA proves a formula of the type ~P <--> P. But then we have: ~P <--> P is equivalent to (P -> ~P) & (~P -> P), which is equivalent to (~P v ~P) & (~~P v P), which is equivalent to ~P & P. Hence, if PA proves ~Prov('G') <--> Prov('G'), PA proves a contradiction. Here's another way of seeing the matter. PA is built on classical logic, whence it proves every instance of P v ~P. So suppose PA proves ~Prov('G') <--> Prov('G'). Suppose then ~Prov('G'). Then, by this equivalence, Prov('G'), whence by conjunction introduction ~Prov('G') & Prov('G). On the other hand, suppose Prov('G'). Then, again by the equivalence, ~Prov('G'), so ~Prov('G') & Prov('G'). Thus, ~Prov('G') v Prov('G') -> (~Prov('G') & Prov('G')). But the antecedent is an instance of the excluded middle, so we can detach the consequent (again, remember that PA is classical) and obtain ~Prov('G') & Prov('G'), which is a contradiction.
As I said, the problem is that you're passing from PA |- S iff PA |- Prov('S') to PA |- S <--> Prov('S'). The former is ok, but the latter is not true; we only have PA |- S --> Prov('S') (that's one of the derivability conditions), whereas Prov('S') --> S is a reflection principle (soundness). In fact, by Löb's theorem, we have that, for any S, PA |- Prov('S') --> S implies PA |- S (cf. section 4.1 of this paper for a sketch of the proof).
(Interestingly, Boolos comments on this theorem on pp. 54ff of The Logic of Provability as follows: "Löb's theorem is utterly astonishing (...). In the first place, it is often hard to understand how vast the mathematical gap is between truth and provability. And to one who lacks that understanding and does not distinguish between truth and provability, [Prov('S') --> S], which the hypothesis of Löb's theorem asserts to be provable, might appear to be trivially true in all cases, whether S is true or false, provable or unprovable.")
Refer to my reply to for a clearer sketch of why truth is not provability, and which has nothing to do with G or whatever. And, again, you're evading my point that, if you want to reduce A to B, the mere fact that B is sufficient to A is not enough: you must also show that B is necessary for A. But this is just what Gödel's theorems deny.
Your juridical reasoning may be convincing in the intuitive level, but, as Williamson has said, in these matters it is not enough to argue impressionistically. As counter-intuitive as it might be, it is demonstrable that truth (on most reasonable axiomatizations of the notion, anyway) is not redundant and is not the same as provability.
In my (philosophy) department (here in Brazil), undergrads are generally introduced to the basics of logic or formal reasoning, say through Priest's A Very Short Introduction or Steinhart's More Precisely. That is the only required logic course for philosophy undergrads. There are a couple more optional courses they can take, but these vary wildly in content. At the graduate student level, they are not required to take any logical course, though there is generally at least one such course every term, again on a wide variety of subjects. I myself (a grad student) have (unofficially) taught a course loosely based on the first part of Boolos, Jeffrey & Burgess's Computability and Logic, and last term we also had a course based on the first four chapters of Shoenfield's Mathematical Logic.
As for the math department (again, at my university, here in Brazil), they are not required to take logic courses, though there are optional classes on logic and set theory. The logic class generally goes through the completeness, compactness, and Löwenheim-Skolem theorems, some times also into incompleteness. The set theory classes generally go through the usual cardinal and ordinal stuff, some times going into a bit more detail on combinatorics, other times scratching the surface of the constructible universe, and one or two crazy professors go as far as forcing.
An example would be the Paris–Harrington theorem which can't be proved in Peano arithmetic but can be proved in second-order arithmetic.
So prima facie there doesn't seem to be a problem with saying that a sentence is true iff it is provable – it's just that a second language is what proves the sentence. This would seem to fit with Tarski's claim that a metalanguage is required to make sense of an object language's truth.
I think it gets a bit dicey; if you can assume anything that doesn't trivialise proof in a system as part of the system as an axiom, and a system proves all its axioms, this trivialises truth. I think such a statement "true iff provable" has to be thought of in terms of "P is true iff there exists system C which proves P", but so long as you can conjure a C which has P as an axiom, P is true since it is by assumption provable in C. Making a statement range over all formal systems and models of them is going to do weird things to any notion of truth by design.
I understand what you mean, but is there an example of a statement that is true but isn't provable in any system? Surely it's impossible to know that a statement is true if it isn't provable?
It might be that "truth as provability" trivialises truth, but do we have any reason to believe that truth isn't trivial? Can we prove that it's something more?
Firstly, good spot about PA |-/- Prov S --> S
As you point out, that false derivational assumption which I took for granted and which led me to
PA |-- Prov('G') <--> ~Prov('G')
implies that PA is inconsistent due to LOM, something I overlooked as i don't think classically.
In fact, that 'Reductio ad absurdum' constitutes a weaker version of Lob's theorem, specifically applied to G.
But all of that said, from a constructivist position it doesn't seem surprising given that ~Prov already doesn't reflect non-derivability. Lob's theorem is just further ammunition for identifying truth directly with the derivable sentences, and for rejecting the interpretation of "prov" as meaning provability, and consequently for rejecting the semantic philosophical interpretation of incompleteness as implying 'arithmetically true but undecidable propositions'.
On a practical point, there's obviously a difference between developing second order arithmetic which can prove the Paris–Harrington theorem and developing a system that has the Paris–Harrington theorem as its only axiom. I don't know how to formalise that difference, but surely there is one (which is why second order arithmetic doesn't trivialise the theorem but this second system does).
Ultimately? I dunno. Trivial truth makes 1+1=3. Trivial truth also makes "truth is trivial is false" true. You know, the usual stuff against trivialism.
I don't know very much at all about truth predicates in formal languages, I think you're better off consulting @Nagase.
Quoting Michael
It trivialises the proof of the statement, but not whether it is true. All truths are equal in terms of truth value. The only way I see to block that "there exists a system C that proves P => P is true" part of the if and only if trivialising truth (for anything which can be stated in a formal language) is to claim that a formal system can't prove its own axioms, and at that point I'm not even sure what a formal system means.
I'm not sure what you mean by this. If we're doing Peano arithmetic then 1 + 1 = 2, whatever any other formal system says. If we're using a formal system where 1 + 1 = 3 then those symbols don't mean what they mean in Peano arithmetic.
If we had a formal system that used the Peano axioms to define the numbers and addition but also axioms that entailed that 1 + 1 = 3 then we'd have an inconsistent formal system, and so could dismiss it on those grounds.
I think if we're considering truth as provability and so therefore trivial then we just drop all talk about "true" and "false" and just talk about sentence P that is provable in F or sentence G[sub]F[/sub] that is provable in C. Does that lead to any sort of strangeness?
Also on this point a sentence like "truth is trivial is false" seems like it would belong in a natural language rather than a formal language like Peano arithmetic. Maybe truth in formal languages work differently to truth in natural languages.
It having no models in the usual way requires that truth and falsity work in the usual way, I think. If you wanna dismiss a formal system for being inconsistent (a provable contradiction) - ultimately the reason you'll do that is because it trivialises truth.
I think I'd do it on practical grounds. If the rules allow me to derive both 2 and 3 from adding 1 to 1 then I don't know how I'd go about using it.
Imagine a game of chess with a rule that says that pawns can only move forward 1 square and a rule that says that pawns can only move forward 2 squares. I'd dismiss it as unplayable, not because I think that it "trivialises the truth" of the rules.
But two different games that have one or the other rule? Both are fine. And it's not that one game is "true" and the other game "false".
I'm feeling content right now. It's TRUE but not provable. In fact pretty much most of my internal experience is not provable but no less true (to me). I wouldn't say it's a contradiction except that empirical data collection and the application of scientific method depends on the equivalence of truth to proof.
Indeed, inconsistency trivialises the rules. If you've got 1+1=3 and 1+1=2, that gives you 0=1, and the whole thing loses the meaning it had. If there is a provable contradiction (and your logic is normal), then the rules no longer matter. The idea of there being a "contradiction" requires a notion of truth to evaluate it. If you lose that, you lose the idea of inconsistency. So what if the system proves 1+1=3 and 1+1=2 at the same time?
Wittgenstein makes a couple of remarks in this area; proving a contradiction can usefully be interpreted as a formal system "jamming" with regard to what it concerns. It ceases to be a useful model of any set of axioms - and that's reflected by the collection of models a formal system has, if there's a contradiction, there are no models which satisfy it. Proving a contradiction gives you a good model of this break down of purpose (with regard to abstract systems of reasoning, rather than providing a good description like a physical model).
I don't think it does. It just requires the axiom of non-contradiction, which some systems like dialetheism do away with (allowing "true" contradictions).
A true contradiction is one which is true and false. You're not gonna get the same notion of contradiction out if you jettison the relevance of truth entirely. AFAIK paraconsistent logics don't jettison truth, they modify how it behaves in a manner that limits explosion/trivialism.
Would you prefer it if I'd said "provable" contradiction? My point was only that I don't think we need a concept of truth to have as an axiom ¬(p ? ¬p), and that the reason I might dismiss a system that allows me to prove p ? ¬p or that has the single axiom p isn't "ultimately ... because it trivialises truth" but because it isn't usable. Whereas if I have one system that allows me to prove p ("there is a number greater than 0 and less than every real") and one system that allows me to prove ¬p then I can use one or the other as desired or appropriate, and I don't need to believe that p is either true or false irrespective of its provability in either system.
On a different note, has anyone come across this paper? I don't have a JSTOR account so can't read it, but it sounds interesting.
Thanks for your comments!
I'm not going to pretend to be able to understand things like Godel, but this position sounds like the same conclusion Ramsey came to about deflating truth to something more like utility.
Unless we appeal non-constructively to the Axiom of Choice, we obtain a set of 'hyperreals' that is isomorphic to a subcountable set of natural numbers with their usual ordering relation. So in a superficial sense we can have infinitesimals in peano arithmetic by defining {1,1/2,1/3..} to be greater than {0,0,0...} even though we have only a subcountable number of such 'hyperrreals'.
You've made a good point. Godel's theorems depend on proof not being necessary for truth but the catch here is Godel, like all mathematicians and logicians I suppose, seems to have felt the need/necessity to prove his incompleteness theorems. Why didn't Godel simply state his theorems without proof? I reckon because he thought proof as necessary for the truth of his incompleteness theorems and then what does he prove? He proves some statements are true despite being unprovable. Isn't that a contradiction?
1. Proof is necessary for truth [Godel assumes and thus proves his incompleteness theorems]
2. The incompleteness theorems proves that proof is unnecessary for truth
3. Proof is unnecessary for truth (from 2)
1 and 3 contradict each other, no? This is a meta-cognitive statement regarding Godel's thought processes.
Despite my views I think it highly probable that I'm mistaken.
Because he wanted to show it to be true. He wanted to convince us of it and not just ask us to accept it on faith.
Yes, and your confusion is the fault of classical modal interpretations of logic that insist on misinterpreting PA's provability predicate as being meta-logical in character or representing knowledge, which it doesn't unless it is applied to theorems that are derivable without meta-logical reasoning.
The reason for all the persistent confusion that remains nearly 100 years after godels' proofs, is because Godel's theorems were baptised with their official philosophical interpretation as relating logic to a transcendental plane of mathematical reality, before the invention of the Turing Machine that collapsed the meta-logical distinction between logic and arithmetic by grounding them both in shared computational semantics; operations that also explicitly recognise the nondeterminism of provability due to the halting problem.
As an aside, the reason why the halting problem constitutes the quickest and easiest proof of Godel's incompleteness theorem is due the recognition that algorithms must halt to produce an answer.
For the logician, the predicate "A is provable" simply means that A is mechanically derivable by following the roles of the respective axiomatic system i.e.
"A is provable" := |--A
No other informal nomenclature about 'truth' is useful or necessary.
However, most philosophers describe logic using alternative nomenclature and then appeal to modal heuristics that only leads to confusion, misunderstanding and unnecessary arguments, for they define
"A is true" := |-- A
"A is provable" := |--- Prov('A')
Formally of course, Prov is equivalent to a prolog compiler written in the language of PA that translates theorems of PA into programs that when executed reveal the theorem of PA they they encode. Writing Prov as Comp, Lob's theorem no longer seems remotely surprising.
Recall that if we have PA |-- A , then we can also derive
PA |-- Comp('A') -> A
( i.e, a compiled program for a derivable theorem can be disassembled to reveal the theorem. )
Lob's theorem says
PA |-- ( Comp('A') --> A ) -> A
( i.e. if any compiled program is executed, then it's conclusion is the same as what the disassembler returns . )
So far, Lob's theorem isn't remotely surprising.
But in the case of Godel sentence G, if we assume that PA is consistent and hence that G isn't derivable, the following cannot be true by Lob's theorem:
PA |-- ( Comp('G') --> G )
i.e. if an undecidable statement is compiled, then it cannot be disassembled.
Bur recall that G is the statement saying
G <---> ~Comp'G')
This indicates that the only way to disassemble Comp('G') would be to substitute G into itself an infinite number of times. So it shouldn't be surprising that Comp('G') doesn't imply that it can be disassembled back into G (assuming consistency).
I suspect that those who find Lob's theorem surprising do so because they assume that compilation is always invertible.
I don't think Löb's theorem supports the constructivist position. That's because truth is generally taken, prima facie to obey the capture and release principles: if T('S'), then S (release), and, if S, then T('S') (capture). But what Löb's theorem shows is that proof does not obey the release principle. So there is at least something suspicious going on here.
Moreover, one can show that the addition of a minimally adequate truth-predicate to PA (one that respects the compositional nature of truth) is not conservative over PA. Call this theory CT (for compositional truth). Then [math]CT \vdash \forall x (\text{Sent}(x) \rightarrow (\text{Prov}(x) \rightarrow T(x)))[/math], where "T" is the truth predicate. As a corollary, CT proves the consistency of PA. So truth, unlike provability, is not conservative over PA.
Finally, you have yet to reply to my argument regarding the computability properties of the two predicates, namely that one does have an algorithm for listing all the theorems of PA, whereas one does not have an algorithm for listing all the truths of PA. So the two cannot be identical.
1. Godel felt a necessity to prove the truth of the incompleteness theorem
2. IF Godel felt a necessity to prove the truth of the incompleteness theorem THEN Godel thinks that proof is necessary to establish truth
Ergo...
3. Godel thinks that proof is necessary to establish truth
4. The incompleteness theorem states that a particular statement is true but unprovable
5. Godel believes the incompleteness theorem
5. IF the incompleteness theorem states that a particular statement is true but unprovable AND Godel believes the incompleteness theorem THEN Godel thinks proof is not necessary to establish truth
6. The incompleteness theorem states that a particular statement is true but unprovable AND Godel believes the incompleteness theorem (from 4 and 5)
Ergo
7. Godel thinks proof is not necessary to establish truth
8. Godel thinks proof is necessary to establish truth AND Godel thinks proof is not necessary to establish truth (contradiction from 3 and 7)
Do you see a problem in my simple argument?
(1) Gödel (well, Gödel, Church, Tarski, Rosser, etc.) showed a bit more than what you are implying. He showed that, for any consistent system containing enough arithmetic (i.e. extending Robinson's arithmetic), the set of theorems of that system is not identical to the set of truths of that system. So, if we just move one level up and claim that truth is provability in a higher system, this won't do, because the theorem will reapply at the higher level separating these sets again.
(2) As for why truth is not trivial, the surprising result here is that any minimally adequate theory of truth (i.e. one that respects the compositional nature of truth) is non-conservative over PA. That is, given a truth predicate, one is able to prove more things about the original system than one could before the introduction of such a predicate. In particular, one is able to prove the consistency of the original system. So adding a truth predicate is not a triviality. If you think about it, this is not that surprising, since the truth predicate can be used to express generalizations that wouldn't be possible without it except by the use of infinitary resources, such as infinite disjunctions or infinite conjunctions, i.e. "Jones always tells the truth".
(3) With regards to Fair's article, I've just read it and didn't find it much convincing. He basically argues that truth must be relative to a theory (instead of a model), introducing a family of operators "In T" (i.e. "In PA", "In the theory of algebraically closed fields of characteristic 0", "In ZFC", etc.) and argues that truth ascriptions are always prefixed by this operator, i.e. the hidden logic form of "2+2=4" is actually "In PA, 2+2=4". I personally think this is an instance of a bad (and unfortunately widespread) philosophical habit of postulating hidden linguistic forms without appealing to linguistic evidence (and thus being ad hoc), but let us leave that to the side. In order to deal with incompleteness, Fair is then lead to work with an analogy from fiction: just as the Sherlock Holmes stories don't settle how many hairs he has in his body, so PA doesn't settle G or other undecidable sentences.
In order to support this, he basically assimilates mathematics to fiction, saying that mathematical objects are mind-dependent, etc. In particular, he argues that mathematical objects "lack the 'open texture' we would expect of mind-independent physical objects" (p. 368), by which he means (presumably) that the properties of mathematical objects are fully determined by our beliefs about them (at least, that's what I gathered from the preceding discussion) and that we could not "failure to notice" some of their important properties. I think this is mistaken. Two historical examples: continuity and computability. In both cases, mathematicians had been working with objects that had those properties, but they didn't fully realize the nature of the properties themselves. It was only centuries after working informally with these objects that we began to understand their nature---and even today there are still disputes about them (e.g. is the continuum formed by points, such as Dedekind cuts, or is it formed by regions, like the intuitionists claim?). Moreover, greater clarity about these properties revealed surprising consequences (the existence of continuous functions that were nowhere differentiable or the fact that any local and atomistic process can be simulated by a Turing Machine).
So, at the end, I think there is a great disanology between mathematical truth and fiction. In the latter case, there is almost no friction, and our conceptions can be given free reign. With the former, however, our conceptions are tightly constrained. That is why truth in mathematics is not as problematic as truth in fiction, I gather.
You seem to be confusing knowledge with truth. Obviously, to establish a proposition as true, I need to, well, establish as such. And, in mathematics, to establish a proposition as truth---i.e. to know it---is precisely to prove it. But there can be true propositions that are unknowable, and hence that we cannot establish, and hence that we cannot prove. That there are such propositions is established by Gödel's theorems. Again, note that, in the form I have presented, the theorem does not rely on pointing to one such proposition and saying "This proposition is true, but we can't know it as true". Rather, it proceeds from general properties about truth and provability to show that these concepts must come apart.
Well, Godel's incompleteness theorem must be part of mathematical knowledge but that's not what matters here. What matters is he's being inconsistent - metacognitively speaking. On one hand, by resorting to proof he endorses the necessity for proof and on the other hand, by accepting his incompleteness theorem, he rejects the necessity for proof.
There is no contradiction. One can hold that proof is necessary to establish truth, yet hold that it is not necessary for truth (cf. my point about unknowable truths). And, in the form I have presented, his theorem does not require him to establish the truth of any unknowable proposition.
That's just word play.
Firstly, the incompleteness theorem has a proof, Godel's, with the express purpose of establishing the truth of the theorem.
Secondly, the incompleteness theorem itself speaks of a statement that's true but unprovably so i.e. the truth of that statement hasn't/can't be established and yet, Godel claims, it's true.
There would only be a contradiction if Gödel claimed that his own theorem was unprovable. Fortunately, he was not an idiot, and therefore did not claim that. What he did claim was that some truths are unprovable (his own theorem not being among those). And the reason why some truths are unprovable was sketched in my first post in this thread, namely the theorems are all capable of being listable by an algorithm, whereas no algorithm can list all truths. Hence, there are truths that will not appear in the list of all theorems, hence, not every truth is a theorem. Again, note that, in this version, no mention is made of a specific unprovable statement, so your reasoning about the "meta-cognitive" level does not apply.
Thanks for all your explanation in this thread, really appreciate it.
I was just addressing the wording of the theorem: there are statements of the language of F which can neither be proved nor disproved in F. Why does it not just say that there are statements of the language of F which can neither be proved nor disproved? Is it because for any statement of the language of F there is some G that can prove or disprove it?
Could you also clarify the situation regarding my example of "there is a number greater than 0 and less than every real"? @sime's reply seems to suggest that I'm misunderstanding the status of the hyperreals. My claim was that the sentence can be provable in one system and that its inverse can be provable in another system, and that that's all there is to the sentence being either true or false.
Well, proof is relative to a system of axioms. That is, we usually define proof, relative to a theory T, as follows: a sequence of statements A1, ..., An is a proof of An in T iff for every i < n+1, either Ai is an axiom of logic, an axiom of T, or it follows from the Aj's (j < i) from the rules of logic. So it doesn't make much sense to ask about a sentence whether it is provable or unprovable tout court, whence the relativization to a given axiomatic system (unless you're asking about whether a formula is a truth of logic, in which case you don't need the relativization to a theory, though you will obviously relativize to the background logic).
As for your example, in the case of some particular theories (such as PA or real analysis), we are interested in theory primarily as a description of a particular object. For example, when in studying PA, we are generally not interested in any discretely ordered ring, rather, we are interested in the natural numbers. So when we are asking about the truths of PA, we are asking about truth in the natural numbers, not truth in any model. Similarly, when we are asking about the truth of a sentence about the reals, we are generally interested in, well, the reals, not the hyperreals. That's not to say that these other objects are not useful or interesting in their own right, just that in the case of those theories, we have an intended model in mind.
Here's a comparison that I find useful. Consider the theory of groups. It consists basically of three axioms (I'll use the additive notation because it is easier to type): x+(y+z)=(x+y)+z, x+e=x, and x+(-x)=e. Now, since there are commutative and non-commutative groups, this theory does not decide the sentence x+y=y+x, and is therefore incomplete. But this is not surprising in the least, because when studying groups, we are not studying a privileged group, so we don't expect the axioms to completely characterize this object. Indeed, the axioms were developed to be as general as possible while still characterizing an interesting class of objects (namely, groups), so it is a virtue of the theory that it is incomplete.
On the other hand, in the case of PA, the theory was crafted to completely characterize a particular object, namely the natural numbers (object here taken in a broad sense, to include structures). Moreover, in the case of second-order PA, Dedekind proved that it does completely characterize its intended object, in a sense: the theory is categorical, which means that every model of the theory is isomorphic to the standard model. Hence it completely captures the structure of the standard model. So it is surprising that there are truths about this system that it the theory is unable to prove.
Don't mention it. I'm glad this has been useful to someone...
I seem to have missed something (or maybe not). Godel's incompleteness theorem states that given an axiomatic system X capable of mathematics there will be mathematical truths, say P, that can't be proved in X. Godel doesn't seem to be saying that such statements are unprovable in every possible axiomatic system, just that it's unprovable in the axiomatic system X.
If so, we would need patch system X with either the statement that's unprovable (P) or another one with which we can prove P - call this new system Y. The catch is that the problem of unprovable true statements will recur in the new system Y too and so on.
Just wanted to ask you two a question:
IF proof isn't necessary for truth then, how do we distinguish between truths and falsehoods? The universal response to claims people make is to ask for proof.
A couple of observations:
(1) First, note that the theorem, in the form I stated, is a bit more general, since it does not rely on any specific unprovable sentences. Thus, even if we know by construction (or other means, such as Kirby-Paris) that a given sentence is unprovable but true, and then add it to the theory, we can't be sure that we have exhausted all the truths---there could be many more true but unprovable sentences of which we are unaware, so merely adding one to the theory will not make it complete. Of course, we could simply take all the true sentences and add it to the theory---but then we wouldn't know what is the resulting theory! (In other words, there would be no algorithm to tell me whether or not a given sentence belongs to the theory)
(2) This failure to identify the truths to be added could be circumvented if we could isolate an easily identifiable set of sentences and prove that adding just this set of sentences is enough to add all the truths. For instance, a natural candidate for such a set is the set of sentences which express consistency statements. That is, we could begin with Con(PA) (a statement saying that PA is consistent), and it to PA to obtain the theory PA + Con(PA), then consider the consistency statement for this theory and add it to obtain PA + Con(PA) + Con(PA + Con(PA)), so on and so forth. By Gödel's second incompleteness theorem, we know that each resulting theory is stronger than its predecessor, so there is at least some hope that this would bear some fruit.
In fact, we can obtain a more interesting result if, instead of working with consistency statements, we work with reflection principles of the sort exemplified by Löb's theorem. That is, define Ref(T) to be the statement "For every sentence S of T, ProvT('S') -> S", where "ProvT" is the provability predicate for T. We can then consider progressions of the form PA + Ref(PA), PA + Ref(PA) + Ref(PA + Ref(PA)), etc. Now, an immediate problem appears here: for each natural number n, we can define Tn to be Tn-1 + Ref(Tn-1 + Ref(Tn-1)). And then we define T(omega) to be the union of all such Tn's. But what happens then? We can obviously continue the procedure, i.e. considering T(omega) + Ref(T(omega)). Here, however, we will need a way to codify ordinals greater than omega inside PA. This is done by what are called ordinal notations.
So how far can we go? Will the process eventually stop somewhere? It is a remarkable theorem by Feferman (cf. "Transfinite Recursive Progressions of Axiomatic Theories") that, in the case of PA, it does stop somewhere, and he gave a precise stopping point for this (if you must know, the stopping point is at [math]\omega^{\omega^{\omega +1}}[/math]). That is, Feferman found that there is a way to code ordinals such that according to this code, there is a certain iteration of the addition of reflection principles that proves every true arithmetical sentence! This is often referred to as Feferman's completeness theorems and is remarkable indeed.
Unfortunately, there is a catch (there's a Brazilian song that says that a ripe fruit hanging near a well-trodden path must be either rotten or its tree full of wasps...). There is more than one way to code ordinals, and Feferman's proof depends heavily on the choice of code. Indeed, he also showed (together with Clifford Spector) that there are infinitely many ways of coding ordinals for which this result is not true. Moreover, to discover the correct coding is as difficult as discovering what are all the true sentences of PA (this is basically because he employs a rather bizarre code that ensures that in every iteration of the construction we "sneak in" a true formula). Hence, there is no real algorithm for extending PA in such a way to obtain a complete extension using reflection principles. The obstacle is the same as before, at some point we don't know anymore what is the theory we are obtaining by this procedure. (For those curious about this, the book by Torkel Franzén, Inexhaustibility: A Non-Exhaustive Treatment is still the best, though be warned that it is technically demanding).
(3) So what is going on? Again, the point is that provability (in the sense of obtaining a proof that we can recognize as such) is different from truth. Note that, in spite of my talk of models in a previous post, this need not be cashed out in strictly platonist terms. One can think about this in terms of the principles we are committed to when reasoning about arithmetic (where the vocabulary of principles and commitment can be taken in a broadly Sellarsian fashion). These principles can be taken to be encoded in the axioms for second-order arithmetic, and here the problem becomes even more evident: second-order logic does not have a complete proof-procedure. So, again, the semantic content of our principles invariably outstrip our capacity to prove things from them.
(4) Lastly, about your question, it is ambiguous. "To distinguish" can be taken to mean "how do we establish that something is true?", in which case you are right that the answer is "by proving it". But it can also be taken to mean "how do we characterize a sentence as true", in which case the answer is not "by proving it", but rather according to Tarski's satisfaction definition (or, if you will, you can say that a sentence of arithmetic is true if it follows semantically from the second-order axioms of PA).
Constructively, Prov doesn't fail either the capture or release properties of a truth predicate with respect to decided sentences, rather Prov doesn't supply negative truth value when classifying undecided sentences that no axiomatic system can decide without either begging the question, or by performing a potentially infinite proof search equivalent to doing the same in Peano arithmetic.
Perhaps part of the confusion/suspicion comes from overlooking the following symmetry in what Peano arithmetic cannot derive
PA |-/- (For All S: S --> Prov('S')) ( since compilation is potentially infinite)
PA |-/- (For All S: Prov('S') --> S ) ( since decompilation is potentially infinite)
Löb's theorem only deduces the existence of an as-of-yet undecided object on the assumption that the decompilation process of it's respective code terminates. And yet the undecided object will only compile into a code in the first place, if it is decidable. Therefore Löb's theorem does not have constructively relevant implications.
Why would you want, let alone expect, a truth predicate to capture and release the properties of potentially infinite objects whose existence is potentially non-demonstrable?
Quoting Nagase
In other words, introducing new axioms to represent undecided formulas generally permits the derivation of new sentences in a vacuous manner.
Quoting Nagase
The set of theorems of PA isn't recursive due to the halting problem, meaning that any proposed test of theoremhood by a "truth predicate" is bound to be either incomplete or to contain an infinite number of mistakes.
Consequently, the "truth" of PA consists of the explicit construction of each and every theorem, doing everything the hard way.
Edit: I rushed this post, so came back and rectified some mistakes.
I think you are focusing too much on the fact that theoremhood is not strongly representable in PA, with the consequence that you are ignoring the fact that it is weakly representable in PA. Indeed, while theoremhood is not computable, it is computably enumerable. In other words, there is an algorithm which lists all and only theorems of PA. It exploits the fact that, given your favorite proof system, whether or not a sequence of formulas is a proof of a sentence of PA is decidable. Call the algorithm which decides that "Check Proof". Here's an algorithm which lists all the theorems of PA, relative, of course, to some Gödel coding:
Step 1: Check whether n is the Gödel number of a sequence of formulas of PA (starting with 0). If YES, go to the next step. Otherwise, go to the next number (i.e. n+1).
Step 2: Decode the sequence of formulas and use Check Proof to see if it is a proof. If YES, go to the next step. Otherwise, go back to Step 1 using as input n+1.
Step 3: Erase all the formulas in the sequence except the last. Go back to Step 1, using as input n+1.
This (horrible) algorithm lists all the theorems, i.e. if S is a theorem of PA, it will eventually appear in this list. Obviously, this cannot be used to decide whether or not a given formula is a theorem, since, if it is not a theorem, then we will never know it isn't, since the list is endless. But, again, it can be used to list all the theorems. My point is that there is nothing comparable for the truths, i.e. there is no algorithm that lists all the truths. In fact, by Tarski's theorem, there can be no such algorithm. So, again, the two lists (the list of all the theorems, the list of all the truths) are not the same, whence the concepts are different.
The upshot of all this is that, in my opinion, constructivists should resist the temptation of reducing truth to provability. Instead, they should follow Dummett and Heyting (on some of their most sober moments, anyway) and declare truth to be a meaningless notion. If truth were reducible to provability, then it would be a constructively respectable notion. But it isn't (because of the above considerations). So the constructivist should reject it. (Unsurprisingly, most constructivists who tried to explicate truth in terms of provability invariably ended up in a conceptual mess---cf. Raatikainen's article "Conceptions of truth in intuitionism" for an analysis that corroborates this point.)
Not only intuitionists (who would require an actual construction), but other practitioners as well. :cool:
I'm still confused as to where and how we disagree. I suspect the issue might be mostly terminological, due to your use of modal notions versus my deflationary/constructive terminology. However it is possibly worth recalling that PA must have the following theorem for any provability predicate
PA |-- Prov('G') --> ~G for any Godel sentence G.
In other words, there cannot be an exhaustive and infallible enumeration of theoremhood within PA. - and here we aren't referring to the failure of ~Prov to enumerate the non-theorems - rather we are referring to the inability of Prov to correctly enumerate all and every derivable theorem.
We can of course construct an infallible Prov by defining it to enumerate only the godel-numbers that have been independently determined to be proofs via brute-force checking. In which case Prov along with the godel-numbering system are merely redundant accountancy of what we've already derived, and in which case Prov sacrifices exhaustivity for infallibility.
Alternatively, prov could be an 'a priori' algorithmic 'guess' as to theoremhood , in which case it can be exhaustive , e.g. by guessing "True" to every godel number, but at the cost of infallibility, in guessing both correctly and incorrectly as to theoremhood.
But we're at least both in agreement it seems, that there isn't an algorithm for listing all and only the actual theorems of PA - which is precisely the reason why truth should be constructively identified with actual derivability, as opposed to being identified with whatever is unreliably or incompletely indicated by a 'provability'/'truth' predicate.
So where and how do we diverge?
Quoting Nagase
Dummett's overall arguments sound roughly similar to my deflationary position of truth in mathematical logic'; software engineers don't say that the operations of a software library has no truth value, rather they define truth practically in terms of software-testing, without appeals to the choice axioms, or the Law of excluded middle.
What i think classical philosophers overlook is that the absolute consistency of PA isn't knowable, or even intelligible. As an absolute notion, undecidability is meaningless.
I'll be very explicit, then: there is, in fact, an algorithm that lists all and only the theorems of PA. This algorithm therefore provides an exhaustive and infallible enumeration of theoremhood of PA. It is exhaustive, i.e. every theorem appears in the list. And it is infallible, i.e. every formula in the list is in fact a theorem. Since for some reason you apparently missed it from my last post, I will reproduce it here again. Choose your favorite Gödel numbering for formulas and sequences. Given this Gödel numbering, there will be an algorithm, call it DecodeS, which, given a number m, first decided whether or not m is the Gödel numbering of a sequence of formulas and, if it is, returns the sequence of formulas for which m is a Gödel number. We also have an algorithm, Check Proof, which, given a sequence of formulas, decided whether or not the sequence of formulas is a proof in PA. Given these, the algorithm is as follows:
Step 1: Input n (starting with 0). Use DecodeS to check if n is the Gödel number of a sequence of a formulas. If YES, go to the next step, otherwise, start again with n+1.
Step 2: Use DecodeS to print the sequence of formulas coded by n. Apply Check Proof to this sequence. If the result is YES, go to the next step. Otherwise, go back to step 1 with input n+1.
Step 3: Erase all the formulas in the sequence except the last. Go back to step 1 with n+1.
Call the above three step algorithm Theorem List. I claim that Theorem List is an exhaustive and infallible enumeration of theoremhood in PA. It is obviously infallible, since Check Proof is infallible. It is also exhaustive, since the algorithm will basically go through every sequence of formulas of PA, so, if P is a theorem of PA, it s bound to find a proof for it eventually.
In other words, the set of theorems of PA is what we call computably enumerable. This is a well-known fact (and the proof is clearly constructive---it is not like the concept of r. e. sets is somehow constructively suspect), so I'm surprised that you are still insisting that it is somehow impossible to generate an exhaustive and infallible list when the above demonstrates that it is not only possible but actual (and it also exhibits the algorithm in question!). Now, you claimed that this alleged impossibility somehow followed from the fact that PA |- Prov('G') --> ~G, but I don't see the relevance of this for listing all and only the theorems.
Yes, there is a proof of the consistency of PA, though whether or not it is finitistically acceptable is debatable. Gentzen proved that the consistency of PA can be proved in PRA + Epsilon_0 induction, i.e. primitive recursive arithmetic augmented by the principle that the ordinal epsilon_0 is well-ordered (it should be noted that PRA + Epsilon_0 induction and PA are incomparable in strength, so the result is not a triviality). See this very nice article by Timothy Chow for more on the topic.
If by G you mean the Gödel sentence, then, yes, the algorithm will miss it. But that's because the algorithm lists all the theorems of PA, and the Gödel sentence is not a theorem of PA!
If a theory is such that: (i) it has a reasonable proof system (i.e. one can check by an algorithm whether or not a sequence of formulas is a proof) and (ii) is recursively axiomatized (i.e. there is an algorithm which tells whether or not something is an axiom of the system), then that theory will have a computably enumerable set of theorems.
And yes, this applies also to classical mathematics such as classical analysis, to the extent that it can be formalized in a reasonable proof system (be it by formalizing in second-order arithmetic or by formalizing it in first-order ZFC or something similar).
What do you mean to communicate here? Do you doubt it could be done? Do you wonder how it's done? Could you produce at least a high-level drilldown of the basic ideas if called upon to do so? Would you like to see what that would look like? Do you wish math would go back to the mid nineteenth century before the age of formalization? I'm wondering what is the purpose of your post. I know the formalisms, I'd be glad to outline them if that's what you're curious about.
Or are you asking why anyone would bother with such pedantry? It's those pesky nineteenth century guys again, noticing that their lack of rigor was causing trouble. For example before the great age of epsilons and deltas, even Cauchy famously wrote an erroneous proof by failing to distinguish between pointwise and uniform convergence.
tl;dr: Did you want to see an outline of a proof of FTC directly from ZF? Or are you wondering why anyone cares?
What is upsetting you? I have simply stated something I haven't done. There are no unstated jabs at modern mathematics. And yes, I am curious to see what that might look like. Nagase gave a nice reply to a question I raised. Since I once went through the process of attaining the exponential function through set theory I am curious how one would prove something like the fundamental theorem from "scratch". But I am not curious enough to work through all the details.
Quoting fishfry
Of course not. I know you think I'm a dinosaur of a mathematician, and I admit I am. I have even avoided holomorphic functions at times in order to investigate more general non-linear conditions in complex dynamics. That really puts me out to pasture. But you know what? It's been a delightful journey and it still is.
I apologize if I have offended you. Let's agree that modern set theory as well as other modern areas of mathematics are very important subjects that some old timers may not fully appreciate. :cool:
I have never held such an opinion. When have I ever said such a thing? If you can link or quote anything I've ever written to that effect I'll stand corrected, but as I have never said any such thing you will not be able to. I have noticed that you very often refer to your status as a retired math professor; and that you often announce your ignorance of virtually everything outside of your specialty, and most of the standard undergrad math curriculum. You've said this probably a dozen times in the past couple of months, most recently in the post I just replied to. Perhaps you're projecting or perhaps you have feelings about this. I am certain I've never commented on these matters at all. You are the one who keeps bringing them up.
I don't understand why you post that you have no idea how to prove FTC from first principles, but then get angry when I ask if you are curious to learn how. I admit I don't get where you're coming from. I was, and still am, curious as to why you would post to the effect that you don't know something, without having the intention of either learning it or objecting to it. And that's what I asked.
From ZF the axiom of infinity gives us [math]\mathbb N[/math]. We use an equivalence relation on [math]\mathbb N \times \mathbb N[/math] to form the integers; and another one on the integers to form the rationals. We build the reals as Dedekind cuts of rationals. One the reals are built we can make rigorous definitions of limits, continuity, derivatives, and Riemann integrals; and then any textbook proof of FTC will suffice.
Integers from naturals: http://web.math.ucsb.edu/~padraic/ucsb_2014_15/ccs_proofs_f2014/ccs_proofs_f2014_lecture5.pdf
Rationals from integers: https://en.wikipedia.org/wiki/Field_of_fractions
Reals from rationals: https://en.wikipedia.org/wiki/Dedekind_cut
Really? I've taught analytic geometry, the calculus sequence, advanced calculus, intro to real analysis (grad), point set topology, statistics and probability, history of mathematics, mathematics of finance, metric spaces, intro to computer science, complex variables, differential equations, special topics in analysis, math for engineering technology, linear algebra, etc.
I have taught neither abstract algebra nor set theory. The one faculty colleague who was a set theorist became more of a math educator and journal editor. We never developed a set theory course due to a lack of student interest as well as the fact that most of us were not competent in that subject. As you have seen.
I have not kept up with more than a small handful of the myriad of directions math has taken during the last century. I got my degree fifty years ago and teaching, administrating, and on and off research kept me busy, along with a family and a serious outdoor avocation. One makes choices.
Please stop the ad hominem attacks.
I apologize.
I only wish to tell you that with your background, every single thing that's been discussed on this forum that you think is beyond you, is actually trivially within your capabilities and knowledge.
Fair enough. When I speak of a topic being "beyond me" it's a cop-out for not having the mental energy at my age (83) to study it, or just a complete lack of interest. I appreciate your comment.
Every so often, however, something a bit out of my purview will intrigue me and I will make an effort to understand it. For example, a couple of years ago the notion of a functional integral sparked my interest, having read of Feynman's Sum of All Paths concept. My brief exposure to the concept fifty years ago was shallow and uncompelling.
That was a delightful exploration, starting with the basic Wikipedia definition, and I wrote a short math note about functional integrals in spaces of complex contours. I enjoy writing math programs, especially graphics, and I came up with some nice imagery. That was fun.
I should not be making dismissive comments about set theory. You, fdrake, Nagase, and a few others have clearly explained ideas in this subject, and it is a powerful link between math and philosophy, and a vital part of the mathematical galaxy. I apologize, and if I slip up in the future you should nail me!
Most of my research efforts have been in classical analysis, very basic dynamical systems in the complex plane, trying to determine convergence/divergence of certain sequences. At one time this was a popular topic, but modern analysis has moved the focus more toward algebraic systems and generalizations.
But I remain attached to the old-fashioned, nuts and bolts, stuff. For example, my latest efforts concern the iteration of linear fractional transformations (f(z)=(az+b)/(cz+d)) when the attracting fixed points are functions of time and are no longer "fixed". Like predator and prey, do the iterates "catch up" with the roving attractors? Modern theory dealing with LFTs is more geometrical and algebraic.
OK. Enough rambling. Thank you for your comments.
We're the main show now.
Quoting jgill
I figured out that you're excessively modest. I misunderstood you and drew false conclusions. You're a teacher and I learned something. Thank you.
Quoting jgill
That's interesting stuff. I never studied formal physics but I watch a lot of Youtube videos.
Quoting jgill
The modern computer tools like LaTeX and computer graphics are incredible. I wish they had those when I studied math. Especially because my handwriting was bad.
Quoting jgill
I have it on good authority that you know a lot more set theory than you're letting on. Perhaps you mean some of the logic stuff, the incompleteness aspects of set theory. As far as my attempting to nail you, I also have it on good authority that you could kick my ass. I saw the videos :-) You dropped some clues, I hope you don't mind. I also found a lovely elementary survey article about infinitesimals in which you mentioned the ultrafilter construction. You are being modest. You know more set theory than most here.
Quoting jgill
Interesting stuff.
Quoting jgill
I do remember the linear fractional transformations from undergrad complex variables so at least I know what those are.
Quoting jgill
I remember predator/prey from diffEq. Volterra-Lotka equations.
Quoting jgill
In another life I wanted to be a professor of math. I envy you your obvious focus and discipline.
That said, I sense a lack of clarification between mathematics qua mathematics -- that is, a system for dealing with the concepts known as numbers -- and the discussion of mathematics; metamathematics, if you wish.