Germanomosconi1

Your deletion of Dirsaka's comment

not(Phi) of degree k+1, which is to be shown to be provable, is a conjunction of an obviously provable formula and not(phi) of degree k+1, so not(phi) of degree k+1 must be shown to be provable. This is never done, it is just assumed on the basis of not(Phi) and not(phi) being provable for not(Phi) and not(phi) of degree k, which degree they were before the substitution for the previous Q by a Q of degree k (the Q = for each u there exists a v such that P(psi), where P is of degree k-1).

Also, the induction is to show that, if the theorem is true for formulas of degree k, it is true for formulas of degree k+1, so the theorem is true for formulas of every degree. This is the same purpose as that the substitution (the substitution is, of course, really part of the induction). If the substitution takes place after the induction, so after the theorem has been shown to be true for formulas of degree k+1, what was the substitution's purpose? Dirsaka (talk) 02:06, 25 July 2023 (UTC)

This comment shows that you completely misunderstood the deduction chain of the proof, and probably you also misunderstood how the principle of induction works, at least for this proof. Later I will post the deduction chain in a more rigorous and precise way, so that you can understand it better. Then, it will be clearer why these objections are not valid. Germanomosconi1 (talk) 08:27, 25 July 2023 (UTC)

Proof

Let k≥1.

Inductive hypothesis: Every formula in R of degree k is either refutable or satisfiable.

Let $\phi$ be a formula of degree k+1; then we can write it as

$\phi =(\forall x)(\exists y)(\forall u)(\exists v)(P)\psi$

where (P) is the remainder of the prefix of $\phi$ (it is thus of degree k-1) and $\psi$ is the quantifier-free matrix of $\phi$. x, y, u and v denote here tuples of variables rather than single variables.

Let now x' and y' be tuples of previously unused variables of the same length as x and y respectively, and let Q be a previously unused relation symbol that takes as many arguments as the sum of lengths of x and y; we consider the formula

$\Phi =(\forall x')(\exists y')Q(x',y')\wedge (\forall x)(\forall y)(Q(x,y)\rightarrow (\forall u)(\exists v)(P)\psi )$

The deduction chain can be written as follows:

1. $\Phi \implies \phi$, clearly.

2. $(Q(x,y)\rightarrow (\forall u)(\exists v)(P)\psi )\equiv (\forall u)(\exists v)(P)(Q(x,y)\rightarrow \psi )$, since the string of quantifiers $(\forall u)(\exists v)(P)$ does not contain variables from x or y.

3. Since these two formulas are equivalent, if we replace the first with the second inside Φ, we obtain the formula Φ' such that Φ≡Φ':

$\Phi '=(\forall x')(\exists y')Q(x',y')\wedge (\forall x)(\forall y)(\forall u)(\exists v)(P)(Q(x,y)\rightarrow \psi )$

4. We form Ψ as follows:

$\Psi =(\forall x')(\forall x)(\forall y)(\forall u)(\exists y')(\exists v)(P)Q(x',y')\wedge (Q(x,y)\rightarrow \psi )$

5. We have $\Phi '\equiv \Psi$, since Φ' has the form $(S)\rho \wedge (S')\rho '$, where (S) and (S') are some quantifier strings, ρ and ρ' are quantifier-free, and, furthermore, no variable of (S) occurs in ρ' and no variable of (S') occurs in ρ.

6. If $\Psi$ is satisfiable, then, considering $\Psi \equiv \Phi '\equiv \Phi$ and $\Phi \implies \phi$, we see that $\phi$ is satisfiable as well.

7. Now, assume that $\Psi$ is refutable. Then so is $\Phi$, which is equivalent to it; thus $\neg \Phi$ is provable.

8. By "functional substitution" rule of inference (for example), if we replace all occurences of Q(x',y') in $\neg \Phi$ with the formula $(\forall u)(\exists v)(P)\psi (x,y|x',y')$, we obtain another provable formula. So, $\neg \Phi$ becomes

$\neg ((\forall x')(\exists y')(\forall u)(\exists v)(P)\psi (x,y|x',y')\wedge (\forall x)(\forall y)((\forall u)(\exists v)(P)\psi \rightarrow (\forall u)(\exists v)(P)\psi ))$

and this formula is provable. Since the part of the formula after the $\land$ is provable, it trivially follows that $\neg \phi$ is provable, and $\phi$ is refutable.

9. Summarizing, we proved these two implications:

• $\Psi$ is satisfiable $\implies$ $\phi$ is satisfiable (by point 6);
• $\Psi$ is refutable $\implies$ $\phi$ is refutable (by points 7, 8).

10. The implications at point 9 entail the following:

$\Psi$ is satisfiable or refutable $\implies$ $\phi$ is satisfiable or refutable.

But the antecedent of this last implication is true by inductive hypothesis, since $\Psi$ has degree k. This implies that $\phi$ is satisfiable or refutable, and the lemma is proved.

Comment: Observing the point 7, it's evident that "$\neg \Phi$ is provable" follows if $\Psi$ is refutable, so there's no deduction error at all.

Furthermore, the substitution doesn't take place after the theorem has been shown to be true for formulas of degree k+1: at point 7, we assumed that $\Psi$ is refutable and accordingly proved that $\neg \Phi$ is provable. And then, at point 8, the substitution takes place. Finally, at point 10, we used the inductive hypothesis to prove that $\Psi$ is either refutable or satisfiable.

From this, it's clear that the substitution does not invalidate the induction argument, since the inductive hypothesis is never used in the formula obtained by the substitution. The inductive hypothesis is used only at point 10 on $\Psi$, and it is legit. Germanomosconi1 (talk) 14:46, 25 July 2023 (UTC)

Reply from Dirsaka

The error in the induction argument is in its attempted justification in 8. of the claim that the formula ¬Φ which is obtained by the substitution for Q in the initial ¬Φ is provable.

8. says that by "functional substitution" rule of inference (for example), if we replace all occurrences of Q(x',y') in ¬Φ with the formula (∀𝑢)(∃𝑣)(𝑃)ψ(( 𝑥, 𝑦|𝑥', 𝑦'), we obtain another provable formula. I don't know what is meant by "'functional substitution' rule of inference", but clearly it is not true that for all formulas A, B, and C, if A is a provable formula and B is some sub-formula of A, if we replace B by C in A, the result A' is still provable. However, Q was chosen to be an arbitrary relation with the right number of variables, so maybe any provable formula containing Q would still be provable after Q is replaced by any formula with the right number of variables, whether true or false.

Again however, wasn't there some constraint imposed on Q after it was described but before 8.? An essential element of the induction is that the completeness theorem be true of Ψ, so we know that Ψ will be either satisfiable or refutable. We know the theorem is true of Ψ since we assume Ψ satisfies the induction hypothesis, so has degree k. You say this is so just after 10. Now look at the definition of Ψ in 4. The first term of the conjunction making up Ψ is (∀𝑥')(∀𝑥)(∀𝑦)(∀𝑢)(∃𝑦')(∃𝑣)(P) Q (𝑥', 𝑦'). Its degree is 1 + degree of P + degree of Q. The degree of P is k -1, so the degree of Ψ is k + degree of Q. Therefore, for Ψ to be known to be either satisfiable or refutable, the degree of Q must be 0. This requirement, of Q having degree 0, for knowing Ψ to be either satisfiable or refutable holds, of course, for any formula we replace Q in Ψ, or equivalently Φ, by, if Ψ or Φ after replacement is to be known to be either satisfiable or refutable.

We assume that Ψ ≡ Φ is not satisfiable, so we need to show it is refutable, i.e., that ¬Φ is provable. We know that, under our assumption, ¬Φ before the substitution for Q is provable. However, the formula Q in ¬Ψ ≡ ¬Φ is replaced by in 8. has degree 1 + degree of P = 1 + (k-1) = k ≥ 1 > 0, so doesn't satisfy the requirement of having degree 0. Thus, it hasn't been shown that ¬Φ is provable, so the induction argument is invalid. Dirsaka (talk) 16:51, 26 July 2023 (UTC)

First of all, the "functional substitution" is a rule of inference of the deductive system used by Gödel to prove its completeness. If you don't know it, you better study a little more the Gödel's proof before trying to disprove it.

Second, we don't assume that Ψ ≡ Φ is not satisfiable, we assume that Ψ ≡ Φ is refutable, from which it follows that ¬Φ is provable.

Third, the fact that at point 8 we replace Q with a formula that has not degree 0 is completely irrelevant, since, as I already said many times, the induction is applied on Ψ, which is another formula that has nothing to do with ¬Φ. When you do the substitution, you simply create another formula, call it ¬Φ' for example, but you don't modify in any way ¬Φ or Ψ, so their degree remains the same, and so the induction remains valid. And of course, the "functional substitution" rule is valid by correctness theorem, since is a rule of the calculus. If you don't understand this, I'm sorry, but I think you need to study better the fundamentals of mathematical logic before making logically unfounded objections. Germanomosconi1 (talk) 21:58, 26 July 2023 (UTC)

Reply to Germanomosconi1

About your three points, in order:

There is no "functional substitution" rule of inference in Gӧdel's proof which allows one to prove what you claim in 8. that it proves. There was something like that claimed in the Wikipedia article, but the author's of that made it up. My Talk page has a note to Felix QW which contains a link to an article of mine which in turn contains a link to the Collected Works of Kurt Gӧdel, from which you can read and copy the three somewhat different versions of the proof which Gӧdel made.

That Φ is refutable implies that ¬Φ is provable is trivial, since " Φ is  refutable" means "¬Φ is provable". Where I got that we assume that Φ is not satisfiable, so we need to show that it is refutable, is that this is the basic structure of the proof. The completeness theorem is equivalent to "each first-order statement is either satisfiable or refutable", so the theorem can be proved, and Gӧdel attempts to prove it this way, by showing that if a first-order sentence Φ is not satisfiable, then it is refutable.

It isn't entirely true that Ψ has "nothing to do" with ¬Φ, since Ψ means the same as Φ; you yourself noted this in 6., but perhaps didn't understand that this shows that Ψ and ¬Φ are negations of each other, having about as much to do with each other as they could without being the same statement. Dirsaka (talk) 00:33, 27 July 2023 (UTC)

I don't know if you're joking, but the fact that ¬Φ is the negation of Ψ is embarrassingly trivial... but again, this is is completely irrelevant for the purpose of the induction. It sounds like you're trying to hold on to anything rather than admit you're wrong...

Also, the substitution rule exists: take the collected works of Gödel Vol. 1, page 105, list of inference rules, point 2. As I said before, you need to study better what you're trying to disprove. Regards. Germanomosconi1 (talk) 01:16, 27 July 2023 (UTC)

Reply to Germanomosconi1

The fact that ¬Φ is the negation of Ψ, and so closely related to it, should be embarrassingly trivial to you, not me. My previous reply was to your three points, in the same order, as I said. My point three, about ¬Φ being the negation of Ψ, was a reply to your point three statement (Germanomosconi1 (talk) 21:58, 26 July 2023 (UTC)) "Third, the fact that at point 8 we replace Q with a formula that has not degree 0 is completely irrelevant, since, as I already said many times, the induction is applied to Ψ, which is another formula that has nothing to do with ¬Φ."

I had already seen the mention of the substitution rule "2. The rule of substitution for propositional and functional variables" in the Gӧdel Collected Works, Vol. 1, p. 105. I didn't believe that you meant this to be what you claim in your 8. proved that when we replace all occurrences of Q in ¬Φ with the formula indicated in 8., we obtain another provable formula. Perhaps I misunderstood what rule 2. was. I took it to be a rather trivial grammatical rule, since Gӧdel didn't discuss it further, which you couldn't possibly think justified your conclusion in 8. Is it the rule you claim in 8. proves that ¬Φ after the substitution for Q is still a provable formula? If so, or even if not, would you please explain in detail what the substitution rule is that you claim in 8. preserves provability of ¬Φ, and show how it does this. This is a critical point in our disagreement about the correctness of the induction argument's passage from formulas of degree k to those of degree k + 1, and so the validity of the Wikipedia claimed proof. Dirsaka (talk) 06:16, 28 July 2023 (UTC)

The fact that ¬Φ is the negation of Ψ doesn't change the complete irrelevance for the induction of the fact that at point 8 we replace Q with a formula that has not degree 0, and things will not change by insisting on that point.

I don't have to explain to you how the substitution rule works, since I'm not your teacher. Having studied proof theory in detail, I know for sure that the rule is valid by the correctness theorem.

If you are not convinced, it is your problem to investigate the matter. You can take Collected Works Vol. I, page 67, note 7, where there is a reference to the Hilbert-Ackermann system, the one used by Gödel in the original proof, as a starting point.

And also, Wikipedia is not the place to publish your supposed confutations. Greetings. Germanomosconi1 (talk) 07:25, 28 July 2023 (UTC)

Just to definitively close the question about the correctness of Gödel's proof, I reproduce here the rule α3) exactly as it is set out in Principles of Mathematical Logic, ch. III, par. 5 by David Hilbert (1950):

"Under certain circumstances, a predicate variable with $n$ argument places may be replaced by a formula which contains at least $n$ free individual variables. Let $F$ be the $n$-adic predicate variable, and ${\mathfrak {A}}$ the formula in which $F$ is to be replaced. From among the individual variables occurring in the formula which is to replace $F$, we select any $n$ whatsoever ordered in any arbitrary way, say, $x_{1},x_{2},\dots ,x_{n}$. The formula which is to be substituted will accordingly be designated by ${\mathfrak {B}}(x_{1},x_{2},\dots ,x_{n})$. The substitution is now permissible only if the remaining free individual variables which may still occur in ${\mathfrak {B}}(x_{1},x_{2},\dots ,x_{n})$ do not occur in the formula ${\mathfrak {A}}$ as bound variables, and if, further, there is no occurrence of $F$ in ${\mathfrak {A}}$ such that a variable occupying an argument place in $F$ occurs as a bound variable in ${\mathfrak {B}}(x_{1},x_{2},\dots ,x_{n})$, provided always that the result of the substitution is a formula. The substitution is accomplished as follows: Considering any specific occurrence of the predicate variable $F$ in ${\mathfrak {A}}$, we find the argument places of $F$ occupied by certain individual variables, which we designate, for the moment, by ${\mathfrak {a}}_{1},{\mathfrak {a}}_{2},\dots ,{\mathfrak {a}}_{n}$. These need not all be different. We now replace $F({\mathfrak {a}}_{1},{\mathfrak {a}}_{2},\dots ,{\mathfrak {a}}_{n})$, at this occurrence of $F$, by ${\mathfrak {B}}({\mathfrak {a}}_{1},{\mathfrak {a}}_{2},\dots ,{\mathfrak {a}}_{n})$, i.e. by the formula obtained from ${\mathfrak {B}}(x_{1},x_{2},\dots ,x_{n})$ when the variables $x_{1},x_{2},\dots ,x_{n}$ are replaced, wherever they occur, by ${\mathfrak {a}}_{1},{\mathfrak {a}}_{2},\dots ,{\mathfrak {a}}_{n}$ respectively. The corresponding substitution is to be made at every occurrence of $F$."

Now, the question is no longer whether Gödel's proof is correct, but whether this rule is sound. In the same work, at ch. III, par. 9, the consistency of the system is proved, which in fact it's a different notion than soundness. The reason why Hilbert didn't prove the soundness is because he did not believe that mathematical logic had a semantics, since he was a formalist.

Indeed, the consistency is a syntactic property, and it is weaker than soundness, which in fact it's a semantic property. The consistency requires that no formula is provable and refutable, while the soundness requires that every provable formula is valid.

However, it's not so difficult to prove by induction on the structure of formulas that if there is a model that falsifies ${\mathfrak {A}}[F/{\mathfrak {B}}(x_{1},x_{2},\dots ,x_{n})]$ (the formula obtained by the substitution), then there is a model that falsfies ${\mathfrak {A}}$. So, by contraposition, the validity is preserved. Germanomosconi1 (talk) 19:58, 30 July 2023 (UTC)

Reply to Germanomosconi1

If Hilbert's functional substitution rule is to be applied to the substitution in 8., F, the predicate variable of the rule which is to be replaced, corresponds to Q of 8., 𝔄, the formula of the rule in which F is to be replaced, corresponds to ¬Φ of 8., and 𝔅, the formula of the rule which is to replace F, corresponds to (∀𝑢)(∃𝑣)(𝑃)ψ of 8. The rule states "The substitution is now permissible only if the remaining free individual variables which may still occur in 𝔅 do not occur in the formula 𝔄 as bound variables,...". The remaining free variables which may still occur in 𝔅 correspond, in 8., to x' and y', and these occur in ¬Φ of 8., which corresponds to 𝔄 of the rule, as bound variables, since x' is quantified in ¬Φ by ∀, and y' is quantified in ¬Φ by ∃, and also because every variable in ¬Φ must be bound, otherwise ¬Φ wouldn't be a meaningful formula. Thus, according to the rule, the substitution is not permissible.

By the way, contrary to popular belief, Hilbert was not a formalist. He created the idea of formalizing a mathematical system, by codifying the logically proper operations involving the symbols in it, to accomplish various ends, based on the meanings assigned to the symbols, then after this had been done as well as possible, basing all mathematical operations in the system on this code of (formal) rules that could be mechanically followed without further referring to the meanings of the operations on the symbols. This was to be done in order to allow any possible consistency proof of mathematics, which he wanted, to proceed by purely mechanical manipulations, in order to prevent it from being polluted by some mathematician's faulty ideas of its terms' meanings causing errors in the proof. He hardly would have suggested formalizing mathematics by removing all meaning from it (which he advocated only for certain purposes) if he didn't believe that mathematics before formalization had meaning. Dirsaka (talk) 22:12, 1 August 2023 (UTC)

As usual, you made procedural errors, and also you misunderstood the rule. The formula ${\mathfrak {B}}$ doesn't correspond to $(\forall u)(\exists v)(P)\psi$, but corresponds to $(\forall u)(\exists v)(P)\psi (x,y|x',y')$, where the variable tuples $x,y$ are replaced with $x',y'$.

Since we select all variables of tuples $x',y'$, we should write ${\mathfrak {B}}(x',y')=(\forall u)(\exists v)(P)\psi (x,y|x',y')$. So, there are no remaining free variables besides those in $x',y'$, and so the substitution is permissible. You should re-read the rule's definition more carefully.

I don't understand why such a stubbornness in carrying out one's mistaken belief, when it would be so much easier to admit that you're wrong. Furthermore, are you so presumptuous as to insinuate that a genius of Gödel's caliber would have made such a blunder, but above all that no expert who revised the proof noticed it? Seriously?

Anyway, it's a matter of fact that Hilbert did not prove the soundness theorem, which highlights the little faith he had in the semantics of logic, or maybe he too was so presumptuous as to think there was no need. Germanomosconi1 (talk) 22:54, 1 August 2023 (UTC)

Reply to Germanomosconi1

The formula which replaces Q in ¬Φ is of degree k. ¬Φ, which is of degree k + 1, so has an additional block of quantifiers, as one of the two conjuncts contains the replacement for Q with an additional block of quantifiers, (∀𝑥')(∃𝑦'), before it, quantifying over. and so binding, the 𝑥' and 𝑦' in Q's replacement which are not quantified in that replacement, so are free in that replacement. Therefore, Q's replacement contains two free variables which are bound in ¬Φ, which contained the Q that was replaced. Therefore, by your own statement of Hilbert's functional substitution rule, the replacement of Q in ¬Φ is not permissible. Q.E.D.

Perhaps you don't understand your own statement of Hilbert's substitution rule, or perhaps you, for whatever reason, understand that your version of the completeness theorem's proof, which claims Hilbert's substitution rule is used at your 8., even though Gӧdel's version doesn't claim that, is invalid, but you bluster onward with accusations, which you don't believe, that the replacement for Q is valid, and that I am the one who doesn't understand. If we get into an edit war, a Wikipedia administrator may get involved, who will notice, or I will call it to his/her attention, that there is some, slight, original research in my comment, but that there is also original research- defective- in the Wikipedia article without my comment, in its attempted justification, which you defend, of the substitution for Q, which is the spurious way that the article, and Gӧdel, complete the induction step supposedly proving the truth of the completeness theorem for formulas of degree k + 1 based on its truth for formulas of degree k. The administrator will ask you for the details of the justification of the replacement for Q, or, if she/he doesn't, I will bring the matter up (and perhaps also the several egregious mistakes or deliberate misstatements you have made in our conversations), and you will not be able to convince her/him of its correctness. You may then claim that the administrator doesn't understand logic, but that claim won't do you any good. Dirsaka (talk) 10:55, 2 August 2023 (UTC)

I'm just curious why an administrator would listen to a logical incompetent like you, who can't understand the ground rules, on a proof that has been considered correct for almost 100 years.

What you don't understand is that "the remaining free individual variables which may still occur" are not the selected variables, but the remaining that aren't been yet selected. And since all variables have been selected, there aren't remaining free individual variables. It's not my own statement, it's a citation to Hilbert's work.

If you can't figure that out either, I'm starting to think you're functionally illiterate. I'm sorry for you, but you still have to study a lot before discussing these topics.

"several egregious mistakes or deliberate misstatements you have made in our conversations": you were referring to yourself in the second person here, of course.

One last thing: don't worry, if we get into an edit war, you will surely lose. Greetings. Germanomosconi1 (talk) 11:13, 2 August 2023 (UTC)

I have no interest in avoiding the edit war. If you restore your comment, I will continue to delete it. You are warned. Germanomosconi1 (talk) 12:01, 2 August 2023 (UTC)

The variables which are the arguments of 𝔅 are just the selected variables. Dirsaka (talk) 12:51, 2 August 2023 (UTC)

Exactly, so if you exclude those there are no others left, so there are no unselected free variables that are bounded in the formula to which the substitution is to be applied. Thus, the substitution is permissible. Germanomosconi1 (talk) 12:54, 2 August 2023 (UTC)

You have it backwards. Look at the fifth sentence in your statement of the Hilbert functional substitution rule, the sentence that begins "The substitution is now permissible...", and draw the correct relevant conclusion from that. Dirsaka (talk) 14:09, 2 August 2023 (UTC)

The correct conclusion is that the substitution is permissible, as I already said. Germanomosconi1 (talk) 14:11, 2 August 2023 (UTC)

Why don't you answer anymore? Don't you know what to hold onto anymore? XD Germanomosconi1 (talk) 08:48, 3 August 2023 (UTC)

Reply to Germanomosconi1

The fifth sentence of your statement of the Hilbert functional substitution rule is a conjunction of two clauses followed by a proviso, the conjunction stating requirements that the substitution be permissible, the proviso stating an additional requirement. The first of the two conjoined clauses states "The substitution is now permissible only if the remaining free individual variables which may still occur in 𝔅(x1,x2,...,x n) do  not occur in the formula 𝔄 as bound variables,". This clause means exactly that if any of the the remaining free individual variables which may still occur in 𝔅(x1,x2,...,xn) occur in the formula 𝔄 as bound variables, the substitution is not now permissible. The remaining free variables which may still occur in 𝔅 are x' and y', and these occur in 𝔄 ( ¬Φ) as bound variables. Therefore, the substitution is not now permissible.

I did not reply immediately to your previous message, which was apparently based on your incorrect understanding of the rule, i.e., that it said that the substitution is not now permissible if any of the unselected variables, which are the variables that are not among the arguments of 𝔅, occur in 𝔄 as bound variables, just to see if you would figure out correctly the implications of my previous reply. You didn't. I am getting tired of correcting your failures, or pretended failures, to understand the simple logic of what I say is the error in the induction part of the Wikipedia article, and to understand my Talk messages. You, however, did me a favor by stating what you meant by Hilbert's substitution rule. This disclosure, while being correct according to the rules of rational argument and of Wikipedia, was the final part of your argument's undoing, since the rule clearly implies that the substitution in question was not permissible, rather than implying, as you claim it does, that it was permissible. Dirsaka (talk) 19:32, 3 August 2023 (UTC)

No, it's your interpretation that is incorrect. If the remaining free variables were the ALL free variables, why Hilbert (or the translator) would use the word "remaining"? There would be no need, he could only say "free variables occurring in the formula", but the author says REMAINING FREE VARIABLES, which means FREE VARIABLES THAT ARE NOT SELECTED. And why the author wrote "which may still occur"? If he meant the all free variables, it's obvious that they still occur, dammit! I'm sure any expert will tell you the same thing. I could also prove you that this is the correct interpretation, but you are too stupid to understand it, so I won't spend more time. Germanomosconi1 (talk) 20:33, 3 August 2023 (UTC)

I added a topic in the article's talk page, so now the discussion is more visible, and you can hear the opinion of others besides me. Germanomosconi1 (talk) 23:24, 3 August 2023 (UTC)

There's no need for the variables $x_{1},\dots ,x_{n}$ to be not bound in ${\mathfrak {A}}$, because they can be renamed in ${\mathfrak {B}}(x_{1},\dots ,x_{n})$ with other distinct variables $y_{1},\dots ,y_{n}$ which don't even appear in ${\mathfrak {A}}$ and in ${\mathfrak {B}}(x_{1},\dots ,x_{n})$, and using ${\mathfrak {B}}(y_{1},\dots ,y_{n})$ in the substitution instead of ${\mathfrak {B}}(x_{1},\dots ,x_{n})$ you get EXACTLY THE SAME resulting formula, but obviously $y_{1},\dots ,y_{n}$ are not bound in ${\mathfrak {A}}$. This finally proves that my interpretation is correct, and so yours not. The end. Germanomosconi1 (talk) 16:10, 9 August 2023 (UTC)