Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > sci.physics.relativity > #667186
| 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.
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
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