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

Groups > sci.physics.relativity > #667188

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.physics.relativity | Previous | Next — Previous 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