Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > sci.physics.relativity > #667125 > unrolled thread

Re: Arrow Functions can do Existential Quantifier (Re: 😂 "Plog-like" - that should be the official term!)

Back to article view | Back to sci.physics.relativity

This discussion starts older than the indexed window; earlier articles aren't shown. The article labeled Started by below is the oldest one visible, not the original post.

Contents

  Re: Arrow Functions can do Existential Quantifier (Re: 😂 "Plog-like" - that should be the official term!) Franz Sneijders <ee@ard.nl> - 2025-11-06 17:44 +0000
    Clueless Moron and Paid Putin Troll (Was: Arrow Functions can do Existential Quantifier) Mild Shock <janburse@fastmail.fm> - 2025-11-06 22:28 +0100
      2.1 Logical variables and equations (Re: Clueless Moron and Paid Putin Troll (Was: Arrow Functions can do Existential Quantifier) Mild Shock <janburse@fastmail.fm> - 2025-11-06 22:35 +0100
        Re: 2.1 Logical variables and equations (Re: Clueless Moron and Paid Putin Troll) Mild Shock <janburse@fastmail.fm> - 2025-11-06 22:42 +0100
          Re: 2.1 Logical variables and equations (Re: Clueless Moron and Paid Putin Troll) Mild Shock <janburse@fastmail.fm> - 2025-11-06 22:48 +0100
      Re: Clueless Moron and Paid Putin Troll (Was: Arrow Functions can do Existential Quantifier) Mariano Amelsvoort <aa@viollr.nl> - 2025-11-06 22:15 +0000
        Re: Clueless Moron and Paid Putin Troll (Was: Arrow Functions can do Existential Quantifier) Mild Shock <janburse@fastmail.fm> - 2025-11-06 23:46 +0100
          What does Type Free mean? (Was: Clueless Moron and Paid Putin Troll) Mild Shock <janburse@fastmail.fm> - 2025-11-06 23:54 +0100
    A noiseless patient Spider is a Pussy Mild Shock <janburse@fastmail.fm> - 2025-11-07 00:03 +0100
      Re: A noiseless patient Spider is a Pussy Jackie Romijnders <jirke@jecjr.nl> - 2025-11-07 00:01 +0000
    2025 Obituary: Skew Confluence (aka “Stews” 😆) (Re: Arrow Functions can do Existential Quantifier) Mild Shock <janburse@fastmail.fm> - 2025-11-07 01:42 +0100
      The quantifer ∃ is just the Combinator K (Schönfinkels C)? (Re: From Feferman to Peyton Jones, no luck with ∃) Mild Shock <janburse@fastmail.fm> - 2025-11-08 21:27 +0100
        Re: The quantifer ∃ is just the Combinator K (Schönfinkels C)? (Re: From Feferman to Peyton Jones, no luck with ∃) Ross Finlayson <ross.a.finlayson@gmail.com> - 2025-11-08 18:20 -0800
          Horn uses Conditional / Clark uses Biconditional (Was: The quantifer ∃ is just the Combinator K (Schönfinkels C)?) Mild Shock <janburse@fastmail.fm> - 2025-11-09 13:05 +0100
            CET is also needed (Was: Horn uses Conditional / Clark uses Biconditional) Mild Shock <janburse@fastmail.fm> - 2025-11-09 13:08 +0100
              Re: CET is also needed (Was: Horn uses Conditional / Clark uses Biconditional) Ross Finlayson <ross.a.finlayson@gmail.com> - 2025-11-09 08:13 -0800
                You have to check Feferman OST [Paradox Hunting] (Was: CET is also needed) Mild Shock <janburse@fastmail.fm> - 2025-11-09 19:57 +0100
                  Prolog semantics is 3-valued or intuitionistic [Feferman prefers partial logic] (Was: You have to check Feferman OST [Paradox Hunting]) Mild Shock <janburse@fastmail.fm> - 2025-11-09 20:11 +0100
                    In Prolog you don't need the down arrow t↓ (Was: Prolog semantics is 3-valued or intuitionistic) Mild Shock <janburse@fastmail.fm> - 2025-11-09 20:16 +0100

#667125 — Re: Arrow Functions can do Existential Quantifier (Re: 😂 "Plog-like" - that should be the official term!)

Mild Shock wrote:

> We use “∃” to bring a fresh logical variable into scope, because we
> really mean “there exists an x such that ···.”

idiot, there is no any x over there. And it doesn't need to be a variable, 
a constant suffices.

[toc] | [next] | [standalone]

#667134 — Clueless Moron and Paid Putin Troll (Was: Arrow Functions can do Existential Quantifier)

Hi,

Its from this paper:

The Verse Calculus:a Core Calculus for Functional Logic Programming
SIMON PEYTON JONES, Epic Games, United Kingdom
GUY STEELE, Oracle Labs, USA
https://simon.peytonjones.org/assets/pdfs/verse-March23.pdf

Don't blame me for what they write.
But mostlikely your eruption is just from
a clueless Nazi Retard, namely the paid

troll you are, getting money from Putin.

Bye

Franz Sneijders schrieb:
> Mild Shock wrote:
> 
>> We use “∃” to bring a fresh logical variable into scope, because we
>> really mean “there exists an x such that ···.”
> 
> idiot, there is no any x over there. And it doesn't need to be a variable,
> a constant suffices.
> 

[toc] | [prev] | [next] | [standalone]

#667135 — 2.1 Logical variables and equations (Re: Clueless Moron and Paid Putin Troll (Was: Arrow Functions can do Existential Quantifier)

Hi,

Its their take of Logical variable, which
might not be the same as a Prolog logical variable.

------------------ cut here ----------------

2.1 Logical variables and equations
A program executes by solving its equations, using
the process of unification. For example,

∃x y z. x = <y,3>; x= <2,z>; y

is solved by unifying x with <y, 3> and with <2, z>;
that in turn unifies <y, 3> with <2, z>, which unifies
y with 2 and z with 3. Finally, 2 is returned as the
result. Note carefully that, as in any declarative
language, logical variables are not mutable; a logical
variable stands for a single, immutable value.

We use "∃" to bring a fresh logical variable into
scope, because we really mean "there exists an x
such that .... "

------------------ cut here ----------------

Of course the above is utter nonsense, written
from somebody who doesn't know what a Prolog logical
variable is, shifting in the same sentence from

the attribution of "immutable" of a variable, to
the attribution of "immutable" of the value
of a variable. This is quite hillarious.

Bye

Mild Shock schrieb:
> Hi,
> 
> Its from this paper:
> 
> The Verse Calculus:a Core Calculus for Functional Logic Programming
> SIMON PEYTON JONES, Epic Games, United Kingdom
> GUY STEELE, Oracle Labs, USA
> https://simon.peytonjones.org/assets/pdfs/verse-March23.pdf
> 
> Don't blame me for what they write.
> But mostlikely your eruption is just from
> a clueless Nazi Retard, namely the paid
> 
> troll you are, getting money from Putin.
> 
> Bye
> 
> Franz Sneijders schrieb:
>> Mild Shock wrote:
>>
>>> We use “∃” to bring a fresh logical variable into scope, because we
>>> really mean “there exists an x such that ···.”
>>
>> idiot, there is no any x over there. And it doesn't need to be a 
>> variable,
>> a constant suffices.
>>
> 

[toc] | [prev] | [next] | [standalone]

#667136 — Re: 2.1 Logical variables and equations (Re: Clueless Moron and Paid Putin Troll)

Hi,

A Prolog logical variable is not immutable,
it transitions all the time from uninstantiated
to instantiated, during unification.

Also the value the logical variable represents
is not immutable, since it might point to a
Prolog term which is non-ground, this

Prolog term might have other Prolog logical variables,
which do also such transitions, making the
while Prolog term transitioniong from less ground

to more ground, or even worse to a larger
term with even more Prolog logical variables,
and so on, leading to the phaenomenon of

perpetual processes or concurrent logic programming.
In particular the existence quantifier ∃ in logic
programming is not unique existence ∃!. For

example the following is true:

∃x x = f(y)

But x has not a "single value", the existence
is more witness to of a kind of skolem function
dependency, namely that for each y, there

is some f(y). What they write is only useful
for a certained moded form of Prolog and unification,
where the equations have unique existence of

ground terms or some other value domain.

Bye

Mild Shock schrieb:
> Hi,
> 
> Its their take of Logical variable, which
> might not be the same as a Prolog logical variable.
> 
> ------------------ cut here ----------------
> 
> 2.1 Logical variables and equations
> A program executes by solving its equations, using
> the process of unification. For example,
> 
> ∃x y z. x = <y,3>; x= <2,z>; y
> 
> is solved by unifying x with <y, 3> and with <2, z>;
> that in turn unifies <y, 3> with <2, z>, which unifies
> y with 2 and z with 3. Finally, 2 is returned as the
> result. Note carefully that, as in any declarative
> language, logical variables are not mutable; a logical
> variable stands for a single, immutable value.
> 
> We use "∃" to bring a fresh logical variable into
> scope, because we really mean "there exists an x
> such that .... "
> 
> ------------------ cut here ----------------
> 
> Of course the above is utter nonsense, written
> from somebody who doesn't know what a Prolog logical
> variable is, shifting in the same sentence from
> 
> the attribution of "immutable" of a variable, to
> the attribution of "immutable" of the value
> of a variable. This is quite hillarious.
> 
> Bye
> 
> Mild Shock schrieb:
>> Hi,
>>
>> Its from this paper:
>>
>> The Verse Calculus:a Core Calculus for Functional Logic Programming
>> SIMON PEYTON JONES, Epic Games, United Kingdom
>> GUY STEELE, Oracle Labs, USA
>> https://simon.peytonjones.org/assets/pdfs/verse-March23.pdf
>>
>> Don't blame me for what they write.
>> But mostlikely your eruption is just from
>> a clueless Nazi Retard, namely the paid
>>
>> troll you are, getting money from Putin.
>>
>> Bye
>>
>> Franz Sneijders schrieb:
>>> Mild Shock wrote:
>>>
>>>> We use “∃” to bring a fresh logical variable into scope, because we
>>>> really mean “there exists an x such that ···.”
>>>
>>> idiot, there is no any x over there. And it doesn't need to be a 
>>> variable,
>>> a constant suffices.
>>>
>>
> 

[toc] | [prev] | [next] | [standalone]

#667138 — Re: 2.1 Logical variables and equations (Re: Clueless Moron and Paid Putin Troll)

Hi,

We can though prove in FOL:

∀y∃!x x = f(y)

Another example with existence,
that doesn't boil down to unique
existence, is this here:

∃x∃y(x = f(y))

One might find it in Prolog as
X = f(_) with an anonymous variable _.
Now its not possible to derive:

/* Not Generally Valid */
∃!x∃y(x = f(y))

Bye

Mild Shock schrieb:
> Hi,
> 
> A Prolog logical variable is not immutable,
> it transitions all the time from uninstantiated
> to instantiated, during unification.
> 
> Also the value the logical variable represents
> is not immutable, since it might point to a
> Prolog term which is non-ground, this
> 
> Prolog term might have other Prolog logical variables,
> which do also such transitions, making the
> while Prolog term transitioniong from less ground
> 
> to more ground, or even worse to a larger
> term with even more Prolog logical variables,
> and so on, leading to the phaenomenon of
> 
> perpetual processes or concurrent logic programming.
> In particular the existence quantifier ∃ in logic
> programming is not unique existence ∃!. For
> 
> example the following is true:
> 
> ∃x x = f(y)
> 
> But x has not a "single value", the existence
> is more witness to of a kind of skolem function
> dependency, namely that for each y, there
> 
> is some f(y). What they write is only useful
> for a certained moded form of Prolog and unification,
> where the equations have unique existence of
> 
> ground terms or some other value domain.
> 
> Bye
> 
> Mild Shock schrieb:
>> Hi,
>>
>> Its their take of Logical variable, which
>> might not be the same as a Prolog logical variable.
>>
>> ------------------ cut here ----------------
>>
>> 2.1 Logical variables and equations
>> A program executes by solving its equations, using
>> the process of unification. For example,
>>
>> ∃x y z. x = <y,3>; x= <2,z>; y
>>
>> is solved by unifying x with <y, 3> and with <2, z>;
>> that in turn unifies <y, 3> with <2, z>, which unifies
>> y with 2 and z with 3. Finally, 2 is returned as the
>> result. Note carefully that, as in any declarative
>> language, logical variables are not mutable; a logical
>> variable stands for a single, immutable value.
>>
>> We use "∃" to bring a fresh logical variable into
>> scope, because we really mean "there exists an x
>> such that .... "
>>
>> ------------------ cut here ----------------
>>
>> Of course the above is utter nonsense, written
>> from somebody who doesn't know what a Prolog logical
>> variable is, shifting in the same sentence from
>>
>> the attribution of "immutable" of a variable, to
>> the attribution of "immutable" of the value
>> of a variable. This is quite hillarious.
>>
>> Bye
>>
>> Mild Shock schrieb:
>>> Hi,
>>>
>>> Its from this paper:
>>>
>>> The Verse Calculus:a Core Calculus for Functional Logic Programming
>>> SIMON PEYTON JONES, Epic Games, United Kingdom
>>> GUY STEELE, Oracle Labs, USA
>>> https://simon.peytonjones.org/assets/pdfs/verse-March23.pdf
>>>
>>> Don't blame me for what they write.
>>> But mostlikely your eruption is just from
>>> a clueless Nazi Retard, namely the paid
>>>
>>> troll you are, getting money from Putin.
>>>
>>> Bye
>>>
>>> Franz Sneijders schrieb:
>>>> Mild Shock wrote:
>>>>
>>>>> We use “∃” to bring a fresh logical variable into scope, because we
>>>>> really mean “there exists an x such that ···.”
>>>>
>>>> idiot, there is no any x over there. And it doesn't need to be a 
>>>> variable,
>>>> a constant suffices.
>>>>
>>>
>>
> 

[toc] | [prev] | [next] | [standalone]

#667139 — Re: Clueless Moron and Paid Putin Troll (Was: Arrow Functions can do Existential Quantifier)

Mild Shock wrote:

> Don't blame me for what they write.
> But mostlikely your eruption is just from a clueless Nazi Retard, namely
> the paid
> 
> troll you are, getting money from Putin.

here is a one with a constant, admit you don't know what you say and what 
you do

 ∃x ∈N: x×x=36

[toc] | [prev] | [next] | [standalone]

#667141 — Re: Clueless Moron and Paid Putin Troll (Was: Arrow Functions can do Existential Quantifier)

Hi,

Please read the verse paper and the
type free hiord paper, to have have
slightest clue what the context is.

Bye

Mariano Amelsvoort schrieb:
> Mild Shock wrote:
> 
>> Don't blame me for what they write.
>> But mostlikely your eruption is just from a clueless Nazi Retard, namely
>> the paid
>>
>> troll you are, getting money from Putin.
> 
> here is a one with a constant, admit you don't know what you say and what
> you do
> 
>   ∃x ∈N: x×x=36
> 

[toc] | [prev] | [next] | [standalone]

#667142 — What does Type Free mean? (Was: Clueless Moron and Paid Putin Troll)

Hi,

I was crediting these guys for arrow functions:

 > Hiord: A Type-Free Higher-Order Logic Programming
 > Language with Predicate Abstraction
 > Daniel Cabeza, Manuel V. Hermenegildo, Manuel V. Hermenegildo
 > https://www.researchgate.net/publication/221052995

What does Type Free mean? It basically
means no bounded quantifiers like in ∃x ∈N.
No restriction per se to natural numbers or

something. Only universal algebra respectively its
incarnation via Herbrand Domains. Did you
see a bounded quantifer of the form ∃x ∈D where

D is some domain in the verse example? I only
see ∃x without the ∈D. What values where they
talking about? I mean they had numbers 3, 2, and

then they had what? Also pairs via <_,_>.

Bye

P.S.: Need help with what a bounded quantifer is:

https://en.wikipedia.org/wiki/Bounded_quantifier


Mild Shock schrieb:
> Hi,
> 
> Please read the verse paper and the
> type free hiord paper, to have have
> slightest clue what the context is.
> 
> Bye
> 
> Mariano Amelsvoort schrieb:
>> Mild Shock wrote:
>>
>>> Don't blame me for what they write.
>>> But mostlikely your eruption is just from a clueless Nazi Retard, namely
>>> the paid
>>>
>>> troll you are, getting money from Putin.
>>
>> here is a one with a constant, admit you don't know what you say and what
>> you do
>>
>>   ∃x ∈N: x×x=36
>>
> 

[toc] | [prev] | [next] | [standalone]

#667143 — A noiseless patient Spider is a Pussy

Hi,

Also fuck off nickname shape shifters.
Especially this asshole, which I
will soon *Plonk*:

Organization: A noiseless patient Spider
Injection-Info: dont-email.me; 
posting-host="89eb5213555265f5de5e65431b3817e6";
	logging-data="1360340"; 
mail-complaints-to="abuse@eternal-september.org"; 
posting-account="U2FsdGVkX1+74X4OBoKm5CsTcGnfiMiu"
From: Franz Sneijders <ee@ard.nl>

Organization: A noiseless patient Spider
Injection-Info: dont-email.me; 
posting-host="d11c789dab5cab76649f04ffd47020b6";
	logging-data="1532278"; 
mail-complaints-to="abuse@eternal-september.org"; 
posting-account="U2FsdGVkX18qJKVbq/ApuA5gOdGYcYvx"
From: Mariano Amelsvoort <aa@viollr.nl>

Bye

Franz Sneijders schrieb:
> Mild Shock wrote:
> 
>> We use “∃” to bring a fresh logical variable into scope, because we
>> really mean “there exists an x such that ···.”
> 
> idiot, there is no any x over there. And it doesn't need to be a variable,
> a constant suffices.
> 

[toc] | [prev] | [next] | [standalone]

#667144 — Re: A noiseless patient Spider is a Pussy

Mild Shock wrote:

> Also fuck off nickname shape shifters.
> Especially this asshole, which I will soon *Plonk*:

sorry man, didn't know you are such sensible. Just to make sure we are 
awake, as a constant is much easier than a variable. A variable is much 
larger, in that mapping context.

never expected these guys can play this good
[ripping...    ] Bombay Dub Orchestra - Strange Constellations [  9,76M]

[toc] | [prev] | [next] | [standalone]

#667145 — 2025 Obituary: Skew Confluence (aka “Stews” 😆) (Re: Arrow Functions can do Existential Quantifier)

In halls of Cambridge, where catnip sways,
Sat pioneers lost in existential haze.
“Here lies a term!” they cried, “both bound and free,
A bag of possibilities, as far as we see.”

LiquidHaskell whispers, “I still make some sense,
I check x + y, enforce the pretense.
But only 1% — the rest, pure ado,
Existentials and predicates, I haven’t a clue.”

Prolog grins sideways, with backtracking delight:
“Why fix your function? Let each path take flight!
X and Y and Z — all three may roam,
I’ll find a solution, or many, for home.”

Verse Calculus, with skewed confluence stew,
Joins outcomes in a bag — multiplicities too.
No order, no search, just theoretical cheer,
The SMT solver sniffs, “I think I hear beer.”

Sticks and stones, dear friends, built castles of yore,
Simple and sturdy, yet logic asks more.
Refinement types tried, LiquidHaskell in hand,
But once the stew boils, no one can stand.

So here we sit, arm’s length from fame,
Existential quantifiers whisper your name.
A mockery? Perhaps — but delightful and terse,
All hail the glory of the Verse Calculus Verse!

Franz Sneijders schrieb:
> Mild Shock wrote:
> 
>> We use “∃” to bring a fresh logical variable into scope, because we
>> really mean “there exists an x such that ···.”
> 
> idiot, there is no any x over there. And it doesn't need to be a variable,
> a constant suffices.
> 

[toc] | [prev] | [next] | [standalone]

#667177 — The quantifer ∃ is just the Combinator K (Schönfinkels C)? (Re: From Feferman to Peyton Jones, no luck with ∃)

Hi,

Lets say we have an ost term t_A for
some sets of pairs such that:

   t_A(x,y) = tt <=> A(x,y)

Question is what is the term t_B for:

   B(x) <=> ∃y A(x,y)

In the Arrow Functions to Horn Clause
translation. The existential quantifier
is a feature of the Clark Completion.

In terms of Cabezas notion:

   t_B = { ''(x) :- t_a(x,y) }

Bye

P.S.: Why does it remind me of the
K Combinator? Well we have:

∃y t_B(K(x,y)) = ∃y t_A(x,y)

Not sure whether this is useful.
Although the above is true because the
combinator K is defined as Kxy = x,

it can be quite misleading, since
this here does not necessarely hold:

/* Not necessarely */
{ y | t_B(K(x,y)) } = { y | t_A(x,y) }

So if Feferman had the empty set, he could
also check for inhabitation, and bootstrap
existential quantifier via parameterized bags:

t_B(x) = ( { y | t_A(x,y) } =/= {} )

But we don't like bags here..

Mild Shock schrieb:
> Hi,
> 
> Now this is an interesting find. It seems
> not only the Verse Calculus by Peyton Jones
> hit a wall with existential quantifier ∃.
> 
> Especially the type free case. Its like in
> Rossy Boys Russell thing, people are not
> anymore trained to think about "individuals",
> 
> the are more bothered by "bags", because this
> is what the Antinomies of the formal revolution
> tought us. But the formal revolution has also
> 
> some nice easter eggs, like Fefermans OST
> ("Operational Set Theory"), an early form of
> Predicte Abstraction. With each formula A is
> 
> associated a term t_A such that:
> 
>      ∀x[A(x) <=> t_A(x) = tt]
> 
> https://math.stanford.edu/~feferman/papers/OperationalST-I.pdf
> 
> The nice thing about the t_A, its a term,
> possibly a open or closed term, depending
> on whether there are parameters, and thats
> 
> what I am now doing for Arrow Functions, when
> the Prolog systems compiles 0rReference(P1,..,Pk),
> its basically a term, an individual, that
> 
> later gets called by call/n, which makes the
> translation for individual to proposition.
> 
> Bye
> 
> P.S.: But somehow Feferman shyed away from
> definition the unbounded existential quantifier
> as a projection, there is a easy geometric
> 
> intution, and every SQL database can do it.
> Instead he falls back to some Hilber Epsilon
> analogue such as:
> 
> Given A(x) = ∃yB(x, y) and t_B for B(x, y);
> then we can take t_A = λx.t_Bx(C(λyt_Bxy)),
> using the general choice operator C.
> 
> https://math.stanford.edu/~feferman/papers/OperationalST-I.pdf
> 
> Funny!
> 
> Mild Shock schrieb:
>>
>> In halls of Cambridge, where catnip sways,
>> Sat pioneers lost in existential haze.
>> “Here lies a term!” they cried, “both bound and free,
>> A bag of possibilities, as far as we see.”
>>
>> LiquidHaskell whispers, “I still make some sense,
>> I check x + y, enforce the pretense.
>> But only 1% — the rest, pure ado,
>> Existentials and predicates, I haven’t a clue.”
>>
>> Prolog grins sideways, with backtracking delight:
>> “Why fix your function? Let each path take flight!
>> X and Y and Z — all three may roam,
>> I’ll find a solution, or many, for home.”
>>
>> Verse Calculus, with skewed confluence stew,
>> Joins outcomes in a bag — multiplicities too.
>> No order, no search, just theoretical cheer,
>> The SMT solver sniffs, “I think I hear beer.”
>>
>> Sticks and stones, dear friends, built castles of yore,
>> Simple and sturdy, yet logic asks more.
>> Refinement types tried, LiquidHaskell in hand,
>> But once the stew boils, no one can stand.
>>
>> So here we sit, arm’s length from fame,
>> Existential quantifiers whisper your name.
>> A mockery? Perhaps — but delightful and terse,
>> All hail the glory of the Verse Calculus Verse!
>>
>> Franz Sneijders schrieb:
>>> Mild Shock wrote:
>>>
>>>> We use “∃” to bring a fresh logical variable into scope, because we
>>>> really mean “there exists an x such that ···.”
>>>
>>> idiot, there is no any x over there. And it doesn't need to be a 
>>> variable,
>>> a constant suffices.
>>>
>>
> 

[toc] | [prev] | [next] | [standalone]

#667178 — Re: The quantifer ∃ is just the Combinator K (Schönfinkels C)? (Re: From Feferman to Peyton Jones, no luck with ∃)

On 11/08/2025 12:27 PM, Mild Shock wrote:
> Hi,
>
> Lets say we have an ost term t_A for
> some sets of pairs such that:
>
>    t_A(x,y) = tt <=> A(x,y)
>
> Question is what is the term t_B for:
>
>    B(x) <=> ∃y A(x,y)
>
> In the Arrow Functions to Horn Clause
> translation. The existential quantifier
> is a feature of the Clark Completion.
>
> In terms of Cabezas notion:
>
>    t_B = { ''(x) :- t_a(x,y) }
>
> Bye
>
> P.S.: Why does it remind me of the
> K Combinator? Well we have:
>
> ∃y t_B(K(x,y)) = ∃y t_A(x,y)
>
> Not sure whether this is useful.
> Although the above is true because the
> combinator K is defined as Kxy = x,
>
> it can be quite misleading, since
> this here does not necessarely hold:
>
> /* Not necessarely */
> { y | t_B(K(x,y)) } = { y | t_A(x,y) }
>
> So if Feferman had the empty set, he could
> also check for inhabitation, and bootstrap
> existential quantifier via parameterized bags:
>
> t_B(x) = ( { y | t_A(x,y) } =/= {} )
>
> But we don't like bags here..
>
> Mild Shock schrieb:
>> Hi,
>>
>> Now this is an interesting find. It seems
>> not only the Verse Calculus by Peyton Jones
>> hit a wall with existential quantifier ∃.
>>
>> Especially the type free case. Its like in
>> Rossy Boys Russell thing, people are not
>> anymore trained to think about "individuals",
>>
>> the are more bothered by "bags", because this
>> is what the Antinomies of the formal revolution
>> tought us. But the formal revolution has also
>>
>> some nice easter eggs, like Fefermans OST
>> ("Operational Set Theory"), an early form of
>> Predicte Abstraction. With each formula A is
>>
>> associated a term t_A such that:
>>
>>      ∀x[A(x) <=> t_A(x) = tt]
>>
>> https://math.stanford.edu/~feferman/papers/OperationalST-I.pdf
>>
>> The nice thing about the t_A, its a term,
>> possibly a open or closed term, depending
>> on whether there are parameters, and thats
>>
>> what I am now doing for Arrow Functions, when
>> the Prolog systems compiles 0rReference(P1,..,Pk),
>> its basically a term, an individual, that
>>
>> later gets called by call/n, which makes the
>> translation for individual to proposition.
>>
>> Bye
>>
>> P.S.: But somehow Feferman shyed away from
>> definition the unbounded existential quantifier
>> as a projection, there is a easy geometric
>>
>> intution, and every SQL database can do it.
>> Instead he falls back to some Hilber Epsilon
>> analogue such as:
>>
>> Given A(x) = ∃yB(x, y) and t_B for B(x, y);
>> then we can take t_A = λx.t_Bx(C(λyt_Bxy)),
>> using the general choice operator C.
>>
>> https://math.stanford.edu/~feferman/papers/OperationalST-I.pdf
>>
>> Funny!
>>
>> Mild Shock schrieb:
>>>
>>> In halls of Cambridge, where catnip sways,
>>> Sat pioneers lost in existential haze.
>>> “Here lies a term!” they cried, “both bound and free,
>>> A bag of possibilities, as far as we see.”
>>>
>>> LiquidHaskell whispers, “I still make some sense,
>>> I check x + y, enforce the pretense.
>>> But only 1% — the rest, pure ado,
>>> Existentials and predicates, I haven’t a clue.”
>>>
>>> Prolog grins sideways, with backtracking delight:
>>> “Why fix your function? Let each path take flight!
>>> X and Y and Z — all three may roam,
>>> I’ll find a solution, or many, for home.”
>>>
>>> Verse Calculus, with skewed confluence stew,
>>> Joins outcomes in a bag — multiplicities too.
>>> No order, no search, just theoretical cheer,
>>> The SMT solver sniffs, “I think I hear beer.”
>>>
>>> Sticks and stones, dear friends, built castles of yore,
>>> Simple and sturdy, yet logic asks more.
>>> Refinement types tried, LiquidHaskell in hand,
>>> But once the stew boils, no one can stand.
>>>
>>> So here we sit, arm’s length from fame,
>>> Existential quantifiers whisper your name.
>>> A mockery? Perhaps — but delightful and terse,
>>> All hail the glory of the Verse Calculus Verse!
>>>
>>> Franz Sneijders schrieb:
>>>> Mild Shock wrote:
>>>>
>>>>> We use “∃” to bring a fresh logical variable into scope, because we
>>>>> really mean “there exists an x such that ···.”
>>>>
>>>> idiot, there is no any x over there. And it doesn't need to be a
>>>> variable,
>>>> a constant suffices.
>>>>
>>>
>>
>

Hm. You mention "Horn clause", which is like a closure
or completion, it's basically a stroke, and then for inference's
sake it seems "I've written Horn clause, done, nyah". Yet, courtesy
the riddle of induction (or the fallacy of induction to be stronger)
another can write another different Horn clause, since "done"
was yet "not yet untrue" while "done, done, done", is a bit more
"not ultimately untrue".

Then, about quantifier disambiguation, it's usually enough framed
about the universal quantifier, while the existential quantifier
deserves its own disambiguation.

exists (> 0)
exists-unique (exactly one)
exists-distinct (more than one)
not-anywhere-not-exists (now it's the universal quantifier)


Then, the universal quantifier has these sorts of example
with common sorts of considerations about them being
the same and about them being different.

for-any
for-each
for-every
for-all

These basically reflect the piece-wise, the pair-wise,
over those, then all those.

So, you might want to go back to Chwistek and Sheffer.

[toc] | [prev] | [next] | [standalone]

#667183 — Horn uses Conditional / Clark uses Biconditional (Was: The quantifer ∃ is just the Combinator K (Schönfinkels C)?)

Hi,

 > Hm. You mention "Horn clause", which is like a closure
 > or completion, it's basically a stroke, and then for inference's
 > sake it seems "I've written Horn clause, done, nyah". Yet, courtesy

A Horn Clause, named after Alfred Horn (February 17,
1918 – April 16, 2001), a American mathematician,
looks like this:

H :- B ,

With :- the left pointing conditional.
The example I gave has the same form:

''(x) :- t_a(x,y)

Respectively fully quantified:

∀x∀y(''(x) ← t_a(x,y))

If you take the so called Clark Completion, Keith Leonard
Clark (born 29 March 1943) a British computer scientist.
the conditional is replaced by a biconditional:

∀x(''(x) ↔ ∃y t_a(x,y))

To form the Clark Completion one has to go
to FOL with equality, and do some movements,
like move some forall quantifiers inside,

then then change the polarity and become exists quantifiers.

Bye

See also here:

[Clark, 1978] Keith Clark. Negation as failure. In Herve
Gallaire and Jack Minker, editors, Logic and Data Bases,
pages 293 322. Plenum Press, New York, 1978.

Ross Finlayson schrieb:
> On 11/08/2025 12:27 PM, Mild Shock wrote:
>> Hi,
>>
>> Lets say we have an ost term t_A for
>> some sets of pairs such that:
>>
>>    t_A(x,y) = tt <=> A(x,y)
>>
>> Question is what is the term t_B for:
>>
>>    B(x) <=> ∃y A(x,y)
>>
>> In the Arrow Functions to Horn Clause
>> translation. The existential quantifier
>> is a feature of the Clark Completion.
>>
>> In terms of Cabezas notion:
>>
>>    t_B = { ''(x) :- t_a(x,y) }
>>
>> Bye
>>
>> P.S.: Why does it remind me of the
>> K Combinator? Well we have:
>>
>> ∃y t_B(K(x,y)) = ∃y t_A(x,y)
>>
>> Not sure whether this is useful.
>> Although the above is true because the
>> combinator K is defined as Kxy = x,
>>
>> it can be quite misleading, since
>> this here does not necessarely hold:
>>
>> /* Not necessarely */
>> { y | t_B(K(x,y)) } = { y | t_A(x,y) }
>>
>> So if Feferman had the empty set, he could
>> also check for inhabitation, and bootstrap
>> existential quantifier via parameterized bags:
>>
>> t_B(x) = ( { y | t_A(x,y) } =/= {} )
>>
>> But we don't like bags here..
>>
>> Mild Shock schrieb:
>>> Hi,
>>>
>>> Now this is an interesting find. It seems
>>> not only the Verse Calculus by Peyton Jones
>>> hit a wall with existential quantifier ∃.
>>>
>>> Especially the type free case. Its like in
>>> Rossy Boys Russell thing, people are not
>>> anymore trained to think about "individuals",
>>>
>>> the are more bothered by "bags", because this
>>> is what the Antinomies of the formal revolution
>>> tought us. But the formal revolution has also
>>>
>>> some nice easter eggs, like Fefermans OST
>>> ("Operational Set Theory"), an early form of
>>> Predicte Abstraction. With each formula A is
>>>
>>> associated a term t_A such that:
>>>
>>>      ∀x[A(x) <=> t_A(x) = tt]
>>>
>>> https://math.stanford.edu/~feferman/papers/OperationalST-I.pdf
>>>
>>> The nice thing about the t_A, its a term,
>>> possibly a open or closed term, depending
>>> on whether there are parameters, and thats
>>>
>>> what I am now doing for Arrow Functions, when
>>> the Prolog systems compiles 0rReference(P1,..,Pk),
>>> its basically a term, an individual, that
>>>
>>> later gets called by call/n, which makes the
>>> translation for individual to proposition.
>>>
>>> Bye
>>>
>>> P.S.: But somehow Feferman shyed away from
>>> definition the unbounded existential quantifier
>>> as a projection, there is a easy geometric
>>>
>>> intution, and every SQL database can do it.
>>> Instead he falls back to some Hilber Epsilon
>>> analogue such as:
>>>
>>> Given A(x) = ∃yB(x, y) and t_B for B(x, y);
>>> then we can take t_A = λx.t_Bx(C(λyt_Bxy)),
>>> using the general choice operator C.
>>>
>>> https://math.stanford.edu/~feferman/papers/OperationalST-I.pdf
>>>
>>> Funny!
>>>
>>> Mild Shock schrieb:
>>>>
>>>> In halls of Cambridge, where catnip sways,
>>>> Sat pioneers lost in existential haze.
>>>> “Here lies a term!” they cried, “both bound and free,
>>>> A bag of possibilities, as far as we see.”
>>>>
>>>> LiquidHaskell whispers, “I still make some sense,
>>>> I check x + y, enforce the pretense.
>>>> But only 1% — the rest, pure ado,
>>>> Existentials and predicates, I haven’t a clue.”
>>>>
>>>> Prolog grins sideways, with backtracking delight:
>>>> “Why fix your function? Let each path take flight!
>>>> X and Y and Z — all three may roam,
>>>> I’ll find a solution, or many, for home.”
>>>>
>>>> Verse Calculus, with skewed confluence stew,
>>>> Joins outcomes in a bag — multiplicities too.
>>>> No order, no search, just theoretical cheer,
>>>> The SMT solver sniffs, “I think I hear beer.”
>>>>
>>>> Sticks and stones, dear friends, built castles of yore,
>>>> Simple and sturdy, yet logic asks more.
>>>> Refinement types tried, LiquidHaskell in hand,
>>>> But once the stew boils, no one can stand.
>>>>
>>>> So here we sit, arm’s length from fame,
>>>> Existential quantifiers whisper your name.
>>>> A mockery? Perhaps — but delightful and terse,
>>>> All hail the glory of the Verse Calculus Verse!
>>>>
>>>> Franz Sneijders schrieb:
>>>>> Mild Shock wrote:
>>>>>
>>>>>> We use “∃” to bring a fresh logical variable into scope, because we
>>>>>> really mean “there exists an x such that ···.”
>>>>>
>>>>> idiot, there is no any x over there. And it doesn't need to be a
>>>>> variable,
>>>>> a constant suffices.
>>>>>
>>>>
>>>
>>
> 
> Hm. You mention "Horn clause", which is like a closure
> or completion, it's basically a stroke, and then for inference's
> sake it seems "I've written Horn clause, done, nyah". Yet, courtesy
> the riddle of induction (or the fallacy of induction to be stronger)
> another can write another different Horn clause, since "done"
> was yet "not yet untrue" while "done, done, done", is a bit more
> "not ultimately untrue".
> 
> Then, about quantifier disambiguation, it's usually enough framed
> about the universal quantifier, while the existential quantifier
> deserves its own disambiguation.
> 
> exists (> 0)
> exists-unique (exactly one)
> exists-distinct (more than one)
> not-anywhere-not-exists (now it's the universal quantifier)
> 
> 
> Then, the universal quantifier has these sorts of example
> with common sorts of considerations about them being
> the same and about them being different.
> 
> for-any
> for-each
> for-every
> for-all
> 
> These basically reflect the piece-wise, the pair-wise,
> over those, then all those.
> 
> So, you might want to go back to Chwistek and Sheffer.
> 
> 

[toc] | [prev] | [next] | [standalone]

#667184 — CET is also needed (Was: Horn uses Conditional / Clark uses Biconditional)

Hi,

Since FOL with equality is used. Question
is but what should be the semantics of (=)/2.
To model some Herbrand semantics,

one usually needs also to add CET, the
Clark Equational Theory. Which are a few
additional axioms about function symbols

and (=)/2. Jacques Herbrand (12 February 1908
– 27 July 1931) was a French mathematician.

Bye

Mild Shock schrieb:
> Hi,
> 
>  > Hm. You mention "Horn clause", which is like a closure
>  > or completion, it's basically a stroke, and then for inference's
>  > sake it seems "I've written Horn clause, done, nyah". Yet, courtesy
> 
> A Horn Clause, named after Alfred Horn (February 17,
> 1918 – April 16, 2001), a American mathematician,
> looks like this:
> 
> H :- B ,
> 
> With :- the left pointing conditional.
> The example I gave has the same form:
> 
> ''(x) :- t_a(x,y)
> 
> Respectively fully quantified:
> 
> ∀x∀y(''(x) ← t_a(x,y))
> 
> If you take the so called Clark Completion, Keith Leonard
> Clark (born 29 March 1943) a British computer scientist.
> the conditional is replaced by a biconditional:
> 
> ∀x(''(x) ↔ ∃y t_a(x,y))
> 
> To form the Clark Completion one has to go
> to FOL with equality, and do some movements,
> like move some forall quantifiers inside,
> 
> then then change the polarity and become exists quantifiers.
> 
> Bye
> 
> See also here:
> 
> [Clark, 1978] Keith Clark. Negation as failure. In Herve
> Gallaire and Jack Minker, editors, Logic and Data Bases,
> pages 293 322. Plenum Press, New York, 1978.
> 
> Ross Finlayson schrieb:
>> On 11/08/2025 12:27 PM, Mild Shock wrote:
>>> Hi,
>>>
>>> Lets say we have an ost term t_A for
>>> some sets of pairs such that:
>>>
>>>    t_A(x,y) = tt <=> A(x,y)
>>>
>>> Question is what is the term t_B for:
>>>
>>>    B(x) <=> ∃y A(x,y)
>>>
>>> In the Arrow Functions to Horn Clause
>>> translation. The existential quantifier
>>> is a feature of the Clark Completion.
>>>
>>> In terms of Cabezas notion:
>>>
>>>    t_B = { ''(x) :- t_a(x,y) }
>>>
>>> Bye
>>>
>>> P.S.: Why does it remind me of the
>>> K Combinator? Well we have:
>>>
>>> ∃y t_B(K(x,y)) = ∃y t_A(x,y)
>>>
>>> Not sure whether this is useful.
>>> Although the above is true because the
>>> combinator K is defined as Kxy = x,
>>>
>>> it can be quite misleading, since
>>> this here does not necessarely hold:
>>>
>>> /* Not necessarely */
>>> { y | t_B(K(x,y)) } = { y | t_A(x,y) }
>>>
>>> So if Feferman had the empty set, he could
>>> also check for inhabitation, and bootstrap
>>> existential quantifier via parameterized bags:
>>>
>>> t_B(x) = ( { y | t_A(x,y) } =/= {} )
>>>
>>> But we don't like bags here..
>>>
>>> Mild Shock schrieb:
>>>> Hi,
>>>>
>>>> Now this is an interesting find. It seems
>>>> not only the Verse Calculus by Peyton Jones
>>>> hit a wall with existential quantifier ∃.
>>>>
>>>> Especially the type free case. Its like in
>>>> Rossy Boys Russell thing, people are not
>>>> anymore trained to think about "individuals",
>>>>
>>>> the are more bothered by "bags", because this
>>>> is what the Antinomies of the formal revolution
>>>> tought us. But the formal revolution has also
>>>>
>>>> some nice easter eggs, like Fefermans OST
>>>> ("Operational Set Theory"), an early form of
>>>> Predicte Abstraction. With each formula A is
>>>>
>>>> associated a term t_A such that:
>>>>
>>>>      ∀x[A(x) <=> t_A(x) = tt]
>>>>
>>>> https://math.stanford.edu/~feferman/papers/OperationalST-I.pdf
>>>>
>>>> The nice thing about the t_A, its a term,
>>>> possibly a open or closed term, depending
>>>> on whether there are parameters, and thats
>>>>
>>>> what I am now doing for Arrow Functions, when
>>>> the Prolog systems compiles 0rReference(P1,..,Pk),
>>>> its basically a term, an individual, that
>>>>
>>>> later gets called by call/n, which makes the
>>>> translation for individual to proposition.
>>>>
>>>> Bye
>>>>
>>>> P.S.: But somehow Feferman shyed away from
>>>> definition the unbounded existential quantifier
>>>> as a projection, there is a easy geometric
>>>>
>>>> intution, and every SQL database can do it.
>>>> Instead he falls back to some Hilber Epsilon
>>>> analogue such as:
>>>>
>>>> Given A(x) = ∃yB(x, y) and t_B for B(x, y);
>>>> then we can take t_A = λx.t_Bx(C(λyt_Bxy)),
>>>> using the general choice operator C.
>>>>
>>>> https://math.stanford.edu/~feferman/papers/OperationalST-I.pdf
>>>>
>>>> Funny!
>>>>
>>>> Mild Shock schrieb:
>>>>>
>>>>> In halls of Cambridge, where catnip sways,
>>>>> Sat pioneers lost in existential haze.
>>>>> “Here lies a term!” they cried, “both bound and free,
>>>>> A bag of possibilities, as far as we see.”
>>>>>
>>>>> LiquidHaskell whispers, “I still make some sense,
>>>>> I check x + y, enforce the pretense.
>>>>> But only 1% — the rest, pure ado,
>>>>> Existentials and predicates, I haven’t a clue.”
>>>>>
>>>>> Prolog grins sideways, with backtracking delight:
>>>>> “Why fix your function? Let each path take flight!
>>>>> X and Y and Z — all three may roam,
>>>>> I’ll find a solution, or many, for home.”
>>>>>
>>>>> Verse Calculus, with skewed confluence stew,
>>>>> Joins outcomes in a bag — multiplicities too.
>>>>> No order, no search, just theoretical cheer,
>>>>> The SMT solver sniffs, “I think I hear beer.”
>>>>>
>>>>> Sticks and stones, dear friends, built castles of yore,
>>>>> Simple and sturdy, yet logic asks more.
>>>>> Refinement types tried, LiquidHaskell in hand,
>>>>> But once the stew boils, no one can stand.
>>>>>
>>>>> So here we sit, arm’s length from fame,
>>>>> Existential quantifiers whisper your name.
>>>>> A mockery? Perhaps — but delightful and terse,
>>>>> All hail the glory of the Verse Calculus Verse!
>>>>>
>>>>> Franz Sneijders schrieb:
>>>>>> Mild Shock wrote:
>>>>>>
>>>>>>> We use “∃” to bring a fresh logical variable into scope, because we
>>>>>>> really mean “there exists an x such that ···.”
>>>>>>
>>>>>> idiot, there is no any x over there. And it doesn't need to be a
>>>>>> variable,
>>>>>> a constant suffices.
>>>>>>
>>>>>
>>>>
>>>
>>
>> Hm. You mention "Horn clause", which is like a closure
>> or completion, it's basically a stroke, and then for inference's
>> sake it seems "I've written Horn clause, done, nyah". Yet, courtesy
>> the riddle of induction (or the fallacy of induction to be stronger)
>> another can write another different Horn clause, since "done"
>> was yet "not yet untrue" while "done, done, done", is a bit more
>> "not ultimately untrue".
>>
>> Then, about quantifier disambiguation, it's usually enough framed
>> about the universal quantifier, while the existential quantifier
>> deserves its own disambiguation.
>>
>> exists (> 0)
>> exists-unique (exactly one)
>> exists-distinct (more than one)
>> not-anywhere-not-exists (now it's the universal quantifier)
>>
>>
>> Then, the universal quantifier has these sorts of example
>> with common sorts of considerations about them being
>> the same and about them being different.
>>
>> for-any
>> for-each
>> for-every
>> for-all
>>
>> These basically reflect the piece-wise, the pair-wise,
>> over those, then all those.
>>
>> So, you might want to go back to Chwistek and Sheffer.
>>
>>
> 

[toc] | [prev] | [next] | [standalone]

#667185 — Re: CET is also needed (Was: Horn uses Conditional / Clark uses Biconditional)

On 11/09/2025 04:08 AM, Mild Shock wrote:
> Hi,
>
> Since FOL with equality is used. Question
> is but what should be the semantics of (=)/2.
> To model some Herbrand semantics,
>
> one usually needs also to add CET, the
> Clark Equational Theory. Which are a few
> additional axioms about function symbols
>
> and (=)/2. Jacques Herbrand (12 February 1908
> – 27 July 1931) was a French mathematician.
>
> Bye
>
> Mild Shock schrieb:
>> Hi,
>>
>>  > Hm. You mention "Horn clause", which is like a closure
>>  > or completion, it's basically a stroke, and then for inference's
>>  > sake it seems "I've written Horn clause, done, nyah". Yet, courtesy
>>
>> A Horn Clause, named after Alfred Horn (February 17,
>> 1918 – April 16, 2001), a American mathematician,
>> looks like this:
>>
>> H :- B ,
>>
>> With :- the left pointing conditional.
>> The example I gave has the same form:
>>
>> ''(x) :- t_a(x,y)
>>
>> Respectively fully quantified:
>>
>> ∀x∀y(''(x) ← t_a(x,y))
>>
>> If you take the so called Clark Completion, Keith Leonard
>> Clark (born 29 March 1943) a British computer scientist.
>> the conditional is replaced by a biconditional:
>>
>> ∀x(''(x) ↔ ∃y t_a(x,y))
>>
>> To form the Clark Completion one has to go
>> to FOL with equality, and do some movements,
>> like move some forall quantifiers inside,
>>
>> then then change the polarity and become exists quantifiers.
>>
>> Bye
>>
>> See also here:
>>
>> [Clark, 1978] Keith Clark. Negation as failure. In Herve
>> Gallaire and Jack Minker, editors, Logic and Data Bases,
>> pages 293 322. Plenum Press, New York, 1978.
>>
>> Ross Finlayson schrieb:
>>> On 11/08/2025 12:27 PM, Mild Shock wrote:
>>>> Hi,
>>>>
>>>> Lets say we have an ost term t_A for
>>>> some sets of pairs such that:
>>>>
>>>>    t_A(x,y) = tt <=> A(x,y)
>>>>
>>>> Question is what is the term t_B for:
>>>>
>>>>    B(x) <=> ∃y A(x,y)
>>>>
>>>> In the Arrow Functions to Horn Clause
>>>> translation. The existential quantifier
>>>> is a feature of the Clark Completion.
>>>>
>>>> In terms of Cabezas notion:
>>>>
>>>>    t_B = { ''(x) :- t_a(x,y) }
>>>>
>>>> Bye
>>>>
>>>> P.S.: Why does it remind me of the
>>>> K Combinator? Well we have:
>>>>
>>>> ∃y t_B(K(x,y)) = ∃y t_A(x,y)
>>>>
>>>> Not sure whether this is useful.
>>>> Although the above is true because the
>>>> combinator K is defined as Kxy = x,
>>>>
>>>> it can be quite misleading, since
>>>> this here does not necessarely hold:
>>>>
>>>> /* Not necessarely */
>>>> { y | t_B(K(x,y)) } = { y | t_A(x,y) }
>>>>
>>>> So if Feferman had the empty set, he could
>>>> also check for inhabitation, and bootstrap
>>>> existential quantifier via parameterized bags:
>>>>
>>>> t_B(x) = ( { y | t_A(x,y) } =/= {} )
>>>>
>>>> But we don't like bags here..
>>>>
>>>> Mild Shock schrieb:
>>>>> Hi,
>>>>>
>>>>> Now this is an interesting find. It seems
>>>>> not only the Verse Calculus by Peyton Jones
>>>>> hit a wall with existential quantifier ∃.
>>>>>
>>>>> Especially the type free case. Its like in
>>>>> Rossy Boys Russell thing, people are not
>>>>> anymore trained to think about "individuals",
>>>>>
>>>>> the are more bothered by "bags", because this
>>>>> is what the Antinomies of the formal revolution
>>>>> tought us. But the formal revolution has also
>>>>>
>>>>> some nice easter eggs, like Fefermans OST
>>>>> ("Operational Set Theory"), an early form of
>>>>> Predicte Abstraction. With each formula A is
>>>>>
>>>>> associated a term t_A such that:
>>>>>
>>>>>      ∀x[A(x) <=> t_A(x) = tt]
>>>>>
>>>>> https://math.stanford.edu/~feferman/papers/OperationalST-I.pdf
>>>>>
>>>>> The nice thing about the t_A, its a term,
>>>>> possibly a open or closed term, depending
>>>>> on whether there are parameters, and thats
>>>>>
>>>>> what I am now doing for Arrow Functions, when
>>>>> the Prolog systems compiles 0rReference(P1,..,Pk),
>>>>> its basically a term, an individual, that
>>>>>
>>>>> later gets called by call/n, which makes the
>>>>> translation for individual to proposition.
>>>>>
>>>>> Bye
>>>>>
>>>>> P.S.: But somehow Feferman shyed away from
>>>>> definition the unbounded existential quantifier
>>>>> as a projection, there is a easy geometric
>>>>>
>>>>> intution, and every SQL database can do it.
>>>>> Instead he falls back to some Hilber Epsilon
>>>>> analogue such as:
>>>>>
>>>>> Given A(x) = ∃yB(x, y) and t_B for B(x, y);
>>>>> then we can take t_A = λx.t_Bx(C(λyt_Bxy)),
>>>>> using the general choice operator C.
>>>>>
>>>>> https://math.stanford.edu/~feferman/papers/OperationalST-I.pdf
>>>>>
>>>>> Funny!
>>>>>
>>>>> Mild Shock schrieb:
>>>>>>
>>>>>> In halls of Cambridge, where catnip sways,
>>>>>> Sat pioneers lost in existential haze.
>>>>>> “Here lies a term!” they cried, “both bound and free,
>>>>>> A bag of possibilities, as far as we see.”
>>>>>>
>>>>>> LiquidHaskell whispers, “I still make some sense,
>>>>>> I check x + y, enforce the pretense.
>>>>>> But only 1% — the rest, pure ado,
>>>>>> Existentials and predicates, I haven’t a clue.”
>>>>>>
>>>>>> Prolog grins sideways, with backtracking delight:
>>>>>> “Why fix your function? Let each path take flight!
>>>>>> X and Y and Z — all three may roam,
>>>>>> I’ll find a solution, or many, for home.”
>>>>>>
>>>>>> Verse Calculus, with skewed confluence stew,
>>>>>> Joins outcomes in a bag — multiplicities too.
>>>>>> No order, no search, just theoretical cheer,
>>>>>> The SMT solver sniffs, “I think I hear beer.”
>>>>>>
>>>>>> Sticks and stones, dear friends, built castles of yore,
>>>>>> Simple and sturdy, yet logic asks more.
>>>>>> Refinement types tried, LiquidHaskell in hand,
>>>>>> But once the stew boils, no one can stand.
>>>>>>
>>>>>> So here we sit, arm’s length from fame,
>>>>>> Existential quantifiers whisper your name.
>>>>>> A mockery? Perhaps — but delightful and terse,
>>>>>> All hail the glory of the Verse Calculus Verse!
>>>>>>
>>>>>> Franz Sneijders schrieb:
>>>>>>> Mild Shock wrote:
>>>>>>>
>>>>>>>> We use “∃” to bring a fresh logical variable into scope, because we
>>>>>>>> really mean “there exists an x such that ···.”
>>>>>>>
>>>>>>> idiot, there is no any x over there. And it doesn't need to be a
>>>>>>> variable,
>>>>>>> a constant suffices.
>>>>>>>
>>>>>>
>>>>>
>>>>
>>>
>>> Hm. You mention "Horn clause", which is like a closure
>>> or completion, it's basically a stroke, and then for inference's
>>> sake it seems "I've written Horn clause, done, nyah". Yet, courtesy
>>> the riddle of induction (or the fallacy of induction to be stronger)
>>> another can write another different Horn clause, since "done"
>>> was yet "not yet untrue" while "done, done, done", is a bit more
>>> "not ultimately untrue".
>>>
>>> Then, about quantifier disambiguation, it's usually enough framed
>>> about the universal quantifier, while the existential quantifier
>>> deserves its own disambiguation.
>>>
>>> exists (> 0)
>>> exists-unique (exactly one)
>>> exists-distinct (more than one)
>>> not-anywhere-not-exists (now it's the universal quantifier)
>>>
>>>
>>> Then, the universal quantifier has these sorts of example
>>> with common sorts of considerations about them being
>>> the same and about them being different.
>>>
>>> for-any
>>> for-each
>>> for-every
>>> for-all
>>>
>>> These basically reflect the piece-wise, the pair-wise,
>>> over those, then all those.
>>>
>>> So, you might want to go back to Chwistek and Sheffer.
>>>
>>>
>>
>

It may remind one of the Curry correspondence.

Of course, in mathematics, that then gets into
compactness and fixed-point theorem(s) and
definition(s) of the direct product of integers.

I.e., in mathematics, "equality" begets infinitary reasoning.

Some years ago, there was a thread on sci.logic
about Curry correspondence, I wrote on it, so,
there's probably something meaningful to it.

In, "the logic", say.

https://sci.logic.narkive.com/36tgd6NK/curry-s-paradox-in-propositional-logic

[toc] | [prev] | [next] | [standalone]

#667186 — You have to check Feferman OST [Paradox Hunting] (Was: CET is also needed)

Hi,

You are still hunting Paradoxes, is
this still a noble occupation?
You have to check Feferman OST etc..

The statement is only, that for A,
formula, there exists t_A a term,
such that:

t_A(x) = tt <=> A(x)

Gödel used the same, t_A is nothing
else than a Gödelization of A. Only
in Gödel numbers were used, and Gödel

usually written as {A}. And already
Gödel showed before Curry all kind of
fixpoint paradoxes. But Feferman does

not allow arbitrary A, and a modern
branch of Feferman OST would be Reverse
mathematics having a bunch of allowed

or disallowed forms of A. What Feferman
OST shows if he makes small large cardinals
plausible, he shows of course also

that the thingy is not inconsistent, i.e.
has no Paradox under certain circumstances.

Have Fun!

Bye

BTW: OST is related to Gödels constructive
universe L, and papers such as these are
full of V = L assumptions:

https://home.inf.unibe.ch/gerhard.jaeger/16-relativizing_OST.pdf

But I don't know how substantial the stuff
there is. I only use the fact that t is a term,
and then terms in my Prolog system Dogelog Player

correspond to compiled code. So t_A is basically
not anymore the original formula A, as already in
OST, but its not so much viewed as a Gödelization

out of the blue, more as a code for some Prolog machine.

Ross Finlayson schrieb:
> It may remind one of the Curry correspondence.
> 
> Of course, in mathematics, that then gets into
> compactness and fixed-point theorem(s) and
> definition(s) of the direct product of integers.
> 
> I.e., in mathematics, "equality" begets infinitary reasoning.
> 
> Some years ago, there was a thread on sci.logic
> about Curry correspondence, I wrote on it, so,
> there's probably something meaningful to it.
> 
> In, "the logic", say.
> 
> https://sci.logic.narkive.com/36tgd6NK/curry-s-paradox-in-propositional-logic 
> 
> 
> 

[toc] | [prev] | [next] | [standalone]

#667187 — Prolog semantics is 3-valued or intuitionistic [Feferman prefers partial logic] (Was: You have to check Feferman OST [Paradox Hunting])

Hi,

But Prolog semantics is often taken 3-valued
or intuitionistic. And what is a Paradox in
classical logic with an absurdity result,

might be only a looping Prolog text when
executed in a Prolog prozessor. For example
this extended Horn Clause, Horn Clause with

negation as failure, here (the Liar):

p :- \+ p

Has a Clark completion which does not have a model:

p <-> ~p

In Feferman OST you find the looping somehow
expressed as free logic, i.e. there is an
operator down arrow ↓, and t↓ expresses

that t has a value. Used by Beeson for example
in an exemplar number theory to express that
division exists as long as you don't divide by

zero, and Feferman refers to Beeson:

7. The Logic of Partial Terms
y ≠ 0 → x/y ↓
https://www.michaelbeeson.com/research/papers/LambdaLogicOriginal.pdf

But for practical purposes this can be a
can of worms, and modern theorem provers have
an Option type which is for example:

Option<T> = nothing | just(T)

The can might be confusion of non-termination
with not in the domain of a function. Especially
when your logic and/or theory has constructivity

and non-constructivity side by side. Which is
usually the case in program verification, and
specification can be non-constructive, while

a Program code can be constructive,

Bye

Mild Shock schrieb:
> Hi,
> 
> You are still hunting Paradoxes, is
> this still a noble occupation?
> You have to check Feferman OST etc..
> 
> The statement is only, that for A,
> formula, there exists t_A a term,
> such that:
> 
> t_A(x) = tt <=> A(x)
> 
> Gödel used the same, t_A is nothing
> else than a Gödelization of A. Only
> in Gödel numbers were used, and Gödel
> 
> usually written as {A}. And already
> Gödel showed before Curry all kind of
> fixpoint paradoxes. But Feferman does
> 
> not allow arbitrary A, and a modern
> branch of Feferman OST would be Reverse
> mathematics having a bunch of allowed
> 
> or disallowed forms of A. What Feferman
> OST shows if he makes small large cardinals
> plausible, he shows of course also
> 
> that the thingy is not inconsistent, i.e.
> has no Paradox under certain circumstances.
> 
> Have Fun!
> 
> Bye
> 
> BTW: OST is related to Gödels constructive
> universe L, and papers such as these are
> full of V = L assumptions:
> 
> https://home.inf.unibe.ch/gerhard.jaeger/16-relativizing_OST.pdf
> 
> But I don't know how substantial the stuff
> there is. I only use the fact that t is a term,
> and then terms in my Prolog system Dogelog Player
> 
> correspond to compiled code. So t_A is basically
> not anymore the original formula A, as already in
> OST, but its not so much viewed as a Gödelization
> 
> out of the blue, more as a code for some Prolog machine.
> 
> Ross Finlayson schrieb:
>> It may remind one of the Curry correspondence.
>>
>> Of course, in mathematics, that then gets into
>> compactness and fixed-point theorem(s) and
>> definition(s) of the direct product of integers.
>>
>> I.e., in mathematics, "equality" begets infinitary reasoning.
>>
>> Some years ago, there was a thread on sci.logic
>> about Curry correspondence, I wrote on it, so,
>> there's probably something meaningful to it.
>>
>> In, "the logic", say.
>>
>> https://sci.logic.narkive.com/36tgd6NK/curry-s-paradox-in-propositional-logic 
>>
>>
>>
> 

[toc] | [prev] | [next] | [standalone]

#667188 — In Prolog you don't need the down arrow t↓ (Was: Prolog semantics is 3-valued or intuitionistic)

Hi,

In Prolog you don't need the down arrow t↓ .
Since you anyway don't have functions.
You can either throw an error for division

by zero or you can fail. This is important
for constraint logic programming. You will
indeed have some partial term effects,

when your constraint implies division by zero,
for example if you ask SWI-Prolog for:

?- 6 #= 2*X

It will probably give you X = 3. On the other
hand if you ask SWI-Prolog for:

?- 6 #= 0*X

It should fail.

Bye

Mild Shock schrieb:
> Hi,
> 
> But Prolog semantics is often taken 3-valued
> or intuitionistic. And what is a Paradox in
> classical logic with an absurdity result,
> 
> might be only a looping Prolog text when
> executed in a Prolog prozessor. For example
> this extended Horn Clause, Horn Clause with
> 
> negation as failure, here (the Liar):
> 
> p :- \+ p
> 
> Has a Clark completion which does not have a model:
> 
> p <-> ~p
> 
> In Feferman OST you find the looping somehow
> expressed as free logic, i.e. there is an
> operator down arrow ↓, and t↓ expresses
> 
> that t has a value. Used by Beeson for example
> in an exemplar number theory to express that
> division exists as long as you don't divide by
> 
> zero, and Feferman refers to Beeson:
> 
> 7. The Logic of Partial Terms
> y ≠ 0 → x/y ↓
> https://www.michaelbeeson.com/research/papers/LambdaLogicOriginal.pdf
> 
> But for practical purposes this can be a
> can of worms, and modern theorem provers have
> an Option type which is for example:
> 
> Option<T> = nothing | just(T)
> 
> The can might be confusion of non-termination
> with not in the domain of a function. Especially
> when your logic and/or theory has constructivity
> 
> and non-constructivity side by side. Which is
> usually the case in program verification, and
> specification can be non-constructive, while
> 
> a Program code can be constructive,
> 
> Bye
> 
> Mild Shock schrieb:
>> Hi,
>>
>> You are still hunting Paradoxes, is
>> this still a noble occupation?
>> You have to check Feferman OST etc..
>>
>> The statement is only, that for A,
>> formula, there exists t_A a term,
>> such that:
>>
>> t_A(x) = tt <=> A(x)
>>
>> Gödel used the same, t_A is nothing
>> else than a Gödelization of A. Only
>> in Gödel numbers were used, and Gödel
>>
>> usually written as {A}. And already
>> Gödel showed before Curry all kind of
>> fixpoint paradoxes. But Feferman does
>>
>> not allow arbitrary A, and a modern
>> branch of Feferman OST would be Reverse
>> mathematics having a bunch of allowed
>>
>> or disallowed forms of A. What Feferman
>> OST shows if he makes small large cardinals
>> plausible, he shows of course also
>>
>> that the thingy is not inconsistent, i.e.
>> has no Paradox under certain circumstances.
>>
>> Have Fun!
>>
>> Bye
>>
>> BTW: OST is related to Gödels constructive
>> universe L, and papers such as these are
>> full of V = L assumptions:
>>
>> https://home.inf.unibe.ch/gerhard.jaeger/16-relativizing_OST.pdf
>>
>> But I don't know how substantial the stuff
>> there is. I only use the fact that t is a term,
>> and then terms in my Prolog system Dogelog Player
>>
>> correspond to compiled code. So t_A is basically
>> not anymore the original formula A, as already in
>> OST, but its not so much viewed as a Gödelization
>>
>> out of the blue, more as a code for some Prolog machine.
>>
>> Ross Finlayson schrieb:
>>> It may remind one of the Curry correspondence.
>>>
>>> Of course, in mathematics, that then gets into
>>> compactness and fixed-point theorem(s) and
>>> definition(s) of the direct product of integers.
>>>
>>> I.e., in mathematics, "equality" begets infinitary reasoning.
>>>
>>> Some years ago, there was a thread on sci.logic
>>> about Curry correspondence, I wrote on it, so,
>>> there's probably something meaningful to it.
>>>
>>> In, "the logic", say.
>>>
>>> https://sci.logic.narkive.com/36tgd6NK/curry-s-paradox-in-propositional-logic 
>>>
>>>
>>>
>>
> 

[toc] | [prev] | [standalone]

Back to top | Article view | sci.physics.relativity

csiph-web