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

Groups > sci.math > #640626

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

Cross-posted to 3 groups.

Show all headers | View raw

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

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