-3
$\begingroup$

[The question has been edited]

Can we have an effectively generated consistent theory $T$, that extends $\sf PA$, such that:

$T + \\ \forall \mathcal S \, [\exists x: \operatorname {Proof}_T(x, \ulcorner \mathcal S \urcorner) \oplus \exists y: \operatorname {Proof}_T(y, \operatorname {neg}(\ulcorner \mathcal S \urcorner))]$

is consistent?

Where "$\operatorname {neg}$" is Rosser's negation function. and "$\oplus$" is exclusive disjunction.

In other words, can $T$ be consistently extended by its own completeness and consistency?

Improve this question
$\endgroup$
14
  • 5
    $\begingroup$ No. Gödel-Rosser theorems are about internal incompleteness/consistency. $\endgroup$
    – godelian
    Commented Jul 27, 2023 at 11:45
  • 2
    $\begingroup$ $\text{Con}_T$ is an assertion in the object theory, that is, the internal notion. This is always what is meant when discussing whether a theory proves its own consistency. There is in general no way to formulate the metatheoretic notion in the object theory, and so it makes no sense to ask whether the theory proves its own metatheoretic consistency. $\endgroup$
    – Joel David Hamkins
    Commented Jul 27, 2023 at 13:04
  • 1
    $\begingroup$ The answer is still the same. The formalized version of the usual proof of the Gödel–Rosser theorem shows that if you take for $S$ the Rosser sentence of $T$, then the formal $T$-provability of either $S$ or $\neg S$ implies the formal $T$-provability of the other one (i.e., formal inconsistency). $\endgroup$
    – Emil Jeřábek
    Commented Jul 27, 2023 at 19:33
  • 1
    $\begingroup$ @ZuhairAl-Johar Just follow the usual argument. If there exists a proof of $\rho$ or its negation, let $x$ be the least proof of either of them. If $x$ is a proof of $\neg\rho$, then (by the definition) $\rho$ holds, and being a $\Sigma_1$-sentence, it is provable. If $x$ is a proof of $\rho$, then the dual $\Sigma_1$-sentence $\rho^\bot={}$“there is a proof of $\rho$ smaller than any proof of $\neg\rho$” holds, hence it is provable, and since $\rho^\bot$ implies $\neg\rho$, $\neg\rho$ is provable. Either way, both $\rho$ and $\neg\rho$ are provable. $\endgroup$
    – Emil Jeřábek
    Commented Jul 28, 2023 at 4:50
  • 2
    $\begingroup$ $\def\pf#1#2{\operatorname{Proof}_T(#1,\ulcorner#2\urcorner)}$I intended $\rho$ to be equivalent to $\exists x\,(\pf x{\neg\rho}\land\forall y\le x\,\neg\pf y\rho)$, in which case $\neg\rho$ is not $\exists x\,(\pf x{\rho}\land\forall y\le x\,\neg\pf y{\neg\rho})$ (this is what I denote $\rho^\bot$), but $\forall x\,(\pf x{\neg\rho}\to\exists y<x\,\pf y\rho)$. But this does not matter; if you use the dual definition as in your comment, then $\neg\rho\to\exists x\,\pf x\rho$ is an instance of the tautology $\exists x\,(A(x)\land B(x))\to\exists x\,A(x)$, hence its formal provability is obvious. $\endgroup$
    – Emil Jeřábek
    Commented Jul 28, 2023 at 13:14

1 Answer 1

Reset to default
3
$\begingroup$

The answer to the edited question is No, there is no such theory $T$, because the incompleteness theorem is provable in PA and hence also in $T$. The theory $T$ will prove that there is no effective complete consistent theory of arithmetic, and in particular, $T$ will prove that $T$ itself (as defined by its effective algorithm) cannot have the property of your exclusive disjunction clause.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .