On 02/04/2026 23:58, olcott wrote:
To be able to properly ground this in existing foundational
peer reviewed papers will take some time.
Do you think 100 years would be enough, or at least some finite time?
On 4/3/2026 2:13 AM, Mikko wrote:
On 02/04/2026 23:58, olcott wrote:
To be able to properly ground this in existing foundational
peer reviewed papers will take some time.
Do you think 100 years would be enough, or at least some finite time?
I have to carefully study at least a dozen papers
that may average 15 pages each. The basic notion
of a "well founded justification tree" essentially
means the Proof Theoretic notion of reduction to
a Canonical proof.
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
The above Prolog determines that LP does not
have a "well founded justification tree".
On 03/04/2026 16:35, olcott wrote:
On 4/3/2026 2:13 AM, Mikko wrote:
On 02/04/2026 23:58, olcott wrote:
To be able to properly ground this in existing foundational
peer reviewed papers will take some time.
Do you think 100 years would be enough, or at least some finite time?
I have to carefully study at least a dozen papers
that may average 15 pages each. The basic notion
of a "well founded justification tree" essentially
means the Proof Theoretic notion of reduction to
a Canonical proof.
The above Prolog determines that LP does not
have a "well founded justification tree".
If you want to illustrate with examples you should have two examples:
one with a negative result (as above) and one with a positive one.
So the above example should be paired with one that has someting
else in place of not(provable(F, G)) so that the result will not be
false.
On 03/04/2026 16:35, olcott wrote:
On 4/3/2026 2:13 AM, Mikko wrote:
On 02/04/2026 23:58, olcott wrote:
To be able to properly ground this in existing foundational
peer reviewed papers will take some time.
Do you think 100 years would be enough, or at least some finite time?
I have to carefully study at least a dozen papers
that may average 15 pages each. The basic notion
of a "well founded justification tree" essentially
means the Proof Theoretic notion of reduction to
a Canonical proof.
The above Prolog determines that LP does not
have a "well founded justification tree".
If you want to illustrate with examples you should have two examples:
one with a negative result (as above) and one with a positive one.
So the above example should be paired with one that has someting
else in place of not(provable(F, G)) so that the result will not be
false.
"Mary went to Walmart and bought a carton of Breyers ice cream"
On 4/4/2026 2:53 AM, Mikko wrote:
On 03/04/2026 16:35, olcott wrote:
On 4/3/2026 2:13 AM, Mikko wrote:
On 02/04/2026 23:58, olcott wrote:
To be able to properly ground this in existing foundational
peer reviewed papers will take some time.
Do you think 100 years would be enough, or at least some finite time?
I have to carefully study at least a dozen papers
that may average 15 pages each. The basic notion
of a "well founded justification tree" essentially
means the Proof Theoretic notion of reduction to
a Canonical proof.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above Prolog determines that LP does not
have a "well founded justification tree".
If you want to illustrate with examples you should have two examples:
one with a negative result (as above) and one with a positive one.
So the above example should be paired with one that has someting
else in place of not(provable(F, G)) so that the result will not be
false.
THIS IS NOT A PROLOG SPECIFIC THING
On 04/04/2026 19:23, olcott wrote:
On 4/4/2026 2:53 AM, Mikko wrote:
On 03/04/2026 16:35, olcott wrote:
On 4/3/2026 2:13 AM, Mikko wrote:
On 02/04/2026 23:58, olcott wrote:I have to carefully study at least a dozen papers
To be able to properly ground this in existing foundational
peer reviewed papers will take some time.
Do you think 100 years would be enough, or at least some finite time? >>>>
that may average 15 pages each. The basic notion
of a "well founded justification tree" essentially
means the Proof Theoretic notion of reduction to
a Canonical proof.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above Prolog determines that LP does not
have a "well founded justification tree".
If you want to illustrate with examples you should have two examples:
one with a negative result (as above) and one with a positive one.
So the above example should be paired with one that has someting
else in place of not(provable(F, G)) so that the result will not be
false.
THIS IS NOT A PROLOG SPECIFIC THING
That's mainly true. However, in como.lang.prolog the discussion should
be restricted to Prolog specific things, in this case to the Prolog
example above and the contrasting Prolog example not yet shown.
On 4/5/2026 2:05 AM, Mikko wrote:
On 04/04/2026 19:23, olcott wrote:
On 4/4/2026 2:53 AM, Mikko wrote:
On 03/04/2026 16:35, olcott wrote:
On 4/3/2026 2:13 AM, Mikko wrote:
On 02/04/2026 23:58, olcott wrote:I have to carefully study at least a dozen papers
To be able to properly ground this in existing foundational
peer reviewed papers will take some time.
Do you think 100 years would be enough, or at least some finite time? >>>>>
that may average 15 pages each. The basic notion
of a "well founded justification tree" essentially
means the Proof Theoretic notion of reduction to
a Canonical proof.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above Prolog determines that LP does not
have a "well founded justification tree".
If you want to illustrate with examples you should have two examples:
one with a negative result (as above) and one with a positive one.
So the above example should be paired with one that has someting
else in place of not(provable(F, G)) so that the result will not be
false.
THIS IS NOT A PROLOG SPECIFIC THING
That's mainly true. However, in como.lang.prolog the discussion should
be restricted to Prolog specific things, in this case to the Prolog
example above and the contrasting Prolog example not yet shown.
In order to elaborate the details of my system
I require some way to formalize natural language.
Montague Grammar, Rudolf Carnap Meaning Postulates,
the CycL language of the Cyc project and Prolog
are the options that I have been considering.
The notion of how a well-founded justification tree
eliminates undecidability is a key element of my system.
Prolog shows this best.
On 04/05/2026 04:25 AM, olcott wrote:
On 4/5/2026 2:05 AM, Mikko wrote:
On 04/04/2026 19:23, olcott wrote:
On 4/4/2026 2:53 AM, Mikko wrote:
On 03/04/2026 16:35, olcott wrote:
On 4/3/2026 2:13 AM, Mikko wrote:
On 02/04/2026 23:58, olcott wrote:
To be able to properly ground this in existing foundational
peer reviewed papers will take some time.
Do you think 100 years would be enough, or at least some finite >>>>>>> time?
I have to carefully study at least a dozen papers
that may average 15 pages each. The basic notion
of a "well founded justification tree" essentially
means the Proof Theoretic notion of reduction to
a Canonical proof.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above Prolog determines that LP does not
have a "well founded justification tree".
If you want to illustrate with examples you should have two examples: >>>>> one with a negative result (as above) and one with a positive one.
So the above example should be paired with one that has someting
else in place of not(provable(F, G)) so that the result will not be
false.
THIS IS NOT A PROLOG SPECIFIC THING
That's mainly true. However, in como.lang.prolog the discussion should
be restricted to Prolog specific things, in this case to the Prolog
example above and the contrasting Prolog example not yet shown.
In order to elaborate the details of my system
I require some way to formalize natural language.
Montague Grammar, Rudolf Carnap Meaning Postulates,
the CycL language of the Cyc project and Prolog
are the options that I have been considering.
The notion of how a well-founded justification tree
eliminates undecidability is a key element of my system.
Prolog shows this best.
Montague was a hipster flake and about the
worst sort of snide hypocrite.
Herbrand on the other hand has a much more
thorough account of that abstract symbolic
language and natural language are equi-interpretable.
Otherwise your account of weak logicist positivism
has that there's a stronger account of a strong
logicist positivism that includes for the like of
Derrida and Husserl an accommodation of the strong
mathematical platonism and including its super-classical
concepts and results.
On 4/5/2026 2:05 AM, Mikko wrote:
On 04/04/2026 19:23, olcott wrote:
On 4/4/2026 2:53 AM, Mikko wrote:
On 03/04/2026 16:35, olcott wrote:
On 4/3/2026 2:13 AM, Mikko wrote:
On 02/04/2026 23:58, olcott wrote:I have to carefully study at least a dozen papers
To be able to properly ground this in existing foundational
peer reviewed papers will take some time.
Do you think 100 years would be enough, or at least some finite time? >>>>>
that may average 15 pages each. The basic notion
of a "well founded justification tree" essentially
means the Proof Theoretic notion of reduction to
a Canonical proof.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above Prolog determines that LP does not
have a "well founded justification tree".
If you want to illustrate with examples you should have two examples:
one with a negative result (as above) and one with a positive one.
So the above example should be paired with one that has someting
else in place of not(provable(F, G)) so that the result will not be
false.
THIS IS NOT A PROLOG SPECIFIC THING
That's mainly true. However, in como.lang.prolog the discussion should
be restricted to Prolog specific things, in this case to the Prolog
example above and the contrasting Prolog example not yet shown.
In order to elaborate the details of my system
I require some way to formalize natural language.
Montague Grammar, Rudolf Carnap Meaning Postulates,
the CycL language of the Cyc project and Prolog
are the options that I have been considering.
The notion of how a well-founded justification tree
eliminates undecidability is a key element of my system.
Prolog shows this best.
On 05/04/2026 14:25, olcott wrote:
On 4/5/2026 2:05 AM, Mikko wrote:
On 04/04/2026 19:23, olcott wrote:
On 4/4/2026 2:53 AM, Mikko wrote:
On 03/04/2026 16:35, olcott wrote:
On 4/3/2026 2:13 AM, Mikko wrote:
On 02/04/2026 23:58, olcott wrote:
To be able to properly ground this in existing foundational
peer reviewed papers will take some time.
Do you think 100 years would be enough, or at least some finite >>>>>>> time?
I have to carefully study at least a dozen papers
that may average 15 pages each. The basic notion
of a "well founded justification tree" essentially
means the Proof Theoretic notion of reduction to
a Canonical proof.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above Prolog determines that LP does not
have a "well founded justification tree".
If you want to illustrate with examples you should have two examples: >>>>> one with a negative result (as above) and one with a positive one.
So the above example should be paired with one that has someting
else in place of not(provable(F, G)) so that the result will not be
false.
THIS IS NOT A PROLOG SPECIFIC THING
That's mainly true. However, in como.lang.prolog the discussion should
be restricted to Prolog specific things, in this case to the Prolog
example above and the contrasting Prolog example not yet shown.
In order to elaborate the details of my system
I require some way to formalize natural language.
Montague Grammar, Rudolf Carnap Meaning Postulates,
the CycL language of the Cyc project and Prolog
are the options that I have been considering.
The notion of how a well-founded justification tree
eliminates undecidability is a key element of my system.
Prolog shows this best.
It is not Prolog computable to determine whether a sentence of Peano arithmetic has a well-founded justification tree in Peano arithmetic.
On 4/6/2026 3:27 AM, Mikko wrote:
On 05/04/2026 14:25, olcott wrote:
On 4/5/2026 2:05 AM, Mikko wrote:
On 04/04/2026 19:23, olcott wrote:
On 4/4/2026 2:53 AM, Mikko wrote:
On 03/04/2026 16:35, olcott wrote:
On 4/3/2026 2:13 AM, Mikko wrote:
On 02/04/2026 23:58, olcott wrote:
To be able to properly ground this in existing foundational
peer reviewed papers will take some time.
Do you think 100 years would be enough, or at least some finite >>>>>>>> time?
I have to carefully study at least a dozen papers
that may average 15 pages each. The basic notion
of a "well founded justification tree" essentially
means the Proof Theoretic notion of reduction to
a Canonical proof.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above Prolog determines that LP does not
have a "well founded justification tree".
If you want to illustrate with examples you should have two examples: >>>>>> one with a negative result (as above) and one with a positive one. >>>>>> So the above example should be paired with one that has someting
else in place of not(provable(F, G)) so that the result will not be >>>>>> false.
THIS IS NOT A PROLOG SPECIFIC THING
That's mainly true. However, in como.lang.prolog the discussion should >>>> be restricted to Prolog specific things, in this case to the Prolog
example above and the contrasting Prolog example not yet shown.
In order to elaborate the details of my system
I require some way to formalize natural language.
Montague Grammar, Rudolf Carnap Meaning Postulates,
the CycL language of the Cyc project and Prolog
are the options that I have been considering.
The notion of how a well-founded justification tree
eliminates undecidability is a key element of my system.
Prolog shows this best.
It is not Prolog computable to determine whether a sentence of Peano
arithmetic has a well-founded justification tree in Peano arithmetic.
A formal language similar to Prolog that can represent
all of the semantics of PA can be developed so that
it detects and rejects expressions that lack well-founded
justification trees.
On 06/04/2026 14:21, olcott wrote:
On 4/6/2026 3:27 AM, Mikko wrote:
On 05/04/2026 14:25, olcott wrote:
On 4/5/2026 2:05 AM, Mikko wrote:
On 04/04/2026 19:23, olcott wrote:
On 4/4/2026 2:53 AM, Mikko wrote:
On 03/04/2026 16:35, olcott wrote:
On 4/3/2026 2:13 AM, Mikko wrote:
On 02/04/2026 23:58, olcott wrote:
To be able to properly ground this in existing foundational >>>>>>>>>> peer reviewed papers will take some time.
Do you think 100 years would be enough, or at least some finite >>>>>>>>> time?
I have to carefully study at least a dozen papers
that may average 15 pages each. The basic notion
of a "well founded justification tree" essentially
means the Proof Theoretic notion of reduction to
a Canonical proof.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above Prolog determines that LP does not
have a "well founded justification tree".
If you want to illustrate with examples you should have two
examples:
one with a negative result (as above) and one with a positive one. >>>>>>> So the above example should be paired with one that has someting >>>>>>> else in place of not(provable(F, G)) so that the result will not be >>>>>>> false.
THIS IS NOT A PROLOG SPECIFIC THING
That's mainly true. However, in como.lang.prolog the discussion should >>>>> be restricted to Prolog specific things, in this case to the Prolog
example above and the contrasting Prolog example not yet shown.
In order to elaborate the details of my system
I require some way to formalize natural language.
Montague Grammar, Rudolf Carnap Meaning Postulates,
the CycL language of the Cyc project and Prolog
are the options that I have been considering.
The notion of how a well-founded justification tree
eliminates undecidability is a key element of my system.
Prolog shows this best.
It is not Prolog computable to determine whether a sentence of Peano
arithmetic has a well-founded justification tree in Peano arithmetic.
A formal language similar to Prolog that can represent
all of the semantics of PA can be developed so that
it detects and rejects expressions that lack well-founded
justification trees.
A language does not detect. For detection you need an algorithm.
On 4/7/2026 3:00 AM, Mikko wrote:
On 06/04/2026 14:21, olcott wrote:
On 4/6/2026 3:27 AM, Mikko wrote:
On 05/04/2026 14:25, olcott wrote:
On 4/5/2026 2:05 AM, Mikko wrote:
On 04/04/2026 19:23, olcott wrote:
On 4/4/2026 2:53 AM, Mikko wrote:
On 03/04/2026 16:35, olcott wrote:
On 4/3/2026 2:13 AM, Mikko wrote:
On 02/04/2026 23:58, olcott wrote:
To be able to properly ground this in existing foundational >>>>>>>>>>> peer reviewed papers will take some time.
Do you think 100 years would be enough, or at least some
finite time?
I have to carefully study at least a dozen papers
that may average 15 pages each. The basic notion
of a "well founded justification tree" essentially
means the Proof Theoretic notion of reduction to
a Canonical proof.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above Prolog determines that LP does not
have a "well founded justification tree".
If you want to illustrate with examples you should have two
examples:
one with a negative result (as above) and one with a positive one. >>>>>>>> So the above example should be paired with one that has someting >>>>>>>> else in place of not(provable(F, G)) so that the result will not be >>>>>>>> false.
THIS IS NOT A PROLOG SPECIFIC THING
That's mainly true. However, in como.lang.prolog the discussion
should
be restricted to Prolog specific things, in this case to the Prolog >>>>>> example above and the contrasting Prolog example not yet shown.
In order to elaborate the details of my system
I require some way to formalize natural language.
Montague Grammar, Rudolf Carnap Meaning Postulates,
the CycL language of the Cyc project and Prolog
are the options that I have been considering.
The notion of how a well-founded justification tree
eliminates undecidability is a key element of my system.
Prolog shows this best.
It is not Prolog computable to determine whether a sentence of Peano
arithmetic has a well-founded justification tree in Peano arithmetic.
A formal language similar to Prolog that can represent
all of the semantics of PA can be developed so that
it detects and rejects expressions that lack well-founded
justification trees.
A language does not detect. For detection you need an algorithm.
unify_with_occurs_check(LP, not(true(LP))).
is a function of the Prolog language that
implements the algorithm.
On 07/04/2026 17:49, olcott wrote:
On 4/7/2026 3:00 AM, Mikko wrote:
On 06/04/2026 14:21, olcott wrote:
On 4/6/2026 3:27 AM, Mikko wrote:
On 05/04/2026 14:25, olcott wrote:A formal language similar to Prolog that can represent
On 4/5/2026 2:05 AM, Mikko wrote:
On 04/04/2026 19:23, olcott wrote:
On 4/4/2026 2:53 AM, Mikko wrote:
On 03/04/2026 16:35, olcott wrote:
On 4/3/2026 2:13 AM, Mikko wrote:
On 02/04/2026 23:58, olcott wrote:
To be able to properly ground this in existing foundational >>>>>>>>>>>> peer reviewed papers will take some time.
Do you think 100 years would be enough, or at least some >>>>>>>>>>> finite time?
I have to carefully study at least a dozen papers
that may average 15 pages each. The basic notion
of a "well founded justification tree" essentially
means the Proof Theoretic notion of reduction to
a Canonical proof.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above Prolog determines that LP does not
have a "well founded justification tree".
If you want to illustrate with examples you should have two >>>>>>>>> examples:
one with a negative result (as above) and one with a positive one. >>>>>>>>> So the above example should be paired with one that has someting >>>>>>>>> else in place of not(provable(F, G)) so that the result will >>>>>>>>> not be
false.
THIS IS NOT A PROLOG SPECIFIC THING
That's mainly true. However, in como.lang.prolog the discussion >>>>>>> should
be restricted to Prolog specific things, in this case to the Prolog >>>>>>> example above and the contrasting Prolog example not yet shown.
In order to elaborate the details of my system
I require some way to formalize natural language.
Montague Grammar, Rudolf Carnap Meaning Postulates,
the CycL language of the Cyc project and Prolog
are the options that I have been considering.
The notion of how a well-founded justification tree
eliminates undecidability is a key element of my system.
Prolog shows this best.
It is not Prolog computable to determine whether a sentence of Peano >>>>> arithmetic has a well-founded justification tree in Peano arithmetic. >>>>
all of the semantics of PA can be developed so that
it detects and rejects expressions that lack well-founded
justification trees.
A language does not detect. For detection you need an algorithm.
unify_with_occurs_check(LP, not(true(LP))).
is a function of the Prolog language that
implements the algorithm.
No, it is not. The question whether a sentence has a well-founded justification tree is a question about one thing so it needs an
algrotim that takes only one input but uunify_with_occurs_check
takes two.
On 4/8/2026 2:08 AM, Mikko wrote:
On 07/04/2026 17:49, olcott wrote:
On 4/7/2026 3:00 AM, Mikko wrote:
On 06/04/2026 14:21, olcott wrote:
On 4/6/2026 3:27 AM, Mikko wrote:
On 05/04/2026 14:25, olcott wrote:A formal language similar to Prolog that can represent
On 4/5/2026 2:05 AM, Mikko wrote:
On 04/04/2026 19:23, olcott wrote:
On 4/4/2026 2:53 AM, Mikko wrote:
On 03/04/2026 16:35, olcott wrote:
On 4/3/2026 2:13 AM, Mikko wrote:
On 02/04/2026 23:58, olcott wrote:
To be able to properly ground this in existing foundational >>>>>>>>>>>>> peer reviewed papers will take some time.
Do you think 100 years would be enough, or at least some >>>>>>>>>>>> finite time?
I have to carefully study at least a dozen papers
that may average 15 pages each. The basic notion
of a "well founded justification tree" essentially
means the Proof Theoretic notion of reduction to
a Canonical proof.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above Prolog determines that LP does not
have a "well founded justification tree".
If you want to illustrate with examples you should have two >>>>>>>>>> examples:
one with a negative result (as above) and one with a positive >>>>>>>>>> one.
So the above example should be paired with one that has someting >>>>>>>>>> else in place of not(provable(F, G)) so that the result will >>>>>>>>>> not be
false.
THIS IS NOT A PROLOG SPECIFIC THING
That's mainly true. However, in como.lang.prolog the discussion >>>>>>>> should
be restricted to Prolog specific things, in this case to the Prolog >>>>>>>> example above and the contrasting Prolog example not yet shown. >>>>>>>>
In order to elaborate the details of my system
I require some way to formalize natural language.
Montague Grammar, Rudolf Carnap Meaning Postulates,
the CycL language of the Cyc project and Prolog
are the options that I have been considering.
The notion of how a well-founded justification tree
eliminates undecidability is a key element of my system.
Prolog shows this best.
It is not Prolog computable to determine whether a sentence of Peano >>>>>> arithmetic has a well-founded justification tree in Peano arithmetic. >>>>>
all of the semantics of PA can be developed so that
it detects and rejects expressions that lack well-founded
justification trees.
A language does not detect. For detection you need an algorithm.
unify_with_occurs_check(LP, not(true(LP))).
is a function of the Prolog language that
implements the algorithm.
No, it is not. The question whether a sentence has a well-founded
justification tree is a question about one thing so it needs an
algrotim that takes only one input but uunify_with_occurs_check
takes two.
The number of inputs does not matter.
If BY ANY MEANS a cycle is detected in the
directed graph of the evaluation sequence of
the expression then the expression is rejected.
True(L, X) := ∃Γ ⊆ BaseFacts(L) (Γ ⊢ X) // copyright Olcott 2018
If for any reason a back chained inference does
not reach BaseFacts(L) then the expression is untrue.
On 4/8/2026 2:08 AM, Mikko wrote:
On 07/04/2026 17:49, olcott wrote:
On 4/7/2026 3:00 AM, Mikko wrote:
On 06/04/2026 14:21, olcott wrote:
On 4/6/2026 3:27 AM, Mikko wrote:
On 05/04/2026 14:25, olcott wrote:A formal language similar to Prolog that can represent
On 4/5/2026 2:05 AM, Mikko wrote:
On 04/04/2026 19:23, olcott wrote:
On 4/4/2026 2:53 AM, Mikko wrote:
On 03/04/2026 16:35, olcott wrote:
On 4/3/2026 2:13 AM, Mikko wrote:
On 02/04/2026 23:58, olcott wrote:
To be able to properly ground this in existing foundational >>>>>>>>>>>>> peer reviewed papers will take some time.
Do you think 100 years would be enough, or at least some >>>>>>>>>>>> finite time?
I have to carefully study at least a dozen papers
that may average 15 pages each. The basic notion
of a "well founded justification tree" essentially
means the Proof Theoretic notion of reduction to
a Canonical proof.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above Prolog determines that LP does not
have a "well founded justification tree".
If you want to illustrate with examples you should have two >>>>>>>>>> examples:
one with a negative result (as above) and one with a positive >>>>>>>>>> one.
So the above example should be paired with one that has someting >>>>>>>>>> else in place of not(provable(F, G)) so that the result will >>>>>>>>>> not be
false.
THIS IS NOT A PROLOG SPECIFIC THING
That's mainly true. However, in como.lang.prolog the discussion >>>>>>>> should
be restricted to Prolog specific things, in this case to the Prolog >>>>>>>> example above and the contrasting Prolog example not yet shown. >>>>>>>>
In order to elaborate the details of my system
I require some way to formalize natural language.
Montague Grammar, Rudolf Carnap Meaning Postulates,
the CycL language of the Cyc project and Prolog
are the options that I have been considering.
The notion of how a well-founded justification tree
eliminates undecidability is a key element of my system.
Prolog shows this best.
It is not Prolog computable to determine whether a sentence of Peano >>>>>> arithmetic has a well-founded justification tree in Peano arithmetic. >>>>>
all of the semantics of PA can be developed so that
it detects and rejects expressions that lack well-founded
justification trees.
A language does not detect. For detection you need an algorithm.
unify_with_occurs_check(LP, not(true(LP))).
is a function of the Prolog language that
implements the algorithm.
No, it is not. The question whether a sentence has a well-founded
justification tree is a question about one thing so it needs an
algrotim that takes only one input but uunify_with_occurs_check
takes two.
The number of inputs does not matter.
On 4/8/2026 6:52 AM, olcott wrote:
On 4/8/2026 2:08 AM, Mikko wrote:
On 07/04/2026 17:49, olcott wrote:
On 4/7/2026 3:00 AM, Mikko wrote:
On 06/04/2026 14:21, olcott wrote:
On 4/6/2026 3:27 AM, Mikko wrote:
On 05/04/2026 14:25, olcott wrote:
On 4/5/2026 2:05 AM, Mikko wrote:
On 04/04/2026 19:23, olcott wrote:
On 4/4/2026 2:53 AM, Mikko wrote:
On 03/04/2026 16:35, olcott wrote:
On 4/3/2026 2:13 AM, Mikko wrote:
On 02/04/2026 23:58, olcott wrote:
To be able to properly ground this in existing foundational >>>>>>>>>>>>>> peer reviewed papers will take some time.
Do you think 100 years would be enough, or at least some >>>>>>>>>>>>> finite time?
I have to carefully study at least a dozen papers
that may average 15 pages each. The basic notion
of a "well founded justification tree" essentially
means the Proof Theoretic notion of reduction to
a Canonical proof.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above Prolog determines that LP does not
have a "well founded justification tree".
If you want to illustrate with examples you should have two >>>>>>>>>>> examples:
one with a negative result (as above) and one with a positive >>>>>>>>>>> one.
So the above example should be paired with one that has someting >>>>>>>>>>> else in place of not(provable(F, G)) so that the result will >>>>>>>>>>> not be
false.
THIS IS NOT A PROLOG SPECIFIC THING
That's mainly true. However, in como.lang.prolog the discussion >>>>>>>>> should
be restricted to Prolog specific things, in this case to the >>>>>>>>> Prolog
example above and the contrasting Prolog example not yet shown. >>>>>>>>>
In order to elaborate the details of my system
I require some way to formalize natural language.
Montague Grammar, Rudolf Carnap Meaning Postulates,
the CycL language of the Cyc project and Prolog
are the options that I have been considering.
The notion of how a well-founded justification tree
eliminates undecidability is a key element of my system.
Prolog shows this best.
It is not Prolog computable to determine whether a sentence of Peano >>>>>>> arithmetic has a well-founded justification tree in Peano
arithmetic.
A formal language similar to Prolog that can represent
all of the semantics of PA can be developed so that
it detects and rejects expressions that lack well-founded
justification trees.
A language does not detect. For detection you need an algorithm.
unify_with_occurs_check(LP, not(true(LP))).
is a function of the Prolog language that
implements the algorithm.
No, it is not. The question whether a sentence has a well-founded
justification tree is a question about one thing so it needs an
algrotim that takes only one input but uunify_with_occurs_check
takes two.
The number of inputs does not matter.
If BY ANY MEANS a cycle is detected in the
directed graph of the evaluation sequence of
the expression then the expression is rejected.
True(L, X) := ∃Γ ⊆ BaseFacts(L) (Γ ⊢ X) // copyright Olcott 2018
If for any reason a back chained inference does
not reach BaseFacts(L) then the expression is untrue.
CORRECTION:
...then the expression is untrue [within the body
of knowledge that can be expressed in language].
On 08/04/2026 14:52, olcott wrote:
On 4/8/2026 2:08 AM, Mikko wrote:
On 07/04/2026 17:49, olcott wrote:
On 4/7/2026 3:00 AM, Mikko wrote:
On 06/04/2026 14:21, olcott wrote:
On 4/6/2026 3:27 AM, Mikko wrote:
On 05/04/2026 14:25, olcott wrote:
On 4/5/2026 2:05 AM, Mikko wrote:
On 04/04/2026 19:23, olcott wrote:
On 4/4/2026 2:53 AM, Mikko wrote:
On 03/04/2026 16:35, olcott wrote:
On 4/3/2026 2:13 AM, Mikko wrote:
On 02/04/2026 23:58, olcott wrote:
To be able to properly ground this in existing foundational >>>>>>>>>>>>>> peer reviewed papers will take some time.
Do you think 100 years would be enough, or at least some >>>>>>>>>>>>> finite time?
I have to carefully study at least a dozen papers
that may average 15 pages each. The basic notion
of a "well founded justification tree" essentially
means the Proof Theoretic notion of reduction to
a Canonical proof.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above Prolog determines that LP does not
have a "well founded justification tree".
If you want to illustrate with examples you should have two >>>>>>>>>>> examples:
one with a negative result (as above) and one with a positive >>>>>>>>>>> one.
So the above example should be paired with one that has someting >>>>>>>>>>> else in place of not(provable(F, G)) so that the result will >>>>>>>>>>> not be
false.
THIS IS NOT A PROLOG SPECIFIC THING
That's mainly true. However, in como.lang.prolog the discussion >>>>>>>>> should
be restricted to Prolog specific things, in this case to the >>>>>>>>> Prolog
example above and the contrasting Prolog example not yet shown. >>>>>>>>>
In order to elaborate the details of my system
I require some way to formalize natural language.
Montague Grammar, Rudolf Carnap Meaning Postulates,
the CycL language of the Cyc project and Prolog
are the options that I have been considering.
The notion of how a well-founded justification tree
eliminates undecidability is a key element of my system.
Prolog shows this best.
It is not Prolog computable to determine whether a sentence of Peano >>>>>>> arithmetic has a well-founded justification tree in Peano
arithmetic.
A formal language similar to Prolog that can represent
all of the semantics of PA can be developed so that
it detects and rejects expressions that lack well-founded
justification trees.
A language does not detect. For detection you need an algorithm.
unify_with_occurs_check(LP, not(true(LP))).
is a function of the Prolog language that
implements the algorithm.
No, it is not. The question whether a sentence has a well-founded
justification tree is a question about one thing so it needs an
algrotim that takes only one input but uunify_with_occurs_check
takes two.
The number of inputs does not matter.
It certainly does. You can't use unify_with_occurs_check to determine
whether ∀x ∀y (x + y = y + x) has a well-founded justification tree.
On 08/04/2026 17:13, olcott wrote:
On 4/8/2026 6:52 AM, olcott wrote:
On 4/8/2026 2:08 AM, Mikko wrote:
On 07/04/2026 17:49, olcott wrote:
On 4/7/2026 3:00 AM, Mikko wrote:
On 06/04/2026 14:21, olcott wrote:
On 4/6/2026 3:27 AM, Mikko wrote:
On 05/04/2026 14:25, olcott wrote:
On 4/5/2026 2:05 AM, Mikko wrote:
On 04/04/2026 19:23, olcott wrote:
On 4/4/2026 2:53 AM, Mikko wrote:
On 03/04/2026 16:35, olcott wrote:
On 4/3/2026 2:13 AM, Mikko wrote:
On 02/04/2026 23:58, olcott wrote:
To be able to properly ground this in existing foundational >>>>>>>>>>>>>>> peer reviewed papers will take some time.
Do you think 100 years would be enough, or at least some >>>>>>>>>>>>>> finite time?
I have to carefully study at least a dozen papers
that may average 15 pages each. The basic notion
of a "well founded justification tree" essentially
means the Proof Theoretic notion of reduction to
a Canonical proof.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above Prolog determines that LP does not
have a "well founded justification tree".
If you want to illustrate with examples you should have two >>>>>>>>>>>> examples:
one with a negative result (as above) and one with a
positive one.
So the above example should be paired with one that has >>>>>>>>>>>> someting
else in place of not(provable(F, G)) so that the result will >>>>>>>>>>>> not be
false.
THIS IS NOT A PROLOG SPECIFIC THING
That's mainly true. However, in como.lang.prolog the
discussion should
be restricted to Prolog specific things, in this case to the >>>>>>>>>> Prolog
example above and the contrasting Prolog example not yet shown. >>>>>>>>>>
In order to elaborate the details of my system
I require some way to formalize natural language.
Montague Grammar, Rudolf Carnap Meaning Postulates,
the CycL language of the Cyc project and Prolog
are the options that I have been considering.
The notion of how a well-founded justification tree
eliminates undecidability is a key element of my system.
Prolog shows this best.
It is not Prolog computable to determine whether a sentence of >>>>>>>> Peano
arithmetic has a well-founded justification tree in Peano
arithmetic.
A formal language similar to Prolog that can represent
all of the semantics of PA can be developed so that
it detects and rejects expressions that lack well-founded
justification trees.
A language does not detect. For detection you need an algorithm.
unify_with_occurs_check(LP, not(true(LP))).
is a function of the Prolog language that
implements the algorithm.
No, it is not. The question whether a sentence has a well-founded
justification tree is a question about one thing so it needs an
algrotim that takes only one input but uunify_with_occurs_check
takes two.
The number of inputs does not matter.
If BY ANY MEANS a cycle is detected in the
directed graph of the evaluation sequence of
the expression then the expression is rejected.
True(L, X) := ∃Γ ⊆ BaseFacts(L) (Γ ⊢ X) // copyright Olcott 2018 >>> If for any reason a back chained inference does
not reach BaseFacts(L) then the expression is untrue.
CORRECTION:
...then the expression is untrue [within the body
of knowledge that can be expressed in language].
That is not useful unless there are methods to determine whether
∃Γ ⊆ BaseFacts(L) (Γ ⊢ X) for every X in some L.
You can't use nify_with_occurs_check/2 to deremine whether True(X, L).
On 4/9/2026 4:17 AM, Mikko wrote:
On 08/04/2026 17:13, olcott wrote:
On 4/8/2026 6:52 AM, olcott wrote:
On 4/8/2026 2:08 AM, Mikko wrote:
On 07/04/2026 17:49, olcott wrote:
On 4/7/2026 3:00 AM, Mikko wrote:
On 06/04/2026 14:21, olcott wrote:
On 4/6/2026 3:27 AM, Mikko wrote:
On 05/04/2026 14:25, olcott wrote:
On 4/5/2026 2:05 AM, Mikko wrote:
On 04/04/2026 19:23, olcott wrote:
On 4/4/2026 2:53 AM, Mikko wrote:
On 03/04/2026 16:35, olcott wrote:
On 4/3/2026 2:13 AM, Mikko wrote:
On 02/04/2026 23:58, olcott wrote:
To be able to properly ground this in existing foundational >>>>>>>>>>>>>>>> peer reviewed papers will take some time.
Do you think 100 years would be enough, or at least some >>>>>>>>>>>>>>> finite time?
I have to carefully study at least a dozen papers
that may average 15 pages each. The basic notion
of a "well founded justification tree" essentially >>>>>>>>>>>>>> means the Proof Theoretic notion of reduction to
a Canonical proof.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above Prolog determines that LP does not
have a "well founded justification tree".
If you want to illustrate with examples you should have two >>>>>>>>>>>>> examples:
one with a negative result (as above) and one with a >>>>>>>>>>>>> positive one.
So the above example should be paired with one that has >>>>>>>>>>>>> someting
else in place of not(provable(F, G)) so that the result >>>>>>>>>>>>> will not be
false.
THIS IS NOT A PROLOG SPECIFIC THING
That's mainly true. However, in como.lang.prolog the
discussion should
be restricted to Prolog specific things, in this case to the >>>>>>>>>>> Prolog
example above and the contrasting Prolog example not yet shown. >>>>>>>>>>>
In order to elaborate the details of my system
I require some way to formalize natural language.
Montague Grammar, Rudolf Carnap Meaning Postulates,
the CycL language of the Cyc project and Prolog
are the options that I have been considering.
The notion of how a well-founded justification tree
eliminates undecidability is a key element of my system.
Prolog shows this best.
It is not Prolog computable to determine whether a sentence of >>>>>>>>> Peano
arithmetic has a well-founded justification tree in Peano
arithmetic.
A formal language similar to Prolog that can represent
all of the semantics of PA can be developed so that
it detects and rejects expressions that lack well-founded
justification trees.
A language does not detect. For detection you need an algorithm.
unify_with_occurs_check(LP, not(true(LP))).
is a function of the Prolog language that
implements the algorithm.
No, it is not. The question whether a sentence has a well-founded
justification tree is a question about one thing so it needs an
algrotim that takes only one input but uunify_with_occurs_check
takes two.
The number of inputs does not matter.
If BY ANY MEANS a cycle is detected in the
directed graph of the evaluation sequence of
the expression then the expression is rejected.
True(L, X) := ∃Γ ⊆ BaseFacts(L) (Γ ⊢ X) // copyright Olcott 2018 >>>> If for any reason a back chained inference does
not reach BaseFacts(L) then the expression is untrue.
CORRECTION:
...then the expression is untrue [within the body
of knowledge that can be expressed in language].
That is not useful unless there are methods to determine whether
∃Γ ⊆ BaseFacts(L) (Γ ⊢ X) for every X in some L.
You can't use nify_with_occurs_check/2 to deremine whether True(X, L).
If there is a finite back-chained inference path from X
to Γ then X is true.
On 4/9/2026 4:08 AM, Mikko wrote:Irrelevant as no connection of the diagram to anything discussed
On 08/04/2026 14:52, olcott wrote:
On 4/8/2026 2:08 AM, Mikko wrote:
On 07/04/2026 17:49, olcott wrote:
On 4/7/2026 3:00 AM, Mikko wrote:
On 06/04/2026 14:21, olcott wrote:
On 4/6/2026 3:27 AM, Mikko wrote:
On 05/04/2026 14:25, olcott wrote:
On 4/5/2026 2:05 AM, Mikko wrote:
On 04/04/2026 19:23, olcott wrote:
On 4/4/2026 2:53 AM, Mikko wrote:
On 03/04/2026 16:35, olcott wrote:
On 4/3/2026 2:13 AM, Mikko wrote:
On 02/04/2026 23:58, olcott wrote:
To be able to properly ground this in existing foundational >>>>>>>>>>>>>>> peer reviewed papers will take some time.
Do you think 100 years would be enough, or at least some >>>>>>>>>>>>>> finite time?
I have to carefully study at least a dozen papers
that may average 15 pages each. The basic notion
of a "well founded justification tree" essentially
means the Proof Theoretic notion of reduction to
a Canonical proof.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above Prolog determines that LP does not
have a "well founded justification tree".
If you want to illustrate with examples you should have two >>>>>>>>>>>> examples:
one with a negative result (as above) and one with a
positive one.
So the above example should be paired with one that has >>>>>>>>>>>> someting
else in place of not(provable(F, G)) so that the result will >>>>>>>>>>>> not be
false.
THIS IS NOT A PROLOG SPECIFIC THING
That's mainly true. However, in como.lang.prolog the
discussion should
be restricted to Prolog specific things, in this case to the >>>>>>>>>> Prolog
example above and the contrasting Prolog example not yet shown. >>>>>>>>>>
In order to elaborate the details of my system
I require some way to formalize natural language.
Montague Grammar, Rudolf Carnap Meaning Postulates,
the CycL language of the Cyc project and Prolog
are the options that I have been considering.
The notion of how a well-founded justification tree
eliminates undecidability is a key element of my system.
Prolog shows this best.
It is not Prolog computable to determine whether a sentence of >>>>>>>> Peano
arithmetic has a well-founded justification tree in Peano
arithmetic.
A formal language similar to Prolog that can represent
all of the semantics of PA can be developed so that
it detects and rejects expressions that lack well-founded
justification trees.
A language does not detect. For detection you need an algorithm.
unify_with_occurs_check(LP, not(true(LP))).
is a function of the Prolog language that
implements the algorithm.
No, it is not. The question whether a sentence has a well-founded
justification tree is a question about one thing so it needs an
algrotim that takes only one input but uunify_with_occurs_check
takes two.
The number of inputs does not matter.
It certainly does. You can't use unify_with_occurs_check to determine
whether ∀x ∀y (x + y = y + x) has a well-founded justification tree.
[00] ∀x
│
└─────> [01] ∀y
│
└─────> [02] Equals
│
├─────> [03] add (Left)
│ │
│ ├─────> [05] x <┐
│ │ │
│ └─────> [06] y <┼─┐
│ │ │ (Shared Pointers)
└─────> [04] add (Right) │ │
│ │ │
├──────> [06] y ─┘ │
│ │
└──────> [05] x ───┘
| Sysop: | DaiTengu |
|---|---|
| Location: | Appleton, WI |
| Users: | 1,114 |
| Nodes: | 10 (0 / 10) |
| Uptime: | 492510:14:55 |
| Calls: | 14,267 |
| Calls today: | 3 |
| Files: | 186,320 |
| D/L today: |
22,438 files (7,304M bytes) |
| Messages: | 2,518,347 |