Re: Formal systems that cannot possibly be incomplete except for unknowns and unknowable

On 07/05/2025 19:17, Mr Flibble wrote:

On Wed, 07 May 2025 19:14:54 +0100, Richard Heathfield wrote:
 

On 07/05/2025 18:55, olcott wrote:

When THERE IS NO CONTRADICTION then proof by contradiction fails.
How do you not get that?

>
I do. You must be talking about the Olcott Problem again, because the
contradiction is inherent in the Halting Problem.
>
It starts with the assumption that a universal halt decider can be
written, and then shows that such a decider can be used to devise a
program that the 'universal' decider can't decide --- a contradiction.
>
But you already know all this.

 The contradiction you speak of is *ill-formed*

No, it's perfectly well-formed.

due to it being a category
(type) error;

No, it's not an error. It's a contradiction.

as such it cannot be used in any proof.

It already has been.
You can impose all the rules you like on your own subset of logic, but you don't get to decide rules for the rest of us.
--
Richard Heathfield
Email: rjh at cpax dot org dot uk
"Usenet is a strange place" - dmr 29 July 1999
Sig line 4 vacant - apply within