On 4/5/2026 2:05 AM, Mikko wrote:It is not Prolog computable to determine whether a sentence of PeanoOn 04/04/2026 19:23, olcott wrote:In order to elaborate the details of my systemOn 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.
>
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.
arithmetic has a well-founded justification tree in Peano arithmetic.
--
Mikko
Les messages affichés proviennent d'usenet.