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

Groups > sci.math > #640228 > unrolled thread

😂 "Plog-like" - that should be the official term!

Back to article view | Back to sci.math

Contents

  😂 "Plog-like" - that should be the official term! Mild Shock <janburse@fastmail.fm> - 2025-10-08 01:15 +0200
    How deep seek went bonkers (Was: 😂 "Plog-like" - that should be the official term!) Mild Shock <janburse@fastmail.fm> - 2025-10-08 01:21 +0200
      Re: How deep seek went bonkers (Was: 😂 "Plog-like" - that should be the official term!) "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2025-10-07 18:30 -0700
    Declarative farts versus MSI Claw AI+, who would win? (Re: 😂 "Plog-like" - that should be the official term!) Mild Shock <janburse@fastmail.fm> - 2025-10-23 14:38 +0200
      Gameified AI Engineers brains blown out [Kurzweil's 2045 Prediction] (Re: Declarative farts versus MSI Claw AI+, who would win?) Mild Shock <janburse@fastmail.fm> - 2025-10-23 15:23 +0200
        The intelligent Cloud, Fog and Edge is evolving (Re: Gameified AI Engineers brains blown out [Kurzweil's 2045 Prediction]) Mild Shock <janburse@fastmail.fm> - 2025-10-24 11:40 +0200
          More Dreams: LLM + Chess = LRM (Re: The intelligent Cloud, Fog and Edge is evolving) Mild Shock <janburse@fastmail.fm> - 2025-10-25 12:52 +0200
            Not for Boris the Loris and Julio the Nazi Retared (Re: More Dreams: LLM + Chess = LRM) Mild Shock <janburse@fastmail.fm> - 2025-10-25 13:10 +0200
      Logtalks Corleone "olive oil business" [Missed the DOP Bandwagon] (Re: Declarative farts versus MSI Claw AI+) Mild Shock <janburse@fastmail.fm> - 2026-04-29 11:32 +0200
        Logtalk is over engineered in a bad sense [Where are the test results] (Re: Logtalks Corleone "olive oil business") Mild Shock <janburse@fastmail.fm> - 2026-04-29 11:55 +0200
          Logtalk just creates its own island of PlUnit (Re: Logtalk is over engineered in a bad sense) Mild Shock <janburse@fastmail.fm> - 2026-04-29 12:11 +0200
            The mechanic with the Vacuum Hypothesis (Re: Logtalk just creates its own island of PlUnit) Mild Shock <janburse@fastmail.fm> - 2026-04-29 12:53 +0200
              Layoff Tsunami and Defunding Rounds [Burger jobs] (Re: The mechanic with the Vacuum Hypothesis) Mild Shock <janburse@fastmail.fm> - 2026-04-29 13:17 +0200
    Arrow Functions can do Existential Quantifier (Re: 😂 "Plog-like" - that should be the official term!) Mild Shock <janburse@fastmail.fm> - 2025-11-06 14:32 +0100
      Resolving Ambiguity in Negation as Failure (Re: Arrow Functions can do Existential Quantifier) Mild Shock <janburse@fastmail.fm> - 2025-11-06 14:33 +0100
        Future Outlook of Logic Programming (Re: Resolving Ambiguity in Negation as Failure) Mild Shock <janburse@fastmail.fm> - 2025-11-06 14:35 +0100
      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
        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
      Prolog PIP-0110: Its a Floating-Point Multiverse? [Stoic Grisu versus Rest of World] (Re: Arrow Functions can do Existential Quantifier) Mild Shock <janburse@fastmail.fm> - 2026-04-29 00:41 +0200
        Testing NVIDIA A10G / XVM Engine v10.2.4 (Permion Federal AI) (Re: Prolog PIP-0110: Its a Floating-Point Multiverse?) Mild Shock <janburse@fastmail.fm> - 2026-04-29 02:15 +0200
          This could be a serious security vulnerability (Re: Testing NVIDIA A10G / XVM Engine v10.2.4) Mild Shock <janburse@fastmail.fm> - 2026-04-29 02:38 +0200
            Re: This could be a serious security vulnerability (Re: Testing NVIDIA A10G / XVM Engine v10.2.4) Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-04-28 18:07 -0700
              Logtalk big time salami slicing [For "Whales" (ultra-high rollers)?] (Was: This could be a serious security vulnerability) Mild Shock <janburse@fastmail.fm> - 2026-04-29 11:20 +0200
                Re: Logtalk big time salami slicing [For "Whales" (ultra-high rollers)?] (Was: This could be a serious security vulnerability) Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-04-30 09:13 -0700
        format/3 that does not have some Spaghetti logic (Re: Prolog PIP-0110: Its a Floating-Point Multiverse?) Mild Shock <janburse@fastmail.fm> - 2026-04-30 17:51 +0200
          Re: format/3 that does not have some Spaghetti logic (Re: Prolog PIP-0110: Its a Floating-Point Multiverse?) Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-04-30 09:11 -0700
    2025 Obituary: Skew Confluence (aka “Stews” 😆) (Re: 😂 "Plog-like" - that should be the official term!) Mild Shock <janburse@fastmail.fm> - 2025-11-07 01:40 +0100
      Backdoor Monkeys from Eternal September (Re: 2025 Obituary: Skew Confluence (aka “Stews” 😆)) Mild Shock <janburse@fastmail.fm> - 2025-11-07 10:16 +0100
        From Vibe-Coding to Vibe-Sniffing (Re: Backdoor Monkeys from Eternal September) Mild Shock <janburse@fastmail.fm> - 2025-11-07 11:08 +0100
      From Feferman to Peyton Jones, no luck with ∃ (Re: 2025 Obituary: Skew Confluence (aka “Stews” 😆)) Mild Shock <janburse@fastmail.fm> - 2025-11-08 20:35 +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:25 +0100
    Not Ross Finlayson: Pioneers Cliff B. Jones (Was: 😂 "Plog-like" - that should be the official term!) Mild Shock <janburse@fastmail.fm> - 2025-11-09 21:16 +0100

Page 2 of 3 — ← Prev page 1 [2] 3  Next page →

#640598 — 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]

#640599 — 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]

#640600 — 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]

#640601 — 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]

#640602 — 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]

#640603 — 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]

#640625 — 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]

#640626 — 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]

#640627 — 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]

#640628 — 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]

#640629 — 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]

#640630 — 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] | [next] | [standalone]

#644909 — Prolog PIP-0110: Its a Floating-Point Multiverse? [Stoic Grisu versus Rest of World] (Re: Arrow Functions can do Existential Quantifier)

Hi,

Thats was fun, maybe somebody did use the Stoic Grisu,
no delusional digits, only zeros:

/* Dogelog Player for Java, Dogelog Player for JavaScript */

?- between(95,105,N), format('~6f', [pi**N]), nl, fail; true.
169526621072093600000000000000000000000000000000.000000
532583587347989900000000000000000000000000000000.000000
1673160685434943000000000000000000000000000000000.000000
5256389317637680000000000000000000000000000000000.000000
16513434064698400000000000000000000000000000000000.000000
51878483143195920000000000000000000000000000000000.000000
162981061522046250000000000000000000000000000000000.000000
512020105551926600000000000000000000000000000000000.000000
1608558602092203000000000000000000000000000000000000.000000
5053435887201532000000000000000000000000000000000000.000000
15875837058619354000000000000000000000000000000000000.000000
true.

/* Dogelog Player for CPython, Scryer Prolog */

?- between(95,105,N), format("~6f", [pi**N]), nl, fail; true.
169526621072093604906820176085840076682051977216.000000
532583587347989896682185959640830761243896709120.000000
1673160685434943094521965146828670065372972449792.000000
5256389317637679918948413843353324366868288372736.000000
16513434064698399680249672647558109095601897472000.000000
51878483143195924744806997083865846970332907307008.000000
162981061522046250302000391689502574507182910341120.000000
512020105551926606134531253131181174736461909458944.000000
1608558602092203016045060452811678201001748662845440.000000
5053435887201532208668864202632055738347047857684480.000000
15875837058619353962143820726017670908628371861667840.000000
    true.

/* SWI-Prolog */

?- between(95,105,N), format('~6f', [pi**N]), nl, fail; true.
169526621072093767166097005299203468260062265344.000000
532583587347990464589654861887602631766932717568.000000
1673160685434944717114733438962303981153075331072.000000
5256389317637684462208165061327499331052576440320.000000
16513434064698415257140248252040994687090885132288.000000
51878483143195987052369299501797389336288857948160.000000
162981061522046416455499864803986687483065445384192.000000
512020105551927104595029672474633513664109514588160.000000
1608558602092204677580055183956519330760574013276160.000000
5053435887201537525580847342295547353575288979062784.000000
15875837058619369912879770145008145754313095225802752.000000
true.

The Prolog systems with the delusional digits made my day,
they even don't agree in the delusional digits itself.

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

#644910 — Testing NVIDIA A10G / XVM Engine v10.2.4 (Permion Federal AI) (Re: Prolog PIP-0110: Its a Floating-Point Multiverse?)

Hi,

Ok, leaving the beaten path of my Prolog system
probing, and look at some newer beast.

This looks bad:

?- format('~6f', [pi**14]), nl.
9122171.18175435

Expected result:

?- format('~6f', [pi**14]), nl.
9122171.181754

Bye

BTW: Tested using this test tester:

X-Machines Virtual Machine (XVM™) is a neurosymbolic virtual AI 
processor which combines neural processes with symbolic reasoning.
https://aws.amazon.com/marketplace/pp/prodview-6luxq22pgmehe

Mild Shock schrieb:
 >>> See also:
 >>> https://prolog-lang.org/ImprovementsForum/0110-format.html

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

#644911 — This could be a serious security vulnerability (Re: Testing NVIDIA A10G / XVM Engine v10.2.4)

Hi,

The 9122171.18175435 is a little offending, what if one
keeps a federal secret after the 6 fraction digit?

Bye

Mild Shock schrieb:
> Hi,
> 
> Ok, leaving the beaten path of my Prolog system
> probing, and look at some newer beast.
> 
> This looks bad:
> 
> ?- format('~6f', [pi**14]), nl.
> 9122171.18175435
> 
> Expected result:
> 
> ?- format('~6f', [pi**14]), nl.
> 9122171.181754
> 
> Bye
> 
> BTW: Tested using this test tester:
> 
> X-Machines Virtual Machine (XVM™) is a neurosymbolic virtual AI 
> processor which combines neural processes with symbolic reasoning.
> https://aws.amazon.com/marketplace/pp/prodview-6luxq22pgmehe
> 
> Mild Shock schrieb:
>  >>> See also:
>  >>> https://prolog-lang.org/ImprovementsForum/0110-format.html
> 
> 

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

#644912 — Re: This could be a serious security vulnerability (Re: Testing NVIDIA A10G / XVM Engine v10.2.4)

On 04/28/2026 05:38 PM, Mild Shock wrote:
> Hi,
>
> The 9122171.18175435 is a little offending, what if one
> keeps a federal secret after the 6 fraction digit?
>
> Bye
>
> Mild Shock schrieb:
>> Hi,
>>
>> Ok, leaving the beaten path of my Prolog system
>> probing, and look at some newer beast.
>>
>> This looks bad:
>>
>> ?- format('~6f', [pi**14]), nl.
>> 9122171.18175435
>>
>> Expected result:
>>
>> ?- format('~6f', [pi**14]), nl.
>> 9122171.181754
>>
>> Bye
>>
>> BTW: Tested using this test tester:
>>
>> X-Machines Virtual Machine (XVM™) is a neurosymbolic virtual AI
>> processor which combines neural processes with symbolic reasoning.
>> https://aws.amazon.com/marketplace/pp/prodview-6luxq22pgmehe
>>
>> Mild Shock schrieb:
>>  >>> See also:
>>  >>> https://prolog-lang.org/ImprovementsForum/0110-format.html
>>
>>
>

Or shaves pennies.

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

#644917 — Logtalk big time salami slicing [For "Whales" (ultra-high rollers)?] (Was: This could be a serious security vulnerability)

Hi,


Ross Finlayson schrieb:
 > Or shaves pennies.

 >>> X-Machines Virtual Machine (XVM™) is a neurosymbolic virtual AI
 >>> processor which combines neural processes with symbolic reasoning.
 >>> https://aws.amazon.com/marketplace/pp/prodview-6luxq22pgmehe

Cost/hour: $200,000.00

LoL

Bye

P.S.: If it could do some quant trading magic, one would
possibly pay so much. But Logtalk is simply too lame:

Version release notes
XVM Engine v10.2.4 is the full engine capable of running
all XVM and Logtalk programs, excluding for logtalk tools.

> On 04/28/2026 05:38 PM, Mild Shock wrote:
>> Hi,
>>
>> The 9122171.18175435 is a little offending, what if one
>> keeps a federal secret after the 6 fraction digit?
>>
>> Bye
>>
>> Mild Shock schrieb:
>>> Hi,
>>>
>>> Ok, leaving the beaten path of my Prolog system
>>> probing, and look at some newer beast.
>>>
>>> This looks bad:
>>>
>>> ?- format('~6f', [pi**14]), nl.
>>> 9122171.18175435
>>>
>>> Expected result:
>>>
>>> ?- format('~6f', [pi**14]), nl.
>>> 9122171.181754
>>>
>>> Bye
>>>
>>> BTW: Tested using this test tester:
>>>
>>> X-Machines Virtual Machine (XVM™) is a neurosymbolic virtual AI
>>> processor which combines neural processes with symbolic reasoning.
>>> https://aws.amazon.com/marketplace/pp/prodview-6luxq22pgmehe
>>>
>>> Mild Shock schrieb:
>>>  >>> See also:
>>>  >>> https://prolog-lang.org/ImprovementsForum/0110-format.html
>>>
>>>
>>
> 
> Or shaves pennies.
> 
> 

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

#644933 — Re: Logtalk big time salami slicing [For "Whales" (ultra-high rollers)?] (Was: This could be a serious security vulnerability)

On 04/29/2026 02:20 AM, Mild Shock wrote:
> Hi,
>
>
> Ross Finlayson schrieb:
>  > Or shaves pennies.
>
>  >>> X-Machines Virtual Machine (XVM™) is a neurosymbolic virtual AI
>  >>> processor which combines neural processes with symbolic reasoning.
>  >>> https://aws.amazon.com/marketplace/pp/prodview-6luxq22pgmehe
>
> Cost/hour: $200,000.00
>
> LoL
>
> Bye
>
> P.S.: If it could do some quant trading magic, one would
> possibly pay so much. But Logtalk is simply too lame:
>
> Version release notes
> XVM Engine v10.2.4 is the full engine capable of running
> all XVM and Logtalk programs, excluding for logtalk tools.
>
>> On 04/28/2026 05:38 PM, Mild Shock wrote:
>>> Hi,
>>>
>>> The 9122171.18175435 is a little offending, what if one
>>> keeps a federal secret after the 6 fraction digit?
>>>
>>> Bye
>>>
>>> Mild Shock schrieb:
>>>> Hi,
>>>>
>>>> Ok, leaving the beaten path of my Prolog system
>>>> probing, and look at some newer beast.
>>>>
>>>> This looks bad:
>>>>
>>>> ?- format('~6f', [pi**14]), nl.
>>>> 9122171.18175435
>>>>
>>>> Expected result:
>>>>
>>>> ?- format('~6f', [pi**14]), nl.
>>>> 9122171.181754
>>>>
>>>> Bye
>>>>
>>>> BTW: Tested using this test tester:
>>>>
>>>> X-Machines Virtual Machine (XVM™) is a neurosymbolic virtual AI
>>>> processor which combines neural processes with symbolic reasoning.
>>>> https://aws.amazon.com/marketplace/pp/prodview-6luxq22pgmehe
>>>>
>>>> Mild Shock schrieb:
>>>>  >>> See also:
>>>>  >>> https://prolog-lang.org/ImprovementsForum/0110-format.html
>>>>
>>>>
>>>
>>
>> Or shaves pennies.
>>
>>
>

Those "traders" who seek "liquidity"
and "investors" who seek "safety",
have that those traders weren't investors
and now there's no liquidity and they got no safety
and now they get nothing.

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

#644930 — format/3 that does not have some Spaghetti logic (Re: Prolog PIP-0110: Its a Floating-Point Multiverse?)

Hi,

How it started:

Trealla Prolog is being updated for the
proposal (only failing some of the table
related tests as of v2.85.19).

How its going:

The test case for ~r and ~R are useless.
Very bad converage for a format/3 that does
not have some Spaghetti logic. Big integer

and negative numbers missing. Now I find:
```
/* Trealla Prolog v2.94.3 */
?- format('~11R', [-7625597484987]), nl.
%%% crash
```
Main problem how does one get coverage
without thinking? Copying from "ghost" Quintus
manual doesn't assure coverage. Theoretically

a coverage tool, that shows code coverage when
a test suite is run, would help. Still it might
not capture certain data points if the code

doesn't have according branching. So it needs
either more human effort or fuzz testing.

https://de.wikipedia.org/wiki/Fuzzing

Bye

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

#644932 — Re: format/3 that does not have some Spaghetti logic (Re: Prolog PIP-0110: Its a Floating-Point Multiverse?)

On 04/30/2026 08:51 AM, Mild Shock wrote:
> Hi,
>
> How it started:
>
> Trealla Prolog is being updated for the
> proposal (only failing some of the table
> related tests as of v2.85.19).
>
> How its going:
>
> The test case for ~r and ~R are useless.
> Very bad converage for a format/3 that does
> not have some Spaghetti logic. Big integer
>
> and negative numbers missing. Now I find:
> ```
> /* Trealla Prolog v2.94.3 */
> ?- format('~11R', [-7625597484987]), nl.
> %%% crash
> ```
> Main problem how does one get coverage
> without thinking? Copying from "ghost" Quintus
> manual doesn't assure coverage. Theoretically
>
> a coverage tool, that shows code coverage when
> a test suite is run, would help. Still it might
> not capture certain data points if the code
>
> doesn't have according branching. So it needs
> either more human effort or fuzz testing.
>
> https://de.wikipedia.org/wiki/Fuzzing
>
> Bye

Fuzzy Wuzzy was a bear, ....

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

Page 2 of 3 — ← Prev page 1 [2] 3  Next page →

Back to top | Article view | sci.math

csiph-web