Can a formal system of arithmetic prove itself consistent for all *grounded* theorems?

Question

I know no formal system containing arithmetic can prove itself consistent. But is it possible to add some ungrounded axiom in the sense described here https://en.wikipedia.org/wiki/Liar_paradox#Saul_Kripke such that the new system can somehow prove the part of itself which concerns all grounded statements, complete? In other words, can we axiomatise some concept whose only bearing on arithmetic is to facilitate the completion of the part of our new theorem that concerns itself with evaluable facts about the numbers.

By this I mean for example, we might start with Peano axioms and "incompletely" define some "arbitrarily large integer" $a$ axiomatically by the axiom $a\geq n\forall n\in\mathbb{N}$ with some suitable definition of what $\geq$ means, or some other suitable axiom.

Is there such an axiom that would render our theory "Peano+" complete in respect of all meaningful statements about any number we might actually encounter, and allows us to ring-fence in some way the part of the theory that is incomplete or possibly inconsistent, and say for certain that the part of the theory that is possibly incomplete or inconsistent is necessarily only concerned with ungrounded statements, i.e. statements about $a$?

In the example of the axiom above, we might say the theorem is "complete for all statements not mentioning $a$." Which would surely be a desirable outcome since by definition, any $n=a$ would be the greatest integer, and the axioms of Peano guarantee there is no greatest integer, so no integer we will ever meet will ever be $a$. Godel's incompleteness theorem would therefore be rendered irrelevant because our new theory would only be incomplete insofar as it would fail to make statements which are not concerned with evaluable facts about the numbers. Every evaluable fact about the numbers, it would be able to prove.

My gut feel is that such an axiom is possible, but that the grounded statements might exclude certain things we can currently say about transcendental numbers and possibly irrational numbers too.

Answer 1

Leaving aside a number of issues (which also applied to your previous question on illogicality) around foundational matters, there is arguably a sense in which the answer to your question is yes: if we pass to an appropriate theory which can talk about the set of all natural numbers - for example, $ZFC$! - then such a theory can indeed prove that $PA$ is consistent (although of course "appropriate" here is subsuming a lot . . .). Note that Godel proved a general theorem about the value of passing to a higher-type theory - see his speed-up theorem - which, while not directly relevant to what you're talking about, seems like it would be interesting to you.

That said, I think your philosophical musings are getting in the way of asking a well-posed question. I strongly recommend that you read a book on first-order logic; I think that will both clarify many issues (especially around Godel's theorem), and also help you put your questions into a precise form that lets them be answered well. In particular, re: this question, note that the passage to ZFC looks nothing like your "arbitrarily large integer $a$", and I have absolutely no idea what you mean by "incompletely define"; moreover, note that it is impossible for any recursive theory to be complete for even the set of sentences asserting that Diophantine equations have/don't have solutions, by the MRDP theorem.

Answer 2

I know no formal system containing arithmetic can prove itself complete. $ \def\nn{\mathbb{N}} \def\t{\text} \def\th{\t{Th}} \def\con{\t{Con}} \def\prov{\square} \def\pa{\t{PA}} $

Wrong. Any inconsistent formal system that can state completeness of itself proves itself complete. [Edit: In my original post I made a stupid careless mistake and said that $\th(\nn)$ proves its own completeness. That cannot be expressed in any meaningful sense because there is no decidable proof validity for $\th(\nn)$, so it does not. What is true is that $\th(\nn)$ is complete but useless for that very reason.]

... "incompletely" define ...

Meaningless. It is akin to asking "Can we incompletely define a flying pig?". Yes we can: A flying pig is some pig that somehow flies.

Godel's incompleteness theorem would therefore be rendered irrelevant

Wrong. Godel's incompleteness theorem is not rendered irrelevant on ill-defined things.

Every evaluable fact about the numbers, it would be able to prove.

Meaningless. Your post has nowhere defined the term "evaluable" and hence it is meaningless. This applies to most of the other terms used in your post as well.

My gut feel ...

is wrong yet again (and I'm talking about your underlying idea, which is terribly distorted in your post due to your lack of understanding of logic). There is no formal system with decidable proof validity that interprets PA and can prove (the translation of) every sentence in the language of arithmetic that is satisfied by $\nn$. See this post for a precise statement and proof. (In the simplest layman terms, absolutely no practical formal system can prove every fact about even just the natural numbers; it is simply impossible to 'push the incompleteness away' from statements that are purely about arithmetic!)

Furthermore, it is absolutely unjustifiable to reject the meaningfulness of unprovable arithmetic sentences if you accept arithmetic in the first place. For any such formal system $S$, the unprovable sentence constructed in the linked post is a $Π_1$-sentence of the form $\forall x\ ( P(x) )$ where $S$ proves the translation of $P(c(n))$ for every $n \in \mathbb{N}$, where $c(n)$ is the term coding for $n$. Note that each such $P(c(n))$ is a sentence with only bounded quantifiers, and hence can be deterministically checked by brute-force, but the universal sentence cannot be proven!