- #1

- 145

- 5

- I
- Thread starter Gjmdp
- Start date

- #1

- 145

- 5

- #2

jedishrfu

Mentor

- 12,022

- 5,672

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.

- #3

- 145

- 5

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

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.

- #4

fresh_42

Mentor

- 13,457

- 10,516

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.@fresh_42 would have better insight into this.

- #5

jedishrfu

Mentor

- 12,022

- 5,672

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,

- #6

- #7

- 145

- 5

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

- #8

fresh_42

Mentor

- 13,457

- 10,516

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

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.

- #9

fresh_42

Mentor

- 13,457

- 10,516

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

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

- #10

jedishrfu

Mentor

- 12,022

- 5,672

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.

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.

Last edited:

- #11

Stephen Tashi

Science Advisor

- 7,353

- 1,354

It's hard to make this question precise. I can't do it, but perhaps stumbling around will help someone else do it.This is, are there theorems for which we can't ever proof that no proof exists for them?

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

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?

- #12

- 448

- 51

Good point. I think that this clarifies the question statement.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".

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.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 implementedwithinthat formal system. His proof, in a manner of speaking, is done by someone standing outside the formal system.

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

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

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:

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.

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

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

From the point of view of set theory though, "true but unproveable statements" is thought a bit differently. Either some statement is a

As you probably knowNo. The undecidable statements are very likely so complicated that nobody ever has any interest in their truth value.

Last edited:

- #13

- 145

- 5

- #14

- 448

- 51

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

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.

Last edited:

- #15

Stephen Tashi

Science Advisor

- 7,353

- 1,354

Double negatives are difficult to parse.I would like to ask whether is there some research/papers on the unprovability of the unprovability of some true statements.

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?

- #16

- 145

- 5

You are right. A better description of what I meant is the undecidability of undecidable 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?

- #17

TeethWhitener

Science Advisor

Gold Member

- 1,846

- 1,186

http://jdh.hamkins.org/are-all-godel-sentences-equivalent/

- #18

Stephen Tashi

Science Advisor

- 7,353

- 1,354

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

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.

- #19

TeethWhitener

Science Advisor

Gold Member

- 1,846

- 1,186

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.

- #20

- 145

- 5

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?

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?

Last edited:

- #21

TeethWhitener

Science Advisor

Gold Member

- 1,846

- 1,186

- #22

- 29

- 0

- #23

nomadreid

Gold Member

- 1,451

- 142

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

- #24

Stephen Tashi

Science Advisor

- 7,353

- 1,354

Standard logic deals withLet A, B be questions answered with "yes" or "no":

B: is P undecidable?

A: is B undecidable?

You mean that "TheIf P is decidable, then B is "no"

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

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!

Last edited:

- #25

yossell

Gold Member

- 365

- 16

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.

- Last Post

- Replies
- 2

- Views
- 625

- Last Post

- Replies
- 8

- Views
- 31K

- Last Post

- Replies
- 4

- Views
- 2K

- Replies
- 1

- Views
- 714

- Replies
- 1

- Views
- 1K

- Replies
- 6

- Views
- 20K

- Replies
- 1

- Views
- 3K

- Replies
- 1

- Views
- 1K

- Last Post

- Replies
- 9

- Views
- 3K

- Last Post

- Replies
- 3

- Views
- 2K