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

Groups > sci.physics.relativity > #667187

Prolog semantics is 3-valued or intuitionistic [Feferman prefers partial logic] (Was: You have to check Feferman OST [Paradox Hunting])

Cross-posted to 3 groups.

Show all headers | View raw

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