I Are there unprovable theorems with unprovable unprovability?

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

 

[SSequence]

=====1===== Re-writing post#28:
$B$: $P$ is undecidable in $S$
$A$: $B$ is undecidable in $S$

If $P$ is decidable in $S$ then we can conclude $B$ as false. Also, $S$ would also disprove $B$ in that case. Therefore $A$ is false. $S$ also disproves $A$ in that case. Hence we have:
$\neg B \rightarrow \neg A$
$A \rightarrow B$ (contrapositive)

=====2===== Now assume $A$ to be true. Then we get:
$\mathrm{true} \rightarrow B$

Which means that $B$ is true. Thus $B$ is decidable in $S$ (how is this step justified?). However, since $A$ is true $B$ should be undecidable in $S$. Since that's a contradiction, $A$ can't be true. Therefore $A$ is false and $B$ is decidable.

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

Now let's try to look through the steps carefully. Via truth-table, we have the following four possibilities for $A$ and $B$.
(a) $A$ true, $B$ true
(b) $A$ true, $B$ false
(c) $A$ false, $B$ true
(d) $A$ false, $B$ false

In part-1 (which I labeled above), you correctly showed that when $B$ is false then we have $A$ as false too. As you can observe that this rules out possibility-(b) from our table. Hence we can rightly conclude $\neg B \rightarrow \neg A$ and $A \rightarrow B$.

In part-2 you assumed to be $A$ and (essentially) tried to conclude that possibility-(a) can't occur. If that works, then we could conclude $A$ to be false and $B$ to decidable. However, on the very least, taking $S$ to be $PA$ and under the assumption of $PA$ being sound, we can find sentences $P$ such that $B$ is undecidable in $PA$ [discussed in post#35].

Also, I can't quite see the reasoning behind the step from $B$ being true to concluding $B$ being decidable (this is what I highlighted). All the other steps look OK to me (if I haven't missed something).

 

[Office_Shredder]

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.

The way I think about this, is that the set of finite length strings you can write down are countable, so the set of real numbers that can actually be identified by the system is countable. The other ones... exist... but are still somehow beyond our ken (even though we both agree we understand exactly what they all look like). Similarly most 1-1 functions between uncountable infinite sets cannot be written down either (and here, we have no idea what they look like). So in what sense could you iterate through all of them and accomplish some task?

 

[SSequence]

@Office_Shredder
This is an interesting and very difficult [at least when we try to consider a question like this in full generality] question in general. My suggestion is that perhaps you could make a separate thread about this (essentially with your last post as OP). I feel that way discussion about this could be more focused (which is required for a difficult question of open-ended nature like this one)?