## Sunday, 2 October 2011

### How Might PA be Inconsistent?

The recent discussion of Edward Nelson's claim to have a found a proof that Peano arithmetic, $PA$, is inconsistent has been very interesting in many ways. The proof has turned out to contain a major flaw and Professor Nelson has very graciously withdrawn the claim. I was not able to follow the alleged proof because I don't know enough about Chaitin's Theorem, or about the properties of the system $Q_0^{\ast}$ being examined. But the episode set me thinking about what might lie behind an inconsistency in $PA$, despite the fact that we have many standard mathematical proofs that $PA$ is consistent (indeed, true).

For readers who are a bit rusty on the properties of first-order arithmetic, here is some background and attempted explanation. $PA$ is a basic mathematical theory which functions, for mathematical logicians, roughly as E. Coli functions for microbiologists. $PA$ is a theory expressed in a first-order formalized language $L_A$ (with identity) with
four primitive non-logical symbols: $0$, $S$, $+$, $\times$
Each of these is, in effect, functional. Along with the variables, $x_1, x_2, \dots$, one can define the terms of the language by saying that $t$ is a term if $t$ is $0$, or a variable, or is obtained by applying $S$, $+$ or $\times$ to previous terms. (This is a recursive definition.) Because $L_A$ has only one primitive predicate symbol, namely $=$, the atomic formulas of $L_A$ are equations, of the form
$t = u$,
where $t$ and $u$ are terms. For reasons of metalogical simplicity, it is usual to assume that the only logical primitives, beyond $=$, are $\neg$, $\rightarrow$ and $\forall$. Other truth-functional connectives can be defined (e.g., $\phi \vee \theta$ is short for $\neg \phi \rightarrow \theta$) and $\exists x \phi$ is short for $\neg \forall x \neg \phi$.

The $L_A$-formulas are defined, again recursively, by saying that $\phi$ is a formula of $L_A$ just if either $\phi$ is an atomic formula (i.e., an equation) or is obtained from previous formulas by applying connectives or a quantifier (i.e., $\forall x$).

The axioms of $PA$ are then specified as the following six individual axioms, and one axiom scheme.
Individual Axioms of $PA$:
$PA1$. $S(x) \neq 0$.
$PA2$. $S(x) = S(y) \rightarrow x = y$.
$PA3$. $x + 0 = x$.
$PA4$. $x + S(y) = S(x + y)$.
$PA5$. $x \times 0 = 0$.
$PA6$. $x \times S(y) = x \times y + x$
and
Induction Scheme: $IND_{\phi}$
$[\phi(0) \wedge \forall x(\phi(x) \rightarrow \phi(S(x)))] \rightarrow \forall x \phi(x)$
where $\phi(x)$ is a formula of $L_A$. The formula $\phi(x)$ may contain other free variables (called "parameters"). $\phi(0)$ means the result of substituting the term $0$ for all free occurrences of $x$ in $\phi$.

The axioms of $PA$ are then the above six and all instances of the Induction Scheme. In addition, there are underlying purely logical axioms, for example,
$\phi \rightarrow (\theta \rightarrow \phi)$
$\forall x \phi \rightarrow \phi(x/t)$
and, usually, one or two inference rules (e.g., Modus Ponens: from $\phi$ and $\phi \rightarrow \theta$, infer $\theta$). A derivation of $\phi$ in $PA$ is a finite sequence $(\theta_1, \dots, \theta_n)$ such that $\theta_n$ is $\phi$, and each, for $i \in \{1, n\}$, $\theta_i$ is either a logical axiom, or an axiom of $PA$, or is obtained by Modus Ponens on some previous $\theta_k$ and $\theta_p$. If there is a derivation of $\phi$ in $PA$, then $\phi$ is a theorem of $PA$, and we write:
$PA \vdash \phi$
Our specification of the axioms $PA$ is parasitic on our prior understanding of the set $N$ of natural numbers and their properties with respect to successor, addition and multiplication. So, one can define an $L$-interpretation $\mathbb{N}$ by specifying that $dom(\mathbb{N}) = N$, and that $0$ refers to $0$, $S$ refers to successor and that $+$ and $\times$ refer to plus and times.

This gives the interpreted language $(L_A, \mathbb{N})$. It is precisely this interpreted language that we have in mind when writing the axioms formally as opposed to informally. The constraint is that we formalize the informally expressed truths into truths of this language, and keep the interpretation fixed. One can verify that each axiom of $PA$ is true in $\mathbb{N}$. (The verification is in a sense circular. For example, the meta-theoretic assumption required to verify that $\forall x(S(x) \neq 0)$ is true is precisely the fact that $0$ is not a successor of any number. But this is no different from showing that the truth of "snow is white" follows from the assumption that snow is white. To show each axiom true, we assume that very axiom.) Since the inference rules are sound, it follows that each theorem of $PA$ is true. Consequently, since $0 = 1$ is not true, it follows that $0=1$ is not a theorem of $PA$. So, $PA$ is consistent. This reasoning can itself be formalized by adding a new truth predicate symbol to the language $L_A$ and setting out the required properties of truth. This leads to the area of axiomatic truth theories.

How might $PA$ be inconsistent? Here are four guesses:
1. Perhaps there is something wrong with the successor axioms (i.e., $PA1$ and $PA2$).
2. Perhaps there is something wrong with the defining clauses for $+$ and $\times$ (i.e., $PA3-PA6$: these are examples of definition by primitive recursion).
3. Perhaps there is something wrong with the induction scheme.
4. Some combination of the above.
The successor axioms force any model of them to be infinite. If $X$ is a set containing say $a$, and $f : X \rightarrow X$ is injective and such that $f(x) \neq a$ (for all $x$), then $X$ must be infinite. From the point of view of the theory itself, the infinity is only "potential" (the axioms $PA1$ and $PA2$ themselves does not assert the existence of an infinite object: rather, the semantic meta-theory asserts the existence of an infinite object---i.e., a model---satisfying them). So, presumably, for an inconsistency to arise with the successor axioms, there must be some problem with potential infinity. However, I really cannot see a genuine argument here, other than a dogmatic rejection of even potential infinity. (The objects in question are mathematical abstract objects, not concrete tokens.)

Perhaps defining arithmetic operations by primitive recursion is problematic, and potentially inconsistent. (There is a standard mathematical proof that it isn't: Dedekind's recursion theorem.) Perhaps because primitive recursions exhibit a kind of "circularity"? (Roughly, $f(n+1)$ is defined in terms of $f(n)$.) But, again, I cannot see a genuine problem, as the circularity is only apparent: a primitive recursive definition of a function $f$ allows one to compute $f(n)$, for any argument $n$, requiring only the values for smaller numbers.

What has been most often suggested is that the induction scheme might lead to an inconsistency somehow. Aside from general ultra-finitist concerns (which I think are based merely on type/token confusion), it's unclear what exactly might happen to generate an inconsistency. What seems a likely proof idea is that one could find a formula $\phi(x)$ and a term $t$ (no matter how specified) such that one can show:
Inductive Inconsistency of $PA$ with respect to $\phi(x)$ and $t$:
(i) $PA \vdash \phi(0)$
(ii) $PA \vdash \forall x(\phi(x) \rightarrow \phi(Sx)))$
(iii) $PA \vdash \neg \phi(t)$
To explain why we have not "observed" an inconsistency, it might be the case that the shortest derivation $d$ of $0=1$ remains incredibly huge. The reason is that the derivation would have to generate a canonical term $SSS....S0$ (say representing the number $n$), and prove $t = SSS...S0$, and apply Modus Ponens $n$ times to get $\phi(t)$, contradicting (iii). But the size of $n$ might be astronomical.

Perhaps an example is a theory $T$ with axioms:
1. $x + 0 = x$.
2. $x + S(y) = S(x + y)$.
3. $x \times 0 = 0$.
4. $x \times S(y) = x \times y + x$
5. $2^{0} = S0$.
6. $2^{S(x)} = 2 \times 2^{x}$
7. $F(0)$
8. $F(x) \rightarrow F(S(x))$
9. $\neg F(2^{2^{2^{2^{2}}}})$
(where $2$ is defined to mean $SS0$)
I think a similar example was first given by Rohit Parikh in the 1970s, though I haven't seen the original. So, this example might be quite different from Parikh's. If I've worked this out right, then $T$ is inconsistent, but the shortest derivation of an inconsistency has length at least $2^{65,536}$ symbols. (On the other hand, I may be wrong in specifying this: there may be a clever trick which allows one to get round the specification of a canonical numeral $SS...S0$ with $2^{65,536}$ occurrences of $S$.)

George Boolos, in a 1987 paper, "A Curious Inference", gave an example of a theory similar to the one above which is inconsistent, where the number of symbols in the shortest such derivation is an exponential stack of $65,536$ 2s. (Actually, Boolos gave a valid inference whose shortest derivation is of this length, but one can easily convert it to an example of such a theory by negating the conclusion formula.)

1. Nice post! There are a lot of technical aspects to Nelson's proposed proof, but I think all philosophers of mathematics would enjoy Chaitin's Theorem:

http://en.wikipedia.org/wiki/Kolmogorov_complexity#Chaitin.27s_incompleteness_theorem

I consider this result to be vastly more mind-blowing than Goedel's incompleteness theorems, even though it's closely related. Simply put, it goes like this.

Let the "Kolmogorov complexity" of a (finite) string of bits be the length of the shortest computer program that prints out that string. Fix a computer language ahead of time, so this is well-defined. Also fix a finitely axiomatizable system of mathematics, which we'll assume is consistent: for example, Peano Arithmetic, or Zermelo-Fraenkel set theory. Then:

There exists a constant L, such that for no string of bits has Kolmogorov complexity that provably exceeeds L.

This is true even though all but finitely many strings have Kolmogorov complexity exceeding L!

In short, while most things are complicated, there's a limit on how complicated we can prove things are.

The proof is nicely sketched in the Wikipedia article.

2. Hi John, many thanks.
Yes I know Chaitin's theorem! It used to be a recurrent theme on sci.logic. Panu Raatikainen has written a couple of things of the topic, maybe 10 years ago or so, concerning confusions that arise concerning its consequences.

In the first para, I think I mis-stated what I meant - what I meant to say is that I don't know the details of how Chaitin meshes with Nelson's proof strategy, in particular with his system $Q_0^{\ast}$ and its properties (e.g., he says a result from Shoenfield is formalizable in this theory - it proves its own quasitautological consistency - but I suppose the details are in his 1986 book Predicative Arithmetic).

Cheers,

Jeff

3. Dear Jeff,

You wrote:

"It is precisely this interpreted language that we have in mind when writing the axioms formally as opposed to informally. The constraint is that we formalize the informally expressed truths into truths of this language, and keep the interpretation fixed. One can verify that each axiom of PA is true in N. (The verification is in a sense circular...)"

I would argue that it is this subjectively-imposed constraint on a 'fixed' interpretation that has perhaps prevented a satisfactory perspective concerning a proof of consistency for PA!

After all, if the intention is to formalise a subjectively conceived informal concept, then the aim of any sound interpretation of the formalisation cannot be to arrive back at the subjectively conceived informal concept.

Rather, the aim would reasonably be to arrive at what can be agreed upon as an objectively verifiable common core of such subjectively conceived concepts.

In other words, the aim would not be to try and justify a formal theory by the subjective interpretation that gave it birth, but to seek an objective interpretation that justifies the theory.

I have argued that this is possible in the paper 'Evidence-Based Interpretations of PA' that I presented at AISB/IACAP 2012, Birmingham last month.

http://alixcomsi.com/34_Evidence_Based_Interpretations_Of_PA_Final_AISB_IACAP_2012.pdf

Regards,

Bhup

4. Many thanks, Bhup.

"I would argue that it is this subjectively-imposed constraint on a 'fixed' interpretation that has perhaps prevented a satisfactory perspective concerning a proof of consistency for PA!"

But there is a satisfactory - by the standards of ordinary mathematics - proof of the consistency of PA. This consists in the observation that its axioms are true and that modus ponens preserves truth.
If one insists on changing the standards of mathematics to Cartesian standards, then of course one might become sceptical. Similarly, if I change my current epistemic standards to Cartesian standards, I may disbelieve that I have hands. But such modification of standards is itself unscientific & irrational.

If you begin with scepticism you will never escape, more or less by definition. This means that, in order to do science and mathematics, one must adopt ordinary scientific standards, not infallibilist Cartesian standards. Ordinary scientific standards do not demand infallibilism or certainty. There is *always* a possibility of error.

So, adopting ordinary, fallible, scientific standards, I see the language of arithmetic as objectively interpreted. Its variables range over $\mathcal{N}$ and the primitive symbols denote the number zero, and the successor, addition and multiplication operations. Otherwise, I can't make sense of the claim that it has anything to do with number theory. I therefore don't see anything subjective about the natural numbers.

I think your claim must be that the language of arithmetic is *uninterpreted*. I disagree with that. Rather, it's is an interpreted language: $(\mathcal{L}, \mathbb{N})$.

Cheers, Jeff

5. Dear Jeff,

Sceptic! Difficult to see myself in that light, though I do prefer ‘convincing’ to ‘satisfactory’ in mathematical argumentation (which is why I have difficulty conceiving of any interpretation that admits completed infinities without qualification).

I assumed that the ‘fixed’ interpretation you referred to in your post was the Standard interpretation of PA over the structure of the natural numbers (I presume that it is this structure that you refer to by $(\mathcal{L}, \mathbb{N})$).

If so, then---even if the above is the intended interpretation (under Tarski’s classical definitions) that may initially motivate a human intelligence in the formalization that is defined as the first order Peano Arithmetic PA---I have essentially argued in my recent AISB/IACAP 2012 paper ‘Evidence-Based Interpretations of PA’ that (and suggested why) this interpretation (of PA) cannot be seen as sound; in the sense that the Axioms of PA are not seen to interpret as objectively true under the interpretation, and that the rules of inference are not seen as preserving such truth objectively under the interpretation.

However, I have further argued in the paper that there is an objectively definable, algorithmic (hence finitary), interpretation of PA (which could be seen as reflecting the way a machine intelligence would interpret PA over the numerals) which is sound; in the sense that the Axioms of PA can be shown to interpret as objectively true under the interpretation, and that the rules of inference can be shown to preserve such truth objectively under the interpretation.

http://alixcomsi.com/34_Evidence_Based_Interpretations_Of_PA_Final_AISB_IACAP_2012.pdf

In a follow-up paper, ‘Some Consequences of Evidence-Based Interpretations of PA’ (link below) that I am currently finalising, I argue further that the Standard interpretation of PA can be shown to be unsound (a conclusion that may perhaps lie implicitly at the heart of the argument that led Ed Nelson to conclude that PA is inconsistent), and suggest why this interpretation cannot validate the PA Induction Axiom schema.

http://alixcomsi.com/39_Consequences_Evidence_Based_Interpretations_Of_PA.pdf

This is the sense in which I remarked ‘… that it is this subjectively-imposed constraint on a 'fixed' interpretation that has perhaps prevented a satisfactory perspective concerning a proof of consistency for PA’.

Regards and thanks for your prompt response,

Bhup

6. Hello again, Bhup,

What would you say the cardinality of $\mathcal{L}$ is?

Cheers,

Jeff

7. Dear Jeff,

Let me respond obliquely to your question.

The philosophical position underlying the argumentation of my posts is that we may need to explicitly recognize the limitations on the ability of highly expressive mathematical languages such as ZF to communicate effectively (unless we can offer a finitary interpretation of ZF); and the limitations on the ability of effectively communicating mathematical languages such as PA (which can be shown to have a finitary interpretation) to adequately express abstract concepts---such as those involving Cantor's first limit ordinal $\omega$.

For instance, in an unpublished critical examination of the proof of Goodstein's Theorem (link below), I argue that we cannot add a symbol corresponding formally to the concept of an infinite' mathematical entity---such as is referred to symbolically in the literature by $\aleph$' or $\omega$'---to the first-order Peano Arithmetic PA without inviting inconsistency; and that no model of PA can admit a constant term greater than' any natural number (which I would term as a completed infinity).

http://alixcomsi.com/10_Goodstein_case_against_1000.pdf

Regards,

Bhup

8. Hi Bhup,

But I'm just asking for the cardinality of something you believe in.
You believe that there is some "formal" thing, which you call "$PA$", in some language $\mathcal{L}$. So, what is the cardinality of $\mathcal{L}$?

Cheers, Jeff

9. Dear Jeff,

You've lost me there!

Cardinal numbers are defined specifically as equivalence classes in a formal set theory such as ZF, which contains a sub-set of finite ordinals that, meta-mathematically, can be effectively put into a 1-1 correspondence with the natural numbers, and whose cardinal number is defined in ZF as $\aleph_{0}$.

PA is a specific, recursively defined, first order Peano Arithmetic, whose domain contains the numerals, which meta-mathematically can also be effectively put into a 1-1 correspondence with the natural numbers.

$\mathcal{L}$ seems to be the informal language of Peano Arithmetic in which the Standard interpretation of PA is defined, and whose domain is that of the of the natural numbers.

So what exactly do you mean by the cardinal number of $\mathca{L}$, or the cardinal number of something that I believe in?

And how exactly would a 'belief' be relevant, or even useful, here?

After all, I may choose to believe that Pegasus exists in a world of my conception in the same way as I choose to believe that 1+1=2 in the same world.

Prima facie, that should have less significance than my being able to convincingly demonstrate to others---with whom I share a common lingua franca---that their belief that Pegasus exists, or that 1+1=2 in their conception, would not 'conflict' with my beliefs or conceptions.

Regards,

Bhup

10. Hi Bhup,

So you think that $\mathcal{L}_{PA}$ is an infinite set with cardinality $\aleph_0$?

Cheers, Jeff

11. Dear Jeff,

Don't quite see how one could view $\mathcal{L}_{PA}$ as a well-defined ZF formula that is also a set in ZF; but OK I pass ... what's the catch?

Regards,

Bhup

12. Hi Bhup,

Well, $\mathcal{L}$ is the set of all expressions/strings. This is infinite, right?
And there are a couple of distinguished subsets, e.g., $Tm(\mathcal{L})$ and $Form(\mathcal{L})$ (both infinite too); and a couple of operations, namely concatenation and substitution.

Cheers, Jeff

13. Dear Jeff,

Yes, of course.

However I would describe them as denumerable (non ZF) sets in order to make clear that they are not formally defined ZF sets.

This is not mere pedantry.

In my proposed ICLA 2013 submission, I show that Goedel's famous 'undecidable' PA formula $[R(x)]$ is not algorithmically computable as always true, even though it is algorithmically verifiable as always true.

Now, $[R(x)]$ is defined as the arithmetical representation in PA of a primitive recursive number theoretic relation $Q(x)$ that, by definition, is algorithmically computable as always true.

This means that, for any natural number $n$ and numeral $[n]$:

If $Q(n)$ is true then $[R(n)]$ is PA-provable;
If $Q(n)$ is false then $[\neg R(n)]$ is PA-provable.

Thus $[R(x)]$ and $Q(x)$ are instantiationally ‘equivalent’ arithmetical relations, but the latter is algorithmically computable whilst the former is not!

This distinction is not possible in ZF, where we would represent the ranges of $[R(x)]$ and $Q(x)$ as completed infinities (i.e. as sets of ordinals in ZF) that define the same ZF relation by the ZF Axiom of Extension.

Regards,

Bhup

14. Hello Bhup,

So I think you agree that $\mathcal{L}$ is an infinite set.

I'm not sure what your formula $[R(x)]$ is meant to be and how it is related to the fixed point $G$ of $Prov_{PA}(x)$.

Cheers, Jeff

15. Dear Jeff,

Yes, we agree that $\mathcal{L}$ is an infinite set.

The formula $[R(x)]$ is the one with Goedel-number $r$ defined by Goedel (in his seminal 1931 paper on formally undecidable arithmetical propositions), for which he first proved that the (fixed point) formula $(\forall x)R(x)$ with Goedel number $17 Gen r$ is not provable in the second-order Peano Arithmetic P (also specifically defined by him in the 1931 paper) if P is consistent; and then proved that the formula $\neg(\forall x)R(x)$ with Goedel number $Neg(17 Gen r)$ is also not provable in P if P is further assumed to be $\omega$-consistent.

Goedel constructed $[R(x)]$ such that, if $[R(x)]$ interprets as the arithmetical relation $R*(x)$ then, for any natural number $n$ and numeral $[n]$:

If $R*(n)$ is a true arithmetical sentence then $[R(n)]$ is not PA-provable.

Regards,

Bhup

16. So, $[R(x)]$ is, in modern notation, $\neg Proof_{PA}(x, \ulcorner G \urcorner)$, where $G$ is such that
$PA \vdash G \leftrightarrow \forall x \neg Proof_{PA}(x, \ulcorner G \urcorner)$?

Cheers, Jeff

17. This comment has been removed by the author.

18. Dear Jeff,

Something odd here!

I would have thought that, in modern notation, $[R(x)]$, would be $\neg Proof_{PA}(x, \ulcorner R(x) \urcorner)$!

We would then have that $[G]$ is $[\forall x R(x)]$, and so $PA \vdash [G \leftrightarrow \forall x \neg Proof_{PA}(x, \ulcorner R(x) \urcorner)]$ would follow trivially.

Perhaps I need to go back to first principles and retrace Goedel's original argument.

Regards,

Bhup

Notation: Although I forgot to do so consistently in my previous post, I try to use square brackets to enclose expressions that denote formulas (uninterpreted strings) of a formal language $L$, so as to distinguish them from expressions that denote interpreted relations and/or functions that are not formulas of $L$.

19. Hello Bhup,

"so $PA \vdash [G \leftrightarrow \forall x \neg Proof_{PA}(x,\ulcorner R(x)\urcorner)]$ would follow trivially."

This is not right. Rather, what I think you have in mind is that $R(x)$ is the formula $\neg Proof_{PA}(x, \ulcorner G \urcorner)$, and $G$ is the formula $\forall x R(x)$.
Then we have:

$PA \vdash [G \leftrightarrow \forall x \neg Proof_{PA}(x,\ulcorner G \urcorner)]$

It's unclear even what your version means, but if it means what I think it means, then its right-to-left direction, i.e., $\forall x \neg Proof_{PA}(x,\ulcorner R(\dot{x}) \urcorner) \rightarrow \forall x R(x)$ is not provable in $PA$. This is not what a fixed point means.

$G$ is a fixed point of the undedicable *provability* predicate $Prov_{PA}(x)$ (which is a $\Sigma_1)$ formula), not the proof predicate $Proof_{PA}(x, y)$, which is decidable.

"... so as to distinguish them from expressions that denote interpreted relations and/or functions that are not formulas of L."

I don't quite get this ... these are *expressions* of English? Why are there any expressions of any language except $L$ involved at all? Why not just write $R(x)$ to mean some formula of the object language $L$, with $x$ free?

Cheers, Jeff

20. This comment has been removed by the author.

21. Dear Jeff,

You’re right, the fixed point $G$ (with which I am not familiar except through its definition only) for the proof predicate $Prov_{PA}(x)$ cannot be $[\forall x R(x)]$.

I was wrongly conjecturing the relation of $G$ to Goedel’s original argument in his 1931 paper.

This argument was based on the primitive recursive relations $prf_{PA}(x, y)$ ($x$ is the GN of a PA-proof of the PA-formula whose GN is $y$) and $q_{PA}(x, y)$ ($x$ is the GN of a PA-proof of the PA-formula---whose GN is $y$---when we replace the variable ‘$y$’ in this formula with its GN, i.e. with the value $[y]$).

Returning to your original query, if $[Q(x, y)]$ expresses $\neg q_{PA}(x, y)$ in PA, and $p$ is the GN of $[\forall x Q(x, y)]$, then $[R(x)]$ is the PA-formula $[Q(x, p)]$ (to which Goedel refers by its GN ‘$r$’), and Goedel’s original undecidable proposition in PA would be the formula $[\forall x R(x)]$ (whose GN Goedel denotes by ‘$17Genr$’).

The reason I use square brackets is to be able to distinguish clearly between the natural number $y$ and the numeral $[y]$ in an argument such as the one above.

Regards,

Bhup

22. Hello Bhup,

Ah, now I see what you mean when you write, "on the primitive recursive relations $prf_{PA}(x,y)$ ...". Normally, one should simply write "on the primitive recursive relations $prf_{PA}$ ...". Here $prf_{PA}$ is a relation, i.e., a subset of $\mathbb{N}^2$. Strictly speaking, "$prf_{PA}(x,y)$" is a sentence of the meta-language, containing variables "$x$" and "$y$". Similarly, it is better to say "the function $f$ ..." It would be a bit misleading to say "the function $f(x)$ ..." Normally, $f(x)$ is the value of the function $f$ on argument $x$ (and "$f(x)$" is a singular term denoting this value). It's important to distinguish a function $f$ from its value $f(x)$; or, analogously, a relation $R$ and the entity $Rxy$ (which is, technically, a truth value, given $x$ and $y$) or the meta-language sentence "$Rxy$".

"$q_{PA}(x,y)$ ($x$ is the GN of a PA-proof of the PA-formula---whose GN is $y$---when we replace the variable ‘$y$’ in this formula with its GN, i.e. with the value $[y]$)."

I don't quite get this? What formula does "... in this formula ..." refer to? I think you intend to refer to some sort of diagonalization?
The usual definition is this. If $\phi(x)$ is a formula with $x$ free, then the diagonalization of $\phi(x)$ is $\phi(\ulcorner \phi \urcorner)$.
So, your relation $q_{PA}$ is the diagonal relation?

Cheers, Jeff

23. Dear Jeff,

1. The modern notation that you prefer seems suited to argumentation in the language of a set theory such as ZF, which defines functions and relations as sets. By the axiom of extensionality, two functions or relations are identical if they define the same set. My AICB/IACAP 2012 paper---and the paper that I have just submitted to ICLA 2013---aim to highlight a curious limitation of such a language.

2. I find that the classical notation followed in Mendelson's Introduction to Mathematical Logic' and Kleene's Introduction to Metamathematics' is not similarly limited, since they treat function/relation symbols in a formal language (such as $R$' in PA or $prf_{PA}$' in Primitive Recursive Arithmetic) as part of the alphabet only for constructing the formulas that denote functions and relations in the language (such as $R(x)$' in PA or $prf_{PA}(x, y)$' in PRA).

3. The distinction is convenient when I argue that there are number theoretical relations / functions that are not computationally identical, even though their corresponding relations / functions over the ZF ordinals may define the same set.

4. More precisely---and expressing it for the moment in the notation that I have been using---if $[(Ax)R(x)]$ is Goedel's undecidable PA formula, then there is a primitive recursive number theoretic relation $q_{PA}(x)$ in PRA (clarified further in 7 below) such that, for any natural number $n$ and numeral $[n]$, we have the metamathematical equivalence:

The PRA expression denoted by $\neg q_{PA}(n)$ evaluates as true in $N$ iff the PA formula denoted by $[R(n)]$ interprets as true in $N$ under any sound interpretation of PA.

5. However, I show that whereas there is an algorithm that will give evidence to show that any member of the denumerable sequence of PRA expressions denoted by $\{\neg q_{PA}(1), \neg q_{PA}(2), \ldots \}$ evaluates as true in $N$, there is no algorithm that will give evidence to show that any member of the denumerable sequence of PA formulas denoted by $\{[R(1)], [R(2)], \ldots \}$ interprets as true in $N$ under a sound interpretation of PA.

6. In the terminology of my paper, whilst the PRA relation $\neg q_{PA}(x)$ is algorithmically computable as always true in $N$, the (metamathematically) instantiationally equivalent PA relation $[R(x)]$ is algorithmically verifiable, but not algorithmically computable, as always true in $N$ under a sound interpretation of PA.

7. As to your final query, I think Wikipedia refers to the argument involved in this case (i.e. Goedel's argument) as indirect self-reference'. Perhaps I should have expressed the metamathematical interpretation of the primitive recursive relation $q_{PA}(x,y)$ unequivocally by writing:

$q_{PA}(x,y)$ ($x$ is the GN of a PA-proof of the PA-formula $[\phi]$---whose GN is $y$---when we replace the variable $y$' in the formula $[\phi]$ (whose GN is $y$) with the numeral $[y]$ that denotes the GN $y$ in PA.'

I am not sure if there is any diagonalisation' involved in the above in the sense of your remarks, since $[\phi]$ is not necessarily a formula in a single variable. The $[\phi]$ considered in Goedel's argument is actually a formula $[\phi (x, y)]$ with two variables.

Thus, in his 1931 paper (as translated in The Undecidable' edited by Martin Davis) Goedel's original definition of the primitive recursive relation $\neg q_{PA}(x,y)$' is expressed as:

$\neg xB_{\kappa}[Sb(y \scriptsize \begin{array}{c} 19 \\ Z(y) \end{array})]$

Kind regards,

Bhup