Thank you.

P1. Nothing happens to the lamp except what is caused to happen to it by pushing the button
P2. If the lamp is off and the button is pushed then the lamp is turned on
P3. If the lamp is on and the button is pushed then the lamp is turned off
P4. The lamp is off at 10:00

From these we can then deduce:

C1. The lamp is either on or off at all tn >= 10:00
C2. The lamp is on at some tn > 10:00 iff the button was pushed at some ti > 10:00 and <= tn to turn it on and not then pushed at some tj > ti and <= tn to turn it off
C3. If the lamp is on at some tn > 10:00 then the lamp is off at some tm > tn iff the button was pushed at some ti > tn and <= tm to turn it off and not then pushed at some tj > ti and <= tm to turn it on

From these we can then deduce:

C4. If the button is only ever pushed at 11:00 then the lamp is on at 12:00
C5. If the button is only ever pushed at 11:00 and 11:30 then the lamp is off at 12:00
C6. If the button is only ever pushed at 11:00, 11:30, 11:45, and so on ad infinitum, then the lamp is neither on nor off at 12:00 [contradiction] — Michael

C1 is a premise. It is the premise that the lamp has only two states. But that's not a substantive problem; only that I'm mentioning that it is a premise.

C2 and C3 together seem to include "only by an immediate predecessor". But I don't see a valid inference for them from the premises. It seems to me that the premises don't preclude that the button can be pushed at 12:00 without there being an immediate predecessor state.

You are not including the premise "The lamp can only be on if immediately preceding it was off. And the lamp can be off only if immediately preceding it was on"?

To reject (1) is to claim that the lamp can spontaneously and without cause be on at 12:00. — Michael

It rejects that having an on/off state is determined by an immediate predecessor state, so when we reject that premise, it is not ruled out that the state at 12:00 is determined in another way. (Yes, this is similar to Benacerraf.)

The lamp can only be on at 12:00 if the button was pushed when the lamp was off to turn it on. — Michael

You're reiterating a premise that we are free to reject since it is impossible given the other premises. Just reiterating it like that is begging the question in this context.

You can couch the hypothetical situation with whatever premises you like. In that sense it's not a matter of me agreeing or disagreeing. And the part about Benacerraf doesn't seem relevant to my previous post, since I am not using referencing Benacerraf's argument in my previous post.

Meanwhile, I don't know what is not understandable about my previous post.

We reject that it is possible for (1) (2) (3) to hold together. So we can reject (1) and be left with a consistent set of two premises. So it is not ruled out that it is possible that there are denumerably many alternating states and that time is infinitely divisible.

Within the context of my view, we can talk about algorithms designed to construct infinite sets (as in your example) but we cannot talk about the complete output of such algorithms. — keystone

Classical mathematics itself first formulated that there is no algorithm that prints all the members of an infinite set and halts.

Cantor's proof holds value within the context of my view. — keystone

How nice. My point is that it is constructive.

So be it. — keystone

Let "so be it" be.

Constructivism is broader than intuitionism. Intuitionism is one form of constructivism. I don't opine as to what other poster's notion of constructivism is, except that it would not be correct to claim that arguments such as Cantor's argument that there is no surjection from the naturals to the reals are not constructive. Similarly, not correct to regard my recent argument about a certain union as not constructive.

But, if I am not mistaken, your argument comes down to: From the assumption that (1) (2) (3) are together possible, we infer that time is not infinitely divisible, not merely that a certain supertask is impossible.

And you see now that a reductio argument is not needed; indeed Cantor did not use a reductio argument.

g is a list of denumerable binary sequences, and we construct a denumerable binary sequence not listed by g.

Or if reals are addressed:

g is a list of reals, and we construct a real not listed by g.

It seems you're trying to point out flaws in my viewpoint by identifying how it differs from yours. — keystone

That is incorrect. In the instance about "can", I merely provided you the information that mathematics doesn't need to use "can" but rather can use "is".

If you want to challenge my perspective effectively, it would be more impactful to identify actual contradictions or limitations within my own ontology rather than highlighting its differences from yours. — keystone

As I've said about four times already, months ago I spent a quite generous amount of time and energy following up the finest details in your proposal, but that ended up in a bust with your continually shifting equivocations, handwaving and contradictions. Now it seems you're proposing yet another revision. I don't have interest in going down another path like that with you.

Meanwhile, when I do mention certain individual misstatements, you repeat your whining that I am not engaging the full glory of your wonderful alternatives. But I don't have to do that merely to correct certain misstatements and provide you with explainations, even though too often you evidence that you lack the maturity and restraint from self-grandiosity to truly think about the explanations.

And I haven't claimed a particular ontology, so "your ontology" is inapposite.

You don't have to keep repeating your point; I understand it. — keystone

You hadn't said that you understand the point, so the point deserved repeating.

Since the complete output of the function cannot be generated all at once — keystone

But you don't have to keep repeating that point, as it has many times been recognized that the there is no finite listing of an infinite set. Even more simply than that there is no finite listing of the members of the infinite union of intervals, we may observe that even more basically there's no finite listing of the set of natural numbers.

I wish you wouldn't presume to speak for "a constructivist standpoint". You do seem to be along the lines of constructivism (along with a notion of potential infinity) but there's a lot more to constructivism than you know about, so I think it invites error when you speak on behalf of constructivism.

For that matter, it is not a given that my argument is not constructive. I constructed an infinite set in the sense that I used only intuitionistic logic to prove the existence of a particular, named set. If I am not mistaken, constructivism in the broadest sense does not disallow construction of infinite sets. It only requires that an assertion of the existence of a set with a certain property is only allowed when at least one particular, named set is proven to have that property. I claimed that there is a set that has the property of being an infinite disjoint union of intervals such that the union is (0 1). And I proved the existence of a particular, named such set. However, granted, the proof requires the axiom of infinity, which may not be considered constructive, since it merely asserts that there exists a successor inductive set without adducing a particular one. However, the axiom of infinity is equivalent to the claim that there exists a set whose members are all and only the natural numbers, which is a particular, named set.

For example, Cantor's proof that there is no enumeration of the set of real numbers is accepted by constructivism. From any enumeration of a set of real numbers, we construct a real number that is not in the range of that enumeration. Constructive.

It seems that you heard about constructivism and your reaction is "Goody, now I can put my own wonderful alternative framework under the banner of a cool, authoritative school of thought" but without actually understanding what all is involved in constructivism.

That seems to drawing an inference from an impossibility.

If we agree that (1) (2) (3) are together impossible, then we can infer anything from the assumption that they are possible.

You're putting the cart before the horse. — Michael

A horse can push a cart, not only pull it.

Before we even consider if and when we push the button it is established that the lamp can only ever be on if the button is pushed when the lamp is off to turn it on. The lamp cannot spontaneously and without cause be on. — Michael

I haven't refused that. But I suggest that 'immediate predecessor' is a good way of couching the matter. Then, we may consider that the problem itself is impossible in the sense that it requires:

(1) a state requires an immediate predecessor state

(2) there is a state at 12:00

(3) there is no predecessor state to the state at 12:00

Whether one agrees with Michael or not, at least he has been making a good faith argument and refining it along the way. And fishfry pertinently presents a dissent that deserves consideration.

But meanwhile there is the crank who posts pure garbage as he shows that he is not even following along in the discussion. In the course of exercising his personal umbrage, he terribly fouls up the subject matter and the path of the conversation here.

The comments below should not have to be belabored, but the crank's trash talk should not be left standing.

The problem under discussion itself is couched in terms of moments* in time and durations of time that are indexed numerically. And the problem supposes that the durations may be divided and that there are infinitely many divisions. *And it is common for people to refer to 'points in time' pretty much in the same sense of 'moments in time'. Again, l have not taken any position about the nature of time or the common understanding of time represented as points on a line. I am only taking the problem as it is presented. The premises and rubrics in the problem are not ones that I have endorsed nor disputed.

Michael claimed to prove that time is not continuous. I pointed out that, for his own purposes, he needs to prove that time is not dense. Again, I haven't taken a position on that question.

The problem presupposes that points in time are ordered, such that 11:00 precedes 11:30 precedes 11:45, etc. A dense order is one in which between any two different points there is yet another point. And the ordering of time in which the thought experiment supposes that time can be divided ad infinitum is a dense order. So, my remark about density is that for Michael's own purpose, he should be claiming to refute that time is dense in that sense and not the weaker claim that time is not continuous. Again, I haven't taken any position of my own about time; I have only taken the problem and poster's arguments on their own terms.

But the crank lashes out with stupid strawmen, getting the path of conversation abysmally mixed up. He irrationally snarls with nonsense projected onto me such as "time consists of two distinct substances", "infinitely dense particles", "the irrational space between the rational numbers".

The crank is a bane.

The sum is not the total addition of all the entries, but the limit of the total addition of all the entries. The total addition of all the entries up to a specific point will converge on/with the sum. — Ludwig V

We just need to say that the infinite sum is the limit of the sequence of finite sums.

The lamp problem is best modeled as a function defined on the ordinal w+1 — fishfry

I understand the idea that the domain is w+1 and I too mentioned it a while back.

The butting of heads over Benacerraf can be reduced at least somewhat if we look closely at the premises. Two options:

(1) We do not make explicit the premise that the state at 12:00 is determined by an immediate predecessor state.

That tends to favor Benacerraf.

(2) We do make explicit the premise that the state at 12:00 is determined by an immediate predecessor state.

That tends to disfavor Benacerraf.

But there is no immediate predecessor state to the state at 12:00, so I find it difficult to conceive also requiring that the state at 12:00 is determined by an immediate predecessor state that does not exist.

they state that "any set of sentences can be a set of axioms." I want to distinguish between what is (i.e. actual) and what can be (i.e. potential). — keystone

The use of 'can' there is merely colloquial. We may state it plainly: Any set of sentences is a set of axioms. More formally: For all S, if S is a set of sentences, then S is a set of axioms.

.

I was referring to reals between 0 an 1, not ALL reals — ssu

It doesn't matter whether we're proving that there is no list of all the reals, or no list of all the reals between 0 and 1, or (as in Cantor's proof) no list of all the denumerable binary sequences.

The point is that we don't need to assume for a reductio (and Cantor did not do that).

If it's about reals between 0 and 1, then let g be any list of reals between 0 and 1 (we don't need to assume for a reductio that it is a list of all reals between 0 and 1). Then we construct a real between 0 and 1 that is not listed.

Isn't then that g is not in the list of all these sequences exactly constructed by diagonalization? — ssu

g is not in the list since g is not a real between 0 and 1. Rather, we construct a real between 0 and 1 that is not in the range of g.

Cantor did it for the denumerable binary sequences: Let g be a list of denumerable binary sequences. We construct a denumerable binary sequence that is not in the range of g.

/

Entscheidungsproblem. My mistake. I overlooked that Turing proved both the unsolvabilty of the halting problem and the unsolvabity of the Entscheidungsproblem. Chuch also independently proved the unsolvability of the Entscheidungsproblem.

Read the proof to its end. The union of the range of the function is an infinite union of disjoint intervals and that union is (0 1).

I have an idea that may help pedagogically.

In discussions about languages, models and theories, the prepositions 'for' and 'of' might get overlooked if one is not reading closely. But we can eschew those prepositions:

language
model (aka 'interpretation' or 'structure' (different from another sense of 'structure' in mathematics))
theory

are key concepts in mathematical logic.

We can stipulate this terminology:

M interprets a language L iff M is a pair <U F> where U is a non-empty universe and F is an interpretation function from the non-logical symbols of L

A theory T is written in a language L

M models a theory T iff every sentence in T is true in M

Then we have:

There are languages L, models M and theories T such that: T is written in L, and M interprets L, but M does not model T.

I find that quote quite understandable, quite clear and not confusing.

In a meta-theory we define 'is a model' and we talk about models for languages for a theory, and we talk about models of theories.

The Enderton reference was to the identity axioms. See page 112 in the logic book. And also, on page 83, he specifies satisfaction regarding '=' so that it adheres to interpreting '=' as the identity relation.

For set theory, an example is Hindman's 'Fundamentals Of Mathematical Logic' in which he is explicit that set theory is a first order theory. And earlier in the book, he gives the logical axioms as including the axioms regarding '=' similarly to the way I did. And he also mentions that the interpretation of '=' is the identity relation.

In general, even if many texts don't belabor that set theory is a first order theory, surely you don't dispute that it is? And that is first order theory with identity. To demonstrate:

Suppose you have only the axioms of set theory and no axioms for identity, then how do you suppose you would derive:

Axyz((x = y & y =z) -> x = z)

Watch out: You can't use "substitution of equals for equals", since that principle is derived from the identity axioms.

More generally, let P be a formula with only x free. How would you derive?:

(P(x) & x = y) -> P(y)

For example:

How would you derive?:

(x is finite & x = y) -> y is finite

Basically, the axiom of extensionality lets you infer equality, but it usually doesn't help in inferring from equality.

Yes, from x and y having the same members, we can infer that x is y. But from "x is y", and without identity axioms, how would we infer very much else?

You need axioms for '=' other than the axiom of extensionality to deduce all the theorems of set theory. And those other axioms are axioms of identity, such as the axiomatization I've been mentioning. You need the identity axioms and the axiom of extensionality to get all the theorems.

Sure, in informal expositions, even as found in many set theory textbooks, we don't belabor our use of the axioms and theorems of identity theory, but take them as implicit in our arguments, especially since the principles (such as substitution of equals for equals) are engrained in mathematical reasoning. But when we rigorously formalize, we need the identity axioms. Meanwhile, such a book as Hinman, which is quite scrupulous does mention the identity axioms explicitly as among the first order axioms and does mention that set theory is a first order theory.

Also: That textbooks might not mention something, especially as textbooks often don't belabor every formal detail (and some hardly even glance upon even basic formal considerations), it is not entailed that we can't specify details that are left out. And even if terminology used is not common (such as, 'identity theory' seems less common than 'first order logic with equality') we should allow the terminology as long as it is defined. And I did exactly define it, as I defined it as the theory axiomatized by the exact axioms I specified.

Classical mathematics is regarded as being formalized by ZFC. ZFC starts with a base of first order logic with identity. Whether called 'first order logic with identity', or 'first order logic with equality', or 'identity theory', the usual axioms, whether named as axioms for 'identity' or axioms for 'equality' are as I mentioned. For example, Enderton's 'A Mathematical Introduction To Logic'.

One of the axioms of identity theory is the law of identity formalized: Ax x=x. So the law of identity pertains to ZFC and, if ZFC is consistent, then ZFC does not contradict identity theory.

Ask anyone who studies set theory, whether ZFC is a first order theory with identity. I can't help that the Google doesn't help to find this.

The Wikipedia article you mentioned is not well written. (1) It doesn't give an axiomatization and (2) It doesn't mention that we can have other symbols in the signature and that by a schema we can generalize beyond a signature with only '='.

But, yes, of course we can use the word 'equality' or the word 'identity', as I said so many times. Perhaps 'equality' is used more often, but the exact formal theory is the same, and is axiomatized as I mentioned.

You haven't convinced me that set equality has anything to do with the law of identity. — fishfry

I gave you fulsome explication. Said yet another way:

The axiom of extensionality gives a sufficient condition for equality. But it doesn't give a necessary condition. So it is not a mathematical definition. A formal mathematical definition for a binary predicate R is of the form:

x R y if and only if (something here about x and y)

A definition of '=' would be of the form:

x = y if and only if (something about x and y)

But the axiom of extensionality is usually given:

If, for all z, z is a member of x if and only if z is a member of y, then x= y.

That is of the form:

If (something about x and y) then x = y. And that is only a sufficient condition, not a biconditional.

But I also mentioned that we could have this variation:

x = y if and only if (for all z, z is a member of x if and only if z is a member of y; and for all z, x is a member of z if and only if y is a member of z).

And that would be a definition, since it gives both a sufficient and necessary condition for x = y.

However, I'll say it yet another way:

Ordinarily, set theory is written with a signature of '=' and 'e', where '=' is logical and 'e' is non-logical, and we have the axioms for first order logic with identity (aka 'idenity theory' or 'first order logic with equality'). Then we add the axiom of extensionality. And then we get (1) as a theorem.

No matter which approach we take, we end up with the same theorems.

you claimed that set equality is "identity," — fishfry

For the third time, I did not say that. And I again told you what I do say. Please stop saying that I said something that I did not say.

I said that set theory adheres to the law of identity but that set theory, with its axiom of extensionality, adds an additional sufficient condition for identity.

I don't know why you don't grasp this:

Ax x= x is an axiom of first order logic with identity. And set theory is a theory that subsumes first order logic with identity. So Ax x=x is also an axiom incorporated into set theory. But also set theory adds the axiom of extensionality.

You seem to be saying that. — fishfry

You are egregiously glossing over what I exactly say. So you form incorrect "seems".

If, for whatever reason, there is a point of my terminology that requires definition for you, then, time permitting, I would supply the definition. Or if there is an argument you can't see to be logical, then, time permitting, I would explain it in even more detail if there even is more detail that could be reasonably provided. However, that can lead to a long chain of definitions back to primitive notions, so it would be better to start at the beginning such as in some chosen textbook. But that does not justify you claiming that I said things that I did not say.

But identity theory, merely syntactically, can't require that '=' be interpreted as standing for the identity relation on the universe as opposed to standing for some other equivalence relation on the universe.
— TonesInDeepFreeze

We're not having the same conversation now. I couldn't even parse that. — fishfry

It parses perfectly even if it seems difficult when one is not familiar with the basic mathematical logic in which symbols are interpreted with models. I'll put it this way:

'=' is a 2-place predicate symbol.

A model (an interpretation) for a language assigns a 2-place relation on the universe to a 2-place relation symbol. In other words, that is an assignment of the meaning, per the model, of the 2-place relation symbol. We call that 'the interpretation of the symbol'. That is semantical.

In general, relation symbols are interpreted differently with different models. But in the special case of '=', we stipulate that, with all models, '=' is stands for the identity relation on the universe for the model.

So my point was that from the mere syntactical presence of '=' in a formula, we can't ensure that '=' stands for the identity relation, and we have to turn to semantics (models) for that.

There is no model of set theory in which extensionality is false. — fishfry

Correct. There are no models of the axiom of extensionality in which the axiom of extensionality is false. But there are models in which the axiom of extensionality is false; they are not models of the axiom of extensionality. Take this is steps:

A model M is for a language.

Theories are written in languages.

So if a theory T is written in a language L, then a model for M for L is model for the language of T.

Given a model M, some sentences in the language L are true in M and some sentences in the language L are false in M.

A theory is a set of sentences closed under provability.

If every sentence in theory T is true in a given model M, then we say "M is a model of T".

So, notice that that there is a difference in meaning between "M is a model for the language L" and "M is a model of the theory T".

That is a crucial thing to understand and keep in mind.

Now, back to the axiom of extensionality.

Let T be any theory that is axiomatized with a set of axioms that includes the axiom of extensionality. If M is a model of T, then the axiom of extensionality is true in M.

But there are models for the language for set theory that are not models of set theory. For example

Let M have universe U = {0 1} and let 'e' be interpreted as the empty relation.

M is a model for the language for set theory, and M is not a model of set theory.

Again, to stress:

There is a difference between a language and a theory writtten in that language.

Let L be a language, and T be a theory written in L, and M be a model for L. It is not entailed that M is a model of T.

/

Urelements. Even though search engines are often deficient, I bet that you can find articles about urelements.

Df. x is an urelement <-> (~Ey yex & ~ x = 0) ('0' here standing for 'the empty sety')

A theorem of Z:

~Ex x is an urelement.

But we could have other axioms where

~Ex x is an urlement

is not a theorem.

And we could have axioms where

Ex x is an urlement

is a theorem.

But a theory that has the theorem:

Exy (x is an urelement & y is an urelement & ~ x = y)

is obviously inconsistent with the axiom of extensionality.

But we could do this:

Axiom: Axy((~ x is an urlement & ~ y is an urelement & Az(z e x <-> z e y)) -> x = y)

In sum: Set theory adopts identity theory and the standard semantics for identity theory, and also the axiom of extensionality. With that, we get the theorem:

Axy(x = y <-> Az((z e x <-> z e y) & (x e z <-> y e z)))

And semantically we get that '=' stands for the identity relation.
— TonesInDeepFreeze

Can't possibly be. — fishfry

It be's. Just as I've explained again. And I'll explain yet another way:

Certain proofs, including in set theory, use the identity axioms I mentioned. Set theory also has the axiom of extensionality, which allows for even more proofs. And we have this theorem of set theory:

Axy(x = y <-> Az((z e x <-> z e y) & (x e z <-> y e z)))

That's all purely syntactical.

Meanwhile, we interpret '=' to stand for the identity relation on the universe of any model for the language for set theory. And that is semantical.

Models of what? — fishfry

Models for the language of set theory. Some of them are models of set theory.

Always keep in mind the distinction between "model M for a language L" and "model M of a theory T" (or, mentioning the language also, "model M of a theory T written in a language L").

How do you know whether having the same members is sufficient for identity unless you already have the axiom of extensionality? In which case you're doing set theory, not identity theory. — fishfry

You're very mixed up thinking that you're somehow disagreeing with me on those points.

Indeed, I am saying that the axiom of extensionality is what makes Az(z e x <-> z e y) sufficient for x = y.

And, indeed, identity theory is not set theory. Rather, identity theory is a sub-theory of set theory:

Every theorem of identity theory is a theorem of set theory. But not every theorem of set theory is a theorem of identity theory: Right off the bat, the axiom of extensionality is not a theorem of identity theory.

And again, we needn't quibble that "pure" identity theory does not have 'e' in its signature. I'm talking about the axioms of identity theory written in a signature that includes 'e'.

I've never seen one. Every one of the hundreds and hundreds of cranks I've seen lacks the self-awareness to understand the ways in which they are a crank.

At that point, it is no longer capable of cleanly separating provability and truth: "How can a model of ZFC be a set, if we want to use ZFC to study sets?" — Tarskian

ZFC is a set of sentences. Any consistent set of sentences has models, and the universe of a model is a non-empty set. There is no incapability of distinguishing the definitions of 'provable in a theory' from 'true in a model'.

the theory is essentially its own model. — Tarskian

That is nonsense. Theories are not models and models are not theories.

I only give up when it talks about the models of ZFC — Tarskian

Set theory says what is the requirement for being a model for set theory is. But set theory (if it is consistent) does not claim that there is model that meets that requirement. And set theory proves that if set theory is consistent if and only if set theory has model. Also, set theory talks about inner models, which a figure of speech for relativization, which also is not problematic.

there might be uncountably many theories (interpretations) — fishfry

No, theories and interpretations are different things. But, yes, I did give reasoning by which there are uncountably many theories and uncountably many interpretations for even just one language.

I'm pretty sure this is correct:

There are exactly denumerably many algorithms. And for every formal theory and set of axioms for that theory, there is an algorithm for whether a sentence is an axiom. So there are only countably many formal theories.
— TonesInDeepFreeze

That's what I believe is true. Only countably many interpretations of each sentence. — fishfry

I didn't say that there are only countably many interpretations of a given sentence. Indeed, there are uncountably many interpretations, as I explained.

natural language could be uncountable, is wrong — fishfry

There are only countably many expressions. But there are uncountably many interpretations even of just one sentence.

Of course we don't need any axioms to do a whole bunch of arithmetic. But just doing a bunch of arithmetical computations is not, in the context of mathematical logic or philosophy of mathematics, what people ordinarily mean by reducing arithmetic to logic.

As I only perused, there's a writeup there about carrying out arithmetic with logic gates.

But to say that arithmetic can be reduced to logic requires showing, for example, the derivation of the axioms of PA from only logical axioms, or even more basically to define the non-logical primitives of PA from logical primitives. And those ain't gonna happen.

I never understood it like that. In fact, I just always ignored it. I always saw it as PA talking about itself. — Tarskian

They ordinary way of writing it up is quite understandable, in context of Godel's original paper and in context of just about any article or book on it. Your way though requires me to regard PA as the meta-theory, which is not a required assumption for the proof.

Yes, PA can "talk about itself" in a certain sense (though I don't know that it can formulate all of the proof when it is a proof about PA). But we don't ordinarily stipulate that the proof about PA is being given in PA. In an ordinary exposition of the proof, it seems to be it would be, at best, an invitation to a lot of confusion to presuppose that the proof is being given in PA.

where is the truth of ZFC? — Tarskian

In, for example, ZFC+"there exists and inaccessible cardinal".

But, yes, of course, that is not an epistemological basis. But that issue is aside the point that one does not ordinarily stipulate that PA itself is the meta-theory.

model theory is only straightforward for the simple case of PA being interpreted by ZFC's truth — Tarskian

I don't know your criteria for straightforwardness, but model theory is rigorously developed, though it does use infinitistic mathematics.

smoke and mirrors — Tarskian

What is an example?

Of course, we understand that computations are finite.

But the specific mathematical statement you made earlier was incorrect. You'd do yourself a favor by recognizing that fact.

You clearly have a lot of knowledge — keystone

My knowledge of mathematics, logic and philosophy is quite meager. But I do have a good grasp of certain basics and an intent not to misstate them (at least within reasonable informal explanations).

Arithmetic can be reduced entirely to logic — Tarskian

What specific reduction do you have in mind?

David Hilbert had a habit of drawing the attention of the entire mathematical world to his agenda. — Tarskian

I don't know that it was a habit, but of course he made his agenda prominent. But that is a far cry from insisting that all his colleagues work on it.

His program, however, was about proving a falsehood, such as "mathematics is complete" (i.e. there is a proof for every truth). Hilbert wanted other mathematicians to find proof for his misguided ideology. — Tarskian

He wanted to prove something. He did not claim that it might not turn out to be untrue. He expected that it would be true, but that's hardly even a foible. And "ideology" suggests connotations that I don't see as warranted.

These vaccines were obviously not tested for long-term consequences. — Tarskian

Correct, of course.

So, according to your remark, the diagonal lemma should be phrased as:

∃ A ( PA ⊢ ( A ⇔ ¬Bew(ÍAÎ ) ) ) — Tarskian

I would not write it that way. But, yes, my point is that the existential quantifier is in the meta-language and not in the scope of the turnstile.

A must also be a sentence in PA — Tarskian

What I wrote:

If F(x) is a formula, then there exists a sentence S such that ('#' for 'the numeral for the Godel number of'):

PA |- S <-> F(#(S))

Applied to the negation of the provability predicate ('P' for the provability predicate):

There exists a sentence G such that:

PA |- G <-> ~P(#(G)) — TonesInDeepFreeze

There is no mess up of what is in the meta-language and what is in the object language there. Look at virtually any article or textbook to see that they are, modulo stylistic and symbol choices, along those lines and not with the existential quantifier in the scope of the turnstile.

PA is its own meta-theory in this case — Tarskian

I don't know. It is a tricky point that I wish I understood better (especially I suspect we would need to be careful where the consistency assumption occurs?). Since it is not needed for PA to be the meta-theory, personally, I think of some other meta-theory. In any case, in ordinary expositions, the existential quantifier is not written after the turnstile. Doing so would mix up the meta-language and object theory, as otherwise would indeed cause get us embroiled in keeping straight what are the theorems of PA as opposed to what are the theorems about PA. Even if PA could be its own metatheory (I don't know whether it a can be while consistent) it is not good to write the meta-theorems such that they are both in the meta-theory and object theory, lest the exposition becomes quite confusing. Moreover, when we move on to mention 'truth', the language for PA cannot be its own meta-language.

If PA is not its own meta-theory in this case, what theory is then the meta-theory? — Tarskian

Whatever you choose that is adequate. Godel performed the proof in ordinary mathematics and reasoning in natural language. On the other hand, set theory works even though it is more than we need. And, though I don't know the details, PRA would serve as an admirably lean basis.