Yes, it would be good if you could present the Tarski's and Godel's theorems in connection with HOL with your own explanations (the proofs and refutations) in clear English with added formulas too (if needed). — Corvus

This sentence is not true: "This sentence is not true" is true. The inner sentence is in Tarski's theory and the outer sentence is in his meta-theory (the next higher order of logic). Tarski never noticed that "This sentence is not true" is not a truth bearer thus the same ask asking is this sentence true or false: "What time is it?"

Tarski never noticed that "This sentence is not true" is not a truth bearer thus the same ask asking is this sentence true or false — PL Olcott

I am not sure how Prolog works in Boolean value settings and execution operations. I have ordered a couple cheap Prolog books by the way. But in Pascal, C and other HLPLs, they have no problems dealing with the paradox cases in the sentence for the operations due to ability to assign the sentences into either Constants or variables. Then the constants or variables can be initialised with boolean values at the start-up of procedures or functions, which sets the variable or constant values to either True or False.

And then operations for checking the constants or variables with the input data or external condition or states, which generate further TF values, in which case then further process of operations could be written depending on the TF values of the checked out variable or constants.

The paradox problems were only problem or paradox because the TF values were reflected from the semantic values in the word "true" or "false" in the sentence rather than the TF values on the whole sentence.

In PASCAL or C, "What time is it?" can be set as True or False in a variable, and can be used to check the condition of the input data for comparing and generating another TF value from the checking operation. I presumed that was what HOL was all about. Being able to assign any sentence or type of data into the vast different type of variables, and manipulate the TF conditions by controlling them. I am not sure how Prolog would do it, yet.

In PASCAL or C, "What time is it?" can be set as True or False in a variable — Corvus

I am not talking about anything like that. I am referring to the (non-existent truth value of the) actual semantic meaning of the English sentence: What time is it?

It is easer for people to see that sentence has no truth value.
On the other hand it should not have taken humanity 2000 years
to continue to fail to understand that self-contradictory sentences
have no truth value.

The Liar Paradox in C++

int main()
{
bool Liar_Paradox = (Liar_Paradox == true);
}

I am not talking about anything like that. I am referring to the (non-existent truth value of the) actual semantic meaning of the English sentence: What time is it? — PL Olcott

I see. But my point was, isn't the main point of using HOL (as also mentioned in the OP title) is being able to set TF values to the non-existent truth value sentences or word such as "What time is it?", and make use of them in the real world applications?

For example, in algorithmic language
Set S = "What time is it?"
Read External Data Q
If Q = S then
S = True
If S = True then Read Time from the System Clock
Write{"Time is 09:00.")
If Q <> S then
S = False
If S = False then
Write("Please type your question again."
End. => Can be translated into any other PL such as C, C++, java, Python or Pascal ..etc

Saying "What time is it?" has no TF value sounds like ignoring the flexibility and applicability of the program languages and also armchair linguistic philosophy of 1950s. :D

I see. But my point was, isn't the main point of using HOL (as also mentioned in the OP title) is being able to set TF values to the non-existent truth value sentences or word such as "What time is it?", and make use of them in the real world applications? — Corvus

No, not at all. Nothing like that. I am only talking about HOL because everyone seems to be totally clueless about knowledge ontologies so I am using HOL as the closest analogy that people are familiar with. We can stipulate that {dogs are animals} as an axiom of our model of the actual world. We cannot stipulate that {dogs are fifteen story office buildings} as an axiom of the model of the actual world.

To create a formal system that never gets stuck in any paradox we have the Prolog/Wittgenstein notion of truth. Provable from Facts makes true. The opposite is provable from Facts makes false. Everything else is not a truth bearer.

I see your point. I was seeing HOL from totally different point of view. In programming languages HOL enables them more flexible and powerful in building rules and operational logics based on the real world applications requirements. Hence, any statements can be assigned into available variables for getting assigned as preset TF values for required operations. In the programming environment, the only source of truths is the external world, not truth tables. New logics get built in the system according to the specs.

I am waiting for a couple of cheap old Prolog books which are on my way. Prolog seems to be the system for Logic programming. It seems to be a PL which has a long history, but seems to be still very much popular even now especially for AI applications.

I am waiting for a couple of cheap old Prolog books which are on my way. Prolog seems to be the system for Logic programming. It seems to be a PL which has a long history, but seems to be still very much popular even now especially for AI applications. — Corvus

I have the classic Clocksin and Mellish. https://www.amazon.com/Programming-Prolog-Using-ISO-Standard/dp/3540006788

I have the classic Clocksin and Mellish. — PL Olcott

The ones I ordered are,
PROLOG ++: The Power of Object-oriented and Logic Programming" by C. Moss.
Prolog Programming for Artificial Intelligence by Bratko.

All my Computer Programming Logic books have a chapter or two on ProLog.

The ones I ordered are,
PROLOG ++: The Power of Object-oriented and Logic Programming" by C. Moss.
Prolog Programming for Artificial Intelligence by Bratko. — Corvus

Untrue unless provable from Facts does seem to be the correct model for the entire body of analytic truth. Analytic truth seems to be essentially nothing more than relations between finite strings.

Untrue unless provable from Facts does seem to be the correct model for the entire body of analytic truth. — PL Olcott

Analytic truth can be true, but wrong. Can "wrong" be "true", and "right" be "false"?

Analytic truth can be true, but wrong. Can "wrong" be "true", and "right" be "false"? — Corvus

Saying that analytic truth can be wrong it like saying that kittens can be 15 story office buildings it cannot possibly ever happen. The closest thing to analytic truth being wrong is when we changed our mind on calling Pluto a Planet. Pluto was a planet until we changed the definition of the term: "Planet".

Saying that analytic truth can be wrong it like saying that kittens can be 15 story office buildings it cannot possibly ever happen. — PL Olcott

Analytic truth can be wrong, when it contradicts the reality. The reality has potential possibility to be otherwise from status quo at any moment of time. Therefore AT has potential possibility of being wrong.

Analytic truth can be wrong, when it contradicts the reality. The reality has potential possibility to be otherwise from status quo at any moment of time. Therefore AT has potential possibility of being wrong. — Corvus

I am stipulating that analytic truth are only those expressions of language that are a correct model of the actual world. It seems a little nutty to define it any other way.

RE: Does Tarski Undefinability apply to HOL ?
SUBTOPIC: Undefinability and Truth
※→.et al,

All "Orders of" logic have a necessity in the concepts and characteristics being defined. That applies to the elemental "quantifiers" in the Tarski Theorem.

As our Friend PL Olcott points out: "mathematics is incomplete." And that presumption profoundly affects the symbolic language (syntax) of logic in the First and Second Orders. Higher-order logic (HOL) is another animal altogether.

Remember, once you begin to apply the various forms of syntax and semantics (algorithms, guidelines, notation rules, or heuristics) to any attempt to solve a question or inquiry, there is no room for a “eureka moment” that is dependent on the human intellect. A “eureka moment” is undefined by any equation and in many cases is incomprehensible.

Most Respectfully,
R

As our Friend PL Olcott points out: "mathematics is incomplete." And that presumption profoundly affects the symbolic language (syntax) of logic in the First and Second Orders. Higher-order logic (HOL) is another animal altogether. — Rocco Rosano

I hypothesize that mathematics is only construed as "incomplete" based on a nonsense meaning of complete. When provable from axioms means true and the opposite is provable from axioms means false then everything else is simply untrue without any {incomplete} in-between.

I am stipulating that analytic truth are only those expressions of language that are a correct model of the actual world. It seems a little nutty to define it any other way. — PL Olcott

Analytic truth can be wrong, if it is wrongly defined, expressed or applied to an incorrect model of the actual world, which is always possible from the human error. Claiming it is absolutely right in all circumstance sounds nutty.

Analytic truth can be wrong — Corvus

That is like saying the integer five may not be any kind of number at all. Everything that is {incorrect} is excluded from the body of {truth}. That people make mistakes has no actual effect what-so-ever on truth itself. If everyone in the universe is certain that X is true and X is not true their incorrect belief does not change this.

That is like saying the integer five may not be any kind of number at all. Everything that is {incorrect} is excluded from the body of {truth}. That people make mistakes has no actual effect what-so-ever on truth itself. If everyone in the universe is certain that X is true and X is not true their incorrect belief does not change this. — PL Olcott

You are not reading what comes after,

Analytic truth can be wrong — Corvus

:)

Analytic truth is a definition fallacy. It is defined as,
1. It is true, even if it is false.
2. Therefore to say it is false, is false even if it is true.

There is always potential possibility of human error in application side of the business due to unknown or changing states of the models in the world, which can make analytic truth wrong.

You are not reading what comes after,
Analytic truth can be wrong — Corvus

{correct} is an aspect of the meaning of the term {truth} so analytic truth cannot possibly be wrong in any way what-so-ever. If it cannot possibly be wrong in any way what-so-ever then it cannot possibly be wrong in any specific way.

If it is "if it is wrongly defined" then it never was any sort of truth at all. If it was "applied to an incorrect model of the actual world", then again it never was any sort of truth at all. {Analytic truth} are only the subset of expressions of language that are actually true even if everyone in the universe disagrees about the truth of these expressions.

This eliminates this terrible mistake by Gödel:

"14 Every epistemological antinomy can likewise be used for a similar undecidability proof." (Gödel 1931:43-44) — PL Olcott

I have to call you on this it to make it explicitly clear. Your reference is to a footnote to an illustrative preliminary proof that Godel presents in the beginning of his1931 paper.

He explicitly limits his argument to systems of sufficient expressive power. He further notes that while his sample expression asserts its own unprovability while at the same time neither itself nor its negation are provable, that it must be true because it asserts its own unprovability. "The proposition undecidable in the system PM is thus decidable by metamathematical arguments."

Thus no mistake, terrible or otherwise.

He explicitly limits his argument to systems of sufficient expressive power. He further notes that while his sample expression asserts its own unprovability while at the same time neither itself nor its negation are provable, that it must be true because it asserts its own unprovability. "The proposition undecidable in the system PM is thus decidable by metamathematical arguments." — tim wood

The terrible mistake is that no self-contradictory expression is any kind of propositional at all. Not only is it a mistake it is a ridiculously stupid mistake as if we spent 2000 years years trying to figure out whether this sentence is true or false: "What time is it".

Self-contradictory expressions are not truth bearers in the same way that questions are not truth bearers. Most of the best experts in the world are still trying to "resolve" the truth value of the liar paradox: "This sentence is not true".

A proposition is a central concept in the philosophy of language, semantics, logic, and related fields, often characterized as the primary bearer of truth or falsity. https://en.wikipedia.org/wiki/Proposition

I am obliged to conclude that what you're writing about has nothing to do with Godel or any of Godel's ideas. But since you claim Godel has made "a ridiculously stupid mistake," it appears you do not know what Godel's ideas are about. Which is too bad, because all you have to do is just read the first section of his 1931 paper, which you cited, and you would have enough of an understanding of his ideas to know that he at least was not mistaken. And as well you might try reading your other citation.

I suspect your usage is a kind of term-of-art that itself has nothing to do with any idea of Godel's.

I am obliged to conclude that what you're writing about has nothing to do with Godel or any of Godel's ideas. But since you claim Godel has made "a ridiculously stupid mistake," it appears you do not know what Godel's ideas are about. Which is too bad, because all you have to do is just read the first section of his 1931 paper, which you cited, and you would have enough of an understanding of his ideas to know that he at least was not mistaken. And as well you might try reading your other citation. — tim wood

In other words you too simply don't understand that epistemological antinomies (AKA self-contradictory expressions) are simply not truth bearers thus have no idea why this statement is pure nonsense:

...14 Every epistemological antinomy can likewise be used for a similar undecidability proof...
(Gödel 1931:43-44)

{correct} is an aspect of the meaning of the term {truth} so analytic truth cannot possibly be wrong in any way what-so-ever. If it cannot possibly be wrong in any way what-so-ever then it cannot possibly be wrong in any specific way. — PL Olcott

Your points seem to be confined in the domain of analytic truth only. In a domain where all in the domain is defined as truth regardless of the real world cases, it doesn't seem to be meaningful or productive keep insisting analytic truth is true in all cases. Jump out from the cave of the analytic truth, you can see that there are the real world and possible world with chaotic situations and events, where truth can be wrong, falsity can be right, and lots of possible unknown events, objects and situations. Analytic truths becomes useless in the all possible world.

Another point is that, you have been talking about the Paradox cases in the old propositional logic only. It looks the paradox is problem, and cannot be handled logically, and devoid of truth value from the old restricted logic. But if you look at the paradox from even PL or FOL, it can be handled no problem.

"This sentence is false" can be generalised into "Some sentence is false" which is not a contradiction. Suddenly it is not explicitly self referencing for the truth value. It generalise the sentence into some sentence which is false out there. HOL generalisation and abstraction would be able to handle far more complex cases with its expanded variables for relations, operations and predicates.

In other words you too simply don't understand that epistemological antinomies (AKA self-contradictory expressions) are simply not truth bearers thus have no idea why this statement is pure nonsense:

...14 Every epistemological antinomy can likewise be used for a similar undecidability proof...
(Gödel 1931:43-44) — PL Olcott

Godel's paper is surprisingly easy to read, although of course not as easy to understand, and the first section his effort to be easy. I've read it and understood it. On the other hand, you've made a claim and on request for clarification have offered nothing in support of it. It's easy to say someone is wrong, but at the same time that means that someone is wrong.

I'm guessing in your system Godelian self-reference is simply ruled out, which you certainly can do. But that makes Godel neither wrong nor a fool, and to say he is simply means that one of you is both.

Your points seem to be confined in the domain of analytic truth only. In a domain where all in the domain is defined as truth regardless of the real world cases — Corvus

That is not true at all. If someone says that a {dog} <is> a fifteen story office building this is ruled as false because there are no {dogs} that <are> fifteen story office buildings in the actual world.

I'm guessing in your system Godelian self-reference is simply ruled out, which you certainly can do. But that makes Godel neither wrong nor a fool, and to say he is simply means that one of you is both. — tim wood

The way that all self-contradictory sentences are ruled out is simple. Self-contradictory sentences cannot be proven or refuted from axioms thus are tossed out as non-truth bearers.
¬TruthBearer(L, x) ≡ ∃x ∈ Language(L) ((L ⊬ x) ∧ (L ⊬ ¬x))

I'm guessing in your system Godelian self-reference is simply ruled out, which you certainly can do. But that makes Godel neither wrong nor a fool, and to say he is simply means that one of you is both. — tim wood

¬TruthBearer(L,x) ≡ ∃x ∈ Language(L) ((L ⊬ x) ∧ (L ⊬ ¬x))
It does seem ridiculously stupid that a formal system could be construed as incomplete on the basis that it cannot prove self-contradictory expressions. We could analogously say that a baker that cannot bake a perfect angel food cakes using only house bricks for ingredients lacks baking skill.

"This sentence is false" can be generalised into "Some sentence is false" which is not a contradiction. — Corvus

Likewise we can generalize cows eat house bricks into cows eat something.
Any nonsense sentence can be changed into a different sentence that is not nonsense.

The way that all self-contradictory sentences are ruled out is simple. Self-contradictory sentences cannot be proven or refuted from axioms thus are tossed out as non-truth bearers. — PL Olcott

This is helpful. But you have omitted a critical qualification: "[C]annot be proven or refuted" from the axioms of the system. But that the sentence in question is absolutely a truth bearer is established by meta-system argument.

"This sentence is not provable." If provable then not provable, and that's a no-no. Clearly then it cannot be provable. Which means that it certainly does have a truth value, that it is provable that it is not provable. Now, if in a system of yours, you wish to make your own ruling on these, you can. But nowhere in that is Godel demonstrated wrong or foolish, and it is wrong and foolish to claim that he is. Unless you can prove it. Can you?

And Godel defaulted from true to provable because he could find no good - adequate - definition of truth.