nomadreid said:
My apologies if I overlooked one of the posts, but it appears that no one has pointed out that "S is provable" ("or S is provably true") is, by itself, ambiguous: the question if something is provable or not is dependent upon (a) the axioms and rules of inference used, and (b) the model in which one is working. One may have particulars implicitly in mind, but one should state them explicitly in such discussions.
Good point. I made some similar points in post#12 (under the heading "note3:"). Given what you have mentioned it seems it would be better to add for clarity that when in post#14 I wrote:
SSequence said:
For PA, here is an older topic:
https://www.physicsforums.com/threads/simplest-independent-first-order-expression-in-pa.955115. As I understand, it has also been studied in detail which strictly increasing (recursive/computable) functions can or can't be proved to be total in PA.
It seems fair to add explicitly here that ##\mathbb{N}## (the actual natural nos.) is assumed as a model here.
yossell said:
I would avoid describing Godel's theorem as showing the existence of true but unprovable statements. Godel's completeness theorem goes through, and can be stated without notion of mathematical truth. What's been shown is the *independence* of a statement P wrt to a set of axioms: on the proviso that the theory is consistent, neither P nor ¬P is provable in the theory.
I don't know about the completeness theorem well-enough formally. I think you are right about the work "unprovable". I assume that 'normally' when one says "unprovable" it should be assumed to be equivalent to:
"unprovable in F"
"undecidable in F"
etc.
It seems to me that a big part of godel's theorem is showing that the "godel sentence" can actually be written as a statement of arithmetic. This part seems to be lost in informal descriptions (or becomes difficult to appreciate). I don't know the important details of this myself (except, somewhat vaguely, that first certain useful primitive recursive functions are represented in PA and then they are used for arithmetization).
That also mean that statements like "this statement is unprovable in F", "this statement is provable in F", "this statement is undecidable in F" as being possible (or not) to convert to actual arithmetic statements is a bit subtle (I am unclear about number of things here).
yossell said:
Godel's original proof did indeed assume w-consistency. But an improvement due to Rosser managed to weaken w-consistency to consistency.
I made a similar point in post#12 (but what you have described is more general).
yossell said:
I'm not sure why it's thought that con(PA) is a known truth. Any proof of con(PA) will involve methods that are stronger than PA. So, *IF* you know that ZFC is true then, I guess, you know that con(PA). But really all we can do is show that, if ZFC is consistent, then so is PA. Your warrant of the consistency of PA will therefore only be as good as your warrant for the consistency of a (typically) stronger theory.
I guess we will have to disagree on the first sentence.
Good point regarding consistency of set-theory implying truth of con(PA). It is a basic point but, somewhat surprisingly, I never thought about it before (more surprising given that I have thought about similar issues quite a bit ... outside the context of maths).
It doesn't seem like the assumption of arithmetic soundness of set theory is required. That is, it seems to me that given:
(i) set-theory is consistent
(ii) set-theory proves con(PA). These (i) and (ii) seem to be sufficient to conclude truth of con(PA). Now we know (ii) to be true. Hence assuming (i) is sufficient to conclude that con(PA) is true.
That's because if we assume (i) true and con(PA) actually false, then this possibility isn't allowed. Because con(PA) being false would be found out via very trivial calculations (in set-theory). And then ~con(PA) along with (ii) will contradict (i)
[which was the assumption
]. Hence the possibility of (i) being true and con(PA) being false is excluded.
Regarding the requirement of strength, making this point more explicit (it might be helpful for someone else), quoting from a
paper (I also linked the same quote on this forum about more than an year ago):
Godel’s theorem does not actually say that the consistency of PA cannot be proved except in a system that is stronger than PA. It does say that Con(PA) cannot be proved in a system that is weaker than PA, in the sense of a system whose theorems are a subset of the theorems of PA—and therefore Hilbert’s original program of proving statements such as Con(PA) or Con(ZFC) in a strictly weaker system such as PRA is doomed. However, the possibility remains open that one could prove Con(PA) in a system that is neither weaker nor stronger than PA, e.g., PRA together with an axiom (or axioms) that cannot be proved in PA but that we can examine on an individual basis, and whose legitimacy we can accept. This is exactly what Gerhard Gentzen accomplished back in the 1930s...
Gjmdp said:
##Definition##: A statement is ##provable## in ##S## if there is a proof (in ##S##) for whether it is true or false.
Unless I am mistaken, it seems to me that this terminology doesn't conform with usual definition of provable. Normally "P is provable in S" would mean "S has proof for P" and "P is disprovable in S" would mean "S has a proof for ~P".
"P is undecidable/independent of S" would mean:
"S doesn't have a proof for P
AND S doesn't have a proof for ~P"
Stephen Tashi said:
You may as well say "Let ##P## be an arbitrary unprovable proposition in ##S##" since that is the only case relevant to what you intend to prove.
As TeethWhitener pointed out, this assumes the formal system ##S## will contain a propostion that deals with the provability of propositions in itself. It is not clear whether a self-consistent formal system of this type exists. (Self-reference is a tricky thing to handle.)
For some specific proposition ##P## writing "##B##: ##P## is an undecidable proposition in ##S##".
I think this is the first point that needs to be considered. But it seems to me that ##B## should be representable as a statement in PA. I am not completely sure (since I don't know the details well-enough). I am reasonably certain because if you take some specific statement in ##P## in PA, then writing: "##P## is independent of PA" simply seems to mean that PA will never prove ##P## or ##\neg P##. This seems like a matter of running a simple algorithm to check whether a certain string will be printed or not.
I could be mistaken and missing something important. However, my "reasonable" guess is that PA should be strong enough to do that. That is, it should be strong enough to represent the statement ##B## where: "##B##: ##P## is independent of PA" ... where ##P## is chosen to be any specific proposition in PA.