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

Groups > sci.physics.relativity > #667177

The quantifer ∃ is just the Combinator K (Schönfinkels C)? (Re: From Feferman to Peyton Jones, no luck with ∃)

Show all headers | View raw

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

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