Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs

On 6/24/2026 5:13 AM, Mikko wrote:
> On 23/06/2026 21:20, olcott wrote:
>> On 6/23/2026 12:32 PM, Ross Finlayson wrote:
>>> On 06/23/2026 09:54 AM, olcott wrote:
>>>> On 6/23/2026 10:51 AM, Ross Finlayson wrote:
>>>>> On 06/23/2026 07:22 AM, olcott wrote:
>>>>>> On 6/22/2026 11:31 PM, Ross Finlayson wrote:
>>>>>>> On 06/22/2026 09:14 PM, olcott wrote:
>>>>>>>> On 6/22/2026 11:00 PM, Ross Finlayson wrote:
>>>>>>>>> On 06/22/2026 01:06 PM, olcott wrote:
>>>>>>>>>> On 6/22/2026 2:50 PM, Alan Mackenzie wrote:
>>>>>>>>>>> [ Followup-To: set ]
>>>>>>>>>>>
>>>>>>>>>>> In comp.theory olcott <[email protected]> wrote:
>>>>>>>>>>>> On 6/22/2026 1:42 PM, Alan Mackenzie wrote:
>>>>>>>>>>>>> In comp.theory olcott <[email protected]> wrote:
>>>>>>>>>>>>>> On 6/22/2026 10:48 AM, Alan Mackenzie wrote:
>>>>>>>>>>>
>>>>>>>>>>>>>>> G is true.
>>>>>>>>>>>
>>>>>>>>>>>>>>> I put it to you you're lying again.  No reputable 
>>>>>>>>>>>>>>> mathematician
>>>>>>>>>>>>>>> would
>>>>>>>>>>>>>>> risk his reputation by saying false things.  If Dag Prawitz
>>>>>>>>>>>>>>> really
>>>>>>>>>>>>>>> did
>>>>>>>>>>>>>>> "agree" (with whom?) that Gödel's sentence G is not true in
>>>>>>>>>>>>>>> Peano
>>>>>>>>>>>>>>> Arithmetic, then produce a citation for this.
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>>>> He never gets to Gödel. He essentially says unprovable
>>>>>>>>>>>>>> means untrue all the time for everything within his
>>>>>>>>>>>>>> own Theory of Grounds of strict Proof Theoretic Semantics.
>>>>>>>>>>>
>>>>>>>>>>>>> You won't understand it, but that _is_ essentially Gödel's
>>>>>>>>>>>>> Incompleteness
>>>>>>>>>>>>> Theorem.  It is a statement that any sufficiently powerful
>>>>>>>>>>>>> system can
>>>>>>>>>>>>> express true things it can't prove.  So Dag Prawitz, had he 
>>>>>>>>>>>>> been
>>>>>>>>>>>>> saying
>>>>>>>>>>>>> the things you falsely attributed to him, would certainly have
>>>>>>>>>>>>> "got" to
>>>>>>>>>>>>> Gödel, and would have understood full well what he was saying.
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>>> You did not pay close enough attention to my exact words.
>>>>>>>>>>>
>>>>>>>>>>> I was right, you didn't understand it.
>>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue
>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue
>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue
>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue
>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue
>>>>>>>>>>
>>>>>>>>>
>>>>>>>>> Yeah, I'm pretty sure that "Dag Prawitz says what Dag Prawitz 
>>>>>>>>> says",
>>>>>>>>> and furthermore "Dag Prawitz doesn't say what Dag Prawitz doesn't
>>>>>>>>> say",
>>>>>>>>> then looking a bit into his tremendous volume of works,
>>>>>>>>> he talks about "natural deduction" then specifically an "inverse
>>>>>>>>> principle" so I think these are key aspects of fundamental logic.
>>>>>>>>>
>>>>>>>>> https://www.researchgate.net/
>>>>>>>>> publication/233365263_On_Inversion_Principles
>>>>>>>>>
>>>>>>>>>
>>>>>>>>> "On Inversion Principles
>>>>>>>>>
>>>>>>>>> Enrico Moriconi∗Laura Tesconi†
>>>>>>>>> May 8, 2007
>>>>>>>>>
>>>>>>>>> Abstract
>>>>>>>>> The idea of an “inversion principle”, and the name itself,
>>>>>>>>> originated in
>>>>>>>>> the work of Paul Lorenzen in the 1950s, as a method to generate
>>>>>>>>> new ad-
>>>>>>>>> missible rules within a certain syntactic context. Some fifteen 
>>>>>>>>> years
>>>>>>>>> later, the idea was taken up by Dag Prawitz to devise a 
>>>>>>>>> strategy of
>>>>>>>>> normalization for natural deduction calculi (this being an
>>>>>>>>> analogue of
>>>>>>>>> Gentzen’s cut-elimination theorem for sequent calculi). Later,
>>>>>>>>> Prawitz
>>>>>>>>> used the inversion principle again, attributing it with a semantic
>>>>>>>>> role.
>>>>>>>>> Still working in natural deduction calculi, he formulated a 
>>>>>>>>> general
>>>>>>>>> type
>>>>>>>>> of schematic Introduction rules to be matched—thanks to the idea
>>>>>>>>> supporting the inversion principle — by a corresponding general
>>>>>>>>> schematic Elimination rule. This was an attempt to provide a
>>>>>>>>> solution to
>>>>>>>>> the problem suggested by the often quoted note of Gentzen.
>>>>>>>>> According to
>>>>>>>>> Gentzen “it should be possible to display the elimination rules as
>>>>>>>>> unique functions of the corresponding introduction rules on the
>>>>>>>>> basis of
>>>>>>>>> certain requirements.” Many people have since worked on this 
>>>>>>>>> topic,
>>>>>>>>> which can be appropriately seen as the birthplace of what are now
>>>>>>>>> referred to as “general elimination rules”, recently studied
>>>>>>>>> thoroughly
>>>>>>>>> by Sara Negri and Jan von Plato. In this paper, we retrace the 
>>>>>>>>> main
>>>>>>>>> threads of this chapter of proof-theoretical investigation, using
>>>>>>>>> Lorenzen’s original framework as a general guide"
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>> Hm, "general elimination rules", seem derivable from De Morgan's
>>>>>>>>> laws,
>>>>>>>>> and that being the usual account of naive deductive analysis, then
>>>>>>>>> since
>>>>>>>>> "natural deduction", which here is held as part of the theory
>>>>>>>>> since it's naturally logical, then has for Gentzen that besides
>>>>>>>>> Kripke
>>>>>>>>> afterward there's also Sheffer and Chwistek before, and instead of
>>>>>>>>> Montague for semantics there's Herbrand for semantics, so, what 
>>>>>>>>> to do
>>>>>>>>> about "inversion principle" is here that the thea-theory has that
>>>>>>>>> it's
>>>>>>>>> what subsumes "non-contradiction principle", here hoping that the
>>>>>>>>> interpretation aligns and thusly that "principle of inversion"
>>>>>>>>> wouldn't
>>>>>>>>> need dis-ambiguation from "inversion principle".
>>>>>>>>>
>>>>>>>>>
>>>>>>>>> https://www.tandfonline.com/doi/abs/10.1080/01445340701830334
>>>>>>>>>
>>>>>>>>>
>>>>>>>>> https://www.strandbooks.com/natural-deduction-a-proof-theoretical-
>>>>>>>>> study-9780486446554.html
>>>>>>>>>
>>>>>>>>> "... [Prawitz'] inversion principle constitutes the foundation of
>>>>>>>>> most
>>>>>>>>> modern accounts of proof-theoretic semantics."
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>> I already have a principle of inversion and furthermore a
>>>>>>>>> principle of
>>>>>>>>> thorough reason as subsuming principles of non-contradiction 
>>>>>>>>> and what
>>>>>>>>> suffices, so, I'll be curious then about what to make of Prawitz'
>>>>>>>>> "inversion principle" since Lorenzen.
>>>>>>>>>
>>>>>>>>>
>>>>>>>>> Of course the concept of an "inversion principle" is as old as the
>>>>>>>>> oldest account of Western philosophy like Heraclitus with dual
>>>>>>>>> monism.
>>>>>>>>> In fact by definition it's about the most basic aspect of
>>>>>>>>> contemplation
>>>>>>>>> and deliberation in abstraction of looking at both sides of issues
>>>>>>>>> and
>>>>>>>>> resolving inductive impasses with analytical bridges after
>>>>>>>>> complementary
>>>>>>>>> duals.
>>>>>>>>>
>>>>>>>>>
>>>>>>>>> https://arxiv.org/abs/2112.14967
>>>>>>>>>
>>>>>>>>> "Prawitz formulated the so-called inversion principle as one of 
>>>>>>>>> the
>>>>>>>>> characteristic features of Gentzen's intuitionistic natural
>>>>>>>>> deduction.
>>>>>>>>> In the literature on proof-theoretic semantics, this principle is
>>>>>>>>> often
>>>>>>>>> coupled with another that is called the recovery principle. By
>>>>>>>>> adopting
>>>>>>>>> the Computational Ludics framework, we reformulate these 
>>>>>>>>> principles
>>>>>>>>> into
>>>>>>>>> one and the same condition, which we call the harmony 
>>>>>>>>> condition. We
>>>>>>>>> show
>>>>>>>>> that this reformulation allows us to reveal two intuitive ideas
>>>>>>>>> standing
>>>>>>>>> behind these principles: the idea of "containment" present in the
>>>>>>>>> inversion principle, and the idea that the recovery principle 
>>>>>>>>> is the
>>>>>>>>> "converse" of the inversion principle. We also formulate two other
>>>>>>>>> conditions in the Computational Ludics framework, and we show that
>>>>>>>>> each
>>>>>>>>> of them is equivalent to the harmony condition."
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>> The "ludicus" is Latin and for accounts of wisdom and knowledge.
>>>>>>>>>
>>>>>>>>>
>>>>>>>>> "In particular, by taking inspiration from the
>>>>>>>>> Brouwer-Heyting-Kolmogorov explanation of logical connectives,
>>>>>>>>> proof-theoretic semantics rests on the idea that we know the
>>>>>>>>> meaning of
>>>>>>>>> a compound sentence when we know what counts as a canonical 
>>>>>>>>> proof of
>>>>>>>>> it.
>>>>>>>>> And if proofs are formalised within the framework of natural
>>>>>>>>> deduction,
>>>>>>>>> then a canonical proof of a sentence A is nothing but a closed
>>>>>>>>> derivation ending with an introduction rule of the main connective
>>>>>>>>> of A."
>>>>>>>>>
>>>>>>>>>
>>>>>>>>> The "canonical proofs" are not unique, in any system strong enough
>>>>>>>>> to make for infinitary reasoning and super-classical results
>>>>>>>>> requiring
>>>>>>>>> analytical bridges about infinity and continuity.
>>>>>>>>>
>>>>>>>>
>>>>>>>> It is the role that "canonical proofs" play in
>>>>>>>> Truth as an Epistemic Notion
>>>>>>>> https://link.springer.com/article/10.1007/s11245-011-9107-6
>>>>>>>> That is the most important gist of his whole work.
>>>>>>>>
>>>>>>>> He later goes on to develop and further elaborate his
>>>>>>>> Theory of Grounds.
>>>>>>>>
>>>>>>>> Atomic Systems in Proof-Theoretic Semantics: Two Approaches
>>>>>>>> Thomas Piecha & Peter Schroeder-Heister do this same sort of
>>>>>>>> thing two different ways.
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>
>>>>>>> Furthermore I say there are "canonical proofs" of inductive sorts 
>>>>>>> that
>>>>>>> make contradictions and thusly destroy each other.
>>>>>>>
>>>>>>>
>>>>>>
>>>>>> Clearly you have no idea what Dag Prawitz means by "canonical 
>>>>>> proofs".
>>>>>> Go find out and then get back to me.
>>>>>>
>>>>>>> This is where "the thorough" and "analytical bridges" make repairs
>>>>>>> of what otherwise is flawed, or for hard constructivist realist
>>>>>>> structuralist model theorists: not-theories (examples of wrong).
>>>>>>>
>>>>>>>
>>>>>>
>>>>>>
>>>>>
>>>>>
>>>>> Induction and counter-induction contradict each other, it's simple,
>>>>> it's the grounds for most things called "paradox".
>>>>>
>>>>>
>>>>
>>>> % This sentence is not true.
>>>> ?- LP = not(true(LP)).
>>>> LP = not(true(LP)).
>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>> false.
>>>>
>>>> After you totally understand how and why the proof
>>>> theoretic semantics of that is correct and resolves
>>>> the Liar Paradox get back to me.
>>>>
>>>> The essential principle involved that I derived
>>>> in my own Minimal Type Theory before I knew that
>>>> Prolog could do the same thing is that:
>>>>
>>>> When the directed graph of the evaluation
>>>> sequence of an expression contains a cycle
>>>> then the input is determined to be incoherent
>>>> on the basis that its proof would never terminate.
>>>> Proof Theoretic Semantics does this exact same thing.
>>>>
>>>> Don't get back to me until you attain the required
>>>> prerequisites. I am sure that you already know
>>>> all about cycles in directed graphs.
>>>>
>>>
>>> Declaring oneself ignorant thus wise
>>> doesn't make much of a case
>>> except being ignorant.
>>>
>>> 300 mile per hour wheelchair: can't take stairs.
>>>
>>> Except down, ....
>>>
>>>
>>
>> So you are going to imply that I am incorrect
>> about Prolog when you yourself remain clueless about Prolog?
>> That would be dishonest.
> 
> No, pointing out that you are worng about Prolog when you are wrong
> about Prolog is never dishohest.
> 

That is correct Prolog and that is the
result of the correct run of correct Prolog.
Implying that I am wrong about Prolog without
pointing out any actual mistake is also DISHONEST.

-- 
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).