Let's denote a sentence $P$ as "weak Godel sentence of theory $T$", if and only if $$[\neg (T \vdash P) \wedge \neg (T\vdash \neg P)] \wedge [Con(T)=Con(T+P) \wedge Con(T)=Con(T+ \neg P)] $$

In English this is: $P$ is independent of $T$ and the addtion of $P$ or $\neg P$ to $T$ doesn't prove the consistency of $T$.

Let's denote a sentence as complex if it has a proper subformula of it that is a sentence, or when de-prenexed it results in a sentence that has a proper subformula of it that is a sentence. A sentence is simple if and only if it is not complex.

Let's fix the language of $T$ to a classical first order logic language that doesn't contain any constants in its signature. By sentence it is meant the usual meaning of a fully quantified formula (i.e. has no free variables).

Definition: $$T \text{ is complete for simple sentences below } Con(T) \iff \forall P (P \text { is a weak Godel sentence of }T \to P \text { is complex})$$

In other words: all sentences if the addition of them or their negation to $T$ doesn't result in a theory that can prove the consistency of $T$, that are simple, then those sentences are decidable by $T$.

Question: is it possible to have a theory that meets Godel's incompleteness criteria and yet is complete for simple sentences below its consistency level?

  • $\begingroup$ What does de-prenexed mean? Is there a good inverse to taking the prenex normal form? $\endgroup$ – Matt F. Dec 3 '18 at 13:24
  • $\begingroup$ Can you give examples complex and simple sentences and explain their motivation? I assume you're trying to avoid sentences that 'hide' consistency statements inside themselves. $\endgroup$ – James Hanson Dec 3 '18 at 17:04
  • $\begingroup$ @MattF. $\varphi$ is a de-prenex form of $\psi$ if and only if $\psi$ is the prenex normal form of $\varphi$, this is obtained from $\psi$ by simply inversing the steps that derived $\psi$ form $\varphi$. Now if there be no formula $\varphi$ that is not a prenex normal form such that $\psi$ is the prenex normal form of it, then the de-prenex form of $\psi$ is $\psi$ itself. $\endgroup$ – Zuhair Al-Johar Dec 3 '18 at 17:52
  • $\begingroup$ I'm trying to avoid sentences that hide any sentences inside them, and the sentences having consistency statements inside them are just examples of complex sentences. example $(Con(T) \to n=1 \lor n=2) \wedge (\neg Con(T) \to n=1)$ $\endgroup$ – Zuhair Al-Johar Dec 3 '18 at 17:58
  • $\begingroup$ the main motivation is that the complex Godel sentence would be composed ultimately of simple sentences that are independent of the theory but of higher consistency strength, and in this manner completeness for simple sentences below the consistency strength of the theory won't effect completeness for complex ones, so we may be able to prove completeness for simple sentences below the consistency level of the theory in concern. $\endgroup$ – Zuhair Al-Johar Dec 3 '18 at 20:19

Unless I'm missing something, every sentence is equivalent to a simple sentence. To see this, take a sentence $\varphi$ and produce an equivalent sentence $\psi$ by the following procedure: Let $x$ be a variable not occuring in $\varphi$. Replace each atomic sub-formula $\chi$ of $\varphi$ by $\chi \wedge x = x$ if $\chi$ is in the scope of an even number of negations and $\chi \vee x \neq x$ if $\chi$ is in the scope of an odd number of negations (we're treating $\alpha \rightarrow \beta$ as $\neg\alpha \vee \beta$). Finally add $\exists x$ to the beginning of the sentence. To see that they're equivalent, note that if $\psi$ holds, then we can pick a witness $c$ for the $\exists x$ quantifier and substitute it in for each instance of $x$, giving a sentence that is clearly equivalent to $\varphi$. Conversely if $\varphi$ holds, then if we let $x$ be any $c$ whatsoever, substituting in $c$ for $x$ in $\psi$ with the first quantifier removed again gives a sentence clearly equivalent to $\varphi$. Finally, every proper subformula of $\psi$ fails to be a sentence, so it is simple.

Edit: Assuming that the language in question contains addition and the theory proves basic facts about arithmetic, there's a more robust way of converting any sentence $\varphi$ into a simple sentence, namely let $x$ and $y$ be variables not appearing in $\varphi$ and let $\varphi^\prime$ be $\varphi$ with each term $t$ replaced with $t+x$. Then an equivalent simple sentence is $\exists x ((\forall y (y = y + x)) \wedge \varphi^\prime)$.

  • $\begingroup$ What about the de-prenexing? Won't that turn your sentence into a complex sentence? $\endgroup$ – Bjørn Kjos-Hanssen Dec 5 '18 at 3:12
  • $\begingroup$ The sentence I describe isn't in prenex form if the original sentence is not in prenex form. Furthermore every sentence is equivalent to one that is not in prenex form. $\endgroup$ – James Hanson Dec 5 '18 at 3:35
  • 1
    $\begingroup$ @BjørnKjos-Hanssen, the phrase “when de-prenexed” which appears in the question is still not well defined. If you have a clear view of what the question ought to say on this, perhaps you can edit the question appropriately. $\endgroup$ – Matt F. Dec 5 '18 at 7:38
  • $\begingroup$ Deprexing means moving in the opposite direction of getting a prenex normal form, so you still can de-prenex a sentence that is not in a prenex normal form! for example the sentence $\forall a (\varphi(a) \wedge \rho)$ this is not in prenex normal form if $\rho$ is a sentence, yet still you can de-prenex it to $\forall a (\varphi(a)) \wedge \rho$. Your sentences can be easily de-prenexed as to get a complex sentence, SO THEY ARE NOT SIMPLE. $\endgroup$ – Zuhair Al-Johar Dec 5 '18 at 11:47
  • 2
    $\begingroup$ @ZuhairAl-Johar That was not completely clear to me from the question and your comments. I've edited my answer with a different construction. $\endgroup$ – James Hanson Dec 5 '18 at 13:19

Partial answer:

If there is such a theory $T$, it would mean that every simple sentence that's independent of $T$, must decide Con($T$).

Note that every $\Pi^0_1$ sentence is equivalent to a simple sentence by Matiyasevich's theorem (every $\Sigma^0_1$ set is diophantine). And I guess we assume $T$ proves Matiyasevich's theorem.

So in particular,

every true $\Pi^0_1$ sentence that's independent of $T$ must decide Con($T$).

(The false $\Pi^0_1$ sentences are refutable in $T$; I think this, with the fact that $T$ is $\Delta^0_1$-axiomatizable, is part of your assumption "meets Gödel's incompleteness criteria".)

I don't know enough about which $\Pi^0_1$ sentences decide Con($T$), but it seems like a tall order that such a theory should exist.

  • $\begingroup$ A silly comment: if the $T$-independent $\Pi^0_1$ sentences decide $Con(T)$, then - since they are true ($T$ disproving all false $\Pi^0_1$ sentences) and $T$ actually is consistent - all $T$-independent $\Pi^0_1$ sentences prove $Con(T)$. Conversely, all the false $\Pi^0_1$ sentences $T$-prove $\neg Con(T)$, and no $\Pi^0_1$ sentence provable from $T$ $T$-proves $Con(T)$. (cont'd) $\endgroup$ – Noah Schweber Dec 5 '18 at 15:39
  • $\begingroup$ So we can enumerate (hence compute) the set of $\Pi^0_1$ sentences not provable (but possibly disprovable) from $T$: they're the ones which $T$ proves imply $Con(T)$. I suspect that we can show that $\{\varphi\in\Pi^0_1:T\not\vdash\varphi\}$ is $\Pi^0_1$-complete, though, and so have a contradiction - does this all seem plausible? $\endgroup$ – Noah Schweber Dec 5 '18 at 15:39
  • $\begingroup$ If $\varphi$ is a false $\Pi^0_1$ sentence then $T\cup\{\varphi\}$ is inconsistent, hence proves $\neg Con(T)$. $\endgroup$ – Noah Schweber Dec 5 '18 at 18:03
  • $\begingroup$ @NoahSchweber OK that sounds right, feel free to write up an answer if you make it work $\endgroup$ – Bjørn Kjos-Hanssen Dec 5 '18 at 18:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.