XPost: sci.logic, sci.math   
   From: janburse@fastmail.fm   
      
   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   
      
   [continued in next message]   
      
   --- SoupGate-DOS v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)