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 <polcott333@gmail.com> wrote:
On 6/22/2026 1:42 PM, Alan Mackenzie wrote:
In comp.theory olcott <polcott333@gmail.com> 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.
I was right, you didn't understand it.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. >>>>>>>>>>>
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.
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 <polcott333@gmail.com> wrote:
On 6/22/2026 1:42 PM, Alan Mackenzie wrote:
In comp.theory olcott <polcott333@gmail.com> 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.
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 <polcott333@gmail.com> wrote:
On 6/22/2026 1:42 PM, Alan Mackenzie wrote:
In comp.theory olcott <polcott333@gmail.com> 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.
On 25/06/2026 00:33, olcott wrote:
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 <polcott333@gmail.com> wrote: >>>>>>>>>>>>>> On 6/22/2026 1:42 PM, Alan Mackenzie wrote:
In comp.theory olcott <polcott333@gmail.com> 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.
Irrelevant. Nobody claimed there be Prolog errors in your queries.
Implying that I am wrong about Prolog without
pointing out any actual mistake is also DISHONEST.
How did Ross FInlayson imply that you were wrong about Prolog?
On 6/25/2026 2:29 AM, Mikko wrote:
On 25/06/2026 00:33, olcott wrote:
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 <polcott333@gmail.com> wrote: >>>>>>>>>>>>>>> On 6/22/2026 1:42 PM, Alan Mackenzie wrote:
In comp.theory olcott <polcott333@gmail.com> 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.
Irrelevant. Nobody claimed there be Prolog errors in your queries.
Implying that I am wrong about Prolog without
pointing out any actual mistake is also DISHONEST.
How did Ross FInlayson imply that you were wrong about Prolog?
If an error is claimed then it must be specifically
pointed out otherwise the clam of error is dishonest.
On 25/06/2026 19:16, olcott wrote:
On 6/25/2026 2:29 AM, Mikko wrote:
On 25/06/2026 00:33, olcott wrote:
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 <polcott333@gmail.com> wrote: >>>>>>>>>>>>>>>> On 6/22/2026 1:42 PM, Alan Mackenzie wrote:
In comp.theory olcott <polcott333@gmail.com> 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.
Irrelevant. Nobody claimed there be Prolog errors in your queries.
Implying that I am wrong about Prolog without
pointing out any actual mistake is also DISHONEST.
How did Ross FInlayson imply that you were wrong about Prolog?
If an error is claimed then it must be specifically
pointed out otherwise the clam of error is dishonest.
Yet you claim that Ross Finlayson be dishonest without pointing
out what is dishonest in his words.
| Sysop: | DaiTengu |
|---|---|
| Location: | Appleton, WI |
| Users: | 1,124 |
| Nodes: | 10 (0 / 10) |
| Uptime: | 23:55:49 |
| Calls: | 14,394 |
| Calls today: | 3 |
| Files: | 186,389 |
| D/L today: |
5,747 files (1,443M bytes) |
| Messages: | 2,544,985 |
| Posted today: | 1 |