Are there unprovable theorems with unprovable unprovability?

[Gjmdp]

This is, are there theorems for which we can't ever proof that no proof exists for them? That would mean that there might be theorems that, no matter how much effort we put into proving/disproving/proving their unprovability, will always remain open. I would like to know whether there is some research into this question, and whether it might seem like there are such type of theorems.

 

[jedishrfu]

I think you're getting overly confused with the terminology. Godel's theorem pretty much sums this up.

https://en.wikipedia.org/wiki/Gödel's_incompleteness_theorems

In any system logic there are things that can't be proven that means we can't prove they are true or false after that there is nothing more to prove.

@fresh_42 would have better insight into this.

 

[Gjmdp]

I think you're getting overly confused with the terminology. Godel's theorem pretty much sums this up.

https://en.wikipedia.org/wiki/Gödel's_incompleteness_theorems

In any system logic there are things that can't be proven that means we can't prove they are true or false after that there is nothing more to prove.

@fresh_42 would have better insight into this.

Yes, but after we prove that they are unprovable there is nothing more to do and we can leave the problem. However, what would happen if there is no such proof of its unprovability? This is, its unprovability is unprovable. We would never come up with a proof that tells us we can't proof the theorem and hence the theorem would always remain open (with useless efforts of mathematicians trying to provide any insight to the problem).

 

[fresh_42]

This is, are there theorems for which we can't ever proof that no proof exists for them? That would mean that there might be theorems that, no matter how much effort we put into proving/disproving/proving their unprovability, will always remain open. I would like to know whether there is some research into this question, and whether it might seem like there are such type of theorems.

We wouldn't call such statements theorems. Theorems do have a proof.

@fresh_42 would have better insight into this.

I'm afraid not. Your reference to Gödel answers the question. Just a remark. This is an existence proof. It is not constructive, hence we cannot name such statements. It is believed that what usually occurs as conjectures in mathematics, which is a tiny part of all possible statements, can either be proven or a counterexample can be found. Even if it takes 350 years.

 

[jedishrfu]

While not answering your question directly, I present this discussion as an aside from math exchange:

https://math.stackexchange.com/questions/2027182/how-do-we-prove-that-something-is-unprovable

I don't think we can know whether we will ever have a prove for something that is unprovable. We know that some proofs consider all such cases as in the 4 color problem. Each case was exhaustively analyzed by a computer program and at the conclusion of its run we knew it to be true ( I left out a lot of related work here like trusting the program considered all cases and was properly debugged...).

However, we know there is the issue of P=NP where we have yet to determine if its true or not. I suspect that would come into play to answer your question.

The best way to prove something is false is to find a counter example so if someone says something is unprovable and we find a counter example then I guess we are done.

Calling @fresh_42 Mayday Mayday Mayday,

 

[jedishrfu]

Thanks, @fresh_42 I was afraid of drowning in the sea of incompleteness. Fortunately, I'm a robot and require little oxygen. My only limit is the pressure at depth. :-)

 

[Gjmdp]

We wouldn't call such statements theorems. Theorems do have a proof.

I'm afraid not. Your reference to Gödel answers the question. Just a remark. This is an existence proof. It is not constructive, hence we cannot name such statements. It is believed that what usually occurs as conjectures in mathematics, which is a tiny part of all possible statements, can either be proven or a counterexample can be found. Even if it takes 350 years.

Isn't it pessimistic that some problems will remain open forever and we won't have a clue about whether they can be proved or not? Maybe we won't ever know whether there is a proof or disproof for problems such as P vs NP...

 

[fresh_42]

However, we know there is the issue of P=NP where we have yet to determine if its true or not. I suspect that would come into play to answer your question.

Calling @fresh_42 Mayday Mayday Mayday,

Lol. I remember a bet between Strassen and someone else whose name I don't remember, maybe von zur Gathen. Anyway, Strassen claimed that $NP\neq P$ would have been proven until some date in the late 90's. Well, that balloon trip across the Alps (the prize) long took place.

I think there is more to it than just a mathematical statement. Nobody believes in $NP=P$ or that the $ERH$ could be false. $ERH$ is apparently difficult to prove, but I don't think impossible. Maybe it's similar to $FLT$, and we need to develop the right tools first. $NP\neq P$ is different as it is generally very hard to prove non existence. We need a significant lower bound, i.e. we have to prove that something is really difficult, and we are not just too stupid to solve. This has a philosophical dimension: Where are our limits?

But all these examples are easy to phrase and because of this, they should be decidable. Maybe the independence of $AC$ from $ZF$ is the closest example we can ever get.

 

[fresh_42]

Isn't it pessimistic that some problems will remain open forever and we won't have a clue about whether they can be proved or not?

No. The undecidable statements are very likely so complicated that nobody ever has any interest in their truth value. Of course you can always phrase a task that is too big to be done, e.g. "classify all nilpotent groups". But that has nothing to do with decidability. A possible solution is simply far too long to write down.

Maybe we won't ever know whether there is a proof or disproof for problems such as P vs NP...

I doubt that.

 

[jedishrfu]

Yes, but this is life and we always hope that someday we will find a way around it.

There are many examples of inconsistencies in our math and science that we must live with until a better scheme comes along. By better, I mean it handles all that we know in a field, handles new stuff and eliminates old inconsistencies. However, I'm sure new ones will appear so that we are assured of future work for our mathematicians and scientists.

I just read recently where there is still debate on the lowly radian as to whether its dimensionless or not and how that causes some inconsistency in our physics formulas that may use it.

 

[Stephen Tashi]

This is, are there theorems for which we can't ever proof that no proof exists for them?

It's hard to make this question precise. I can't do it, but perhaps stumbling around will help someone else do it.

First we should change "theorems" to the phrase "true, but unprovable statements".

Technically, Godel's result applies only to particular formal systems. I can't state the restrictions on those systems without looking them up!

Let's assume we have straightened out the above issues. Then there is the simpler question of what it means to prove a true statement can't be proven. As I understand it, Godel treats a formal system, but his reasoning is not implemented within that formal system. His proof, in a manner of speaking, is done by someone standing outside the formal system.

If that's the case then where would a person stand to prove "it can't be proven that statement x is unprovable"? We'd have to consider a formal system S1 and another formal system S2 such that S2 deals with proving things in formal system S1 are unprovable. If we want to use Godel's reasoning to analyze S2 then S2 must satisfy the restrictions specified in Godel's theorem (which I have neglected to look up). So does a formal system S2 that implements Godel's reasoning about S1 satisfy the restrictions required by Godels theorem? I don't know. Can we nest one Godel on top of another?

 

[SSequence]

It's hard to make this question precise. I can't do it, but perhaps stumbling around will help someone else do it.

First we should change "theorems" to the phrase "true, but unprovable statements".

Good point. I think that this clarifies the question statement.

Let's assume we have straightened out the above issues. Then there is the simpler question of what it means to prove a true statement can't be proven. As I understand it, Godel treats a formal system, but his reasoning is not implemented within that formal system. His proof, in a manner of speaking, is done by someone standing outside the formal system.

That's right. Though "if" we take $F$ to be sound then the truth of godel statement will be evident. Evident from the "outside" but still evident.

=======================

Also assuming $F$ to be consistent, $F$ won't be able to prove $con(F)$. That's all that godel's theorem says by itself. But that does not mean that we can't prove $con(F)$ by "some other means" that we can be highly/absolutely certain about. For example, con(PA) is known truth. As I have read based upon how proof ordinals are derived, it seems to me that the same would be true for good number of other systems which have a "very well-understood" notation.

Whether there are true but unproveable statements (in "some" absolute sense) is different and is related to assumption (or lack of it) of excluded middle over a certain "domain of problems".Note1:
There are two (or more I think?) variations of godel's theorems (it is assumed that the conditions required for F in the theorems are satisfied). At least two of them are:
(a) $F$ is sound [regarding natural numbers at least]
So first and second theorem are:
(1a) "If F is sound then F is incomplete."
(2a) "If F is sound then con(F) can't be proved in F."

One thing to note is that it is easy to see that we have 2a→1a.

(b) $F$ is consistent
So first and second theorem are:
(1b) "If F is consistent then F is incomplete."
(2b) "If F is consistent then con(F) can't be proved in F."

For example, for a proof of (2b) see this older post by @stevendaryl (post#7) https://www.physicsforums.com/threads/godel-and-diagonalization.904105. (also disregard my posts after post#9 in that thread ... I am somewhat confused there since it was a more difficult point).

Note2:
Then there is more complicated issue of $\omega$-consistency. I am definitely "fuzzy" about this so I don't want to confuse/mislead anyone here. Based on what little I know essentially $\omega$-consistency would imply usual consistency (for some formal system F) but the converse may not necessarily be true. That is, for some system F, consistency may not imply $\omega$-consistency.

Intuitively, seemingly, lack of $\omega$-consistency seems to mean that there is no model of F whose natural numbers are the same as our usual ones (or possibly, some meaning close to it).

Note3:
From the point of view of set theory though, "true but unproveable statements" is thought a bit differently. Either some statement is a (i) Provable in ZFC (true in every model) (ii) Disprovable (false in every model) (iii) Can't be proved or disproved. In that case it may be true in some models and false in others.

No. The undecidable statements are very likely so complicated that nobody ever has any interest in their truth value.

As you probably know [but maybe perhaps some people may not have read], Harvey Friedman has spent significant effort on hundreds of simple statements that are independent of set theory. As to how simple they can be considered or not, since "simple" is a natural language concept I guess it would depend on interpretation of it.

 

[Gjmdp]

I would like to ask whether is there some research/papers on the unprovability of the unprovability of some true statements. It seems like an important concept in Mathematics, but haven't found much research/interest on it.

 

[SSequence]

I would like to ask whether is there some research/papers on the unprovability of the unprovability of some true statements. It seems like an important concept in Mathematics, but haven't found much research/interest on it.

It seems to me that terms like "independence"/"undecidability***1" seem to be close to what you are trying to write. If it isn't that then I am not sure what you are trying to look for.

So when you write "unprovability of some true statements", one reasonable interpretation of it is statements that are unproveable in some formal system but are "actually true". If we are talking about set theory then one can talk about (large) cardinals etc. Also see the end of post#12. But these are quite advanced topics (I am not even remotely close to getting to them).

What I tried to write in last paragraph about "actually true" can be a bit tricky though. Most mathematicians would regard arithmetic/number-theoretic statements to be either true or false [interpreted in a model whose "natural numbers" really are finite ordinals]. But, in general, when independence triggers (in set theory) for statements outside of these [for example, such as CH] the views on these can diverge greatly [it would depend on the nature of the specific statement, I guess]. I do not what is general view on this [that is, independence (from set theory) of number-theoretic vs. non number-theoretic statements]. Nor I have enough knowledge on this to give an informed comment.

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.***1 Undecidability of course can have two different meanings: (i) lack of provability/unprovability of a (specific) statement in certain formal system (ii) undecidable as in an "undecidable set". Most people are aware of this distinction, but for someone new to this it may be helpful to point it out.

 

[Stephen Tashi]

I would like to ask whether is there some research/papers on the unprovability of the unprovability of some true statements.

Double negatives are difficult to parse.

Suppose we have a formal system S1 and a statement s that is True in S1. If S1 is consistent and s is provable in S1 then we cannot prove that s is unprovable in S1. So this is the trivial case of the "unprovability that s is unprovable". That satisfies your double negative in a trivial manner. We can't prove that provable statements are unprovable - in whatever system S2 we are using to reason about S1 if system S2 is consistent.

The trivial case seems unworthy of a research paper. Can you give an example of a nontrivial case?

 

[Gjmdp]

Double negatives are difficult to parse.

Suppose we have a formal system S1 and a statement s that is True in S1. If S1 is consistent and s is provable in S1 then we cannot prove that s is unprovable in S1. So this is the trivial case of the "unprovability that s is unprovable". That satisfies your double negative in a trivial manner. We can't prove that provable statements are unprovable - in whatever system S2 we are using to reason about S1 if system S2 is consistent.

The trivial case seems unworthy of a research paper. Can you give an example of a nontrivial case?

You are right. A better description of what I meant is the undecidability of undecidable statements.

 

[TeethWhitener]

Joel David Hamkins has an interesting blog post on the uniqueness of Godel sentences under different notions of provability:
http://jdh.hamkins.org/are-all-godel-sentences-equivalent/

 

[Stephen Tashi]

You are right. A better description of what I meant is the undecidability of undecidable statements.

Undecidable statements are undecidable by definition. So the description needs more work to avoid triviality.

I don't think you should immediately give up on your question. Trying to make it nontrivial may teach us all things about formal logic.

 

[TeethWhitener]

You might also take a look at provability logics:
https://plato.stanford.edu/entries/logic-modal/#ProLog
The idea is to adapt the semantics of modal logic into a framework which models provability in the Gödelian sense. So $\Box A$ would mean “A is provable,” rather than the standard “A is necessary.” $Con(F)$ would be expressed as $\neg \Box \perp$. And Godel’s second incompleteness theorem would assert:
$\neg\Box\perp\rightarrow\neg\Box\neg\Box\perp$
In a sense similar to @Stephen Tashi ’s post above, this already kind of answers OP’s question. From the above semantics: consistency simply means a contradiction is unprovable. So Godel’s second theorem states that consistency implies non-provability of consistency. Or in other words, if a contradiction is unprovable, then it is unprovable that a contradiction is unprovable.

 

[Gjmdp]

I came up with a proof for that there the undecidability of statements is decidable:

Let A, B be questions answered with "yes" or "no":

B: is P undecidable?
A: is B undecidable?

If P is decidable, then B is "no". Hence B is decidable, thus A is "no". This means that P decidable -> (A = "no").

("->" means implication)

Assume A = "yes", P is undecidable since

P decidable -> (A = "no")
(P decidable->0) has to evaluate to 1 => (P decidable) = 0

Which means that B = "yes". However since A = "yes", B should be undecidable. Contradiction. Hence A can't be "yes".

Is this correct?

 

[TeethWhitener]

The logical manipulations seem fine, but as others have said, this is probably going to depend on how the predicate “decidable” behaves. (Also, as others have said, “decidable,” “provable,” etc., aren’t necessarily synonymous.) Does “decidable” imply an algorithmic decision procedure? Then it might not be trivial to say that “It is decidable that p is undecidable.” I don’t know; I’m not a complexity theorist. In terms of Gödelian provability, your argument seems to follow a similar line to Godel’s 2nd theorem, and I already showed a context where you run into trouble: what if P is a contradiction? Then the logical manipulations are meaningless because the entire system is a tautology. These questions are ultimately going to boil down to very fundamental questions about what properties you allow your predicates to have.

 

[H_A_Landman]

Any statement S which is logically equivalent to "S is unprovable" cannot consistently be proven to be unprovable. Because if you could prove that, then you would also have proven S to be true, which would mean that it's provable and hence not unprovable.

 

[nomadreid]

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.

For example, unless it is a contradiction, any meaningful statement that is unprovable in one system of axioms is provable in another (just as any meaningful statement that is not a tautology that is provable in one system of axioms is unprovable in another). Any meaningful statement that is undecidable in one system is true in another and false in yet another.

(Relevant as well: any meaningful statement which is not a contradiction is true under some interpretation, just as any meaningful statement which is not a tautology is false under some interpretation.)

A good example is the continuum hypothesis: undecidable under the standard axioms of set theory (ZFC), provable in Gödel's constructible universe, and unprovable using forcing (e.g., Cohen's). Each one of these assertions is provable in systems which are more powerful than the respective systems of the statement.

Or, a rough statement: the statement that arithmetic is consistent is unprovable using (the same system of) arithmetic, but is provable using algebra.

One may look at all this as restrictions, but in a positive way, just as a composer understands the particular system in which she is trying to compose music.

Finally, this gives me a chance to quote one of my favourite mathematics jokes: "The Axiom of Choice is obviously true, the Well-ordering Theorem is obviously false, and I am unsure about Zorn's Lemma."

 

[Stephen Tashi]

Let A, B be questions answered with "yes" or "no":

B: is P undecidable?
A: is B undecidable?

Standard logic deals with propositions. A proposition must be either True or False and cannot be both True and False. Not all English sentences are propositions. Not all sentences that give a "yes" or "no" answer are propositions. So you don't have a proof until you can demonstrate that P, B and A are propositions.

If P is decidable, then B is "no"

You mean that "The answer to B is 'no'". But is the answer a proposition?

Sentences with unquantified variables in them are not propositions. For example, "x > 7" is not a proposition unless we are in context where "x" is known to be a specific number. The term for expressions like "x > 7" is propositional function. A propositional function can used to form a proposition by quantifying it. For example, "There exists a number x such that x >7" and "For each number x, x > 7" are each propositions. (One of them is True and one of them is False.) In your proof, you must establish that the letters represent specific propositions. They can't represent unquantified variables.

What is an "undecidable" proposition? What's the difference between an "undecidable" proposition and an "unprovable" proposition? We can't give technical definitions to these concepts by thinking of life and mathematics in general!

 

[yossell]

I'm not sure about some of the assertions that have been made here.

The Godel formula is not non-constructive. It's mathematically artificial, but it can be written down.

There are arithmetically 'natural' statements which are not provable in PA. Such as the Paris-Harrington theorem.

https://en.wikipedia.org/wiki/Paris–Harrington_theorem
_________

P vs NP may indeed be undecidable.

e.g https://www.scottaaronson.com/blog/?p=1948
_______

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'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.
_______________

Godel's argument can indeed be formalised within PA. PA can prove that, if PA is consistent, then the Godel sentence is neither provable nor refutable. But, of course, as PA cannot prove its own consistency (providing it is consistent!), it cannot prove the Godel sentence itself.

However, a stronger statement -- that there are truths of PA that are not provable -- is not provable within PA. Luckily, that's not Godel's theorem.
________

Godel's original proof did indeed assume w-consistency. But an improvement due to Rosser managed to weaken w-consistency to consistency.

 

[zinq]

There very well may be true statements (such as, about the integers) that cannot be proved true and cannot be proved unprovable (with a given system of axioms).

One candidate for this is the Twin Prime Conjecture (TPC), which states that there exists an infinite number of pairs of prime numbers (p,q) such that q-p = 2. Like (3,5), (5,7), (11,13), (17,19), etc. There is no question but that it is either true, or else it is false. (Because we can imagine an infinite verification that runs through all positive integers n testing n and n+2 for whether they are both primes. At the end of this hypothetical verification it would be known whether the total number of them was finite.)

Whether TPC is true or false, it may be that this is the case for nothing that we would ordinarily consider to be a "reason", but only that by pure chance the occurrences of prime numbers just happens to permit, or not permit, an infinite number of twin primes. But this may be totally incorrect, since related theorems have been proven in recent years as an outgrowth of a theorem of Yitang Zhang in 2013.

The best improvement so far on Zhang's original theorem proves that the smallest number K such that [For infinitely many prime numbers p, the next prime number is P+K] satisfies K ≤ 246. (This number has not been improved since 2014.)

 

[yossell]

There is no question but that it is either true, or else it is false. (Because we can imagine an infinite verification that runs through all positive integers n testing n and n+2 for whether they are both primes. At the end of this hypothetical verification it would be known whether the total number of them was finite.)

But there is a question about such 'infinite' verifications. We can't complete an infinite process and so there's a question whether we can talk about verification here.

For instance, would you argue that the continuum hypothesis is either true or false because you can just run through all the 1-1 functions between the set of well orderings and the powerset of the natural numbers and at the end of this hypothetical verification it would be known whether they had the same cardinality. Sure, it's a bigger cardinality to run through -- but is there any principled reason for allowing that we can imagine an infinite verification for one and not the other?

 

[Gjmdp]

I will try again. I have read carefully all your posts and I am still trying to learn about this topic, I am sorry if I still make basic mistakes. Since I am not familiar with decidability (I am familiar with it only in the context of computability), I will refer to provability of statements.

$\textbf{Proof of the existence of a proof of the unprovability of unprovable statements.}$

Let $P$ be an arbitrary proposition and $S$ a formal system.

$Definition$: A statement is $provable$ in $S$ if there is a proof (in $S$) for whether it is true or false.

Let $A$ and $B$ be the following propositions:

$B$: "$P$ is unprovable in $S$"
$A$: "$B$ is unprovable in $S$"

If $P$ is provable in $S$, then $B$ is $false$. Hence $B$ would be provable in $S$, thus $A$ would be $false$. We then deduce that:
(1) ("$P$ is provable in $S$") $\rightarrow$ ($A$ = $false$).

Assume $A$ = $true$. $P$ should be unprovable since from (1) and ($A$ = $false$) = $false$:

("$P$ is provable in $S$" $\rightarrow$ $false$) has to evaluate to $true$ $\implies$ ("$P$ is provable in $S$") = $false$

Which means that $B$ = $true$, thus $B$ is provable. However since $A$ = $true$, $B$ should be unprovable on $S$. We found a contradiction. Hence $A$ can't be $true$, thus $B$ is provable.

Hence if a proposition $P$ can't be proven to be true or false in $S$, we can always come up with a proof that guarantees us this unprovability.

 

[TeethWhitener]

Hence B would be provable in S,

This statement is problematic for me. It might be the case that B is provable (in some system), but saying that B is provable in S requires some assumptions about what S can and cannot talk about. Whether this difficulty can be overcome, I don’t know off the top of my head. But I’m not convinced it’s that simple.

 

[Gjmdp]

This statement is problematic for me. It might be the case that B is provable (in some system), but saying that B is provable in S requires some assumptions about what S can and cannot talk about. Whether this difficulty can be overcome, I don’t know off the top of my head. But I’m not convinced it’s that simple.

You are right. I guess you could just assume S is complex enough to discuss about provability of statements (like in ZFC).

 

[zinq]

yossell wrote: "But there is a question about such 'infinite' verifications. We can't complete an infinite process and so there's a question whether we can talk about verification here.

"For instance, would you argue that the continuum hypothesis is either true or false because you can just run through all the 1-1 functions between the set of well orderings and the powerset of the natural numbers and at the end of this hypothetical verification it would be known whether they had the same cardinality. Sure, it's a bigger cardinality to run through -- but is there any principled reason for allowing that we can imagine an infinite verification for one and not the other?"

I'm a mathematician who believes in infinite sets and doesn't worry about the fact that a human being cannot complete an infinite process in the real world. Your mileage may vary.

I came up with the idea of verifying (or not) the Continuum Hypothesis (CH) almost exactly in the way you are describing about 50 years ago, and I absolutely would argue that CH is necessarily either really true or really false for that reason. Independent of our ability to ever prove it.

I have found that many mathematicians accept the idea of a countably infinite verification for, say, TPC, but will not accept one of larger cardinality, such as for CH — exactly the two examples that I usually use when discussing this subject.

So to answer your last question, I do not see any principled reason to accept a countably infinite verification but to reject one of higher cardinality.

 

[Stephen Tashi]

$\textbf{Proof of the existence of a proof of the unprovability of unprovable statements.}$

That statement needs logical quantifiers. Do you asserting the nonexistence of any proof for the unprovability of at least one unprovable statement? Or are you asserting the nonexistence of any proof for any unprovable statement I wish to choose?

Let $P$ be an arbitrary proposition and $S$ a formal system.

So you are dealing with any $P$ that I wish to choose.

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.

$Definition$: A statement is $provable$ in $S$ if there is a proof (in $S$) for whether it is true or false.

Let $A$ and $B$ be the following propositions:

$B$: "$P$ is unprovable in $S$"

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.)

$A$: "$B$ is unprovable in $S$"

The self-referential caution also applies to the definition of $A$.

If $P$ is provable in $S$, then $B$ is $false$. Hence $B$ would be provable in $S$

Normally we don't introduce discussions in a theorem that contradict the hypothesis of the theorem. (The theorem you stated deals only with case where $P$ is unprovable.)

However, I understand that you need to say something and it's easier to say it in a "positive" version than in a "negative" version.

You are using "the logic of properties". In that logic we abbreviate the proposition that a thing has a property with notation like $Q(x)$ to indicate "x has the property Q". Let's use $prov(x)$ to mean "x has the property of being provable".

You are using the assumption that provability obeys the law
$((B \equiv prov(P)) \land prov(P) ) \implies prov(B)$

(Here the notation $X \equiv Y$ does not indicate $X$ and $Y$ have identical properties for whatever properties we wish to consider. It only indicates that $X$ and $Y$ have the same property as far as Truth or Falsity goes. )

I think this is a reasonable assumption if all the proposition involved exist in $S$, but it needs to be explicitly stated.

thus $A$ would be $false$. We then deduce that:(1) ("$P$ is provable in $S$") $\rightarrow$ ($A$ = $false$).

Better notation is $\lnot B \implies \lnot A$

Assume $A$ = $true$. $P$ should be unprovable since from (1) and ($A$ = $false$) = $false$:

("$P$ is provable in $S$" $\rightarrow$ $false$) has to evaluate to $true$ $\implies$ ("$P$ is provable in $S$") = $false$
Which means that $B$ = $true$, thus $B$ is provable.

More concisely, the principle called "contraposition" says that $x \implies y$ is logically equivalent to $\lnot y \implies \lnot x$. Let $x$ be $\lnot A$ and let $y$ be $\lnot B$. By contraposition we get $A \implies B$.

However since $A$ = $true$

It's hard to follow the proof at this point because it isn't clear which assumptions are in force. Are we assuming $prov(P)$ or are we assuming $\lnot prov(P)$ ?

...
Hence if a proposition $P$ can't be proven to be true or false in $S$, we can always come up with a proof that guarantees us this unprovability.

I think you are saying Let $B \equiv \lnot prov(P)$ Then $\lnot prov(P) \implies prov(B)$.

Let $B = \lnot prov(P)$. If the formal system $S$ contains the logical principle $X \implies X$ then $\lnot prov(P) \implies \lnot prov(P)$ That is a proof of $B$ (provided we are assuming $\lnot prov(P)$ is True). So we conclude $\lnot prov(P) \implies prov(B)$.

 

[SSequence]

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:

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.

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).

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).

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...

$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"

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.

 

[SSequence]

OK the previous post was discussing various point. Just to bring some focus on the part related to OP's puzzle posted in post#20 and post#28.

Let $P$ be a true/false statement expressible in PA. Let's focus on the following statement:
$B$: "$P$ is independent of $PA$"

That is, $B$ is true if, for example, $P$ is a statement which PA can neither prove or disprove. For example, if $P$ was con(PA) then $B$ would be true.

While if $P$ be a correct but relatively simpler number-theoretic proposition for example [say something encountered as a routine exercise/lemma in an elementary course] then $B$ would be false. That's because, in that case, $P$ would be proveable in PA.

====================

Now as I mentioned towards the end of last post (also mentioned in post#29,32), the first thing we need to consider is whether the statement $B$ is expressible in PA or not. As I mentioned in the end of last post, $B$ does seem to be likely to be expressible in PA.

So I thought I would ask this as a question on MSE (to remove any doubt about expressibility of $B$). But it seems a simple search seemed to confirm that $B$ is indeed expressible in PA (hence there doesn't seem to be a need to ask such a question). Here is the link [1] I found.

So assuming the formal system $S$ in post#28 to be PA, both the statements $B$ and $A$ should be expressible in PA. Now one would need to look carefully to see what the OP tried to prove there (and whether all the steps are warranted).[1] To paraphrase the gist of question linked [I am not quite getting reasoning in the answer (which I presume is correct, since it is written by an experienced user) ... even the first part of it].

The question stated a unary predicate [open predicate with one variable] which was:
Undec(x) is true iff x is the (godel) number of sentence which is independent of PA

Now if $P$ is some true/false sentence that is expressible in PA, it will have some number. Let's say is 100. So we could write:
Undec(100) is true iff 100 is the (godel) number of sentence which is independent of PA

Rewriting it we get:
Undec(100) is true iff $P$ is independent of PA

Hence Undec(100) is basically the statement $B$ mentioned in the beginning of post. As mentioned in the question the predicate Undec(x) is expressible in PA. Hence $B$ is expressible in PA.

 

[SSequence]

Making a new post because I can't edit the previous one. OK I think I at least understand one aspect a bit better.

The "real" natural numbers are assumed as intended model (as is default when this type of sentence is omitted). The soundness of PA is also an assumption in the post below [note that most of the time only consistency is a required ... so this is def. a stronger assumption].

Once again, as in previous post, let $P$ be a true/false sentence in PA. Also define $B$ to be the statement :
" $B$ is true iff $P$ is independent of PA "
As I described in previous post, $B$ is also expressible in PA. I think I get the idea behind why there are at least some choices of sentences $P$ such that $B$ will also be undecidable in PA [meaning independent of PA ... i.e. PA won't prove or disprove $B$].

Essentially, let's assume $P$ be a goldbach-type statement such that following two properties hold: (1) $P$ is Independent of PA (2) $P$ is true. Note that because $P$ is independent of PA [by property (1) of $P$], we have $B$ as true.
Now we have the following possibilities:
(A) PA proves $B$
(B) PA disproves $B$
(C) PA can't decide $B$ (meaning it can't prove/disprove it)

---------- Consider the possibility-(A) in which PA proves $B$. If PA proves "$P$ is independent of PA" then can PA prove $P$? My guess is that it is very unlikely that this wouldn't be the case [logic behind this in next paragraph]. But now (assuming what I wrote in last sentence holds), if PA proves $P$ then it goes against our assumption of $P$ being independent of PA [property-(1) of $P$ assumed above]. Hence this possibility isn't allowed.

Note that if $P$ is independent of PA then the following reasoning tells us why $P$ cannot be false [and that's why $P$ has to be true by excluded middle]. If $P$ was false then PA would easily prove that to be the case via trivial calculations and hence PA would prove $\neg B$ [leading to ~con(PA)].

---------- Consider the possibility-(B) in which PA disproves $B$. But since $B$ is actually true this goes against the soundness assumption made in the beginning of the post.

---------- Therefore possibility-(C) must be the case.