Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!eternal-september.org!.POSTED!not-for-mail
From: Richard Heathfield <rjh@cpax.org.uk>
Newsgroups: comp.theory
Subject: Re: Formal systems that cannot possibly be incomplete except for
 unknowns and unknowable
Date: Wed, 7 May 2025 19:32:09 +0100
Organization: Fix this later
Lines: 38
Message-ID: <vvg8v9$158tp$5@dont-email.me>
References: <vv97ft$3fg66$1@dont-email.me>
 <b47c9e70d415c1e5e469aaab846f0bd05e4bcc51@i2pn2.org>
 <vvall0$o6v5$1@dont-email.me> <vvc33h$25atc$1@dont-email.me>
 <vvcgja$1voc$1@news.muc.de> <vvd6pf$34l9k$1@dont-email.me>
 <vvdads$13pc$1@news.muc.de> <vvdcld$3arjo$1@dont-email.me>
 <vvg6r9$15e69$1@dont-email.me> <vvg7uu$158tp$4@dont-email.me>
 <SsNSP.398812$4AM6.210386@fx17.ams4>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Wed, 07 May 2025 20:32:09 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="1de3d45e2783553e22f3c2216cb20b34";
	logging-data="1221561"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1+ZTLV8PoxmBIxAbHgJNGXtlxi/Hk1iUmIikhh4RxYtyw=="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:3cXBCKP8PZ+RF783Vfmxe37CUAQ=
Content-Language: en-GB
In-Reply-To: <SsNSP.398812$4AM6.210386@fx17.ams4>
Bytes: 2580

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