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


Groups > sci.physics.relativity > #667186

You have to check Feferman OST [Paradox Hunting] (Was: CET is also needed)

From Mild Shock <janburse@fastmail.fm>
Newsgroups sci.physics.relativity, sci.logic, sci.math
Subject You have to check Feferman OST [Paradox Hunting] (Was: CET is also needed)
Date 2025-11-09 19:57 +0100
Message-ID <10eqo5s$1mbe$1@solani.org> (permalink)
References (5 earlier) <10eo92q$5dr2$3@solani.org> <ybCdnaDnPLr1Z5L0nZ2dnZfqnPti4p2d@giganews.com> <10eq01f$15ek$1@solani.org> <10eq087$15hs$1@solani.org> <_eicnVLpOupeII30nZ2dnZfqn_WdnZ2d@giganews.com>

Cross-posted to 3 groups.

Show all headers | View raw


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