From Newsgroup: sci.logic

On 06/25/2015 06:00 PM, X.Y. Newberry wrote:

George Greene wrote:

On Wednesday, June 24, 2015 at 9:41:07 PM UTC-4, Newberry wrote:

Furthermore Enderton states that in PA and even in PA minus induction
the diagonal lemma is provable, i.e.

|- sigma <--> beta(#sigma)

"PA minus induction" is generally called "Robinson Arithmetic"; that
system
is often denoted by a capital Q, and it seems to be THE WEAKEST system
that
is STRONG enough to prove the diagonal lemma. PLEASE SEE here:
https://en.wikipedia.org/wiki/Robinson_arithmetic#Metamathematics

If I am reading it correctly he means that every instance of this schema >>> is provable.

That's right; it's provable for every definable unary predicate beta(.).

I of course claim that there are logics where
the diagonal lemma does not hold.

That claim is hardly original with you.

Would you care to share with us the original claim?

We were just talking about standard classical vanilla first-order logic.
But any system strong enough to make all these recursive functions
representable
will allow the proof to through.

--- Synchronet 3.22a-Linux NewsLink 1.2

From Newsgroup: sci.logic

On 09/28/2026 11:34 AM, Ross Finlayson wrote:

On 06/25/2015 06:00 PM, X.Y. Newberry wrote:

George Greene wrote:

On Wednesday, June 24, 2015 at 9:41:07 PM UTC-4, Newberry wrote:

Furthermore Enderton states that in PA and even in PA minus induction
the diagonal lemma is provable, i.e.

|- sigma <--> beta(#sigma)

"PA minus induction" is generally called "Robinson Arithmetic"; that
system
is often denoted by a capital Q, and it seems to be THE WEAKEST system
that
is STRONG enough to prove the diagonal lemma. PLEASE SEE here:
https://en.wikipedia.org/wiki/Robinson_arithmetic#Metamathematics

If I am reading it correctly he means that every instance of this
schema
is provable.

That's right; it's provable for every definable unary predicate beta(.). >>>

I of course claim that there are logics where
the diagonal lemma does not hold.

That claim is hardly original with you.

Would you care to share with us the original claim?

We were just talking about standard classical vanilla first-order logic. >>> But any system strong enough to make all these recursive functions
representable
will allow the proof to through.

Induction can be arrived at via inverse from the outset.

Induction, the naive, always admits counter-induction besides
co-induction, then for simply classifying where counter- and
co-induction do or don't exist, besides the naive where it's
also "co-" and ignores "counter-".


--- Synchronet 3.22a-Linux NewsLink 1.2