I do not have the expertise to address your post, Newberry, but you will find that, like me, there is nobody reading this forum who is actually competent in mathematical philosophy.

@TonesInDeepFreeze or @fishfry might be able to help. I was a math prof years ago but can't assist you here. You might send them a message and see if they are interested. Just a thought.

I am not sure this is addressed in those books. But are you acquainted with peter smith's book and Smullyan's books?

Assuming this is a current post...

Please try to explain your thesis in natural-language terms, in the way that Bertrand Russell did in his Introduction to Mathematical Philosophy, for example. There are many competent mathematical philosophers reading the forum who aren't necessarily proficient in a system of logical symbolism.

You're one step ahead. Wanted to ask the same!

Another book which should be on every logician shelfs is Logic of provability by George Boolos. I started reading it years ago, I believe this should be covered there not sure 100 percent because I never finished reading this book. I read it back in my undergraute years as a student of maths and physics combined.

My question is this. How do we add the reflection schema to a theory such that the proof predicate Prov_U() includes the reflection schema itself. Would the following do the trick?

P8: P_1 & P_2 & … & P_7 & Prov_T(⌜phi⌝) → phi — Newberry

You can only if P8: is defined in your theory. Otherwise, do equivalence or some other logic axioms. Or embed Prov_T() in Prov_U().

It was claimed that there are capable philosophers of mathematics who are unfamiliar with basic logical notation. Maybe there are, but I don't know of any other than philosophers prior to the widespread use of notation in mathematical logic. To responsibly philosophize in modern context about subjects such as incompleteness does require understanding at least the basic technical material. We can outline certain notions with minimal notation, but at a certain point, if we wish not to oversimplify at the cost of being misinformational, we need to use some symbolisms. (For the most excellent discussion for the layman of incompleteness, refer to Franzen's 'Godel's Theorems', which is a beautifully written and truly insightful presentation.)

I am rusty in the subject of incompleteness, so my remarks might require corrections, but here is a sketch of some of the terminology and notions. To truly understand these notions, starting from the beginning, I recommend Kalish, Montague and Mar's 'Logic: Techniques Of Formal Reasoning' as an introduction to symbolic logic, then onto Enderton's 'Set Theory' for needed set theoretical context, then Enderton's 'A Mathematical Introduction To Logic' for mathematical logic including incompleteness):

(Throughout, where certain results are actually due to Godel-Rosser, for simplicity I'll refer merely to Godel. Also, Godel himself did not refer to 'the standard model', as the notion of a formal model was formalized a few years later by Tarski, but it's easier to discuss Godel with the notion, as the notion can reasonably be said to be implicit with Godel.)

PA is a theory in first order logic with identity, with the signature:

0 - constant, intuitively 'zero'
S - 1-place operation, intuitively 'successor'
+ - 2-place operation, intuitively 'addition'
* - 2-place operation, intutively 'multiplication'

The axioms of PA:

For all n and k, and for all formulas F:

0 not= Sn
i.e. 0 is not a successor

if Sn = Sk, then n = k
i.e. the successor function is 1-1

n+0 = n

n+Sk = S(n+k)

n*0 = 0

n*Sk = (n*k)+n

if (F(0) and for all n, F(n) then F(Sn)), then for all n, F(n)
i.e. (thinking of F as expressing a property) if F is true of 0 and whenever F is true of a natural number then it is true of that number's successor, then F is true of all natural numbers.

PA is a formal theory (i.e., a recursively axiomatized theory) in the sense that it is computable whether any given formula is or is not an axiom, and it is computable whether any given sequence of formulas is or is not a proof.

/

Let w = the set of natural numbers.

The standard interpretation of PA is the structure:

<w, zero, successor_on_w, addition_on_w, multiplication_on_w>

/

(Throughout, by 'symbol', 'sequences of symbols', 'sequence of sequences of symbols' I mean of PA.)

A formula is a certain kind of sequence of symbols. A sentence is a certain kind of formula. A proof is a certain kind of sequences of formulas. A theorem is a sentence that is the last entry in a proof. A theory is a set of theorems. So PA is the set of theorems derivable from the axioms of PA.

A theory is consistent if and only there is no sentence in the theory such that both it and its negation are members of the theory, which is to say that there is no sentence such that both it and its negation are theorems of the theory.

A theory is complete if and only if for any sentence, either it or its negation is a theorem.

Note that any inconsistent theory is complete, since an inconsistency proves every sentence.

The incompleteness theorem pertains to many theories, but in this thread we are looking in particular at PA, so the incompleteness theorem for PA is: If PA is consistent then PA is not complete. (To simplify discussion, throughout I will assume that PA is consistent. With the assumption that PA is consistent, the incompleteness theorem is: PA is incomplete.)

Godel showed 1-1 functions having pairwise disjoint ranges:

g from the set of symbols into w
g' from the set of sequences of symbols into w
g'' from the set of sequences of sequences of symbols into w

For any symbol, sequence of symbols, or sequence of sequences of symbols it is computable what its value is per the functions, and for any natural number it is computable what its symbol, sequence of symbols, or sequence of symbols is, if any, per the inverses of the functions.

For any s that is a symbol, sequence of symbols, or sequence of sequences of symbols, we may refer to #(s), which is the value of s per the pertinent function. We call #(s) "the Godel number of s".

/

(Throughout, by 'sentence', 'proof', and 'theorem' I mean of PA.)

Godel then showed how such predicates as 'is a sentence', 'is a proof', and 'provable' can be defined in the language of PA.

Then Godel showed a particular sentence, call it 'G', such that G <-> not-provable(#(G)), that is, #(G) is not the Godel number of a theorem of PA, which is to say that G is not a theorem. Moreover, the negation of G is not a theorem, since it is a theorem if and only if it is not a theorem, which is impossible. So there is a sentence such that neither it nor its negation is a theorem, which is to say that PA is incomplete.

/

But to PA we can add G itself as an axiom. Call this theory PA'. And PA' is consistent, but there is a sentence G' of PA' such that neither G' nor its negation are theorems of PA'. Ad infinitum.

As I understand, it is suggested that we could add have a theory PA$ (still in the language of PA) that is PA with an added axiom schema:

For all formulas F,

provable(#(F)) -> F

/

I deleted my questioning whether that is a properly defined set of axioms. Yes, it looks properly defined and recursive:

We take any formula F, then calculate its Godel number, say n, then we have as an axiom:

provable(n) -> F.

But now I wonder whether U is a well defined, let alone recursively, axiomatized theory if it includes this axiom schema:

For all formulas F,

provable_U(#(F)) -> F

There you've defined the axioms of U in terms of the theorems of U, which, if I'm not mistaken, is circular, not well-defined.

We say, "provable_U(n)" is defined as "n is the Godel number of a formula that is provable in U", which means "there is a sequence of formulas, each of which is an axiom or derivable from the axioms, and n is the Godel number of the last formula in that sequence". But "is an axiom" is defined in a way that presupposes having defined "provable_U", thus circular.

So I don't see how it can be a well-defined, let alone recursive axiomatization, of U, though it is a recursive axiomatization of another theory U'.

There are many competent mathematical philosophers reading the forum who aren't necessarily proficient in a system of logical symbolism — alan1000

If you are speaking of philosophers of mathematics I suspect most if not all are conversant with this sort of symbolism. I doubt many read this forum.

So what's your opinion if we only stay within Newberry's parameter?

I don't know what you mean by 'Newberry's [the poster's] parameter' or 'only staying within' it.

This is his question, which I'm interested if anyone could answer it:

My question is this. How do we add the reflection schema to a theory such that the proof predicate Prov_U() includes the reflection schema itself. Would the following do the trick?

P8: P_1 & P_2 & … & P_7 & Prov_T(⌜phi⌝) → phi — Newberry

Please read his entire OP.

I read the post. Then I went back to the first place that, as far as I can tell, he doesn't make sense. His theory U is not defined; his proposed definition is circular, so such questions that mention it are nugatory unless we first fix that definition.

I read the post. Then I went back to the first place that, as far as I can tell, he doesn't make sense. His theory U is not defined; his proposed definition is circular, so such questions that mention it are nugatory unless we first fix that definition. — TonesInDeepFreeze

Yeah. He's defining U in terms of T.

He's defining U in terms of T. — L'éléphant

First, I see a purported definition of U that mentions U in the definiens, which is circular.

Second, I see T mentioned in the definiens of a definition of P8, but I don't see a prior definition of T.

Third, I don't see T mentioned in his purported definition of U.

Take his post one step at a time. When he purports to define U, he is circular. So we have to stop there and fix that.

Recursive definitions also look circular, but they are not. I am pretty sure this can be done. I was told something to the effect that it was a fixed point of the hierarchy of theories

T' = T + (Ex)Prf_T(x, ⌜F⌝) --> F
T" = T' + (Ex)Prf_T'(x, ⌜F⌝) --> F
. . .

(don't quote me), or something like that. And that is perhaps somehow equivalent tp P8. Not sure what fixed point means in this context or how it can be constructed.
(BTW, I know the resulting system is inconsistent.)

Well, “(Ex)Prf_T(x, ⌜F⌝) --> F” says that if there exists a proof of F then F is the case. This is neither an axiom nor a theorem of PA. This may seem odd. For how is it possible that if a proof of F exists we cannot conclude F. My understanding is that even if a proof “exists” it could be infinitely long. Thus we may not be able to effectively prove F.

Adding “(Ex)Prf_T(x, ⌜G⌝) --> G” (G is Gödel’s sentence) creates the theory T’ which is also incomplete and has its own Gödel’s sentence G’. My question is how to add the entire hierarchy at once. The resulting system will be inconsistent, but there is a purpose to this madness.

Recursive definitions also look circular, but they are not. — Newberry

Correct. But, as far as I can tell, your purported definition is not justified by any instance of a definition by recursion theorem. That is, yours is merely circular and not recursive.

a fixed point of the hierarchy of theories

T' = T + (Ex)Prf_T(x, ⌜F⌝) --> F
T" = T' + (Ex)Prf_T'(x, ⌜F⌝) --> F — Newberry

Then we would have to see a proof that there does exist such a fixed point that has the properties you claim.

even if a proof “exists” it could be infinitely long — Newberry

Though there may be contexts with a notion of infinitely long proofs, I don't know how the notion of infinitely long proofs would enter into this context in which I would take it we are considering the ordinary notion of proof in which proofs are finite.

PS. We could take the union of all those theories. (And maybe not hard to show that it is recursively axiomatized? We might need to use simultaneous recursion?) But I don't know whether that would be what you're looking for.

PPS. I'm not sure, but I think that not just showing that the union is a recursive axiomatization might require simultaneous recursion, I think simultaneous recursion might be required even to define the set that we taken the union of.

Also, what fixed point do you have in mind?

Also, what fixed point do you have in mind? — TonesInDeepFreeze

This caught my attention although I am not following the discussion, not in my bailiwick. I've worked with these things quite a bit in Banach spaces, etc. but not in this context. What's going on?

There is a fixed point lemma in the proof of incompleteness:

G <-> prov(#G)

But I don't know what fixed point is involved in the sequence of theories under consideration.