Algorithm to force decidability of statements using an intuitionistic series of new axioms

106 Views Asked by At

Say that a set $\Phi$ is a finite set of statements in Peano arithmetic is meekly consistent if it contains no "inner,immediate" contradiction, i.e. for any statements $\alpha,\beta$, it does not contain any of $\lbrace \alpha,\neg{\alpha} \rbrace$, $\lbrace\alpha\wedge\beta,\neg{\alpha}\rbrace$, $\lbrace\alpha\wedge\beta,\neg{\beta}\rbrace$, $\lbrace\alpha\vee\beta,\neg{\alpha},\neg{\beta}\rbrace$, $\lbrace\alpha,\alpha\Rightarrow\beta, \neg{\beta}\rbrace$, $\lbrace \alpha,\beta,\neg{\alpha\wedge\beta} \rbrace$, $\lbrace \alpha,\neg{\alpha\vee\beta} \rbrace$, $\lbrace \beta,\neg{\alpha\vee\beta} \rbrace$ or $\lbrace \forall x \alpha(x),\neg{\alpha(c)}\rbrace$ where $c$ is a constant. Thus for example $\lbrace\alpha,\alpha\Rightarrow\beta,\beta\Rightarrow\gamma,\neg{\gamma}\rbrace$ is meekly consistent but not consistent in the usual sense.

Consider pairs $(\Phi,n)$ where $\Phi$ is a meekly consistent finite set of statements in Peano arithmetic and $n$ is an integer. Say that $p'=(\Phi',n')$ is an elementary intuitionistic extension of $p=(\Phi,n)$ iff either $n'=n+1$ and $\Phi'=\Phi$, or $n'=n$ and $\Phi'=\Phi\cup \lbrace \phi \rbrace$ where

-$\Phi\cup\lbrace\phi\rbrace$ stays meekly consistent.

-$\phi$ satsifies the intuitionistic constraint : if $\phi$ is of the form $\exists x \alpha(x)$, then $\alpha(k)\in\Phi$ for some $k\leq n$.

Next, say that $p'$ is an intuitionistic extension of $p$ if there is a chain of elementary intuitionistic extensions starting with $p$ and ending with $p'$. We call $p$ accessible from $A$ (or $A$-accessible for short) when it is an intuitionistic extension of $(A,0)$, where $A$ is a finite set of axioms (or provably true statements) of Peano arithmetic.

For a finite set $\cal F$ of statements in Peano arithmetic, we say that $\cal F$ is decided by $p=(\Phi,n)$ iff $\Phi$ contains $\phi$ or $\neg\phi$ for any $\phi\in{\cal F}$.

If we do not worry about effectiveness, it is obvious that for any $A$, any $\cal F$ is decided by some $A$-accessible $p$ : use "Skolemization" and for any true existential statement $\exists \alpha(x)$ in $\cal F$, simply walk up the integers until you encounter a witness $i$ satisfying $\alpha(i)$. Once you have done that for each one of them, the intuitionistic constraint becomes vacuous for all true statements, so you can finish by inserting all the true statements in $\cal F$, along with the negations of the false statements in $\cal F$.

It is quite another matter to ask if there is a computable algorithm that produces an $A$-accessible $p$ deciding $\cal F$, from any given $\cal F$ and $A$. Intuitively all the obstacles to such an algorithm comes from logical connections between statements in the finite set $\cal F$, and we should be able to enumerate those obstructions in finite time, so such an algorithm should exist. I don't know how to turn that intuition into a proof however.

1

There are 1 best solutions below

6
On

What I find strange in your definition is that you don't ask that for formulae $\phi$ meekly consistent to be "satisfied" by $\Phi$. What I mean is for $\phi=\alpha\vee\beta$ you ask only that $\neg \alpha\notin\Phi$ or $\neg\beta\notin \Phi$ but you don't ask that $\alpha\in\Phi$ or $\beta \in \Phi$.

So I think that you can trivially build an accessible $p$ for any set $F$ of statements in Peano arithmetic. I show this by recurrence on the number of statement in $F$:

$F=\{\phi\}$: two cases either $\phi\in A$ and then $p=(A,0)$ decide $F$, or $\phi\notin A$ then $p=(A\cup\{ \neg \phi\},0)$ is an elementary intuitionistic extension of $(A,0)$ and $p$ decide $F$.

Assume now that one can build an accessible $p=(\Phi,n)$ for any set $F$ of $k$ statements in Peano arithmetic.

Let $F=F'\cup\{\phi\}$ be a set such that $F'$ contains $k+1$ statements in Peano arithmetic. Let $p=(\Phi,n)$ be such that $p$ is accessible and $p$ decide $F'$ (it is computable by hypothesis). Either $\phi\in\Phi$ and then $p$ decide $F$. Or $\phi\notin\Phi$ and thus $p'=(\Phi\cup\{ \neg \phi\},n)$ is an elementary intuitionistic extension of $p=(\Phi,n)$ and thus is accessible and $p'$ decide $F$.

Hence for any (finite) $F$ you can build an accessible $p$ such that $p$ decide $F$.