Then why bother with a machine/program? You have simply gone to the trouble of creating a data-base - in theory because there are significant problems im creating one for real. — tim wood

I am referring to the finite set of finite strings that encode the actual general knowledge true facts of the world. I refer to general knowledge because this is finite. That no one has written them all down in one place does not mean that they do not exist.

The only reason that "cats are animals" is true is that it is stipulated to be true thus allocating semantic meaning to otherwise utterly meaningless finite strings. Language different than English does this same thing with their own set of finite strings.

My True(L,x) predicate is defined to return true or false for every
finite string x on the basis of the existence of a sequence of truth
preserving operations that derive x from — PL Olcott

Assuming then it returns true for all true strings and false for all false ones, right?

So are you going here for the solution for the Entscheidungsproblem? Seems something like that.

Finite string expressions that are not truth-bearers are rejected
as a type mismatch error for every formal system of bivalent logic.

Truthbearer(English, "This sentence is not true") is false.
Truthbearer(English, "This sentence is true") is false.
Truthbearer(English, "a fish") is false.
Truthbearer(English, "some fish are alive") is true. — PL Olcott

So with this assumption you think you can state that the Church-Turing thesis has no truth-bearing?

Assuming then it returns true for all true strings and false for all false ones, right? — ssu

Yes and non truth-bearers are screened out.
Truthbearer(L,x) ≡ (True(L,x) ∨ True(L,~x))
False ≡ True(L,~x))

So are you going here for the solution for the Entscheidungsproblem? Seems something like that. — ssu

Yes. https://simple.wikipedia.org/wiki/Entscheidungsproblem

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

Truthbearer(L,x) ≡ (True(L,x) ∨ True(L,~x))

Epistemological antinomies no longer for the basis for any undecidability proof they are
simply rejected as a type mismatch error for every formal system of bivalent logic.

So with this assumption you think you can state that the Church-Turing thesis has no truth-bearing? — ssu

The only issue that I am correcting is the notion of decidability.
The notion of computation remains the same.

This user has been deleted and all their posts removed.

The only issue that I am correcting is the notion of decidability.
— PL Olcott
A great thing! But tell, how have you corrected it? — tim wood

If there are no sequence of truth preserving operations from the verbal semantic meaning of expression x {true on the basis of its meaning} to x or ~x then the expression is rejected as not a truth bearer thus a type mismatch error for every system of bivalent logic. LP := ~True(L, LP) is the best known example of this.

This user has been deleted and all their posts removed.

↪PL Olcott And this is just no correction at all. Near as i can tell from both reading your posts and your listed citations, all you have done is invoke an idea of a list of propositions that you have decreed "true facts." And there being no undecidable propositions among them - being excluded by you - you declare undecidability corrected. Unless you can mix in some sense, this stands both as nonsense and nonsensical — tim wood

When we have all of the truth facts of the world or even all the true facts about logic, math and computation then it is easy to see that epistemological antinomies and their negation cannot be derived from these true facts. LP := ~True(L, LP) then True(L, LP) is false and True(L, ~LP) is false.

This user has been deleted and all their posts removed.

Then what did Godel do and how did he do it? Or rather, inasmuch as he rigorously derives his undecidable proposition, on what basis do you claim it impossible? And now I insist on your using English unless you are using symbols to prove/demonstrate a point. — tim wood

It is much simpler to see what Tarski did, Gödel hid the missing inference steps
behind Gödel numbers and diagonalization.

This is Tarski's formalized Liar Paradox
x ∉ True if and only if p
where the symbol 'p' represents the whole sentence x
https://liarparadox.org/Tarski_275_276.pdf

This is stated more simply as LP := ~True(L ,LP)

Tarski found out that ~True(L, LP) is true (in his meta theory) and
True(L,LP) is not provable in his theory and this got him confused.

This sentence is not true: "This sentence is not true" is true because
"This sentence is not true" is not true.

https://liarparadox.org/Tarski_275_276.pdf

This user has been deleted and all their posts removed.

Does it escape your notice that the theory, to be efficacious in the desired manner, has been enriched and has to be enriched? Or that the enriched thing - or any enriched thing - is not the same as the thing not enriched? — tim wood

There has never actually been any need for this enrichment, it has always been
expressible in a single formal system with a single formal language as I elaborate below.

x ∉ True if and only if p
where the symbol 'p' represents the whole sentence x

His intention was for formalize the actual Liar Paradox
It would then be possible to reconstruct the antinomy of the liar in the
metalanguage, by forming in the language itself a sentence x such that
the sentence of the metalanguage which is correlated with x asserts that
x is not a true sentence. https://liarparadox.org/Tarski_247_248.pdf

The above is Is better stated as: p ↔ p ∉ True
his self-reference is a little clumsy and the above is still not quite
actual self-reference.

It is standard convention to formalize self-reference incorrectly
ϕ(x) there is a sentence ψ such that S ⊢ ψ ↔ ϕ⟨ψ⟩.
*The sentence ψ is of course not self-referential in a strict sense*,
but mathematically it behaves like one.
https://plato.stanford.edu/entries/self-reference/#ConSemPar
That whole article was ONLY about self-reference

x := y means x is defined to be another name for y
https://en.wikipedia.org/wiki/List_of_logic_symbols

Thus Tarski's p is better stated as: p := p ∉ True
even better as: p := ~True(Tarski-theory, p)
p says that it is not true in Tarski's-theory.

It took me 500 hours studying those four pages of Tarski to get to that point.
You probably won't be able to get there by skimming those two pages.

It is much simpler to see what Tarski did, Gödel hid the missing inference steps
behind Gödel numbers and diagonalization.

This is Tarski's formalized Liar Paradox
x ∉ True if and only if p
where the symbol 'p' represents the whole sentence x
https://liarparadox.org/Tarski_275_276.pdf

This is stated more simply as LP := ~True(L ,LP)

Tarski found out that ~True(L, LP) is true (in his meta theory) and
True(L,LP) is not provable in his theory and this got him confused.

This sentence is not true: "This sentence is not true" is true because
"This sentence is not true" is not true. — PL Olcott

Even if I'm just an amateur on these issues, I think here's a mistake.

Gödel isn't just coming up with the Liar paradox and "hiding" the missing inference steps behind Gödel numbers and diagonalization. Many people do think that Gödel has fallen into the trap of self reference and is talking about basically the paradox, but he isn't.

He is talking about provability and makes a formal mathematical statement not of "this sentence is not true", but "this sentence is unprovable" or "the sentence (s) in unprovable". It isn't a paradox as the statement simply is unprovable, not illogical. While proving or giving a proof in mathematics is very close and usually the same thing to computation, then it's no wonder that the undecidability results are so close to each other (Gödel, Turing, Tarski).

And they aren't confused. Their findings aren't something that just can be assume away, it simply would be illogical to do that.

For myself the clearest example of this diagonalization is for you to say something that you don't say. Now, does there exist something that you don't ever say? Of course! But simply you cannot say it. It doesn't go away by assumption.

This user has been deleted and all their posts removed.

Gödel isn't just coming up with the Liar paradox and "hiding" the missing inference steps behind Gödel numbers and diagonalization. Many people do think that Gödel has fallen into the trap of self reference and is talking about basically the paradox, but he isn't. — ssu

Did you notice that I changed the subject to Tarski?
Tarski does the same thing as Gödel yet shows his work.

Let's stipulate that your "verbal model..," which is practically impossible and I suspect theoretically impossible, exists. I assume you mean that finite stings will be input, and that in every case the output will be, correctly, a T or an F. How will it work? — tim wood

We can see that when we formalize the Liar Paradox correctly
LP := ~True(L, LP)

and not the clumsy way that Tarski formalized it :
x ∉ True if and only if p
where the symbol 'p' represents the whole sentence x

There is no need for any separate theory and meta-theory.
True(L, LP) is false
True(L, ~LP) is false

Truthbearer(L,x) ≡ (True(L,x) ∨ True(L,~x))
Truthbearer(L,LP) is false

and we get the same result as the Tarski meta-theory directly in L
~True(L, LP) is true.

OK, these all are undecidability results and hence are quite similar.
Yet these findings aren't a repeat finding of a paradox. As also @tim wood stated, what Gödel shows is that there's a true, but unprovable sentences.

Referring to the https://plato.stanford.edu/entries/truthmakers/#Max about truthmakers, it seems that you make a similar argument like Rodriguez-Pereyra (2006c) to the refutation of Milne (2005). Hence you want to refer to the Liar Paradox here. (According to Rodriguez-Pereyra, because (M) is akin to the Liar sentence there’s no reason to suppose that (M) is meaningful either).

Or as you say in the OP:

Finite string expressions that are not truth-bearers are rejected
as a type mismatch error for every formal system of bivalent logic. — PL Olcott

Yet Milne has the gist of this: the problem here is that there indeed are true, but unprovable truths. It really doesn't go away by thinking that forbidding paradoxes, forbidding negative self reference or diagonalization and then assuming that everything can be done and all is well.

Hence if the maximalist view is that "For every truth, then there must be something in the world that makes it true" it still holds, with the simple caveat: yet not all of these truths can be proven to be true.

Hopefully you get what I'm trying to say here.

what Gödel shows is that there's a true, but unprovable sentences. — ssu

He doesn't actually show that and if he didn't hide his work we could see that he doesn't really show that. He doesn't even claim that, yet what he does claim is a little incoherent. G is true in PA yet not provable in PA. The way that we know G is true is that G is provable in meta-math.

Yet Milne has the gist of this: the problem here is that there indeed are true, but unprovable truths. — ssu

I have studied these actual papers. Milne is actually saying that there are some expressions that we know are true yet have no way what-so-ever to know that they are true. If an expression utterly lacks any criterion measure showing that it is true then it remains untrue.

The thing that all of these writers currently lack is shown below:
TT := True(L, TT)
TM := Has-a-Truthmaker(L, TM)
LP := ~True(L, LP)

True(L, TT) is false
True(L, ~TT) is false

True(L, TM) is false
True(L, ~TM) is false

True(L, LP) is false
True(L, ~LP) is false

Copyright 2024 PL Olcott

HERE IS WHY NONE OF THEM ARE TRUTH-BEARERS
BEGIN:(Clocksin & Mellish 2003:254)
equal(X, X).
?- equal(foo(Y), Y).

that is, they will allow you to match a term against an uninstantiated
subterm of itself. In this example, foo(Y) is matched against Y, which
appears within it. As a result,Y will stand for foo(Y), which is
foo(foo(Y)) (because of what Y stands for), which is foo(foo(foo(Y))),
and so on. So Y ends up standing for some kind of infinite structure.
END:(Clocksin & Mellish 2003:254)

This user has been deleted and all their posts removed.

He doesn't actually show that and if he didn't hide his work we could see that he doesn't really show that. He doesn't even claim that, yet what he does claim is a little incoherent. — PL Olcott

:brow:

Gödel is incoherent?

Milne is actually saying that there are some expressions that we know are true yet have no way what-so-ever to know that they are true. If an expression utterly lacks any criterion measure showing that it is true then it remains untrue. — PL Olcott

Interesting to talk about the same issue in two threads at the same time, but anyway...

Ok, let's think about some of these expressions. And no, I haven't seen the actual Milne's paper, so I cannot say more when I have just the one link. (Is it free and obtainable by the net?)

Now, can you give an answer you don't give? It would be illogical if you could. Are there in existence these kind of answers? Obviously yes. What defines them? Obviously the answers that you, @PL Olcott gives.

The above shows just what the problem is when you "Cantor's diagonalization" or basically negative self reference.

So what your problem in using diagonalization?

From your Stanford reference we have, "Let φ be the sentence, "φ is not true." That is, we have φ, simple enough and we need nothing else.
-------------
Now, in plain English, using φ, describe how your "system" works.

What you claim is that it knows what is true and what is not. I'm very skeptical, because of many arguments against this, and also not least because you have been singularly non-responsive through at least two threads and many posts. — tim wood

I want to mostly Gödel and focus on how a True(L,x) predicate would actually apply to the properly formalize Liar Paradox.
LP := ~True(L, LP)

<Tarski Undefinability>
We shall show that the sentence x is actually undecidable
and at the same time true ... (page 275)

the proof of
the sentence x given in the metatheory can automatically be
carried over into the theory itself: the sentence x which is
undecidable in the original theory becomes a decidable sentence
in the enriched theory.
https://liarparadox.org/Tarski_275_276.pdf (page 276)
</Tarski Undefinability>

When we stick with theory L we get the same results, thus no need for any metatheory
True(L, LP) is false
True(L, ~LP) is false
Truthbearer(L,x) ≡ (True(L,x) ∨ True(L,~x))

So what Tarski says is undecidable in his theory is actually not a truth-bearer in his theory.
What Tarski said is provable in his metatheory making it true in his theory is
~True(L, LP) is true in his theory because LP is not a truth-bearer in L.

Ok, let's think about some of these expressions. And no, I haven't seen the actual Milne's paper, so I cannot say more when I have just the one link. (Is it free and obtainable by the net?) — ssu

Not every truth has a truthmaker II PETER MILNE
https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=e5f9578348844874f5d2542dcaff8d481e016483

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

The above shows just what the problem is when you "Cantor's diagonalization" or basically negative self reference.

So what your problem in using diagonalization? — ssu

When we can directly see the cycle in the directed graph of the evaluation
sequence of an expression (thus not an acyclic directed graph) then we can
see the expression is not provable because there is something wrong with it.

When we hide this behind Gödelization and diagonalization we can still see
that that expression X is unprovable yet lose the fact that X is unprovable
because there is something wrong with it.

Undecidability, Provability, True(L,x) and Tarski Undefinability are all inherently interrelated.

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

The key missing piece is that no one ever noticed that epistemological antinomies are simply not truth-bearers, thus must be rejected by any formal system of bivalent logic. Once rejected they cannot form any basis for any undecidability proof.

From your Stanford reference we have, "Let φ be the sentence, "φ is not true." That is, we have φ, simple enough and we need nothing else.
-------------
Now, in plain English, using φ, describe how your "system" works. — tim wood

In plain English:
"φ is not true."
What is φ not true about?
φ is not true about being not true.
What is φ not true about being not true about?
φ is not true about being not true about being not true...
Ok so φ NEVER gets to the actual point.

This user has been deleted and all their posts removed.

From reading your citation, it appears you're looking for a truth-maker for φ and not finding one. And from the reading, it is not clear that it needs one; i.e., φ is a truth-bearer. The problem, of course, is that if φ is true, then it is not true, and if it is not true, then it is true. — tim wood

Hence conclusively proving that φ cannot bear the truth value of true or the truth value of false.
That does not make True(L, φ) inconsistent. When True(L, φ) is false and True(L, ~φ) is false then φ is rejected are inherently incorrect. No sense moving beyond this point until after you totally get it.

This user has been deleted and all their posts removed.

It makes it undecidable - it appears you do not know what the words you use mean - and certainly not "inherently incorrect." — tim wood

A truth-bearer is an expression of language X that can be possibly evaluated to a Boolean value.

What the logicians call an undecidable expression X the philosophers of logic correctly assess
as not truth-bearer X.

Here is a much more formal way of saying the same thing:

Back in 2019 I created a formal system that detects cycles in the evaluation of an expression:
https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF

Initially it took any MTT expression and output the directed graph
of the evaluation sequence of this expression. The current system
only outputs the XML of the expression yet the directed graph can
still be derived manually.

The directed graph nodes numbers are on the left (00,01,02) and the nodes
that they transition to (directed graph edges) are on the right (01,02,00)
LP := ~True(L, LP)
00 Not 01
01 True 02, 00 // cycle detected
02 L

It turns out the Prolog can also detect cycles in the directed
graph of the evaluation sequence of an expression.

The SWI-Prolog implementation of unify_with_occurs_check/2 is cycle-safe
and only guards against creating cycles, not against cycles that may
already be present in one of the arguments.
https://www.swi-prolog.org/pldoc/man?predicate=unify_with_occurs_check/2

?- LP = not(true(LP)).
LP = not(true(LP)).

?- unify_with_occurs_check(LP, not(true(LP))).
false.

In other words Prolog has detected a cycle in the directed graph of the
evaluation sequence of the structure of the Liar Paradox. Experts seem
to think that Prolog is taking "not" and "true" as meaningless and is
only evaluating the structure of the expression.

This user has been deleted and all their posts removed.

For example, let your database, described above, be represented by, "The cat sleeps on the couch." You now test "finite" strings against your database, and those that pass are "true," those that don't, "false." And you can do that. But what has that to do with true and false, or knowledge of any kind, or anything undecidable? How does that show that Godel was mistaken or incoherent? Or that Tarski was confused? — tim wood

Any cycle in the directed graph of the evaluation sequence of any expression conclusively proves that this expression is not a truth-bearer thus must be rejected by any formal system of bivalent logic.

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

This is also true for any {epistemological antinomy} AKA self-contradictory expression. If X cannot possibly be evaluated to true or false (for whatever reason) then X must be rejected by any formal system of bivalent logic.

This user has been deleted and all their posts removed.

And any time you want to prove me wrong your keyboard is within easy reach. — tim wood

I either have to explain it in technical terms that you don't understand or explain
it in plain English where too much important meanings slip through the cracks.

The key most important point that can be summed up using the technical terms
of philosophy is that {epistemological antinomies} are not {truth-bearers}.