Do you know if I can find the proof that the existential theory of Z with the structure of addition , divisibility and the relation (∃s∈Z)m=nps is undecidable, besides the one of the paper of J. Denef “The diophantine problem for polynomial rings of positive characteristic” ? In the paper of Denef, the corollary is … Read more
Let $PA_{\omega}$ be just like $PA$ except that $PA_{\omega}$-proofs can use any number of applications of the recursive $\omega$-rule. The recursive $\omega$-rule allows the following: For each formula $\varphi$ with one free variable, if there is a unary total recursive function $f$ such that $\forall n \in N$, $f(n)$ is the code of a proof … Read more
Ordinal analysis is typically described as characterizing recursive ordinals in a theory T, but there is a sense in which it can characterize all T-ordinals, even those that are nonrecursive. Specifically, in such ordinal analysis, we want a canonical – recursive set of terms – recursive well-ordering ‘≺‘ of terms – assignment formula φ converting … Read more
In my previous question The inconsistency of Graham Arithmetics plus ∀n,n<g64, I introduced an extension of Robinson Arithmetics with the recursive definition of Tetraction, a small fragment of arithmetics which I have christened Graham (if someone comes up with a better name, please enter it in comments). I have also added an axiom which makes … Read more
If I am not mistaken, the provably total functions of PA are exactly those definable in terms of the functionals of higher type T, as introduced by Gödel in his 1958 Dialectica paper. In particular, for theories Σn−IA, the fragments of PA where induction is restricted to Σn formulae, and for the classes of functions … Read more
Previously asked on MSE. Given a simple graph G=(V,E) and an edge uv∈E, the contraction of uv refers to the replacement of the vertices u and v with a new vertex w such that the edges incident on w correspond to the ones that were incident on either u or v. Edge contraction comes up … Read more
Let EA+CE be elementary arithmetic with cut elimination theorem. Is there a simple (1-)consistency proof of EA over EA+CE? I think that a naïve consistency proof of EA fails because an evaluation function of terms of EA is not elementary recursive. Of course, CE implies totality of a superexponential function (by a theorem of Statman, … Read more
Two pieces of hearsay I have encountered about Robinson’s Q: Q fails to satisfy the Löb derivability conditions; Pudlák criticised the Löb derivability conditions and suggested rival, weaker conditions. Which leads to three questions, if the above are right: Which derivability condition(s) does Q not satisfy; What were Pudlák’s rival conditions and what was his … Read more
We have all been there, when a formula works for the first 30 parameters, but it is not sufficient for a proof. My question is where one can actually just check a finite number of cases, to conclude that a formula is correct. That is, let f,g:S→N be two functions from some (infinite) set S, … Read more
For every true arithmetical statement T, there are T-incomparable Π^0_1 statements, but can we find them uniformly in \text{Theory}(T)? Specifically, are there computable A and B such that for all arithmetical statements T⊢\text{EA}: A_T and B_T are Π^0_1 statements uniformity: \text{Theory}(T’) = \text{Theory}(T) ⇒ \text{EA}⊢(A_{T’}⇔A_T)∧(B_{T’}⇔B_T) incomparability: if T is true, then T⊬A_T⇒B_T and T⊬B_T⇒A_T. If … Read more
