Re: Within Proof Theoretic Semantics Gödel's G has n o meaning in PA

On 07/05/2026 03:55 PM, olcott wrote:
> On 7/5/2026 5:15 PM, Ross Finlayson wrote:
>> On 07/05/2026 02:45 PM, olcott wrote:
>>> On 7/5/2026 4:30 PM, Ross Finlayson wrote:
>>>> On 07/05/2026 01:25 PM, olcott wrote:
>>>>> On 7/5/2026 2:56 PM, Ross Finlayson wrote:
>>>>>> On 07/05/2026 09:33 AM, olcott wrote:
>>>>>>> On 7/5/2026 9:52 AM, Tristan Wibberley wrote:
>>>>>>>> On 04/07/2026 16:31, Tristan Wibberley wrote:
>>>>>>>>> On 06/05/2026 20:37, Julio Di Egidio wrote:
>>>>>>>>>> On 02/05/2026 20:47, Scott Hoge wrote:
>>>>>>>>>>
>>>>>>>>>>> In Cantor's theorem, we do not actually construct a diagonal.
>>>>>>>>>>> Rather, we presuppose that we can enumerate a set, and then,
>>>>>>>>>>> /purely on the grounds of possibility/, conceive a diagonalized
>>>>>>>>>>> non-element.
>>>>>>>>>>
>>>>>>>>>> Nope, as explained and re-explained ad nauseam around here:
>>>>>>>>>> just the resident trolls won't get it.
>>>>>>>>>>
>>>>>>>>>> Cantor's diagonal argument, the one with the binary sequences,
>>>>>>>>>> is indeed constructive: a definition of anti-diagonal of *any*
>>>>>>>>>> (infinite) list is provided, and the proof that the anti-diagonal
>>>>>>>>>> cannot be in the list is quite constructive.
>>>>>>>>>
>>>>>>>>> "quite" but not "completely".
>>>>>>>>>
>>>>>>>>> A constructive operation is defined, but a diagonal number is
>>>>>>>>> constructed just when that constructive operation is applied to a
>>>>>>>>> constructible list.
>>>>>>>>
>>>>>>>> I should note for the less knowledgable readers of course it's less
>>>>>>>> often than that, it is only that often for systems such as the one
>>>>>>>> Julio
>>>>>>>> and Phoenix are using which allows dequantification of universally
>>>>>>>> quantified statements into the system proper which then have
>>>>>>>> derivable
>>>>>>>> statements containing actual constructions of the constructible
>>>>>>>> objects
>>>>>>>> they apply to by virtue of their original quantification. Of
>>>>>>>> course,
>>>>>>>> dequantification of fantastically quantified statements doesn't
>>>>>>>> make a
>>>>>>>> statement about nonconstructible objects because there aren't any
>>>>>>>> outside of the fantastical quantification.
>>>>>>>>
>>>>>>>> By which I don't mean to argue the countability of the set of
>>>>>>>> reals as
>>>>>>>> defined in what we call Cantor's Proof of the Uncountability of the
>>>>>>>> Reals to include objects quantified over by fantatstical
>>>>>>>> quantification
>>>>>>>> but not by universal quantification, but it does make some meaning
>>>>>>>> clearer.
>>>>>>>>
>>>>>>>> While some of the sets might have objects in the system proper,
>>>>>>>> some of
>>>>>>>> the members of some of the sets clearly do not.
>>>>>>>>
>>>>>>>
>>>>>>> % This sentence is not true.
>>>>>>> ?- LP = not(true(LP)).
>>>>>>> LP = not(true(LP)).
>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>>>>> false.
>>>>>>>
>
>>
>> Gemini agrees with not-you.
>>
>>
>
> OK then the point that I was trying to make is
> exactly what Gemini said right here:
> https://share.gemini.google/1dJnMwOZ2k5F
>
>
>
>

I tend not to follow links like that, post the transcript.


Point being though that "Prawitz' PTS" has _recovery_ and
the outer products not just inner products, since complementary
duals, and that accounts of inductive ignorance and _elimination_
are not full accounts of logic.


About what's "agreeably arguable" and "arguably agreeable",
try Claude instead, or Kimi, either less "automatically agreeable"
then Gemini or Grok, where ChatGPT is about in the middle, then
though that they're all quite alike as model reasoners.


Anyways language includes its own account within itself,
so there are first-class models of cycles, and then that
the resolution of mathematical paradox ends-with there
not being any, not starts-with there not being any.


Then, novelty has that simply repeating the argument
does not strengthen it, indeed, it weakens it,
then the fact that "LP" its assignment trivially
short-circuits to not-true-LP resulting false
then is nothing. I.e., that implementation just balks
since its type system has no context, not having
context first-class itself.




About the un-countability of the complete-ordered-field
or "field-reals" yet countability of a continuous domain
like "line-reals", basically has that "non-Cartesian functions"
exist in accounts of the continuous and for geometry,
which simply has that primitive-recursive-arithmetic
and its usual account of Cartesian functions (elements re-move-able,
mappings re-order-able) doesn't suffice to describe geometric relation.


So, it's a theorem in any account of descriptive set theory
"strong enough for geometry" that the existence of non-Cartesian
functions is a theorem, then that there are models of continuous
domains (extent, density, completeness, measure) that are countable
like the line-reals, un-countable like the field-reals, and variously
countable and un-countable and even of greater cardinality like
the signal-reals, since there exist non-Cartesian functions so
it's entirely consistent their existence together, that since
they have constructive demonstractions each, otherwise would
simply, and always, contradict each other.



So, any account of theory intending to describe mathematics
results having line-reals, field-reals, and signal-reals,
about the nature of the continuous and discrete after
the nature of the infinite and finite.



Then, "Russell's retro-thesis" is similarly a retro-finitist's,
wishing what's so, here it's called "hypocritical".