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

Groups > sci.math > #640625

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

Cross-posted to 3 groups.

Show all headers | View raw

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

Back to sci.math | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread

Thread

😂 "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

csiph-web