Path: news.eternal-september.org!eternal-september.org!feeder3.eternal-september.org!news.quux.org!news.nk.ca!rocksolid2!i2pn2.org!.POSTED!not-for-mail
From: Richard Damon <richard@damon-family.org>
Newsgroups: sci.logic,sci.math
Subject: Re: Proving the consistency of the body of knowledge expressed in
 language
Date: Tue, 1 Apr 2025 21:03:44 -0400
Organization: i2pn2 (i2pn.org)
Message-ID: <5291692f30e9ce584a11767533cd27d2070117a6@i2pn2.org>
References: <vrfvbd$256og$2@dont-email.me> <vrh432$39r47$1@dont-email.me>
 <vrhami$3fbja$2@dont-email.me> <vrj9lu$1791p$1@dont-email.me>
 <vrjn82$1ilbe$2@dont-email.me> <vrmpc1$bnp3$1@dont-email.me>
 <vrmteo$cvat$6@dont-email.me> <vru000$33rof$1@dont-email.me>
 <vrug71$3gia2$6@dont-email.me>
 <0306c3c2d4a6d05a8bb7441c0b23d325aeac3d7b@i2pn2.org>
 <vrvnvv$ke3p$1@dont-email.me> <vs0egm$1cl6q$1@dont-email.me>
 <vs1f7j$296sp$2@dont-email.me> <vs3ad6$2o1a$1@dont-email.me>
 <vs4sjd$1c1ja$8@dont-email.me> <vs63o2$2nal3$1@dont-email.me>
 <vs6v2l$39556$17@dont-email.me> <vs8hia$13iam$1@dont-email.me>
 <vs8uoq$1fccq$2@dont-email.me> <vsb4in$14lqk$1@dont-email.me>
 <vsb9d5$19ka5$1@dont-email.me>
 <04aa9edbe77f4e701297d873264511f820d85526@i2pn2.org>
 <vsbu9j$1vihj$1@dont-email.me> <vsdlso$3shbn$2@dont-email.me>
 <vsen5l$th5g$5@dont-email.me> <vsg1b2$2ed9k$1@dont-email.me>
 <vsh9c9$3mdkb$2@dont-email.me>
 <3c542bc45e3edfbb46a0fee714003c202dd30773@i2pn2.org>
 <vshsfd$90ss$2@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Wed, 2 Apr 2025 01:15:36 -0000 (UTC)
Injection-Info: i2pn2.org;
	logging-data="2747098"; mail-complaints-to="usenet@i2pn2.org";
	posting-account="diqKR1lalukngNWEqoq9/uFtbkm5U+w3w6FQ0yesrXg";
User-Agent: Mozilla Thunderbird
In-Reply-To: <vshsfd$90ss$2@dont-email.me>
X-Spam-Checker-Version: SpamAssassin 4.0.0
Content-Language: en-US

On 4/1/25 7:22 PM, olcott wrote:
> On 4/1/2025 5:30 PM, Richard Damon wrote:
>> On 4/1/25 1:56 PM, olcott wrote:
>>> On 4/1/2025 1:33 AM, Mikko wrote:
>>>> On 2025-03-31 18:33:26 +0000, olcott said:
>>>>
>>>>>
>>>>> Anything the contradicts basic facts or expressions
>>>>> semantically entailed from these basic facts is proven
>>>>> false.
>>>>
>>>> Anything that follows from true sentences by a truth preserving
>>>> transformations is true. If you can prove that a true sentence
>>>> is false your system is unsound.
>>>>
>>>
>>> Ah so we finally agree on something.
>>> What about the "proof" that detecting inconsistent
>>> axioms is impossible? (I thought that I remebered this).
>>>
>>
>> No, the proof is that it is impossible to prove that a system is 
>> consistant. (sort of the opposite of what you are thinking of).
>>
>> Proving inconsistancy is easy, you just need one example.
>>
>> Proving the non-existance isn't as easy, and for a complicated enough 
>> system, can't be done, as you need to search an infinite space for the 
>> problem, which we can't be sure we have finished,
>>
> 
> I have always only been referring to the consistency
> of a finite set of axioms. Just test each one against
> all the others. When we use a type hierarchy we only
> have to do this for axioms with compatible types.

And, if they can support the needed level of logic, Godel has shown that 
they can not prove their own consistancy.

> 
> If we are only allowed to apply the single truth
> preserving operation of semantic logical entailment
> then we know the whole system must be consistent.
> https://en.wikipedia.org/wiki/Logical_consequence#Semantic_consequence

You mean your logic has no "And" or "Or" or "Not" operations?

> 
> We bypass any need for model theory by having the full
> semantics embedded directly in the formal language.

Not sure you can do that. You haven't been very good at being right in 
the past.

So, which step of Tarski's proof doesn't follow that requirement?

(Not that you disagree with his conclusion, but is logical operation 
violated this rule).

> 
>> Sort of like we can easily prove that a machine halts, but simulating 
>> it to that point (like a real emulator can do for DDD), but showing 
>> that a machine is non-halting can be more of a problem. Sometimes we 
>> can find an induction property to let us prove it, but not always.
> 
>