Path: news.eternal-september.org!eternal-september.org!.POSTED!not-for-mail
From: Mikko <mikko.levanto@iki.fi>
Newsgroups: sci.logic
Subject: Re: How a True(X) predicate can be defined for the set of analytic knowledge
Date: Fri, 4 Apr 2025 11:43:32 +0300
Organization: -
Lines: 111
Message-ID: <vso63k$31vm4$1@dont-email.me>
References: <vrfvbd$256og$2@dont-email.me> <vsckdc$2l3cb$1@dont-email.me> <cd467496ff18486f746047b3b1affc4927981c0c@i2pn2.org> <vsct12$2ub5m$1@dont-email.me> <3ab00594a6cdaa3ca8aa32da86b865f3a56d5159@i2pn2.org> <vsd1p9$379dn$3@dont-email.me> <45167877871179050e15837d637c4c8a22e661fd@i2pn2.org> <vsenb0$th5g$7@dont-email.me> <4c1393a97bc073e455df99e0a2d3a47bfc71d940@i2pn2.org> <vsfe66$1m8qr$4@dont-email.me> <7286761fb720294d7a87d883fc82c8f8cf95a460@i2pn2.org> <vsfl7f$1s8b0$3@dont-email.me> <6edcdf0fa4f6ec503240b27a5801f93c470ed7d6@i2pn2.org> <vsh931$3mdkb$1@dont-email.me> <vsivgk$1fjla$1@dont-email.me> <vsjmtj$26s7s$2@dont-email.me> <a4fce1db1fdba9c5eba3e64dc7dba83caff192cf@i2pn2.org> <vskobk$378kj$4@dont-email.me> <ad60872952cbc941149035f6569a7bd4d21766f2@i2pn2.org> <vskt3k$378kj$14@dont-email.me> <82f475a36dde2b1f95ea47820f94c20f15f519db@i2pn2.org> <vsl2mu$3o5ji$2@dont-email.me> <9f9c8721a1e0f985d6e66ccc705335c4e9d15996@i2pn2.org> <vsmude$1ltd2$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Fri, 04 Apr 2025 10:43:33 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="670086d25131323072cd2a1bcb3678f0";
	logging-data="3210948"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1+tFFRW3CuyAU4pYdQ4y9hI"
User-Agent: Unison/2.2
Cancel-Lock: sha1:nZDLlwyjbKvmYtCEm3j7Ddt7NiI=

On 2025-04-03 21:26:05 +0000, olcott said:

> On 4/3/2025 6:06 AM, Richard Damon wrote:
>> On 4/3/25 12:27 AM, olcott wrote:
>>> On 4/2/2025 10:09 PM, Richard Damon wrote:
>>>> On 4/2/25 10:51 PM, olcott wrote:
>>>>> On 4/2/2025 8:56 PM, Richard Damon wrote:
>>>>>> On 4/2/25 9:30 PM, olcott wrote:
>>>>>>> On 4/2/2025 5:05 PM, Richard Damon wrote:
>>>>>>>> On 4/2/25 11:59 AM, olcott wrote:
>>>>>>>>> On 4/2/2025 4:20 AM, Mikko wrote:
>>>>>>>>>> On 2025-04-01 17:51:29 +0000, olcott said:
>>>>>>>>>> 
>>>>>>>>>>> 
>>>>>>>>>>> All we have to do is make a C program that does this
>>>>>>>>>>> with pairs of finite strings then it becomes self-evidently
>>>>>>>>>>> correct needing no proof.
>>>>>>>>>> 
>>>>>>>>>> There already are programs that check proofs. But you can make your own
>>>>>>>>>> if you think the logic used by the existing ones is not correct.
>>>>>>>>>> 
>>>>>>>>>> If the your logic system is sufficiently weak there may also be a way to
>>>>>>>>>> make a C program that can construct the proof or determine that there is
>>>>>>>>>> none.
>>>>>>>>>> 
>>>>>>>>> 
>>>>>>>>> When we define a system that cannot possibly be inconsistent
>>>>>>>>> then a proof of consistency not needed.
>>>>>>>> 
>>>>>>>> But you can't do that unless you limit the system to only have a finite 
>>>>>>>> number of statements expressible in it, and thus it can't handle most 
>>>>>>>> real problems
>>>>>>>> 
>>>>>>>>> 
>>>>>>>>> A system entirely comprised of Basic Facts and Semantic logical 
>>>>>>>>> entailment cannot possibly be inconsistent.
>>>>>>>>> 
>>>>>>>> 
>>>>>>>> Sure it can.
>>>>>>>> 
>>>>>>>> The problem is you need to be very careful about what you allow as your 
>>>>>>>> "Basic Facts", and if you allow the system to create the concept of the 
>>>>>>>> Natural Numbers, you can't verify that you don't actually have a 
>>>>>>>> contradition in it.
>>>>>>>> 
>>>>>>> 
>>>>>>> It never has been that natural numbers have
>>>>>>> ever actually had any inconsistency themselves
>>>>>>> they are essentially nothing more than an ordered
>>>>>>> set of finite strings of digits.
>>>>>> 
>>>>>> No, but any logic system that can support them
>>>>> 
>>>>> Can be defined in screwy that has undecidability
>>>>> or not defined in this screwy way.
>>>>> 
>>>>> Basic facts and expressions semantically entailed
>>>>> by the basic facts cannot have undecidability[math].
>>>>> 
>>>> 
>>>> Wrong, Godel shows that having the properties of the Natural numbers is enough.
>>>> 
>>> 
>>> They are merely an ordered set of finite strings of digits.
>> 
>> No, the Natural Numbers are NOT "finite strings" but that is just a 
>> representation for them, and a given number can have many 
>> representations.
>> 
>> And they are just an ordered set, but there are a number of semantic 
>> properties of the members. Things like 2 + 3 is 5, and 2 * 3 is 6, and 
>> that some numbers are called "prime" because the only way to decompose 
>> them with multiplication is themselves times one, but other numbers can 
>> be decomposed as the product of other numbers, and the set of prime 
>> numbers (with their powers) has a one to one relationship to the set of 
>> numbers, every product set resulting in just a single number and every 
>> number having just a single product set.
>> 
>> From this, and the fact that a logic system that can support these 
>> concepts WILL have a statement in it that is true and unprovable in the 
>> system.
> 
> Natural numbers are merely an ordered set of concepts
> that are associated with some form of encoding.

An encoding is not a part of the concept of natural numbers.
That they satisfy Peano axioms usually is.

> Even
> arithmetic is added on top of the notion of natural
> numbers.

At least one function must be primitive. Usally it is the successor.
If first order logic is used the primitive functions addition and
multiplication are needed. With second or higher order logic they
are not necessary.

The induction axiom schema (in first order logic) or the induction
axion (in second or higher order logic) is an exential aspect of
the concept of natural numbers.

An alternative approach is to start with a theory of something else
and define some (or all) its elements as natural numbers. In that
approach the functions of artihmetic (at least addition and
multiplication) must be defined. Often some set theory is used as
the starting point. A theory of finite strings could also be used
and would give a natural encodeing that other theories don't.

-- 
Mikko