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

Groups > sci.math > #640630

In Prolog you don't need the down arrow t↓ (Was: Prolog semantics is 3-valued or intuitionistic)

Cross-posted to 3 groups.

Show all headers | View raw

Hi,

In Prolog you don't need the down arrow t↓ .
Since you anyway don't have functions.
You can either throw an error for division

by zero or you can fail. This is important
for constraint logic programming. You will
indeed have some partial term effects,

when your constraint implies division by zero,
for example if you ask SWI-Prolog for:

?- 6 #= 2*X

It will probably give you X = 3. On the other
hand if you ask SWI-Prolog for:

?- 6 #= 0*X

It should fail.

Bye

Mild Shock schrieb:
> Hi,
> 
> But Prolog semantics is often taken 3-valued
> or intuitionistic. And what is a Paradox in
> classical logic with an absurdity result,
> 
> might be only a looping Prolog text when
> executed in a Prolog prozessor. For example
> this extended Horn Clause, Horn Clause with
> 
> negation as failure, here (the Liar):
> 
> p :- \+ p
> 
> Has a Clark completion which does not have a model:
> 
> p <-> ~p
> 
> In Feferman OST you find the looping somehow
> expressed as free logic, i.e. there is an
> operator down arrow ↓, and t↓ expresses
> 
> that t has a value. Used by Beeson for example
> in an exemplar number theory to express that
> division exists as long as you don't divide by
> 
> zero, and Feferman refers to Beeson:
> 
> 7. The Logic of Partial Terms
> y ≠ 0 → x/y ↓
> https://www.michaelbeeson.com/research/papers/LambdaLogicOriginal.pdf
> 
> But for practical purposes this can be a
> can of worms, and modern theorem provers have
> an Option type which is for example:
> 
> Option<T> = nothing | just(T)
> 
> The can might be confusion of non-termination
> with not in the domain of a function. Especially
> when your logic and/or theory has constructivity
> 
> and non-constructivity side by side. Which is
> usually the case in program verification, and
> specification can be non-constructive, while
> 
> a Program code can be constructive,
> 
> Bye
> 
> Mild Shock schrieb:
>> Hi,
>>
>> You are still hunting Paradoxes, is
>> this still a noble occupation?
>> You have to check Feferman OST etc..
>>
>> The statement is only, that for A,
>> formula, there exists t_A a term,
>> such that:
>>
>> t_A(x) = tt <=> A(x)
>>
>> Gödel used the same, t_A is nothing
>> else than a Gödelization of A. Only
>> in Gödel numbers were used, and Gödel
>>
>> usually written as {A}. And already
>> Gödel showed before Curry all kind of
>> fixpoint paradoxes. But Feferman does
>>
>> not allow arbitrary A, and a modern
>> branch of Feferman OST would be Reverse
>> mathematics having a bunch of allowed
>>
>> or disallowed forms of A. What Feferman
>> OST shows if he makes small large cardinals
>> plausible, he shows of course also
>>
>> that the thingy is not inconsistent, i.e.
>> has no Paradox under certain circumstances.
>>
>> Have Fun!
>>
>> Bye
>>
>> BTW: OST is related to Gödels constructive
>> universe L, and papers such as these are
>> full of V = L assumptions:
>>
>> https://home.inf.unibe.ch/gerhard.jaeger/16-relativizing_OST.pdf
>>
>> But I don't know how substantial the stuff
>> there is. I only use the fact that t is a term,
>> and then terms in my Prolog system Dogelog Player
>>
>> correspond to compiled code. So t_A is basically
>> not anymore the original formula A, as already in
>> OST, but its not so much viewed as a Gödelization
>>
>> out of the blue, more as a code for some Prolog machine.
>>
>> Ross Finlayson schrieb:
>>> 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.math | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread

Thread

😂 "Plog-like" - that should be the official term! Mild Shock <janburse@fastmail.fm> - 2025-10-08 01:15 +0200
  How deep seek went bonkers (Was: 😂 "Plog-like" - that should be the official term!) Mild Shock <janburse@fastmail.fm> - 2025-10-08 01:21 +0200
    Re: How deep seek went bonkers (Was: 😂 "Plog-like" - that should be the official term!) "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2025-10-07 18:30 -0700
  Declarative farts versus MSI Claw AI+, who would win? (Re: 😂 "Plog-like" - that should be the official term!) Mild Shock <janburse@fastmail.fm> - 2025-10-23 14:38 +0200
    Gameified AI Engineers brains blown out [Kurzweil's 2045 Prediction] (Re: Declarative farts versus MSI Claw AI+, who would win?) Mild Shock <janburse@fastmail.fm> - 2025-10-23 15:23 +0200
      The intelligent Cloud, Fog and Edge is evolving (Re: Gameified AI Engineers brains blown out [Kurzweil's 2045 Prediction]) Mild Shock <janburse@fastmail.fm> - 2025-10-24 11:40 +0200
        More Dreams: LLM + Chess = LRM (Re: The intelligent Cloud, Fog and Edge is evolving) Mild Shock <janburse@fastmail.fm> - 2025-10-25 12:52 +0200
          Not for Boris the Loris and Julio the Nazi Retared (Re: More Dreams: LLM + Chess = LRM) Mild Shock <janburse@fastmail.fm> - 2025-10-25 13:10 +0200
    Logtalks Corleone "olive oil business" [Missed the DOP Bandwagon] (Re: Declarative farts versus MSI Claw AI+) Mild Shock <janburse@fastmail.fm> - 2026-04-29 11:32 +0200
      Logtalk is over engineered in a bad sense [Where are the test results] (Re: Logtalks Corleone "olive oil business") Mild Shock <janburse@fastmail.fm> - 2026-04-29 11:55 +0200
        Logtalk just creates its own island of PlUnit (Re: Logtalk is over engineered in a bad sense) Mild Shock <janburse@fastmail.fm> - 2026-04-29 12:11 +0200
          The mechanic with the Vacuum Hypothesis (Re: Logtalk just creates its own island of PlUnit) Mild Shock <janburse@fastmail.fm> - 2026-04-29 12:53 +0200
            Layoff Tsunami and Defunding Rounds [Burger jobs] (Re: The mechanic with the Vacuum Hypothesis) Mild Shock <janburse@fastmail.fm> - 2026-04-29 13:17 +0200
  Arrow Functions can do Existential Quantifier (Re: 😂 "Plog-like" - that should be the official term!) Mild Shock <janburse@fastmail.fm> - 2025-11-06 14:32 +0100
    Resolving Ambiguity in Negation as Failure (Re: Arrow Functions can do Existential Quantifier) Mild Shock <janburse@fastmail.fm> - 2025-11-06 14:33 +0100
      Future Outlook of Logic Programming (Re: Resolving Ambiguity in Negation as Failure) Mild Shock <janburse@fastmail.fm> - 2025-11-06 14:35 +0100
    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
      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
    Prolog PIP-0110: Its a Floating-Point Multiverse? [Stoic Grisu versus Rest of World] (Re: Arrow Functions can do Existential Quantifier) Mild Shock <janburse@fastmail.fm> - 2026-04-29 00:41 +0200
      Testing NVIDIA A10G / XVM Engine v10.2.4 (Permion Federal AI) (Re: Prolog PIP-0110: Its a Floating-Point Multiverse?) Mild Shock <janburse@fastmail.fm> - 2026-04-29 02:15 +0200
        This could be a serious security vulnerability (Re: Testing NVIDIA A10G / XVM Engine v10.2.4) Mild Shock <janburse@fastmail.fm> - 2026-04-29 02:38 +0200
          Re: This could be a serious security vulnerability (Re: Testing NVIDIA A10G / XVM Engine v10.2.4) Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-04-28 18:07 -0700
            Logtalk big time salami slicing [For "Whales" (ultra-high rollers)?] (Was: This could be a serious security vulnerability) Mild Shock <janburse@fastmail.fm> - 2026-04-29 11:20 +0200
              Re: Logtalk big time salami slicing [For "Whales" (ultra-high rollers)?] (Was: This could be a serious security vulnerability) Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-04-30 09:13 -0700
      format/3 that does not have some Spaghetti logic (Re: Prolog PIP-0110: Its a Floating-Point Multiverse?) Mild Shock <janburse@fastmail.fm> - 2026-04-30 17:51 +0200
        Re: format/3 that does not have some Spaghetti logic (Re: Prolog PIP-0110: Its a Floating-Point Multiverse?) Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-04-30 09:11 -0700
  2025 Obituary: Skew Confluence (aka “Stews” 😆) (Re: 😂 "Plog-like" - that should be the official term!) Mild Shock <janburse@fastmail.fm> - 2025-11-07 01:40 +0100
    Backdoor Monkeys from Eternal September (Re: 2025 Obituary: Skew Confluence (aka “Stews” 😆)) Mild Shock <janburse@fastmail.fm> - 2025-11-07 10:16 +0100
      From Vibe-Coding to Vibe-Sniffing (Re: Backdoor Monkeys from Eternal September) Mild Shock <janburse@fastmail.fm> - 2025-11-07 11:08 +0100
    From Feferman to Peyton Jones, no luck with ∃ (Re: 2025 Obituary: Skew Confluence (aka “Stews” 😆)) Mild Shock <janburse@fastmail.fm> - 2025-11-08 20:35 +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:25 +0100
  Not Ross Finlayson: Pioneers Cliff B. Jones (Was: 😂 "Plog-like" - that should be the official term!) Mild Shock <janburse@fastmail.fm> - 2025-11-09 21:16 +0100

csiph-web