2
$\begingroup$

Let $\mathfrak{T} = (\mathsf{L}, \mathsf{S},\mathsf{P})$ be a formal system for natural numbers, where $\mathsf{L}$ is a first order language for syntax capable of expressing basic arithmetic, $\mathsf{S}$ is the corresponding structure (model) for semantics whose universe is natural numbers $\mathbb{N}$, and $\mathsf{P} = (\mathsf{Ax}, \mathsf{D})$ is our proof system. $\mathsf{Ax}$ is the set of axioms containing first order logic axioms and Peano axioms and $\mathsf{D}$ is the set of our deduction rules containing Modus Ponens.

Definition. We say that $\mathfrak{T}$ is arithmetically sound if for every WFF $\varphi$, $\vdash \varphi$ implies $\mathsf{S} \vDash_s \varphi$ holds for every assignment $s$.

Definition. We say that $\mathfrak{T}$ is arithmetically complete if for every WFF $\varphi$, $\mathsf{S} \vDash_s \varphi$ holds for every assignment $s$ implies $\vdash \varphi$.

Remark. The above definitions of soundness and completeness are different from those used in the well-known soundness and completeness theorems of predicate logic. In those theorems, the underlying structure is arbitrary, while the underlying structure $\mathsf{S}$ in the above definitions must satisfy some minimal requirements.

Definition. We say that $\mathfrak{T}$ is verifiable, if there is an algorithm that takes a string of symbols in the language $\mathsf{L}$ and returns, according to $\mathsf{P}$, that whether this string is a valid proof or not.

I was given the following form of Godel's first incompleteness theorem.

Theorem. For every formal system $\mathfrak{T}$ for natural numbers that is arithmetically sound and verifiable, there is an undecidable WFF $\varphi$ about natural numbers, i.e. $\nvdash \varphi$ and $\nvdash (\neg \varphi)$.

Questions

  1. Assuming arithmetic soundness and verifiability of $\mathfrak{T}$, is existence of an undecidable $\varphi$ equivalent to arithmetic incompleteness of $\mathfrak{T}$?
  2. Can $\varphi$ be any WFF or it should be a sentence in the above theorem?
$\endgroup$
5
  • $\begingroup$ The completeness of Godel Incompleteness Theorem is not the same completeness of Godel Completeness Theorem. See many many related posts on this site. $\endgroup$ Commented Jul 27, 2024 at 10:17
  • $\begingroup$ @MauroALLEGRANZA: Can you give me a clue? As far as I understand, we have fixed a structure $\mathcal{N}$ for natural numbers in the Godel's incompleteness theorem. So, $\vDash \varphi$ means that $\varphi$ is true for any assignment $s$ in our structure $\mathcal{N}$. $\endgroup$ Commented Jul 27, 2024 at 10:28
  • $\begingroup$ @MauroALLEGRANZA: I tried to make my question more precise. Could you take a look again? I understand that the term complete may having different meanings in logic, so I made myself clear of what I mean here. I don't think my pitfall is misinterpreting this term. $\endgroup$ Commented Jul 27, 2024 at 13:14
  • 1
    $\begingroup$ Ok to 1. You say that a formal system (including non-logical axioms) is complete wrt to a structure if it proves every formula that holds in that structure. Well, GIT proves the existence of an undecidable sentence $\varphi$, that means that both it and its negation are unprovable. But one of them is true in every structure satisfying the axioms. $\endgroup$ Commented Jul 28, 2024 at 6:13
  • $\begingroup$ Re 3. It is a nitpicking issue, not very relevant to understand GIT. Neither x=0 nor its negation are derivable per se, unless you consider it implicitly universally quantified. $\endgroup$ Commented Jul 28, 2024 at 6:17

2 Answers 2

Reset to default
1
$\begingroup$

Assume $\mathfrak{T}$ is sound and verfiable.

I could show that arithmetic incompleteness of $\mathfrak{T}$ implies the existence of an undecidable WFF. Actually, if $\mathfrak{T}$ is arithmetically incomplete, then there is a WFF $\varphi$ such that $\mathsf{S} \vDash_{s_{\circ}} \varphi$ for some assignment $s_{\circ}$ and $\nvdash \varphi$. By way of contradiction, if we have $\vdash (\neg \varphi)$, then arithmetic soundness implies that $\mathsf{S} \vDash_s (\neg \varphi)$ holds for every $s$, which contradicts our assumption that $\mathsf{S} \vDash_{s_{\circ}} \varphi$. Consequently, we have a WFF such that $\nvdash \varphi$ and $\nvdash (\neg \varphi)$.

The other direction also holds if we assume that $\varphi$ is a sentence, so it has no free variables. Suppose there is an undecidable sentence $\varphi$, so $\nvdash \varphi$ and $\nvdash (\neg \varphi)$. We would like to show that $\mathfrak{T}$ is arithmetically incomplete. By the way of contradiction, assume that this is not the case, so arithmetic completeness of $\mathfrak{T}$ implies that $\mathsf{S} \nvDash_{s_1} \varphi$ and $\mathsf{S} \nvDash_{s_2} (\neg \varphi)$ for some assignments $s_1$ and $s_2$. Since $\varphi$ is a sentence, its truth value only depends on $\mathsf{S}$ and does not depend on any assignment. Consequently, we conclude that $\mathsf{S} \nvDash \varphi$ and $\mathsf{S} \nvDash (\neg \varphi)$, which contradicts with the truth table of negation.

However, I could not show that $\mathfrak{T}$ is arithmetically incomplete if and only if there is an undecidable sentence.

$\endgroup$
0
0
$\begingroup$

The completeness of Godel Incompleteness Theorem is not the same completeness of Godel Completeness Theorem.

The Incompleteness Theorem says that, for specific formal theories with suitable conditions, among whuch consistency, there is an undecidable sentence.

The Completeness Theorem for predicate logic says that every logical consequence of a set of formulas (axioms) is provable.

Cooking them together wrt first-order arithmetic: neither the undecidable sentence nor its negation are logical consequences of first-order Peano axioms.

This implies that the undecidable formula (or its negation) is true in $\mathbb N$ but it is not true in every model of (first-order) Peano axioms: there are nonstandard models of arithmetic.

In conclusion, a theory has an undecidable sentence iff it is negation incomplete.

$\endgroup$

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.