On 13/04/2026 17:52, olcott wrote:You keep arguing on the basis of ignorance of proofOn 4/13/2026 2:05 AM, Mikko wrote:An ad-hominem with an unproven premise disqualifies your comment.On 12/04/2026 16:22, olcott wrote:>On 4/12/2026 4:32 AM, Mikko wrote:>On 11/04/2026 17:27, olcott wrote:>On 4/11/2026 3:06 AM, Mikko wrote:>On 09/04/2026 16:35, olcott wrote:>On 4/9/2026 4:08 AM, Mikko wrote:>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 ───┘
There are no cycles in this tree
Can we interprete this to mean that you admit that the predicate
unify_with_occurs_check is not useful for determination whether
∀x ∀y (x + y = y + x) has a well-founded justification tree ?
My example was to merely prove that the Liar Paradox
has never been anything besides incoherent nonsense.
I showed this in an existing well understood logic
programming language.
I.e., yes, we can interprete your diagram to mean that you admit that
the predicate unify_with_occurs_check is not useful for determination
whether ∀x ∀y (x + y = y + x) has a well-founded justification tree.
Consequently, you agree that your claims to the contrary were false.
>
I started with the most salient case within
the most well-known language that can prove
my point. T^he above case if my own Minimal Type
Theory.
>
Olcott's Minimal Type Theory
G ↔ ¬Prov[PA](⌜G⌝)
Directed Graph of evaluation sequence
>
00 ↔ 01 02
01 G
02 ¬ 03
03 Prov[PA] 04
04 Gödel_Number_of 01 // cycle
Nice to see that you don't disagree.
When you understand proof theoretic semantics well
enough then you understand that within the coherent
foundation of PTS Gödel 1931 Incompleteness becomes
an instance of incoherent semantics.
Though an ad-hominem would disqualify it even if the premise were
proven.
theoretic semantics, like a kindergarten kid that
says I just don't believe in algebra.
Olcott's Minimal Type Theory
G ↔ ¬Prov[PA](⌜G⌝)
Directed Graph of evaluation sequence
00 ↔ 01 02
01 G
02 ¬ 03
03 Prov[PA] 04
04 Gödel_Number_of 01 // cycle
Ordinary unadulterated proof theoretic semantics
already has the complete and perfect foundational
basis to reject these inputs as semantically incoherent.
1.2 Inferentialism, intuitionism, anti-realism
Proof-theoretic semantics is inherently inferential,
as it is inferential activity which manifests itself
in proofs. It thus belongs to inferentialism (a term
coined by Brandom, see his 1994; 2000) according to
which inferences and the rules of inference establish
the meaning of expressions Schroeder-Heister, Peter,
2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/#InfeIntuAntiReal
--
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.
This required establishing a new foundation
Les messages affichés proviennent d'usenet.