Actual interaction with the world that requires sense input from the sense organs is specifically excluded from the body of analytic knowledge. — PL Olcott

A 128-bit integer GUID refers to a single unique sense meaning, thus the class living animal {dog} has its own unique GUID. — PL Olcott

I still can't make any sense out of this. What is the difference between a "sense input" and a "sense meaning"? The only way we can even know that there are such things as dogs is through sense input.

I still can't make any sense out of this. What is the difference between a "sense input" and a "sense meaning"? The only way we can even know that there are such things as dogs is through sense input. — EricH

I am providing the means for a computer to compute Boolean True(L, x) where L is a language such as English and x is an expression of that language. When I show how this can be coherently accomplished then the Tarski Undefinability Theorem is refuted.

When I show how this can be coherently accomplished then the Tarski Undefinability Theorem is refuted. — PL Olcott

This is a very ambitious project - if you succeed then the name PL Olcott will become world famous.

But so far I can't make any sense of what you're saying - this is why I'm trying to get some basic terminology clear. I'll ask again. What is the difference between a "sense input" and a "sense meaning"?

But so far I can't make any sense of what you're saying - this is why I'm trying to get some basic terminology clear. I'll ask again. What is the difference between a "sense input" and a "sense meaning"? — EricH

That you can hear dogs actually barking with your ears is a sense input from your
ears to your mind. Hearing dogs bark is the sense meaning of "dogs bark". These
things cannot be expressed using words thus are not Analytic(Olcott).

“Analytic” sentences, such as “Pediatricians are doctors,” have historically been characterized as ones that are true by virtue of the meanings of their words alone and/or can be known to be so solely by knowing those meanings. The Analytic/Synthetic Distinction

When we exclude those aspects of meanings such as the actual sound of dogs barking and include every element of human general knowledge that can be expressed using words expressly including that some “Pediatricians are rich” then we have the subset of human knowledge that can be processed by a computer program.

3ab2c577-7d38-4a3c-adc9-c5eff8491282 stands for the living animal dog, this is the same way that the Cyc project identifies unique sense meanings, — PL Olcott

How do the users know the unique ID? How does the Cyc Project know that is the ID it has to select the answer for the query?

It's Wikipedia, so you can always edit it.

How do the users know the unique ID? How does the Cyc Project know that is the ID it has to select the answer for the query? — Corvus

I would estimate that the users use ordinary English and the Cyc lexical analyzer converts words into GUIDs. The parser can determine which of the multiple GUIDs for the same word is most probably from context. My cat drank of bowl of milk would not refer to Caterpillar Earth moving equipment or Harvey Milk.

I'm not in the practice of editing Wikipedia articles. Meanwhile, my points about the article stand. More generally, a good amount of caution is warranted when referencing Wikipedia.

(1) The article conflates a language with a theory.

(2) The proof in the article handwaves past the crucial lemma, thus appearing to commit a serious non sequitur. — TonesInDeepFreeze

I have studied these things in my mind continuously for decades. Mathematics uses the term "theory" to mean a set of axioms. Everyone else means a set of ideas that might be true.

My current understanding of a subset of undecidable decision problems is that this undecidability can be easily abolished the same way that ZFC conquered Russell's Paradox. ZFC prevents self-contradictory expressions from coming into existence by forbidding the creation of sets that are members of themselves.

Usage may vary. One prominent definition of 'theory' is that a theory is a set of sentences closed under derivability. Then, any set of axioms determines a theory.

It is a common misconception on Internet forums that ZFC avoids inconsistency by disallowing sets to be members of themselves.

Yes, the axiom of regularity, which is adopted in ZFC, disallows that a set can be a member of itself. But the axiom of regularity does not block inconsistency. What avoids inconsistency is not having the axiom schema of unrestricted comprehension. If we have the axiom schema of unrestricted comprehension, then we get inconsistency, no matter whether we also have the axiom of regularity or not, and no matter whether there may be sets that are members of themselves or not.

Indeed, since the logic is monotonic, adding an axiom cannot avoid inconsistency. The only way to avoid inconsistency is to delete the axioms that provide inconsistency.

ZFC is undecidable. That means that there is no decision procedure to determine whether a given sentence in the language of ZFC is or is not a theorem of ZFC.

It is a common misconception on Internet forums that ZFC avoids inconsistency by disallowing sets to be members of themselves.

Yes, the axiom of regularity, which is adopted in ZFC, disallows that a set can be a member of itself. — TonesInDeepFreeze

You just contradicted yourself. I will be more precise. ZFC eliminates the possibility
of inconsistency that is caused by allowing sets to be members of themselves.

An isomorphic solution would solve the halting problem. A halt decider is not allowed
to be applied to any input to refers to itself.

I did not contradict myself.

And, again, as I just explained, disallowing sets from being members of themselves does not avoid inconsistency. Again, as I just explained, inconsistency can be avoided only by deleting axioms (such as unrestricted comprehension) and not by adding them (such as regularity).

The fact that ZFC avoids inconsistency by not having unrestricted comprehension does not contradict that ZFC also has the axiom of regularity that disallows sets from being members of themselves. Moreover, the purpose of the axiom of regularity is not to avoid inconsistency but rather to facilitate the study of sets as in a hierarchy indexed by the ordinals. It is a nice feature of the axiom of regularity that it disallows sets being members of themselves, as many people regard it counter-intuitive or against the basic concept of 'set' that there are sets that are members of themselves. But the axiom of regularity, even with that feature, is not how set theory avoids inconsistency.

And, again, as I just explained, disallowing sets from being members of themselves does not avoid inconsistency. — TonesInDeepFreeze

When we ask the question: Does a barber shave everyone that does not shave themselves? is allowed to be rejected as an incorrect question then the paradox goes away. ZFC prevents this question from even being expressed as sets.

Moreover, the purpose of the axiom of regularity is not to avoid inconsistency but rather to facilitate the study of sets as in a hierarchy indexed by the ordinals. — TonesInDeepFreeze

Thereby preventing inconsistency in the same way that type theory prevents inconsistency.

What is incorrect is the assumption that there is a barber who shaves all and only those who do not shave themselves.

And we don't even need any set theory to prove that, for any property P, there is no x such that, for all y, Pxy if and only if ~Pyy. We prove that by pure logic alone. So, perforce, we prove it in set theory too.

/

The hierarchy of sets is not type theory nor higher order logic. ZFC is a first order theory. The context here is not type theory nor a higher order logic, but rather first order set theory:

The main point here could not be more clear: The logic is monotonic, so adding an axiom can't block inconsistency.

Said another way:

Let G and H be sets of formulas, and P a formula:

If G proves P, then G union H proves P.

So, if set theory without the axiom of regularity proves a contradiction, then set theory with the axiom of regularity proves a contradiction.

The schema of unrestricted comprehension proves a contradiction. So the schema of unrestricted comprehension with also the axiom of regularity proves a contradiction.

So the contradiction can't be avoided by adding the axiom of regularity to any set of axioms, but rather the contradiction can be avoided only by not having the schema of unrestricted comprehension.

So, if set theory without the axiom of regularity proves a contradiction, then set theory with the axiom of regularity proves a contradiction. — TonesInDeepFreeze

My post is about a single coherent way around all of these issues.
The key mistake of decision theory is that the notion of decidability requires a decider
to correctly answer a self-contradictory (thus incorrect) question otherwise an input
is construed as undecidable.

Whatever the case may be with your characterization of the subject, at least we know that disallowing sets to be members of themselves does not avoid Russell's paradox but rather, as to first order set theory, Russell's paradox is avoided by not having the schema of unrestricted comprehension.

The key issue with decision theory is that deciders are required to correctly
answer a self-contradictory (thus incorrect) questions.

The key difficulty with resolving this issue that most modern day philosophers
do not understand that both of these questions are equally incorrect:
(a) Is this sentence true or false: "What time it is?"
(b) Is this sentence true or false: "This sentence is not true."

They do not understand that the Liar Paradox is simply not a truth bearer.

All steps in proofs are statements, not questions.

All steps in proofs are statements, not questions. — TonesInDeepFreeze

The decision problem form of a formal proof <is> a yes/no question about an input.
The formal proof shows the steps of how X is derived from Y in Z.
The decision problem version answers the question: Can X be derived from Y in Z?
When X is a theorem of Z then the premises are empty.

In computability theory and computational complexity theory, a decision problem is a computational problem that can be posed as a yes–no question of the input values.
Decision problem

One can couch things as questions. But the proofs themselves do not have questions in them.

a good amount of caution is warranted when referencing Wikipedia. — TonesInDeepFreeze

Huge amount.

One can couch things as questions. But the proofs themselves do not have questions in them. — TonesInDeepFreeze

Proofs always have the provability question associated with them:
Whether or not a proof exists is.

a good amount of caution is warranted when referencing Wikipedia.
— TonesInDeepFreeze

Huge amount. — Lionino

I have found that it always succinctly and clearly presents an accurate view of
every technical subject that I have ever referenced as measured by its correspondence
with many other sources.

"Is there a proof of T?" is a question.

But a proof of T does not have questions in it.

Yet I showed exactly what is amiss in the Wikipedia article recently cited.

Yet I showed exactly what was amiss in the Wikipedia article recently cited. — TonesInDeepFreeze

That is a degree of detail that is totally irrelevant to my point so I did not
examine it at all. My point is the Tarski anchored his Undefinability
Theorem in the actual Liar Paradox.

So far hardly any modern or ancient philosophers seem to understand
that the Liar Paradox is not a truth bearer thus has no truth value thus
is not in the domain of any decision problem or formal proof.

"Does there exist a proof of T?" is a question. — TonesInDeepFreeze

Is the question associated with every formal proof or lack thereof.

It's not a question of what was relevant to your point. I cited faults in the article, whether or not those faults bear on your point.

Tarski's proof doesn't work the way you describe it.

/

For any sentence T, set of axioms S and set of rules R, we may ask the question "Is T derivable from S with R?" That fact doesn't entail the counterfactual that there are questions in proofs. Tarski's proof does not have questions in it.

Tarski's proof doesn't work the way you describe it. To see that, you just need to read the article that you yourself say is "clear and accurate". — TonesInDeepFreeze

The proof of Tarski's undefinability theorem in this form is again
by reductio ad absurdum. Suppose that an L-formula True(n)

as above existed, i.e., if A is a sentence of arithmetic, then
True(g(A)) holds in N if and only if A holds in N. Hence for all

A, the formula True(g(A)) ⟺ A holds in N. But the diagonal
lemma yields a counterexample to this equivalence, by

giving a "liar" formula S such that S ⟺ ¬True(g(A)) holds
in N. This is a contradiction QED.

https://en.wikipedia.org/wiki/Tarski%27s_undefinability_theorem

This correctly recognizes that the Liar Paradox is not a truth bearer.
LP = "This sentence is not true."
Boolean True(English, LP) is false
Boolean True(English, ~LP) is false

I have found that it always succinctly and clearly presents an accurate view of
every technical subject that I have ever referenced as measured by its correspondence
with many other sources. — PL Olcott

I imagine that that happens because you learn from there. I find nonsense there all the time. The people who run it are oligophrenic. So I avoid it like a plague.