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

Groups > sci.physics.relativity > #667185

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

Cross-posted to 3 groups.

Show all headers | View raw

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

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

Thread

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

csiph-web