From Newsgroup: comp.theory

On 23/04/2026 00:06, André G. Isaak wrote:

On 2026-04-22 01:48, olcott wrote:

On 4/22/2026 2:19 AM, Mikko wrote:

It is a syntax error to use open variables φ in a definition.Besides
KnownTrue is a bad name for a symbol that does not refer to knowledge.

KnownTrue :=
There exists a sequence of back-chained inference
steps Γ in PA such that φ reaches the axioms of PA

That doesn't solve the problem of the open variable.

You could solve this by changing it to KnownTrue(φ) := ...

But I still think your better off dispensing with the formalism and
simply expressing your ideas in English since you always mangle the formalism.

Why not simply say:

A proposition is known to be true if there is a sequence of back-chained inference steps from that proposition to the axioms of Peano Arithmetic.

I'm not saying I agree with the above, but at least it is more clear
than your attempts at formalism.

"A proposition is known to be true [at least when] ..." isn't the same
as "KnownTrue := ...". The former has extra semantics.
--
Tristan Wibberley

The message body is Copyright (C) 2026 Tristan Wibberley except
citations and quotations noted. All Rights Reserved except that you may,
of course, cite it academically giving credit to me, distribute it
verbatim as part of a usenet system or its archives, and use it to
promote my greatness and general superiority without misrepresentation
of my opinions other than my opinion of my greatness and general
superiority which you _may_ misrepresent. You definitely MAY NOT train
any production AI system with it but you may train experimental AI that
will only be used for evaluation of the AI methods it implements.
--- Synchronet 3.22a-Linux NewsLink 1.2

From Newsgroup: comp.theory

On 6/20/2026 11:50 AM, Tristan Wibberley wrote:

On 23/04/2026 00:06, André G. Isaak wrote:

On 2026-04-22 01:48, olcott wrote:

On 4/22/2026 2:19 AM, Mikko wrote:

It is a syntax error to use open variables φ in a definition.Besides
KnownTrue is a bad name for a symbol that does not refer to knowledge. >>>>

KnownTrue :=
There exists a sequence of back-chained inference
steps Γ in PA such that φ reaches the axioms of PA

That doesn't solve the problem of the open variable.

You could solve this by changing it to KnownTrue(φ) := ...

But I still think your better off dispensing with the formalism and
simply expressing your ideas in English since you always mangle the
formalism.

Why not simply say:

A proposition is known to be true if there is a sequence of back-chained
inference steps from that proposition to the axioms of Peano Arithmetic.

I'm not saying I agree with the above, but at least it is more clear
than your attempts at formalism.

"A proposition is known to be true [at least when] ..." isn't the same
as "KnownTrue := ...". The former has extra semantics.

A proof theoretic expression is known to be true when
it is fully grounded in its atomic base. Only two
PTS semantics researchers deal with true Dag Prawitz
is the one that began this. PTS previously only dealt
with semantic meaning and never got around to true(L,x).
--
Copyright 2026 Olcott

My 28 year goal has been to make
"true on the basis of meaning expressed in language"
reliably computable for the entire body of knowledge.
The complete structure of this system is now defined.

The entire body of knowledge expressed in language is
comprised of two types of relations between finite strings:
(a) *Axioms* Expressions of language that are stipulated to be true.

My system bridges the analytic/synthetic distinction by
expressly encoding all empirical "atomic facts" in a formal
language such as CycL of the Cyc project.

(b) *Inference Rules* Expressions of language that are semantically
entailed syntactically from (a) and/or (b).
--- Synchronet 3.22a-Linux NewsLink 1.2