The n-Category Café

Over on Google+, Terry Tao writes:

I have read through the outline. Even though it is too sketchy to count as a full proof, I think I can reconstruct enough of the argument to figure out where the error in reasoning is going to be. Basically, in order for Chaitin’s theorem (10) to hold, the Kolmogorov complexity of the consistent theory T has to be less than $\ell$. But when one arithmetises (10) at a given rank and level on page 5, the complexity of the associated theory will depend on the complexity of that rank and level; because there are going to be more than $2^\ell$ ranks and levels involved in the iterative argument, at some point the complexity must exceed $\ell$, at which point Chaitin’s theorem cannot be arithmetised for this value of $\ell$.

(One can try to outrun this issue by arithmetising using the full strength of $\mathrm{Q}_0^*$, rather than a restricted version of this language in which the rank and level are bounded; but then one would need the consistency of $\mathrm{Q}_0^*$ to be provable inside $\mathrm{Q}_0^*$, which is not possible by the second incompleteness theorem.)

I suppose it is possible that this obstruction could be evaded by a suitably clever trick, but personally I think that the FTL neutrino confirmation will arrive first.

probably a stupid question, but if it would be true that Peano arithmetic is inconsistent, then what did Gerhard Gentzen do wrong? I thought he showed the consistency of the Peano aximons (but with methods outside of Peano arithmetic)…

A bit of expansion on my previous remarks. (I was unable to figure out how to write in math mode on this platform, unfortunately; sorry.)

Nelson’s argument is an attempt to modify the Kritchman-Raz proof of the second incompleteness theorem, which in turn is based on the Chaitin incompleteness theorem. (I recommend reading the Kritchman-Raz Notices article, by the way.)

The Chaitin incompleteness theorem is a rigorous version of the Berry paradox. Roughly speaking, it says that if a number x has Kolmogorov complexity K(x) greater than l, and T is a consistent theory, then T will be unable to prove that K(x) is actually greater than l, *provided that l is sufficiently large depending on T* (in particular, l has to be larger than the complexity of T itself). In particular, it provides a simple proof of the first incompleteness theorem. The proof proceeds by running Berry’s “first uninteresting number” argument, where “number” should be replaced by a pair (x,p) where x is a number and p is a proof (using some reasonable ordering on pairs to define “first”), and “(x,p) is uninteresting” means “p is a proof in T that K(x) > l.” This gives a number x for which both K(x) \leq l (provided l is larger than the complexity of T), and for which T can prove that K(x) > l, demonstrating the inconsistency of T.

The Kritchman-Raz argument combines Chaitin’s theorem with a version of the unexpected hanging paradox to prove the second incompleteness theorem, that a reasonable consistent theory T cannot prove its own consistency. The idea is to take the number l provided from Chaitin’s theorem, and try to count the number \mu of the numbers less than 2^{l+1}+1 that have Kolmogorov complexity greater than l. Clearly there \mu is at least 1, because there are only 2^{l+1} programs of length l or less. If \mu is exactly 1, then one can run all programs of length l or less in parallel until all but one of the numbers less than 2^{l+1}+1 is outputted, thus proving that the remaining number has complexity greater than l; but this contradicts Chaitin’s theorem. Thus \mu is at least 2. But if \mu is exactly 2, one can run all the programs of length l or less in parallel until all but two of the numbers less than 2^{l+1}+1 are outputted, proving (in T) that the remaining two numbers have complexity greater than l, again contradicting Chaitin’s theorem (here we have to implicitly use the fact that T can prove its own consistency). We can continue this argument 2^{l+1}+1 times to conclude that \mu > 2^{l+1}+1, which is absurd.

What Nelson is trying to do is to modify the Kritchman-Raz argument using a theory slightly weaker than PA that he calls Q_0^*. Of course, we know that this theory cannot prove its own consistency (if it is consistent), by the second incompleteness theorem. However, the theory is hierarchical, and roughly speaking contains a nested sequence Q_1 \subset Q_2 \subset Q_3 \subset \ldots of increasingly stronger theories, such that each Q_{i+1} can prove the consistency of the predecessor Q_i. The idea is to run the Kritchman-Raz argument to show that Q_1 can prove that \mu>1, that Q_2 can prove that \mu>2, and so forth, until one shows that Q_{2^{l+1}+1} (and thus Q_0^* and PA) can prove that \mu > 2^{l+1}+1, which is absurd.

Unfortunately, in order to make this work, all of the intermediate theories Q_1,Q_2,\ldots need to have Kolmogorov complexity less than l, in order to be able to invoke Chaitin’s theorem for these intermediate theories. But there are over 2^{l+1} of these theories, and so at least one of them has to have complexity greater than l, so the argument does not seem to work.

[Let me see if I can get the tex to work – DC]

A bit of expansion on my previous remarks.

Nelson’s argument is an attempt to modify the Kritchman-Raz proof of the second incompleteness theorem, which in turn is based on the Chaitin incompleteness theorem. (I recommend reading the Kritchman-Raz Notices article, by the way.)

The Chaitin incompleteness theorem is a rigorous version of the Berry paradox. Roughly speaking, it says that if a number $x$ has Kolmogorov complexity $K(x)$ greater than $l$, and $T$ is a consistent theory, then $T$ will be unable to prove that $K(x)$ is actually greater than $l$, provided that $l$ is sufficiently large depending on $T$ (in particular, $l$ has to be larger than the complexity of $T$ itself). In particular, it provides a simple proof of the first incompleteness theorem. The proof proceeds by running Berry’s “first uninteresting number” argument, where “number” should be replaced by a pair $(x,p)$ where $x$ is a number and $p$ is a proof (using some reasonable ordering on pairs to define “first”), and “$(x,p)$ is uninteresting” means “$p$ is a proof in $T$ that $K(x) \gt l$.” This gives a number $x$ for which both $K(x) \leq l$ (provided $l$ is larger than the complexity of $T$), and for which $T$ can prove that $K(x) \gt l$, demonstrating the inconsistency of $T$.

The Kritchman-Raz argument combines Chaitin’s theorem with a version of the unexpected hanging paradox to prove the second incompleteness theorem, that a reasonable consistent theory T cannot prove its own consistency. The idea is to take the number $l$ provided from Chaitin’s theorem, and try to count the number $\mu$ of the numbers less than $2^{l+1}+1$ that have Kolmogorov complexity greater than $l$. Clearly there $\mu$ is at least $1$, because there are only $2^{l+1}$ programs of length $l$ or less. If $\mu$ is exactly $1$, then one can run all programs of length $l$ or less in parallel until all but one of the numbers less than $2^{l+1}+1$ is outputted, thus proving that the remaining number has complexity greater than $l$; but this contradicts Chaitin’s theorem. Thus $\mu$ is at least $2$. But if $\mu$ is exactly $2$, one can run all the programs of length $l$ or less in parallel until all but two of the numbers less than $2^{l+1}+1$ are outputted, proving (in $T$) that the remaining two numbers have complexity greater than $l$, again contradicting Chaitin’s theorem (here we have to implicitly use the fact that $T$ can prove its own consistency). We can continue this argument $2^{l+1}+1$ times to conclude that $\mu \gt 2^{l+1}+1$, which is absurd.

What Nelson is trying to do is to modify the Kritchman-Raz argument using a theory slightly weaker than PA that he calls $Q_0^{\ast}$. Of course, we know that this theory cannot prove its own consistency (if it is consistent), by the second incompleteness theorem. However, the theory is hierarchical, and roughly speaking contains a nested sequence $Q_1 \subset Q_2 \subset Q_3 \subset \ldots$ of increasingly stronger theories, such that each $Q_{i+1}$ can prove the consistency of the predecessor $Q_i$. The idea is to run the Kritchman-Raz argument to show that $Q_1$ can prove that $\mu \gt 1$, that $Q_2$ can prove that $\mu \gt 2$, and so forth, until one shows that $Q_{2^{l+1}+1}$ (and thus $Q_0^{\ast}$ and PA) can prove that $\mu \gt 2^{l+1}+1$, which is absurd.

Unfortunately, in order to make this work, all of the intermediate theories $Q_1,Q_2,\ldots$ need to have Kolmogorov complexity less than $l$, in order to be able to invoke Chaitin’s theorem for these intermediate theories. But there are over $2^{l+1}$ of these theories, and so at least one of them has to have complexity greater than $l$, so the argument does not seem to work.

The following remarks from my conversation on Google+ may be helpful for people who know less logic than I do. I’ll end with a question for people who know more.

Someone said:

The part of the outline I really really don’t understand is everything to do with the formal systems $Q_0$ , $Q_0^*$ (roughly) of Robinson Arithmetic (said to be weaker than first-order Peano Arithmetic).”

The system $Q$ is “Robinson arithmetic”, a version of arithmetic much weaker than Peano arithmetic because it’s finitely axiomatizable and lacks the axiom schema of mathematical induction… but still strong enough that Gödel’s theorem applies! There’s a nice introduction here:

• Wikipedia, Robinson arithmetic.

On the other hand $Q_0$ is a slight variant of $Q$, apparently introduced by Nelson. In this variant Robinsons axiom

$$x \ne 0 \implies \exists y \, S y = x$$

is replaced by introducing a unary function symbol $P$ (predecessor) and two axioms:

$$P0 = 0$$

$$x \ne 0 \implies x = S P x$$

The technical advantage is that now no axioms have quantifiers! Gödel’s theorem still applies.

I don’t understand $Q_0^*$. The star stands for some kind of “relativization” process I never learned about. Could someone explain this?

Q^* can in fact prove a *form* of its own consistency. (This is also discussed in Sam Buss’s thesis chapter 7 for slightly stronger theories like S^i_2 which are still interpretable in Q. These theories are much weaker than PA).

As far as I understand from his outline, a very high level description of Nelson argument is as follows:

1. Q^* proves that Q^* is consistent’.

(This is a theorem from his previous work, Predicative Arithmetic. It can also be proven in PRA.)

2. PRA can prove KR result for Q^* (with consistency replaced with this weaker notion of consistency’). So PRA thinks that Q^* cannot prove its own consistency’.

(This seems to be what is new.)

3. PRA prove two contradictory results, therefore PRA is inconsistent.

This is a copy of a personal e-mail message I sent to Edward Nelson today.

Dear Prof. Nelson,

here is what is wrong with your proof of inconsistency of PRA. (The mistake in the proof I’m going to describe below is the same one found by Terrence Tao, by the way, but I will explain it in more detail.)

Formula numbers and page numbers refer to the outline:

http://www.math.princeton.edu/~nelson/papers/outline.pdf

Obviously, the $\ell$ in Chaitin’s theorem (formula (10)) depends on the theory $T$, so I will denote it by $\ell(T)$. (By the way, this $\ell(T)$ is what Terence Tao calls the “Kolmogorov complexity” of the theory $T$.)

Setting $\ell=\ell(Q_0^*)$, then, if $Q_0^*$ proves $K(\xi) \gt \ell$, then $Q_0^*$ is inconsistent.

Now let’s review the argument presented at the top of page 5. Working within $Q_0^*$, assume $\mu=1$. From this we obtain $\rho, \lambda, \xi$ and a $(\rho,\lambda)$-proof of $K(\xi)\gt \ell$. Now Chaitin’s theorem yields that $Q_0^*$ is inconsistent, i.e., that $Q_0^*$ proves (say) $not(0=0)$. But, (and here is the catch) Chaitin’s theorem does not yield that we have a $(\rho,\lambda)$-proof of $not(0=0)$!! So the first displayed formula on page 5 (line 7) is not correct.

Here is what is going on. Chaitin’s theorem can indeed be used to establish the implication:

there is a $(\rho,\lambda)$-proof of $K(\xi)\gt \ell$ $\implies$ there is a $(\rho,\lambda)$-proof of $not(0=0)$

but the relevant $\ell$ here is not $\ell(Q_0^*)$, but some other number $\ell(\rho,\lambda)$ which, roughly speaking, is the $\ell$ of the “theory” obtained by restricting proofs in $Q_0^*$ to $(\rho,\lambda)$-proofs. (More precisely, the relevant $\ell(\rho,\lambda)$ is defined in terms of the length of the Chaitin Turing machine that only inspects $(\rho,\lambda)$-proofs, rather than all proofs in $Q_0^*$.)

Best regards,
Daniel Tausk

I’d like to make some comments about Nelson’s reasoning other than his proof.

Nelson objects to “believing in ω as a real object” but then goes on to believe in ω. For instance, he uses Godel’s Completeness Theorem (p. 9, Elements), which depends on the existence of ω and is infinitary reasoning par excellence. And he believes in the totality of the successor function, where the ontological force of Peano Arithmetic really lays.

Nelson has no trouble believing in ω. All his complaints are simply a bait-and-switch for his worries about induction. Prime facie induction does not depend on believing in ω as a real object, as it makes a claim about the numbers that there are, and nothing whatever about *what* numbers there are. How does Nelson connect the two? By claiming that “the induction axiom schema is usually justified as follows…” (p. 11). I’m not a master of mathematical history, but the little that I know makes me doubt that the schema is or has been usually justified “as follows”. I, for one, would never think of justifying induction in this way. Perhaps a or some footnotes are in order here?

Finally, I have to disagree with the poster’s “The problem is making a consistent system of arithmetic that can prove itself consistent.” There are systems of arithmetic which can prove themselves consistent. There are natural systems of arithmetic which can prove themselves consistent. The problem, if problem there is, is developing a consistent, meaningful system of mathematics (e.g/ including analysis) that can prove itself consistent.

Herein (in one of the answers provided) you can find a link to a paper on a weak system of arithmetics, which seemingly proves its own consistency. Basically, as far as I understand it, in this system even multiplication is not total, and that in turn prevents Godel’s full-blown argument to apply:

http://mathoverflow.net/questions/9864/presburger-arithmetic

Anyway, I do not think that is the point.

The issue at stake (not in Nelson’s PA claim, but in the ultrafinistist’s program) is:

can we emancipate mathematics from N?

In other words, can we do away with all sorts of infinity (actual or potential), without depriving ourselves of its luxury?

By this I mean the following: if we built our mathematical world from, say, the initial segment
{0, 1, ….1000000000000000}, it wouldn’t be too good (too rigid, too crisp). But if, on the other hand, we had an arithmetical universe in which there are such beasts as finite inaccessible integers (yes, you have read the oxymoron correctly, it is not a typo), that would be way more interesting. Having parts (or perhaps all) of Cantor ‘s paradise squeezed down to the finitary realm, that would be, I trust, a real garden of eden, for mathematicians, for mathematical physicists (so they stop trying to make space-time discrete still using calculus), and finally it would be an excellent topic for Greg Egan’s next SF novel….

Over on Google+ I wrote:

Ultrafinitists don’t believe that really large natural numbers exist. The hard part is getting them to name the first one that doesn’t.

Richard Elwes replied, pointing out a conversation between the ultrafinitist Alexander Esenin-Volpin and the master of large infinities, Harvey Friedman. Friedman challenged Esenin-Volpin to name the first number that doesn’t exist:

I raised just this objection with the (extreme) ultrafinitist Esenin-Volpin during a lecture of his. He asked me to be more specific. I then proceeded to start with $2^1$ and asked him whether this is “real” or something to that effect. He virtually immediately said yes. Then I asked about $2^2$, and he again said yes, but with a perceptible delay. Then $2^3$, and yes, but with more delay. This continued for a couple of more times, till it was obvious how he was handling this objection. Sure, he was prepared to always answer yes, but he was going to take $2^{100}$ times as long to answer yes to $2^{100}$ then he would to answering $2^1$. There is no way that I could get very far with this.

I believe that after each question Esenin-Volpin was mentally counting to the desired power of 2, to verify that it really exists.

(In other words, he was checking that it could be constructed by repeatedly applying the successor operation to the number 0.)

On a digressive personal note: I met Esenin-Volpin back when I was grad student at MIT. He is quite a jolly fellow, despite having been imprisoned by the Soviets three times for his dissident political views.

They locked him a mental hospital — for “pathological honesty”, according to the famous dissident Vladimir Bukovsky. According to Wikipedia,

Volpin was the first dissident in the history of the Soviet Union who proclaimed that it is possible and necessary to defend human rights by strictly observing the law.

I know his student Christer (now Catherine) Hennix much better, and had many arguments with him, as he claimed all my mathematical research was founded on sand. At the time, my work involved a lot of analysis, based on principles that he disbelieved and argued against. I found that rather upsetting. I think I could handle it better now.

I much more enjoyed talking to Henry Flynt, the “cognitive nihilist” who founded concept art, but seems to have decided that only really worthwhile radical act is to undermine the foundations of mathematics. He had me explain Gödel’s theorem and other results from mathematical logic, a subject he was attempting to destroy. But somehow he didn’t hold my being a mathematician against me; he’s just too nice a guy.

I’m not exactly sure how I got hooked up with all these extremists, but it’s a darn good thing I did, since I met my wife Lisa through them. They were all part of the same art scene.

John wrote: ”In other words, he was checking that it could be constructed by repeatedly applying the successor operation to the number 0.”

I’m not an expert so can someone explain what all the fuss is about whether we can imagine applying the successor function repeatedly? Why can’t we pretend that we can?
Sorry for my vague question.

I have a question about Nelson’s paper, and a stupid one at that. Please note that I’m just a student, and my area is mostly mechanics and applied maths, but more abstract areas of mathematics and have always fascinated me, even though I don’t fully understand or have the time/desire to understand a lot of things.

I haven’t had the time to read the whole paper, but anyway - in every step leading up to the proof of inconsistency of PA, does he use only theorems that are not based on PA? In my understanding, if the proof is based on theorems that can be derived only from the axioms of PA, the proof is invalid.

Sorry if I posted something stupid, but this question has been bugging me since I stumbled onto this page.

So John it seems that much of this is about self reference is this correct?

And in that wikipedia article it says:

‘Edward Nelson criticizes the classical conception of natural numbers because of the circularity of its definition’

But how can we ever ‘get started’ if we dont accept the axioms?

How difficult is it to understand Godels theorems?

John, “But if you can prove within PA that PA is inconsistent, then PA is inconsistent.”

Gödel’s second incompleteness theorem implies that a consistent theory may prove its own inconsistency. For example, let $T = PA + \neg Con(PA)$. We know (assuming $PA$ is consistent), that $PA \nvdash Con(PA)$. Hence, $PA + \neg Con(PA)$ is consistent. In general, $PA$ also proves $Con(PA + \phi) \rightarrow Con(PA)$. So, $PA \vdash Con(PA + \neg Con(PA)) \rightarrow Con(PA)$. So, $PA + \neg Con(PA) \vdash \neg Con(PA + \neg Con(PA))$. So, $T \vdash \neg Con(T)$. But $T$ is consistent.

So, $T$ is a consistent theory which proves its own inconsistency. Of course, $T$ is not sound. (I.e., $\mathbb{N} \nvDash T$.) And $T$ is $\omega$-inconsistent, since $T$ proves .

(If this example is not liked because it assumes the consistency of $PA$, then let $S$ be any consistent extension of $I \Sigma_1$. Then $S + \neg Con(S)$ is a consistent theory which proves its own inconsistency.)

So, a proof within $PA$ that $PA$ is inconsistent establishes only that $PA$ is $\omega$-inconsistent. But it might still be consistent.

Jeff

Obviously I can’t speak for Nelson, but some quick points:

An ultra-finitist doesn’t need to deny the existence of the successor. It is a simple finitely describable object i.e. a simple operation (or algorithm if you like) to obtain the successor of a given number, no need to think of it as the graph of a function which is an infinite object.

The fact that Nelson tries to present the material in a way that classical mathematicians can understand doesn’t mean that he needs to do it that way, the presentation doesn’t mean that he believes in existence of them, e.g. you don’t need to talk about non-standard models of arithmetic at all.

An ultra-finitist does not need to give a natural number whose successor is not defined. If you can give a number (in unary) to an ultra-finitist, he can (probably) compute the successor of it (in principle), but the problem is that you cannot give very large numbers in unary to him. Also the time that is needed to compute the successor can increase with the size of input. Let’s say I give you a string of symbols which is 10000 pages long and claim that it is a natural number in unary, it will take you some time even to check my claim that it is really a number in unary. What is common mathematical practice is to use symbols and expressions (if you prefer terms of number type that are not in their normal form) in place of canonical numbers corresponding to them, but you need to prove that you can turn them into their normal canonical form, and the proof is not trivial, it depends on the operations that you are allowed to use. If we are talking about computing the successor operation, you need to give the input in its canonical unary form which you may not be able to do. Probably no one will ever apply the successor operation to 10^10^1000, not because there is a problem with successor but because no one is going to write that 10^10^1000 in its canonical normal form.

About the amount of classical analysis that can be carried out predictively (in Nelson’s sense), take a look at this. Note: BFTA is interpretable in Q.

Aside from other issues with this proof, given that it is part of an argument for something less than finitism, I’d at least expect it to be constructive.

To be constructive, it should give a particular derivation of “false” in the system(s) it claims to be inconsistent. If it can’t, then isn’t it just making vague, ungrounded statements about derivations without actually giving the concrete example of interest? How are we supposed to believe in such a thing if no one can tell us what it is?

If there were a non-constructive proof of a contradiction in PA, it could be transformed to a constructive proof. This follows from the Gödel-Gentzen double-negation translation.
http://en.wikipedia.org/wiki/G%C3%B6del%E2%80%93Gentzen_negative_translation

Not that I hope that Nelson is right, but not everything that Tao says is correct either…

see my post in FOM

http://www.cs.nyu.edu/pipermail/fom/2011-October/015830.html

Here’s another question from a nonmathematician. Suppose Nelson’s proof had turned out sound (or suppose that some other analogous proof does). What would then be the next steps for the mathematics community? What kinds of projects (whether salvage projects or reconstruction projects) would likely be called for? I have difficulty imagining that if PA were proven inconsistent that mathematicians would just throw out (when not specifically studying inconsistent systems) everything that depends on PA and say, “Oh, well, it was all good while the dream lasted.” In other words, if PA were proven inconsistent, what would be the next set of moves?

If Nelson’s proof had checked, there would have been a philosophical battle to sort out what kind of changes were better suited to provide a proper foundation for mathematics. But it is pretty obvious to me, from reading Nelson’s Outline, that he thought the problem was not simply with the axiom scheme for induction, but with induction itself. Nelson’s book “Radically Elementary Probability,” which is gorgeous and available freely, gives an idea of what might have happened.

I proved the inconsistency of arithmetic in an entirely different way. The P vs. NP problem is a golden opportunity for any inconsistency conjecture. P or NP consists of an infinite no. of languages where each language consists of an infinite no. of strings. A simple encoding of the Kleene-Rosser paradox brings the result (by diagonalization):

e(KR)in NP iff e(KR) not in NP.

See full papers at: http://kamouna.wordpress.com

For an easy beginner’s intro to the work of Kritchmann and Raz, see:

• John Baez, Chaitin’s theorem and the surprise examination paradox.

Also, Henry Flynt has alerted me to the existence of this paper on the arXiv, written by two of the ultra-finitists mentioned earlier:

• Alexander S. Yessenin-Volpin and Christer Hennix, Beware of the Gödel–Wette paradox.

The first sentence in the abstract seems to claim they’ve found an inconsistency in arithmetic, but I haven’t read the paper yet, and of course I make no claims for its validity. I mainly mention it because this blog entry is one of the few places one can find information on ultra-finitism.

I would like to inform that commonly with Dr Teodor J. Stepien, I delivered a talk “On consistency of Peano’s Arithmetic System”, at the Conference “2009 European Summer Meeting of Association for Symbolic Logic, Logic Colloquium’09” (July 31 - August 5, 2009, Sofia, Bulgaria). In this talk, we presented a sketch of the proof of the consistency of Peano’s Arithmetic System (of course, the full proof was constructed by us before the mentioned Conference “Logic Colloquium 2009”). This proof is ABSOLUTELY elementary, i.e. there are used ONLY the axioms of first-order logic and the axioms of Peano’s Arithmetic System. Hence, from the construction of this proof, it follows that Gödel’s Second Incompleteness Theorem is INVALID. The abstract of the talk mentioned above, was published in “The Bulletin of Symbolic Logic” : T. J. Stepien and L. T. Stepien, “On the consistency of Peano’s Arithmetic System”, Bull. Symb. Logic 16 , 132 (2010). The link to the Proceedings of the Conference “2009 European Summer Meeting of Association for Symbolic Logic, Logic Colloquium’09”, where this above mentioned abstract was placed: http://www.math.ucla.edu/~asl/bsl/1601-toc.htm

A proof that ZFC has no any omega-models

http://www.cs.nyu.edu/pipermail/fom/2013-February/016986.html

“”Then the theorem is that the class of functions computable in this way is precisely the class of polynomial-time functions. This is an astonishing result”“

Linear logician have achieved something similar too.

Also, there is roughly 3 case of induction (or recursion) : zero (aka not an induction), one (simple repetition, like a loop), and many (more than one repetition, something more like a tree). Those base case can be combined in order to get “bigger” induction. For instance, repetition is linear, repetition of repetition is quadratic, etc.

Restricting combination of reccurence patterns will only restrict expressivity. I don’t know how someone can expect to find a non termination proof…

Nelson strikes again, this time at Inconsistency of Primitive Recursive Arithmetic, arXiv:1509.09209