Thus a single formal system have every order of logic giving every expression of language in this formal system its own Truth() predicate at the next higher order of logic. — PL Olcott

I don't understand this.

You're off to the races into transfinite-order logics. If I understand the question of the title, it is equivalent to asking if Godel's incompleteness (theorem) is entirely resolved at some higher level of logic. My guess is not.

Thus a single formal system have every order of logic giving every expression of language in this formal system its own Truth() predicate at the next higher order of logic. — PL Olcott

And if nothing else, this is the clue, "next higher order...". It appears you want to get to the point where there is no higher order. And that would seem to lead to a set-of-all-sets type of contradiction.

And if nothing else, this is the clue, "next higher order...". It appears you want to get to the point where there is no higher order. And that would seem to lead to a set-of-all-sets type of contradiction. — tim wood

It has always seemed to me that Tarski's Undefinability theorem fails when applied to a knowledge ontology inheritance hierarchy (KOIH). It has only occurred to me recently that KOIH is essentially type theory which is essentially HOL. https://en.wikipedia.org/wiki/Ontology_(information_science)

You shall have to keep it simple with me. From what I've read, all the incompleteness/undefinability theorems only apply to systems of "sufficient" power and interest. I find this online, "The theorem applies more generally to any sufficiently strong formal system, showing that truth in the standard model of the system cannot be defined within the system."

Your question (again, if I understand it), is can there be a super-strong formal system that is not incomplete. I am guessing not. And I'm sure a rigorous discussion would be well, rigorous.

Your question (again, if I understand it), is can there be a super-strong formal system that is not incomplete. I am guessing not. And I'm sure a rigorous discussion would be well, rigorous. — tim wood

It seems that all of the formal systems that these two apply to only have a single order of logic. When we define a formal system that simultaneously has an unlimited number of orders of logic then there is always one more order of logic as needed.

Which is to say - just between us in case we're both wrong - that each system being itself deficient requires a successor system to fix it, but that simply creating a new deficiency. Ordinal arithmetic being formidable, I don't see an escape.

↪PL Olcott Which is to say - just between us in case we're both wrong - that each system being itself deficient requires a successor system to fix it, but that simply creating a new deficiency. Ordinal arithmetic being formidable, I don't see an escape. — tim wood

That a formal system can be defined with a single order of logic seems isomorphic to an encyclopedia defined with only the "C" volume. Of course such a system would be incomplete, yet it is a little silly to define systems or encyclopedias this way.

You're off to the races into transfinite-order logics. If I understand the question of the title, it is equivalent to asking if Godel's incompleteness (theorem) is entirely resolved at some higher level of logic. My guess is not. — tim wood

I cannot give a rigorous answer, but I agree with this. If Tarski's undefinability theorem is basically that "arithmetical truth cannot be defined in arithmetic", or that true Gödel numbers are not definable arithmetically, meaning there’s no first-order formula for this, I think it does go for higher order logics. For those higher order logics there is their own true but unprovable Gödel number.

But I'm the amateur here, so don't quote me.

(PS, why two threads?)

I cannot give a rigorous answer, but I agree with this. If Tarski's undefinability theorem is basically that "arithmetical truth cannot be defined in arithmetic", or that true Gödel numbers are not definable arithmetically, meaning there’s no first-order formula for this, I think it does go for higher order logics. For those higher order logics there is their own true but unprovable Gödel number. — ssu

There is always an unprovable expression in one order of logic that is provable in the next order. When all orders of logic are included in the same formal system then such a system cannot be incomplete. I posted this in two forums because the more appropriate forum has hardly any views.

I imagine Tarski's indefinability theorem would. AFAIK second order logic already has diagonalization results - so it's either inconsistent or incomplete. You don't need to go above first for it. So long as you put enough arithmetic in, you're going to get the self referential bullshit that sets up these paradoxes.

I imagine Tarski's indefinability theorem would. AFAIK second order logic already has diagonalization results - so it's either inconsistent or incomplete. You don't need to go above first for it. So long as you put enough arithmetic in, you're going to get the self referential bullshit that sets up these paradoxes. — fdrake

Anything that can't be proved in one order of logical can be proved or refuted in the next. A formal system having every order of logic cannot be incomplete. A formal system having only one order of logic is like the "C" volume of an encyclopedia only having articles that begin with the letter "C".

When all orders of logic are included in the same formal system then such a system cannot be incomplete. — PL Olcott

Um, no.
I'm going to try to condense a proof due to Emil Post, in The Undecidable, Ed. Davis, 1965, pp. 304-337, esp. pp. 308-317

Let B be understood as a recursively enumerable set of numbers. Let B1, B2,...Bn, B(n+1)... be simply a listing of such sets with duplicates omitted and arranged perhaps by length and lexicographically for sets the same length.

Let (Bn,n) be simply the proposition, true or false, that n is in the set Bn.

By interlacing the Bns and the integers, e.g., B1,1; B2,1; B1,2; B1, 3; B2,2; B3,1, and so on, there are generated all the distinct couples Bn,n.

Call this set E, of all the expressions Bn,n, understood in each case as the expression that n is in the set Bn.

From E generate the set T of all Bn,n such that the number n is in Bn; i.e. true. The complement of T will be ~T, that is, all those Bn,n such that n is not in Bn.

Let F be any recursively enumerable subset of ~T. That is, if Bn,n is in F, it is in ~T, and n is not in the set generated by Bn.

Now it gets a little bit tricky.

Now generate the members of F. If a member of F is of the form Bn,n, place n in a set of positive integers called S. S being recursively enumerable will correspond to some B, call it Bv such that S=Bv. Construct Bv,v; that is, the proposition that v is in Bv.

And now I quote directly. "Now by construction, S consists of those members of F of the form Bn,n. Suppose that Bv,v is in F. Then,... Bv,v being false, v would not be in... Bv. That is, v would not be in S. But Bv,v being of the form Bn,n, v would be in S. Our assumption leading to a contradiction, it follows that Bv,v is not in F. But v can only be in S by Bv,v being in F. Hence, v is not in S. Finally, Bv,v says that v is in S.... Bv,v is therefore false; that is, Bv,v is in ~T.

"...[ S]ince Bv,v of ~T is not in F, T and F together can never exhaust E.... We can then say that no recursively generated logic relative to E is complete, since F alone will lead to the Bv,v not in F." That is. given the logic determined by T and F, Bv,v must be undecidable.

"[They, (the ideas here presented)] implicitly justify the generalization that every symbolic logic is incomplete...." (316)

A formal system having only one order of logic is like the "C" volume of an encyclopedia only having articles that begin with the letter "C". — PL Olcott

And a complete set would have everything from A to Z. But in our case, you can't have a complete set.

A formal system having only one order of logic is like the "C" volume of an encyclopedia only having articles that begin with the letter "C".
— PL Olcott
And a complete set would have everything from A to Z. But in our case, you can't have a complete set. — tim wood

...14 Every epistemological antinomy can likewise be used for a similar undecidability proof...
(Gödel 1931:43-44) Epistemological antinomies (AKA self-contradictory expressions) must be excluded from every formal system of logic because they are not truth bearers. I can't follow your other proof, yet it seems to follow the principle that every simple idea can be made convoluted enough that it can no longer be understood.

Anything that can't be proved in one order of logical can be proved or refuted in the next. A formal system having every order of logic cannot be incomplete. A formal system having only one order of logic is like the "C" volume of an encyclopedia only having articles that begin with the letter "C". — PL Olcott

I don't think this is true.

Every theorem of 0th order logic has a corresponding theorem in 1st order logic. Like P=>Q goes to For all X P ( X ) implies Q ( X )
Every theorem of 1st order logic has a corresponding theorem in 2nd order logic.

I'm fairly certain that generalises, but haven't come up with a proof sketch. i.e. nth order logic lets you express and prove all the things that are in (n-1)th order logic and more.

Now consider that you're taking the set of all provable statements of all logics up to the nth order. That will then be the set of provable statements of the nth order logic, due to the hierarchy.

You've stipulated that n>2, so your logic is strictly more expressive than 2nd order logic.

Incompleteness results apply to 2nd order logic, since you can axiomatise the natural numbers with + and * in it. That's more than enough arithmetic for Tarski and Godel.

So your big union of logics is one logic - of the highest order you designate. And so long as it contains 2nd order logic, you can derive incompleteness results for it.

Moreover, I think you're claiming that you end up axiomatising the (n-1)th's logic's metalanguage in the nth logic's syntax? But when you end up having such a tower of logics and take their the union, it isn't quite that you'd be taking the union of their metalanguages as well, there'd need to be a single unifying metalanguage in which the formulae of all the levels could be expressed. The truth and provability symbols in the metalanguage would thus apply for theorems applying to the big union logic, rather than having a plethora of distinct symbols in different metalanguages - though concepts like 1st order derivable could maybe be phrased in that expansive metalanguage for the union of the logics.

Similarly, there would need to be one type of object which would model all the formulas. I'd conjecture set theory would work for all of them. Reason being you can think of quantification of order n as ranging over a set which allows quantification over collections of sets (n-1) recursions deep. Like 0th order logic allows no quantification. 1st allows quantification over singletons, 2nd allows.... quantification over sets. 3rd allows... quantification over sets of sets, which is kinda just quantification over sets.

So it would surprise me if this giant logic wasn't a version of "set theory in disguise" (like second order logic was called by Quine), to which incompleteness results already apply.

seems to follow the principle that every simple idea can be made convoluted enough that it can no longer be understood. — PL Olcott

That's a convenient principle. Btw, how do you know when an idea is just that simple?

seems to follow the principle that every simple idea can be made convoluted enough that it can no longer be understood.
— PL Olcott
That's a convenient principle. Btw, how do you know when an idea is just that simple? — tim wood

When we envision the inherent structure of the set of all knowledge that can be expressed using language then we can see that "incompleteness" and "undecidability" are mere errors in disguise.

Now consider that you're taking the set of all provable statements of all logics up to the nth order. That will then be the set of provable statements of the nth order logic, due to the hierarchy. — fdrake

For every nth order logic that can be shown to be incomplete there is an n+1 order logic that completes it.

there'd need to be a single unifying metalanguage in which the formulae of all the levels could be expressed. — fdrake

Yes, definitely.

The truth and provability symbols in the metalanguage would thus apply for theorems applying to the big union logic, rather than having a plethora of distinct symbols in different metalanguages — fdrake

One metalanguage that can refer to one of more elements at any level within the type hierarchy.

"[They, (the ideas here presented)] implicitly justify the generalization that every symbolic logic is incomplete...." (316) — tim wood

It would seem that for every n order or logic there would necessarily be an n+1 order of logic provability predicate for this N order of logic.

There are many ways to further extend second-order logic. The most
obvious is third, fourth, and so on order logic. The general principle,
already recognized by Tarski (1933 [1956]), is that in higher order
logic one can formalize the semantics—define truth—of lower order logic.
https://plato.stanford.edu/entries/logic-higher-order/ — Stanford

What is your point? We suppose - that's the best I can do - that a proposition undecidable in L is decidable in L', and one in L' in L'', and so forth. But apparently there is no Lωω...ω that is itself complete.

Higher-order logic is the union of first-, second-, third-, ..., nth-order logic; i.e., higher-order logic admits quantification over sets that are nested arbitrarily deeply. — PL Olcott

Do we need more than first and second order logic in practical uses?

↪PL Olcott What is your point? We suppose - that's the best I can do - that a proposition undecidable in L is decidable in L', and one in L' in L'', and so forth. But apparently there is no Lωω...ω that is itself complete. — tim wood

A knowledge ontology inheritance hierarchy capable of formalizing the entire body of human knowledge that can be expressed using language need not be incomplete in the Gödel sense. Such a system would essentially be a type hierarchy from type theory thus isomorphic to HOL.
https://en.wikipedia.org/wiki/Ontology_(information_science)

Higher-order logic is the union of first-, second-, third-, ..., nth-order logic; i.e., higher-order logic admits quantification over sets that are nested arbitrarily deeply.
— PL Olcott

Do we need more than first and second order logic in practical uses? — Corvus

For formalizing the entire body of human knowledge that can be expressed using language we need this:

By the theory of simple types I mean the doctrine which says that the objects of thought ... are divided into types, namely: individuals, properties of individuals, relations between individuals, properties of such relations, etc.
https://en.wikipedia.org/wiki/History_of_type_theory#G%C3%B6del_1944 — History of Type Theory

There seems to be a finite limit to the number of orders of logic needed.

For formalizing the entire body of human knowledge that can be expressed using language we need this: — PL Olcott

Let's try this. Suppose you have your "this," call it T. Now suppose you have some expression. Is it or its negation in T? If so, great! You're done. If not, then you have to figure out if it should be or not. And using existing knowledge, you cannot (if you could, it or its negation would already be in T).

Best you can do is add it as axiomatic in some way, or fundamental. Now you have T'. Now a new expression, same business, and you get T'', and so on and so forth. You might argue, and imo quite reasonably, that in collections of data this doesn't really arise. But in math-logic it exactly does. That is, there is no terminal Tωω...ω in math-logic.

And this concerns among other things differences between finite and infinite sets. .

Let's try this. Suppose you have your "this," call it T. Now suppose you have some expression. Is it or its negation in T? If so, great! You're done. If not, then you have to figure out if it should be or not. And using existing knowledge, you cannot (if you could, it or its negation would already be in T). — tim wood

There is a great debate about whether an expression of language
can be true without a truth maker.

Truthmaker Maximalism defended GONZALO RODRIGUEZ-PEREYRA
https://philarchive.org/archive/RODTMD

A truth without a truthmaker is like a cake without a baker,
non-existent.

True and unprovable is self-contradictory once one understands
how true really works the way that I and Wittgenstein do.
https://www.liarparadox.org/Wittgenstein.pdf

A knowledge ontology inheritance hierarchy capable of formalizing the entire body of human knowledge that can be expressed using language need not be incomplete in the Gödel sense. — PL Olcott

This at least seems true. Mainly because such a listing lacks the power of systems that are incomplete in the Godel sense, and in fact have nothing to do with it. Your groceries list can stand for such a body of knowledge, and nothing incomplete about it.

True and unprovable — PL Olcott

Properly and correctly qualified as unprovable within the system out of which it arose, but proved true by other means.

Btw, true is an adjective indicative of a quality that true statements have. Good luck with any attempt to comprehensively further define just what that quality exactly is.

Btw, true is an adjective indicative of a quality that true statements have. Good luck with any attempt to comprehensively further define just what that quality exactly is. — tim wood

Analytic TRUE is a constant property of some expressions of language defined in terms of its relation to other expressions of language. An expression of language is TRUE if and only if it is (a) stipulated to be true, or (b) semantically derived from expressions of language that are stipulated to be true.

For formalizing the entire body of human knowledge that can be expressed using language we need this: — PL Olcott

High-Order Logic seems to be more flexible and powerful for the real world cases due to its expanded variables availability for the properties and relations.

There seems to be a finite limit to the number of orders of logic needed. — PL Olcott

I was under impression that higher than 3rd-order logic would be for the multiple set theories and advanced calculus applications, therefore they wouldn't be used for describing the empirical world cases.