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

Groups > sci.physics.relativity > #667184

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