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