...to prove there is no proof G in F requires a sequence of
inference steps that prove that they themselves do not exist. — PL Olcott

G is not a deduction in F. That would be silly.

Rather, Gödel shows using arithmatization and the diagonalization that the structure of F is such that there must be WFF such as G. He's not using the deductive power of F to prove that G is unprovable.

When Carol says "no" indicating that "no" is an incorrect answer
this makes "no" the correct answer thus not incorrect thus Carol is wrong. — PL Olcott

I gave you a perfectly acceptable alternative interpretation of what is happening (which you did not address). You are just applying an interpretation without any context or justification of why it MUST be taken that way; what appears to you as formal logic is just an implication you see as self-evident and singular, when it is just your imposed requirement.

Carol does not need to be “indicating… an incorrect answer”, she could be indicating there IS NO sense of correctness in this “question”, and thus how CAN she “answer” at all—the “correct” “answer” is to throw up her hands and say “no”, as if to say: “What?”. Another way to interpret this is that, of course, Carol CAN answer ‘no’, she can say whatever she wants, defying your idea of correctness with her own truth to herself, in protest. But with no world, you make the rules, so, sure, make them however you’d like. What you’ve proven is that such a question must be in an abstract environment with closed dictated rules, as if playing with a machine you programmed. So why bring a human (poor Carol) into it?

she could be indicating there IS NO sense of correctness in this “question”, and thus how CAN she “answer” at all—the “correct” “answer” is to throw up her hands and say “no”, as if to say: “What?”. Another way to interpret this is that, of course, Carol CAN answer ‘no’, she can say whatever she wants, defying your idea of correctness with her own truth to herself, in protest. — Antony Nickles

Exactly. That's what I attempted to explain to @PL Olcott, but it is impossible to agree with him, because according to his point, there will always be an incorrect answer because the question is 'posed' to Carol. It seems that poor Carol is guilty of everything regarding this tricky dilemma!

You have Carol not playing the game. I wouldn't play , either. Fair call.

G is not a deduction in F. That would be silly.

Rather, Gödel shows using arithmatization and the diagonalization that the structure of F is such that there must be WFF such as G. He's not using the deductive power of F to prove that G is unprovable. — Banno

In other words Gödel uses a convolulted mess to show THAT G IS unprovable in F
in F while carefully hiding WHY G is unprovable in F.

Antinomy It is a term often used in logic and epistemology, when describing a paradox or
unresolvable contradiction. https://www.newworldencyclopedia.org/entry/Antinomy

Gödel acknowledges that his G is {a proposition which asserts its own unprovability}
and also acknowledges that any {epistemological antinomy} (self-contradictory G) will do.

...14 Every epistemological antinomy can likewise be used for a similar undecidability proof...
...We are therefore confronted with a proposition which asserts its own unprovability. 15 ...
(Gödel 1931:43-44)

Gödel, Kurt 1931.
On Formally Undecidable Propositions of Principia Mathematica And Related Systems

https://mavdisk.mnsu.edu/pj2943kt/Fall%202015/Promotion%20Application/Previous%20Years%20Article%2022%20Materials/godel-1931.pdf

Carol does not need to be “indicating… an incorrect answer”, she could be indicating there IS NO sense of correctness in this “question” — Antony Nickles

Her answer of "no" indicates that she cannot correctly answer "no"
yet because "no" is the correct answer her answer of "no" is incorrect.

Can Carol correctly answer “no” to this [yes/no] question?
The revised question requires Carol to answer from the solution set.
Any lack of answer from {yes, no} or answer from {yes,no} is not a
correct answer.

Carol's question was written by a PhD computer science professor to show
that the halting problem specification is inconsistent.

I have spoken with him directly many times and he agrees with me that an
equivalent way of saying this is that input D to decider H makes this question:
"Does your input halt on its input?" a self-contradictory thus incorrect question
for H when D is defined to do the opposite of whatever H says.

Exactly. That's what I attempted to explain to PL Olcott, but it is impossible to agree with him, because according to his point, there will always be an incorrect answer because the question is 'posed' to Carol. It seems that poor Carol is guilty of everything regarding this tricky dilemma! — javi2541997

Can Carol correctly answer “no” to this [yes/no] question?

Was written by a PhD computer science professor as an analogy to the
conventional halting problem proofs where an input D has been defined
to do the opposite of whatever program H says.

His purpose in doing this was to show that because the question
"Does your input halt on its input? is self-contradictory for some
program/input pairs that for these pairs it is an incorrect question.

We still agree with everyone else that when an input D does the
opposite of whatever program H says that H cannot correctly say
what input D will do.

The key distinction that we make is that this does not place any actual
limit on computation. That H cannot answer an incorrect question is the
same as the fact that a baker cannot bake a perfect angle food cake
using only house bricks for ingredients. It is incorrect for us to say that
her baking skills are limited on that basis.

As long as you acknowledge that, again, the “solution set” is YOUR requirement, not revealing anything but the answer you dictate. What you have imposed as “correct” suppresses any other interpretation and thus only has one set of answers.

Now of course if you are programming a computer than the terms are set and thus easy to force into a corner, but leave it as a formal logic problem or a programming issue for it says nothing about selves or human contradiction. Yes we have expectations and implications and consequences, but we still live in a culture and answer for ourselves in a specific circumstance with possibilities that we act within, or defy.

As long as you acknowledge that, again, the “solution set” is YOUR requirement, not revealing anything but the answer you dictate. What you have imposed as “correct” suppresses any other interpretation and thus only has one set of answers. — Antony Nickles

Yes this makes it exactly the same as the halting problem's input D
that does the opposite of whatever Boolean value that decider H says.

Since the analogy of Carol's question is much easier to understand
it provides great leverage in understanding the error of the halting
problem proofs

The whole purpose of Carol's question was to show that the halting
problem specification derives a self-contradictory thus incorrect
question for some program/input pairs.

When we show this then the inability of some H to say what
input D will do when D is defined to the opposite of whatever
H says is simply an incorrect question for H.

If some program/input pairs are incorrect questions then the lack
of the ability of H to provide a correct answer is the same as the
lack of the ability of a baker to bake a perfect angel food cake using
only house brick for ingredients.

while carefully hiding WHY G is unprovable in F. — PL Olcott

Well, no. He carefully shows why G is unprovable.

Well, no. He carefully shows why G is unprovable. — Banno

Not at all. Diagonalization only shows THAT an expression
is unprovable, it abstracts away WHY. If we were to formalize
this question: "What time is it (yes or no)?" diagonalization
could show THAT it cannot be correctly answered and have
no idea that the reason WHY it cannot be answered is a type
mismatch error. Diagonalization makes sure to discard these
details.

it abstracts away WHY. — PL Olcott

An odd view.

You would presumably, for consistency's sake, say the same for Turing Machines, Lambda calculus, and Markov Algorithms; each of which have similar issues. Do you also reject the uncountability of the reals?

If so, we might leave this conversation here.

You would presumably, for consistency's sake, say the same for Turing Machines, — Banno

Not at all and now I show my words are sustained by Gödel's words.
The last paragraph is proven by all that comes before it.

My unique take on Gödel 1931 Incompleteness (also self-referential)
Any expression of the language of formal system F that asserts its
own unprovability in F to be proven in F requires a sequence of
inference steps in F that prove they themselves do not exist.

It is not at all that F is in any way incomplete.
It is simply that self-contradictory statements cannot be proven
because they are erroneous.

The most important aspect of Gödel's 1931 Incompleteness theorem are
these plain English direct quotes of Gödel from his paper
...there is also a close relationship with the “liar” antinomy,14 ...
...14 Every epistemological antinomy can likewise be used for a similar undecidability proof...
...We are therefore confronted with a proposition which asserts its own unprovability. 15 ...
(Gödel 1931:43-44)

Gödel, Kurt 1931.
On Formally Undecidable Propositions of Principia Mathematica And Related Systems

https://mavdisk.mnsu.edu/pj2943kt/Fall%202015/Promotion%20Application/Previous%20Years%20Article%2022%20Materials/godel-1931.pdf

Antinomy
It is a term often used in logic and epistemology,
when describing a paradox or unresolvable contradiction.
https://www.newworldencyclopedia.org/entry/Antinomy

Quoted from above
...14 Every epistemological antinomy can likewise be used for a similar
undecidability proof...

...We are therefore confronted with a proposition which asserts its own
unprovability...

Thus in my simple version we can see WHY {a proposition that asserts
its own unprovability} in F cannot be proven in F. It is because such
a proposition is an {epistemological antinomy} in F.

I have also showed that an input D that does the opposite of whatever
program H says is an {epistemological antinomy} for H.

Do you also reject the uncountability of the reals? — Banno

We can map every real to an integer and it does seem that we have some reals left over.
If we imagine that there can be such a thing as immediately adjacent points on a
number line, then these points would map to the integers. 1.0 + infinitesimal would
be the next point on a number line.

You seem to me to be doing no more than recursive assertion. It is because it is because it is because...

The "Why" you are after is simply that there are more WFF, more Turing Machines and more Markov algorithms than can be counted.

Cheers.

↪PL Olcott You seem to me to be doing no more than recursive assertion. It is because it is because it is because... — Banno

{epistemological antinomy} is the end all be all of why for these things.
Professor Hehner calls this exact same idea {inconsistent specification} and
I call this exact same idea {self-contradictory question}. Gödel calls it
{epistemological antinomy}.

When ordinary people hear the term {epistemological antinomy} they translate
it into {some complex thing that I don't understand} in their or internal dialogue.
That is why I use the much clearer term {self-contradictory question}.

That post doesn't tell me anything.

PL Olcott That post doesn't tell me anything. — Banno

The reason why the halting problem is not solvable is that its specification does
not forbid self-contradictory questions. When we change the specification such
the self-contradictory questions cannot exist then the conventional proofs fail to
show that the halting problem is not solvable.

The reason that the halting problem persists is that the number of possible Turing machines is not enumerable; but any Turing machine designed to check for a halt can only check at most an enumerable number of Turing machines. It therefore cannot check if every Turing machine will halt.

The reason that the halting problem persists is that the number of possible Turing machines is not enumerable; but any Turing machine designed to check for a halt can only check at most an enumerable number of Turing machines. It therefore cannot check if every Turing machine will halt. — Banno

That simply changes the subject away from an input deriving a self-contradictory
thus incorrect question for a specific decider. The most favorite rebuttal tactic of
all of my reviewers is to make sure to always change the subject before there is
ever any closure on any point.

Perhaps this indicates that there is a problem with the approach you have taken.

After all, what I said above is the case; that is the reason for the halting problem. One way to treat this is as a reductio, showing that your approach has problems.

After all, what I said above is the case; that is the reason for the halting problem. One way to treat this is as a reductio, showing that your approach has problems. — Banno

When I stopped tolerating infinite digression it ceased.

...a self-contradictory thus incorrect question... — PL Olcott

There are issues here as well, since a question is not the sort of thing that is apt to contradiction. A pair of statements can contradict; some statements can contradict themselves; but questions that are infelicitous are "inappropriate" or "ill-founded" or some such rather than contradictory.

Austin would have a field day.

When I stopped tolerating infinite digression it ceased. — PL Olcott

So again, for consistency, mustn't you also reject Cantor's Diagonal argument as well?

a question is not the sort of thing that is apt to contradiction. — Banno

Then correctly answer this question:
Is this sentence (true or false): "This sentence is not true."

Well, we've dealt with that already, and as showed, it's problematic for you to insist on a yes or no answer. But there are various ways of dealing with the liar. You earlier went with claiming that it was not a proposition, not eligible for a truth value, Another approach might be to drop bivalence, after Kripke. OR one could go with the revision theory of truth.

Also, "This sentence is not true" is not a question. So I'm unclear as to how your reply addresses the point that a question is not apt to contradiction.

And further the liar does not play a role in the issue at hand, Gödel incompleteness and Halting. The sentence of interest is not "This sentence is not true" but "this sentence is not provable".

So again, for consistency, mustn't you also reject Cantor's Diagonal argument as well? — Banno

Well?

↪PL Olcott Well, we've dealt with that already, and as ↪Antony Nickles showed, it's problematic for you to insist on a yes or no answer. — Banno

Not when we are mathematically mapping Carol's question to an input D to a halt decider H that does the opposite of whatever Boolean value that H returns. It is impossible for Carol to correctly answer her question for the same reason and in the same way that it is impossible for H to return the correct halt status of D.

Also, "This sentence is not true" is not a question. — Banno

The question is: >>>Is this sentence true: "This sentence is not true."<<<

And further the liar does not play a role in the issue at hand, Gödel incompleteness and Halting. — Banno

Gödel says that it does.
The most important aspect of Gödel's 1931 Incompleteness theorem
are these plain English direct quotes of Gödel from his paper:
...there is also a close relationship with the “liar” antinomy,14 ...
...14 Every epistemological antinomy can likewise be used for a similar undecidability proof...

The Liar Antinomy <is> an epistemological antinomy.
So Gödel agrees that incorrect questions are a thing.

I don't see this conversation progressing.

↪PL Olcott I don't see this conversation progressing. — Banno

Only because when I make a correct point you simply
ignore rather than acknowledge it.

I form a perfect incorrect question and then you change the words
and form a strawman rebuttal of those changed words.

The question is: >>>Is this sentence true: "This sentence is not true."<<<

I've answered that.

...as ↪Antony Nickles showed, it's problematic for you to insist on a yes or no answer. But there are various ways of dealing with the liar. You earlier went with claiming that it was not a proposition, not eligible for a truth value, Another approach might be to drop bivalence, after Kripke. OR one could go with the revision theory of truth. — Banno

Here's where we are up to: can you explain how you reject diagonalisation for Gödel but not for Cantor? Or do you reject Cantor's argument, too?