---
author:
- 'Michael Pfender[^1]'
date: |
    April 2014\
    last revised 
title: 'A positive solution to Hilbert’s 10th problem'
---

Introduction {#introduction .unnumbered}
============

Within theory $\ZFC^+ = \ZFC+\Con_{\ZFC}$ of Zermelo-Fraenkel **set** theory with axiom of choice $\AC,$ strengthened by formula $\Con_{\ZFC}$ which is to express $\ZFC$’s *internal,* *gödelised* consistency, we solve Hilbert’s 10th problem positively: we organise decision of diophantine polynome codes—decision on overall *non-nullity*—as an enumerative $\mu$-recursive race for a (first) zero (*counterexample*), against race for a first internal $\ZFC$-non-nullity *proof* for a given such polynomial code, given as the (nested) list of coefficients. Comparison with Matiyasevich’s negative solution of Hilbert’s 10th problem gives inconsistency of theory $\ZFC+\Con_{\ZFC}$ whence self-inconsistency $\ZFC \derives \neg \Con_{\ZFC}.$ In a final section we plug our positive solution of the problem into the constructive framework of *p.r. non-infinite descent theory* $\piR=\PR+(\pi)$ out of *Arithmetical Foundations* in the References.

This is to give a decision algorithm for each single diophantine equation (in a uniform way), as asked in the original Hilbert’s 10th problem.

Hilbert’s 10th Problem
======================

We attempt a positive solution to Hilbert’s 10th problem. In its original form it reads:

10\. DETERMINATION OF THE SOLVABILITY OF A DIOPHANTINE EQUATION Given a diophantine equation with any number of unknown quantities and with rational integer numerical coefficients: *To devise a process according to which it can be determined by a finite number of operations whether the equation is solvable in rational integers.*

\[translation quoted from 1993.\]

Formally, this text allows for a separate decision algorithm (“process”) for each diophantine polynomial. But it is clear that a decision-*family* must be *uniform* in a suitable sense.

*Correctness* of our alleged $\mu$-recursive decision algorithm $\nabla_{\ZFC}: \mr{DIO} \parto \two=\set{0,1}$ builds, within $\ZFC^+,$ on diophantine soundness inferred by $\Con_{\ZFC}$ over $\ZFC.$ Termination follows from (countable) Choice. This already within $\ZFC.$ Together this gives the wanted decision $\nabla=\nabla_{\ZFC}$ within $\ZFC^+,$ of all polynome codes in $\mr{DIO}\subset\N.$

Comparison with Matiyasevich’s negative Theorem, *unsolving* Hilbert’s 10th Problem, theorem in particular of (classically quantified Arithmetical Theory) $\ZFC^+,$ gives a contradiction within $\ZFC^+,$ hence [self-inconsistency]{} of $\ZFC,$ and from that in particular $\omega$-inconsistency.

In a final section we show correctness and irrefutable termination of *localised* decision $\nabla[D]$—for each single diophantine polynomial $D=D(\vec{x})$—within the constructive framework of p.r. *finite-descent-theory* $\piR=\piR+\Con_{\piR}$ out of op.cit.

Polynome coding and code evaluation
===================================

Diophantine polynomials $D = D(\vec{\xi}): \Z^* \to \Z$ (“in $\DIO$”) are LaTeX/**ASCII** coded into $$\mr{DIO} \defeq \Z^{\an{*}} \iso \union_{m\geq1} \Z[\xi_1,\ldots,\xi_m]  
                 = \union_{m \geq 1} \Z[\xi_1][\xi_2] \ldots [\xi_m]$$ as nested coefficient *lists* $\Z^{\an{*}} \subset \N.$

$[\,$The symbols $\xi_i$ are the *indeterminates.*$\,]$

### Example: {#example .unnumbered}

$$\begin{aligned}
D = D(\xi_1,\xi_2)  
& = (2\cdot\xi_1^{\,0}+3\cdot \xi_1^{\,1}- 4\cdot\xi_1^{\,3})\cdot\xi_2^{\,0} \\ 
& \quad
    +(0\cdot\xi_1^{\,0}+3\cdot\xi_1^{\,1}-7\cdot\xi_1^{\,2})\cdot\xi_2^{\,1}  
                                           + (1-4\cdot\xi_1)\cdot\xi_2^{\,2}\end{aligned}$$

is coded 1-1 as (nested) [coefficient list]{} $$\begin{aligned}
\ccode{D}  
& = \an{\an{2;3;0;4};\an{0;3;-7};\an{0};\an{1;-4}}: \\ 
& \one \to \mr{DIO} \bydefeq \Z^{\an{*}} \subset \N: \\
& \text{\emph{defined element, point} of $\mr{DIO}$}\end{aligned}$$

### PR evaluation of $\mbf{DIO}$ codes: {#pr-evaluation-of-mbfdio-codes .unnumbered}

Evaluation $\mr{ev} = \mr{ev}(d,\vec{x}): \mr{DIO} \times \Z^*$ is PR [defined]{} $$\begin{aligned}
& \mr{ev}(d,\an{\vec{x};x_{m+1}\,}) = \mr{ev}(d,\an{x_1;\ldots;x_m;x_{m+1}\,})\\
& \defeq \mr{ev}(\horner(d,x_{m+1}),\an{\,\vec{x}\,}): \\
& \mr{DIO} \times \Z^* \supset \Z[\vec\xi,\xi_{m+1}] \times \Z^{m+1} 
    \ovs{\iso} (\Z[\vec\xi] [\xi_{m+1}] \times (\Z^m \times \Z) \\
& \xto{\iso} (\Z[\vec\xi][\xi_{m+1}] \times \Z) \times \Z^m 
              \ovs{\horner \times \id} \Z[\vec\xi] \times \Z^m \xto{\ev} \Z,\end{aligned}$$ recursively by iterative application of Horner’s schema to the hitherto trailing argument, until all of the arguments (constants or variables) are substituted into their corresponding indeterminates $\xi_j.$

Result then is the integer $\mr{ev}(d,\vec{x}),$ constant or integer variable.

For the **example** above, $D = D(\xi_1,\xi_2),$ with argument string $\an{x_1;x_2} :\,= \an{23;64} \in \Z^*,$ we get $$\begin{aligned}
& \mr{ev}(d,\an{x_1;x_2}) 
    = \mr{ev}(\an{\an{2;3;0;4};\an{0;3;-7};\an{0};\an{1;-4}},\an{23;64}) \\
  %& = ?? \horner(\mr{ev}(\an{\an{2+3\cdot\xi_1^1+0\cdot\xi_1^2+4\cdot\xi_1^3};
  %&            \an{\an{0;3;-7}\cdot\xi_1}+\an{1-4\cdot\xi_1}},64),23) \\ 
  %& = \horner(\an{\an{2+3\cdot\xi_1+4\cdot\xi_1^3}\cdot64^0;
  %           \an{-7}\cdot64^1+\an{0\cdot64^2}
  %             +\an{1-4\cdot\xi_1}\cdot64^3},23) \\
  %& = \horner(\an{((((4\cdot\xi_1+0)\cdot\xi_1)+3)\cdot\xi_1+2)\cdot64^0 +\\
  %&   \qquad\qquad\qquad\qquad           
  %    (-7\cdot64^1)+(0\cdot64^2)+(4\cdot64^1-1)\cdot64^3},23) \\
  %& = (((4\cdot23+0)\cdot23)+3)\cdot23+2\ -7\cdot64\cdot23\ +\ 0\cdot23^2
  %                                         + (-4\cdot64+1)\cdot23^4 \\
& = \horner(\,
    ((((-4\cdot64+1)\cdot\xi_1+0))
                       \cdot\xi_1 +(-7\cdot64+3)\cdot64)\cdot\xi_1 \\
& \qquad\qquad\qquad\qquad\qquad\qquad\quad
    + ((4\cdot64+0)\cdot64+3)\cdot64+2\,,23\,) \\
& = ((((-4\cdot64+1)\cdot23+0))\cdot23 +(-7\cdot64+3)\cdot64)\cdot23 \\
& \qquad\qquad\qquad\qquad\qquad\qquad
    + ((4\cdot64+0)\cdot64+3)\cdot64+2\end{aligned}$$ **First step:** apply Horner’s schema to coefficient list $d \in \mr{DIO}$ und (trailing) Argument $x_2:$ [indeterminate]{} $\xi_1$ is [coded]{} by [list nesting]{} and is seen as a *constant*, as an element of intermediate ring $\Z[\xi_1]:$ $$\Z[\xi_1,\xi_2] \bydefeq \Z[\xi_1][\xi_2] \bydefeq (\Z[\xi_1])\,[\xi_2].$$ **Last—here second—step:** evaluation of $\Z[\xi_1]$ polynomial in remaining indeterminate $\xi_1$ on remaining argument $x_1,$ by a last application of Horner’s schema.

Arithmetical frame theories
===========================

We consider here as frame theories—for our decision algorithm – **on one hand** classically quantified arithmetical theories $\T = \bfQ+\AC$ with (countable) axiom of choice, as in particular Zermelo-Fraenkel set theory $\T = \ZFC = \ZF+\AC.$ Frame then is the strengthening $$\T^+ = \T+\Con_\T = \ZFC+\Con_{\ZFC}$$ of $\T$ by its own consistency-*formula* $$\begin{aligned}
\Con_\T &=& \neg\,(\exists\,k \in \N)\,\Pro_\T(k,\code{\false}) \\
&=& (\forall k)\,\neg\,\Pro_\T(k,\code{\false})\ (\text{G\"odel}),\end{aligned}$$ see 1977 and op.cit. Strengthening by this consistency formula will provide for *correctness* of our *decision process* (Hilbert).

**On the other hand** we take as frame the Free-Variables (categorical) theory $\T = \PR = \PRa$ of *Primitive Recursion with predicate abstraction into subsets* $$(\chi = \chi(a): A \to \two) 
  \boldsymbol\mapsto \set{A:\chi}=\set{a\in A:\chi(a)}$$ out of op.cit., $\T = \bfS$ in Smorynski’s notation, as well as *descent theory* $\piR = \piR^+ = \piR+\Con_{\piR}:$ that theory is self-consistent, $\piR \derives \Con_{\piR,}$ main result of op.cit.

A $\mu$-recursive race for decision
===================================

We **define** an enumerative *race*—for $d \in \mr{DIO}$ thought *passive, fixed,* and $k \in \N$ *running*—for satisfaction of $$\begin{aligned}
& \ph_0(d,k) = [\,\ev(d,\ct_*k)=0\,]\ \text{against} \\
& \ph_1(d,k) = \Pro_{\T}(k,\code{(\vec{x})\ev(d,\vec{x})\neq 0}):
  \mr{DIO} \times \N \to \two = \set{0,1}, \\
& \ct_* = \ct_*\,k: \N \ovs{\iso} \Zlist
  \ \text{Cantor-type \emph{count},}\  
    \vec{x} \in \Z^*\ \text{free under code.}\end{aligned}$$

This race towards *termination* is defined as a—formally partial—$\mu$-recursive mapping as follows within the theory $\hatT$ of *partial PR maps,* i.e. of (partially defined) *$\mu$-recursive maps,* cf. again op.cit.: $$t = t(d) = \mu\set{k\,|\,\ph_0(d,k)\,\lor\,\ph_1(d,k)}: 
                                          \mr{DIO} \parto \N. \quad (*)$$

**Decision candidate** then is $$\begin{aligned}
\nabla d =
& \begin{cases}
  0\ \myif\ \ph_0(d,t(d)) \\
  1\ \myif\ \ph_1(d,t(d)) \\
  \end{cases} \\
& \quad \\
=
& \begin{cases}
  0\ \myif\ \ev(d,\ct_*(t(d)))=0 \\
        \qquad (\emph{zero found}) \\
  1\ \myif\ \Pro_{\T}(t(d),\code{\ev(d,\vec{x})\neq 0}) \\
        \qquad (\text{\emph{internal proof} found
                        for \emph{global non nullity}})
  \end{cases} \\
& : \mr{DIO} \overset{(\id,t)} {\parto} \mr{DIO} \times \N \to \two.\end{aligned}$$

**Question:** Is $\nabla$ *well-defined* as a partial map? In which frame?

### Well-definedness of the decision within $\T^+ = \ZFC^+=\ZFC+\Con_{\ZFC} = \T+\Con_\T:$ {#well-definedness-of-the-decision-within-t-zfczfccon_zfc-tcon_t .unnumbered}

$$\begin{aligned}
\T^+\ \derives\ 
& \ph_0(d,k)\,\land\,\ph_1(d,k') \\
&     \qquad (\text{\emph{cases-overlap} 
                        {$\mathit{Assumption}$}}) \\
& \implies \ev(d,\ct_*k)=0 \\
& \quad\,\land\,\Pro_\T(k',\code{(\vec{x})\,\ev(d,\vec{x})\neq 0}) \\
& \implies \Pro_\T(j(k,k'),\code{\false}) \\
    %& \implies \gleichnull\,\land\,(\vec{x})\,\ungleichnull \\
    %& \quad \text{by \emph{diophantine Soundness} of}\ \ZFC+\ConZFC \\
& \implies \neg\,\Con_\T \implies \false, \\
& j=j(k,k'): \N^2\to \N\ \text{suitable.}\end{aligned}$$

**Consequence:** $$\T^+\ \derives\ \neg\,[\ph_0(d,k)\,\land\,\ph_1(d,k')\,]: 
                                     \mr{DIO} \times \N^2 \to \two,$$ $\nabla = \nabla_{\T}(d): \mr{DIO} \parto \N$ is *well-defined* as a (*formally partial*) $\mu$-recursive map, within $\T^+ = \T+\Con_\T.$

### Well-definedness of decision within *descent* theory $\piR:$ {#well-definedness-of-decision-within-descent-theory-pir .unnumbered}

We consider now *descent theory* $\piR$ out of op.cit.  strengthening $\PR$ by axiom $(\pi)$ of *non-infinite endo driven descending complexity with complexity values in polynomial semiring $\N[\omega],$* and its logical properties, in particular *soundness* giving $\piR\derives \Con_{\piR}.$

Decision $\nabla=\nabla_{\piR}(d):\mr{DIO}\parto \two$ is in fact well-defined as a partial PR map, within theory $\piR,$ since—in parallel to the above case $\T = \ZFC:$ $$\begin{aligned}
\piR\ \derives\ 
& \ph_0(d,k)\,\land\,\ph_1(d,k') \\
&     \qquad (\text{\emph{cases-overlap} 
                        {$\mathit{Assumption}$}}) \\
& \implies \ev(d,\ct_*k)=0 \\
& \quad\,\land\,\Pro_{\piR}(k',\code{(\vec{x})\,\ev(d,\vec{x})\neq 0}) \\
& \implies \Pro_{\piR}(j(k,k'),\code{\false}) \\
    %& \implies \gleichnull\,\land\,(\vec{x})\,\ungleichnull \\
    %& \quad \text{by \emph{diophantine Soundness} of}\ \ZFC+\ConZFC \\
& \implies \text{``$\neg\,\Con_{\piR}$''} \implies \false, \\
& j=j(k,k'): \N^2\to \N\ \text{suitable.}\end{aligned}$$ The latter since $\piR\derives \Con_{\piR}.$

### Well-definedness of DIO-decision within $\PR$ itself {#well-definedness-of-dio-decision-within-pr-itself .unnumbered}

Decision $\nabla=\nabla_{\PR}(d):\mr{DIO}\parto \two$ is well-defined as a partial PR map, within theory $\hatPRa$ of partial PR maps since $$\begin{aligned}
\hatPRa\ \derives\ 
& \ph_0(d,k)\,\land\,\ph_1^{\DIO}(d,k') \\
&     \qquad (\text{\emph{cases-overlap} 
                        {$\mathit{Assumption}$}}) \\
& \Iff \ev(d,\ct_*k)=0 \\
& \quad \land\,\Pro_{\DIO}(k',\code{(\vec{x})\,\ev(d,\vec{x})\neq 0}) \\
& \implies \Pro_{\DIO}(j(k,k'),\code{\false}) \\
    %& \implies \gleichnull\,\land\,(\vec{x})\,\ungleichnull \\
    %& \quad \text{by \emph{diophantine Soundness} of}\ \ZFC+\ConZFC \\
& \implies \false, \\
& j=j(k,k'): \N^2\to \N\ \text{suitable.}\end{aligned}$$ The latter by *diophantine soundness* of $\T=\PR,$ see 1977, <span style="font-variant:small-caps;">Theorem</span> **4.1.4**.

Decision Correctness
====================

**Decision Correctness, result-0-case:** $$\begin{aligned}
\T \derives\ 
& [\,\ph_0(d,t(d)) 
    \implies \mr{ev}(d,\ct_*\,\circ\,t(d))=0\,] \\
& \subseteq\,\true_{\mr{DIO}}: 
    \mr{DIO} \overset{(\id,t)} {\parto} \mr{DIO} \times \N \to \two:\end{aligned}$$ **If** race-for-decision $\nabla$ *terminates* on DIO-code $d,$ with **result** $0,$ **then** (evaluation of) $d$ has (at least) one zero, namely $$\ct_*\,\circ\,t(d) \in \N.$$

### Correctness, result-1-case: {#correctness-result-1-case .unnumbered}

$$\begin{aligned}
\T \derives\ 
& \ph_1(d,k) \implies \Pro_{\DIO}(k,\code{\ev(d,\vec{x})\neq 0}) \\
& \implies \ev(d,\vec{x})\neq 0: 
  (\mr{DIO} \times \N) \times \Z^* \to \two, \\
& (d \in \mr{DIO},\ k \in \N,\ \vec{x} \in \Z^*\ \text{all free}), \\
& \quad
    \text{or, with quantifier decoration:} \\
\T \derives\
& (\forall\,d \in \mr{DIO})(\forall\,k \in \N)
    (\forall\, \vec{x} \in \Z^*) \\
& [\,\ph_1^{\T} (d,k) \implies \Pro_{\DIO}(k,\code{\ev(d,\vec{x})\neq 0}) \\
& \implies \ev(d,\vec{x})\neq 0\,].\end{aligned}$$

**If** race-for-decision $\nabla$ *terminates* on DIO-code $d,$ with **result** $1,$ **then** (evaluation of) $d$ has no zeroes.

This because of *Diophantine Soundness* of $\T,$ see 1977, <span style="font-variant:small-caps;">Theorem</span> **4.1.4** again.

### Correctness in result-1-case, under termination condition: {#correctness-in-result-1-case-under-termination-condition .unnumbered}

Substitution of $t(d)$ for $k$ in the above gives $$\begin{aligned}
\T^+,\piR,\PR\ \derives\ 
& [\,\ph_1^{\DIO} (d,t) \implies \ev(d,\vec{x})\neq 0\,] 
  \subseteq\,\true_{\mr{DIO} \times \Z^*},\\
& d \in \mr{DIO},\ \vec{x} \in \Z^*\ \text{both free}: \end{aligned}$$ *Correctness* of $\nabla(d)$ where defined, in *both* defined cases: in case of reaching **result** 0, as well as in case of reaching **result** 1.

Termination
===========

We show first

**Pointwise non-derivability of non-termination:**

For no diophantine *point* $d_0: \one \to \mr{DIO}$ $\T$ derives non-termination of $t$ at $d_0.$

**Proof:** a contradiction: appropriate $\ulj$ is available from $(\bullet)$ via derivation-to-$\Proof$-internalisation (*gödelisation*).

$[\,$For the time being we consider $\T$ as frame, not (yet) $\T^+=\T+\Con_\T.\,]$

For $\T = \bfQ$ quantified, with (countable) *axiom of choice* $\ACC,$ in particular $\bfQ = \PA+\ACC$ Peano Arithmetic with choice, we define the *undecided part* of $\mr{DIO}$ as $$\begin{aligned}
\Psi &=& \Psi^{\bfQ} \\    
&=& \set{d \in \mr{DIO}:\forall\,k\ \mr{ev}(d,\ct_*\,k) \neq 0 \\
&& \,\land\,\forall\,k
  \ \neg\,\Pro_{\bfQ}(k,\code{(\vec{x})\,\mr{ev}(d,\vec{x}) \neq 0)})} \\
&\subset& \mr{DIO} = \Zlist \subset \N. \end{aligned}$$ With this definition we get $$\begin{aligned}
\bfQ \derives\
& \Psi \neq \emptyset
    \implies \choice_{\Psi}: \one \to \Psi \subset \N\ \emph{total} \\
& (\text{choice available by $\ACC:$ non-empty sets have 
        \emph{defined points}}) \\
& \implies \mu\set{d:t(d)\ \text{non-terminating}}:\one \to \Psi\ \emph{total.}  \end{aligned}$$ This means: the [assumption]{} of (formal) *existence* of a $d \in \mr{DIO}$ for which decision race $t: \mr{DIO} \parto \N$ does *not* terminate, leads to a (*defined*) point $$d_0:\one \to \mr{DIO}$$ for which $t$ derivably does not terminate.

But this is **excluded** by pointwise non-derivability above of non-termination, within frame $\bfQ$ assumed consistent.

So we have shown $$\begin{aligned}
& \bfQ,\PA+\ACC \derives\ \Psi = \emptyset,\ \text{i.\,e.} \\ 
& \bfQ \derives\ (\forall d\in \mr{DIO})[\exists k\,\ev(d,\mr{ct}_*k)=0 \\
& \qquad\qquad
  \lor \exists k\,\Pro_{\DIO}(k,\code{(\vec{x})\,\ev(d,\vec{x}}) \neq 0)],\end{aligned}$$ whence

**Termination Theorem:** $\bfQ,\ZFC,\PA+\ACC$ derive race $t$ to terminate on all diophantine codes $d,$ on all $d \in \mr{DIO} = \Zlist.$

Correct termination of decision $\nabla$
========================================

**In particular** ($\bfQ^+ = \bfQ+\ACC$ stronger than $\bfQ$): $$\begin{aligned}
& \bfQ^+\ \textbf{derives} \\
& \quad 
    \text{overall termination of $\mu$-recursive} \\ 
& \quad
    \text{termination race}\ 
                         t=t^{\bfQ}(d):\mr{DIO} \to \N: \\
& \bfQ^+\ \derives\
    [\,(\forall\,d \in \mr{DIO})\ t(d) \in \N
                   \ \text{{\emph{defined}}}\,]\end{aligned}$$

**Hence,** by Decision Correctness within $\bfQ^+:$

$\bfQ^+$ [$\mathbf{derives}$]{}\
[overall *correct* termination]{} of $\mu$-recursive *decision*\
$\nabla: \mr{DIO} \to \two,$ **main result** here: $$\begin{aligned}
& \nabla(d) \\
& = \begin{cases}
      0\ \myif\ \mr{ev}(d,t(d)) = 0 \\
      \qquad 
        \ [ \ \implies d\ \emph{has}
                         \ \text{a zero}\ \vec{z} \in \Z^*\ ] \\
      1\ \myif\ \Pro_{\DIO} 
              (t,\code{(\forall\,\vec{x})
                      \ \mr{ev}(d,\vec{x}) \neq 0}) \\
      \qquad 
        \ [ \ \implies d\ \text{has}\ \emph{no}\ \text{zero}\ ] 
    \end{cases}: \mr{DIO} \to \two.\end{aligned}$$

Comparison with Matiyasevich’s\
negative result
===============================

*Main result* above says in terms of the theory $\mathbf{TM}$ of TURING machines, by the established part of CHURCH’s thesis:

*For concrete diophantine polynomials* $D = D(\vec{x}): \Z^m \to \Z:$

For quantified arithmetical choice theories $\bfQ+\ACC$ like $\ZFC$ and already $\PA+\ACC,$

$\bfQ^+ = \bfQ+\Con_{\bfQ}$ [$\mathbf{derives}$]{}:

*TURING machine ${{\mrTM}}_{\nabla_{\bfQ}}$ corresponding—CHURCH—to totally defined $\mu$-recursive decision map $$\nabla_{\bfQ}: \mr{DIO} \to \set{0,1},$$ *when written* *coefficient list* $\ccode{D}$ of a diophantine polynomial $D$ on its (initial) TAPE, eventually **reaches** *HALT state,* leaves result $0$ (as its *final* TAPE) $\mathbf{iff}$ $D$ *has* a zero\
$\vec{z}:$ $D(\vec{z}) = 0,$ and **result** $1$ $\mathbf{iff}$ $D$ is overall *non-null*:\
$(\forall\,\vec{x} \in \Z^*)\,[\,D(\vec{x}) \neq 0\,].$*

This contradicts **Matiyasevich’s** THEOREM *unsolving* Hilbert’s 10th problem, within theory $\bfQ^+$ which strengthens his framework of Peano Arithmetic $\PA+\ACC$ with countable axiom of choice. Whence

### Conclusion: {#conclusion .unnumbered}

-   $\ZFC^+ = \ZFC+\ConZFC$ is contradictory, so

-   $\ZFC\derives\neg\,\ConZFC:$ $\ZFC$ *is internally inconsistent,*

-   same for theory $\PA+\ACC:$

    *Peano-Arithmetic with axiom of countable choice is internally inconsistent*

-   **Question:** is already Peano Arithmetic $\PA$ by itself internally inconsistent? It would be if axiom $\ACC$ of countable choice were derivable within $\PA$ or independent from $\PA,$ as is axiom of choice $\AC$ from **set** theory. This would mean that formal existential quantification is incompatible with free-variables Primitive Recursive Arithmetic $\PR.$

### Discussion {#discussion .unnumbered}

-   After his talk at Humboldt University Berlin, I have mailed to Matiyasevich the question, if his *unsolving* of Hilbert’s 10th problem is really constructive: it depends heavily on formal existential quantification. No reply: may be he considers this question when present paper will be brought to his attention.

-   I have submitted the 200? version of present work, claiming self-inconsistency $\PA\derives \neg\,\Con_{\PA},$ to the *Journal of Symbolic Logic.* The (anonymous) referee:

    *... this is certainly false. ...* Robert ’Rob’ ed.: *under these circumstances etc.*

**What is such editorial policy good for?**

Hilbert 10 constructively
=========================

In this section we show that the *local* version $\nabla[D]: 1 \parto 2$ of the $\mu$-recursive *decision algorithm* $\nabla = \nabla_{\DIO}(d): \mathit{DIO} \parto \two$ *irrefutably* *decides* *each (single)* diophantine equation—*correctly*—when placed in p.r. *non-infinite-descent theory* $\piR=\PR+(\pi)$ of op.cit.  in the References.

This will give a positive solution to Hilbert’s 10th problem in that constructive framework, at least when stated in its original form quoted in first section above.

Formally, this **problem** allows for solution by a separate decision algorithm (“process”) for each diophantine polynomial. By *localisation* at a given polynomial, we extract such a decision-*family* from the forgoing sections, and formalise it within $\piR.$

We index that family (externally) by the *diophantine constants* $\delta:\one \to \mr{DIO} \subset \N,$ among which the diophantine polynomials $$D = D(\vec{x}) = D(x_1, \ldots, x_{\bs{m}}): \Z^{\bs{m}} \to \Z$$ are represented by their coefficient list codes $\ccode{D}: \one \to \mr{DIO}.$

**Definition:** For PR predicates $\ph_0, \ph_1: A \times \N \to \two$ we define the *race winner predicate* $$\mu_{\lor}[\ph_0,\ph_1]: A \to \two$$ between $\ph_0$ and $\ph_1$ slightly assymmetrically by $$\begin{aligned}
&& \mu_{\lor} [\ph_0,\ph_1] = \mu_{\lor} [\ph_0,\ph_1](a)\\
&& \defeq
(\mathit{dc} \circ (\ph_0,\ph_1)) 
  \parcirc (A \times \mu[\ph_0 \,\lor\, \ph_1]) \parcirc \Delta_A: \\
&& A \to A \times A \parto A \times \N \to \two \times \two 
       \overset{\mathit{dc}} {\longrightarrow} \two, \ \text{with} \\
&& \mathit{dc} = \mathit{dc}(u,v): \two \times \two \parto \two 
   \ \text{defined by} \\
&& \mathit{dc}(u,v) \defeq
\begin{cases}
0 \ \text{if}\ u = 1, \\
1 \ \text{if}\ u = 0\ \land\ v = 1, \\
\text{\emph{definably undefined} if}\ u = v = 0.
\end{cases}\end{aligned}$$ This (partial) race winner predicate $\mu_{\lor}[\ph_0,\ph_1](a): A \parto \two$ is characterised—within $\bs{S}=\PR$ as well as in $\bs{S}=\piR$—by $$\begin{aligned}
  \bs{S} \derives\, 
           & [\,\ph_0 (a,n) 
                \,\land\, \underset{i<n} {\land}\,\neg\,\ph_1(a,n)
                 \implies \mu_{\lor}[\,\ph_0,\ph_1\,](a)=0\,] \\
           & \land\, [\,\ph_1(a,n)
             \,\land\,\underset{i \leq n}{\land}\,\neg\,\ph_0(a,n) 
                \implies \mu_{\lor}[\,\ph_0,\ph_1\,](a)=1\,]. \end{aligned}$$ We allow us to write for this intuitively—in classical terms of a (partial) case-distinction: $$\mu_{\lor}[\,\ph_0,\ph_1\,](a) = 
  \begin{cases}
    0 \ \text{if}\  \mu\ph_0(a) < \infty
                       \,\land\,\mu\ph_0(a) \leq \mu\ph_1(a), \\ 
    1 \ \text{if}\  \mu\ph_1(a) < \infty 
                             \,\land\,\mu\ph_1(a) < \mu\ph_0(a).
  \end{cases}$$ Our decision family $$\nabla[\delta]: 1 \parto \two,\ \delta: \one \to \mr{DIO} \subset \N$$ now is defined in the present $\mu$-recursive frame as this type of race winning, of PR search for a zero (in the evaluation) of $\delta$ against PR search for a (first) internal non-nullity *proof* for (the evaluation) of $\delta,$ namely by $$\begin{aligned}
\nabla[\delta] 
& \defeq \mu_{\lor} [\ph_0[\delta],\ph_1[\delta]]: 1 \parto \two, 
  \ \text{with} \\
\ph_0[\delta](k) 
& \defeq [\,\ev(\delta,\ct_*(k)) = 0\,]: \N \to \two, \\ 
\ph_1[\delta](k) 
& \defeq \Pro_{\bs{S}}(k,\code{(\vec{x})\ev(\delta,\vec{x}) \neq 0}.\end{aligned}$$ Here $$\ev = \ev(d,x): \N \times \N \supset \mr{DIO} \times \Z^* \to \Z$$ is evaluation with the characteristic **evaluation property** $$\begin{aligned}
& \ev(\ccode{D},(x_1,\ldots,x_{\bs{m}}))
  = D(x_1, \ldots, x_{\bs{m}}): Z^{\bs{m}} \to \Z,\end{aligned}$$ realised by (iterated) ’s schema (each application reduces the number of remaining variables by 1), or by “brute force” evaluation of monomials.

Decision Correctness
--------------------

**Soundness Recall:** Main result of op.cit.  in the References is (logical) *soundness* of theory $\piR:$

-   For a (p.r.) predicate $\chi = \chi(a): A \to \two$ we have $$\piR\,\derives\ \Pro_{\piR}(k,\code{\chi})  
      \implies \chi(a): \N \times A \to \two,$$ $a \in A$ free, meaning here *for all* $a\in A,$ and $k \in \N$ free, meaning here *exists* $k\in\N.$ This entails

-   *$\PR$ soundness* of $\piR:$ For a p.r. predicate $\chi = \chi(a): A \to \two,$ $$\piR\,\derives\ \Pro_{\PR}(k,\code{\chi})  
      \implies \chi(a): \N \times A \to \two,$$ as well as in particular

-   *Diophantine soundness* of $\piR:$ for a diophantine polynomial $D=D(\vec{x}):\Z^*\to \two$ $$\piR\,\derives\ \Pro_{\piR}(k,\code{(\vec{x})D(\vec{x})\neq 0})  
      \implies D(\vec{x})\neq 0,$$ $k\in \N,\ \vec{x}\in \Z^*$ free.

-   Already $\PR^+ = \PR+\Con_{\PR}$ is diophantine sound. This needs an extra Proof.

    We consider here frame $\bs{S}=\piR,$ $$\piR^+ = \piR+\Con_{\piR} = \piR,$$ the latter by op.cit. equivalent to soundness of theory $\piR.$

Namely from PR Soundness we get the

**Local Correctness-Lemma** for $\nabla[\delta]$ in $\piR:$ The partial $\PR$-map $\nabla[\delta]:\one \parto \two$ has the following correctness properties:

$\piR \derives\ :$

-   $\delta$ does not fall in *both* of the two defined-cases stated for $\nabla[\delta],$

-   $\nabla[\delta] = 0 
     \implies \ev(\delta,\ct_{*}\circ \mu\ph_0 [\delta])=0:$ $\delta$ is implied to have available a zero in its *evaluation,*

-   $\nabla[\delta] = 1  \implies \ev(\delta,\vec{x}) \neq_Z 0,$ $\vec{x}$ free in $\Z^*$: $\delta$ is implied to be evaluated globally non-null, in particular:

-   By diophantine evaluation for $D = D(x_1, \dots x_{\bs{m}}): \Z^* \to \Z$ diophantine:

    -   $\nabla[D] := \nabla[\ccode{D}] = 0 
         \implies D(\ct_*(\mu\ph_0 [\ccode{D}]))=0:$

        $D$ is implied to have a zero, as well as

    -   $\nabla[D]=1 \implies [\,D(\vec{x}) \neq 0\,],$ here again $\vec{x}$ free over $\Z^*:$

        $D$ is implied to be globally non-null ****

Decision Termination
--------------------

The final question to treat for this—canonical—family $$\nabla = \nabla_{\mbf{DIO}}[\delta]:\one \parto \two, 
  \ \delta: \one \to \mr{DIO} \subset \N$$ of *local*—$\mu$-recursive—decision algorithms, is *termination,* for each $\delta,$ in particular for $\delta = \ccode{D},$ $D = D(\vec{x})$ diophantine.

**Assume** $\nabla[d_0]$ *not* to terminate for a particular *constant* $d_0: \one \to \mr{DIO},$ in particular $d_0$ of form $D_0 = D_0(\vec{x}).$

Since we argue here purely *syntactically*—within the *theory* $\widehat{\bs{S}} \bs{\supset} \bs{S} \bs{=} \PR+(\mr{abstr})$ of *partial* p.r. maps—no modelling in mind except some primitive recursive *Meta*mathematics (these in turn gödelised within $\bs{S}$)—we discuss the stronger assumption

$\nabla[d_0]$ $\T$-*derivably* does *not* terminate for a given diophantine constant $d_0: \one \to \mathit{DIO},$ $\T$ an extension of $\bs{S}.$

This **assumption** reads: $$\T \derives\,(k)\psi[d_0](k):$$ here $k$ is free over $\N,$ and the PR predicate $\psi[d_0](k): \N \to \two$ is defined by $$\begin{aligned}
& \psi[d_0](k) = \psi_0[d_0](k) \land \psi_1[d_0](k)\ \text{with} \\
& \psi_0[d_0](k) = [\,\ev(d_0,\ct_*(k)) \neq 0 \,], \text{and} \\
& \psi_1[d_0](k) = \neg\,\Pro_{\T}(k,\code{\ev(d_0,\vec{x})\neq 0}).\end{aligned}$$ So the assumption (“of the contrary”) reads: $$\begin{aligned}
\T \derives\, 
& [\,\ev(d_0,\ct_{*}(k) ) \neq 0 \,] \\
& \land \neg\,\Pro_{\T}(k,\code{(\vec{x})\ev(d_0,\vec{x}) \neq 0}).\end{aligned}$$ Here $k\in\N$ is the only free variable in the *accessible* level, $\vec{x}$ is free over $\Z^*,$ but *encapsulated* within gödelisation, *not visible* on the object language level.

The derivably-non-termination assumption $$\T \derives\, \psi[d_0](k),\ k\ \free,$$ would entail in particular (first conjunct $\psi_0[d_0]$): $$\T \derives\, \ev(d_0,\ct_*(k)) \neq 0:\N\to\two.$$

*Internalising* (*formalising*) this metamathematical statement, we (would) get by Proof-Internalisation— 1977—a *constant* $p_0: \one \to \mathit{Proof}_\T \subset \N$ *guilty* for this last statement: $$\T \derives\ \Pro_\T(p_0,\code{\ev(d_0,\vec{x}) \neq 0});$$ this would give, by definition of $\nabla[d_0]:$ $$\T \derives \nabla[d_0] = 1,$$ a contradiction to our assumption that $d_0$ be derivably *not decided* by $\nabla_{\DIO},$ to $\T \derives \psi[d_0].$

**Conclusion:**

-   $\piR=\piR+\Con_{\piR}$ derives the alleged decision algorithm (family) $\nabla = \nabla_{\DIO}[D]:\one \parto \two$ to be *correct* for each diophantine polynomial (if defined).

-   no diophantine polynomial $D=D(\vec{x})$ can come with a $\T$-proof (i.p. a $\piR$-proof) showing $\nabla[D]$ to be *undefined,* *not* to terminate, in other words:

-   *correct termination* of the $\mu$-recursive *decision family* $\nabla = \nabla_{\DIO}[D]$ at each diophantine polynomial is $\piR$-*irrefutable,* in the sense that **otherwise**—refutation— $$\begin{aligned}
    & \piR \derives \Pro_{\piR}(q,\code{\mr{false}}),  
      \ q: \one \to \N\ \text{a suitable PR point,}                                                                                    \end{aligned}$$ inconsistency of (self-consistent) theory $\piR$ would be the consequence.

Outlook {#outlook .unnumbered}
-------

Irrefutable correct termination of *uniform* decision algorithm $$\nabla_{\DIO}=\nabla_{\DIO}(d):\mr{DIO}\parto\two,\ d\in\mr{DIO}\ \free$$ is treated within the general framework of

*Arithmetical Decision* to come.

[99]{}

ed. 1977: *Handbook of Mathematical Logic.* North Holland.

1931: Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. *Monatsh. der Mathematik und Physik* **38,** 173-198.

1970: Mathematische Probleme. Vortrag Paris 1900. *Gesammelte Abhandlungen.* Springer.

1993: *Hilbert’s Tenth Problem*. The MIT Press.

2014a: *Consistency Decision,*

arXiv 2014.

2014b: *Arithmetical Foundations,* $\gamma$ version, www3.tu-berlin.de/preprint/mathematik/Preprint-8-2014

1977: The Incompleteness Theorems. Part D.1 in ed. 1977.

[^1]: michael.pfender@alumni.tu-berlin.de
