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

Groups > sci.physics.relativity > #667138

Re: 2.1 Logical variables and equations (Re: Clueless Moron and Paid Putin Troll)

Cross-posted to 2 groups.

Show all headers | View raw

Hi,

We can though prove in FOL:

∀y∃!x x = f(y)

Another example with existence,
that doesn't boil down to unique
existence, is this here:

∃x∃y(x = f(y))

One might find it in Prolog as
X = f(_) with an anonymous variable _.
Now its not possible to derive:

/* Not Generally Valid */
∃!x∃y(x = f(y))

Bye

Mild Shock schrieb:
> Hi,
> 
> A Prolog logical variable is not immutable,
> it transitions all the time from uninstantiated
> to instantiated, during unification.
> 
> Also the value the logical variable represents
> is not immutable, since it might point to a
> Prolog term which is non-ground, this
> 
> Prolog term might have other Prolog logical variables,
> which do also such transitions, making the
> while Prolog term transitioniong from less ground
> 
> to more ground, or even worse to a larger
> term with even more Prolog logical variables,
> and so on, leading to the phaenomenon of
> 
> perpetual processes or concurrent logic programming.
> In particular the existence quantifier ∃ in logic
> programming is not unique existence ∃!. For
> 
> example the following is true:
> 
> ∃x x = f(y)
> 
> But x has not a "single value", the existence
> is more witness to of a kind of skolem function
> dependency, namely that for each y, there
> 
> is some f(y). What they write is only useful
> for a certained moded form of Prolog and unification,
> where the equations have unique existence of
> 
> ground terms or some other value domain.
> 
> Bye
> 
> Mild Shock schrieb:
>> Hi,
>>
>> Its their take of Logical variable, which
>> might not be the same as a Prolog logical variable.
>>
>> ------------------ cut here ----------------
>>
>> 2.1 Logical variables and equations
>> A program executes by solving its equations, using
>> the process of unification. For example,
>>
>> ∃x y z. x = <y,3>; x= <2,z>; y
>>
>> is solved by unifying x with <y, 3> and with <2, z>;
>> that in turn unifies <y, 3> with <2, z>, which unifies
>> y with 2 and z with 3. Finally, 2 is returned as the
>> result. Note carefully that, as in any declarative
>> language, logical variables are not mutable; a logical
>> variable stands for a single, immutable value.
>>
>> We use "∃" to bring a fresh logical variable into
>> scope, because we really mean "there exists an x
>> such that .... "
>>
>> ------------------ cut here ----------------
>>
>> Of course the above is utter nonsense, written
>> from somebody who doesn't know what a Prolog logical
>> variable is, shifting in the same sentence from
>>
>> the attribution of "immutable" of a variable, to
>> the attribution of "immutable" of the value
>> of a variable. This is quite hillarious.
>>
>> Bye
>>
>> Mild Shock schrieb:
>>> Hi,
>>>
>>> Its from this paper:
>>>
>>> The Verse Calculus:a Core Calculus for Functional Logic Programming
>>> SIMON PEYTON JONES, Epic Games, United Kingdom
>>> GUY STEELE, Oracle Labs, USA
>>> https://simon.peytonjones.org/assets/pdfs/verse-March23.pdf
>>>
>>> Don't blame me for what they write.
>>> But mostlikely your eruption is just from
>>> a clueless Nazi Retard, namely the paid
>>>
>>> troll you are, getting money from Putin.
>>>
>>> Bye
>>>
>>> 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