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
Subject: Re: How a True(X) predicate can be defined for the set of analytic
 knowledge
Date: Sun, 6 Apr 2025 07:47:33 -0400
Organization: i2pn2 (i2pn.org)
Message-ID: <7ecf6da5800609f614ec7ebd2b7c1b59e1a1f3bd@i2pn2.org>
References: <vrfvbd$256og$2@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> <vslc7n$26a4$2@dont-email.me>
 <vsmnql$1bbrc$3@dont-email.me> <vsqljd$1maks$1@dont-email.me>
 <vss5h9$375du$3@dont-email.me>
 <00551250a1506d54c73efe83d7289afb4fd35f01@i2pn2.org>
 <vssrb3$3pobo$2@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Sun, 6 Apr 2025 11:49:08 -0000 (UTC)
Injection-Info: i2pn2.org;
	logging-data="3369611"; mail-complaints-to="usenet@i2pn2.org";
	posting-account="diqKR1lalukngNWEqoq9/uFtbkm5U+w3w6FQ0yesrXg";
User-Agent: Mozilla Thunderbird
Content-Language: en-US
X-Spam-Checker-Version: SpamAssassin 4.0.0
In-Reply-To: <vssrb3$3pobo$2@dont-email.me>

On 4/5/25 11:10 PM, olcott wrote:
> On 4/5/2025 5:19 PM, Richard Damon wrote:
>> On 4/5/25 4:58 PM, olcott wrote:
>>> On 4/5/2025 2:20 AM, Mikko wrote:
>>>> On 2025-04-03 19:33:41 +0000, olcott said:
>>>>
>>>>> On 4/3/2025 2:09 AM, Mikko wrote:
>>>>>> On 2025-04-03 02:51:32 +0000, olcott said:
>>>>>>
>>>>>>> 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.
>>>>>>
>>>>>> And you can't define it otherwise.
>>>>>>
>>>>>
>>>>> Yes it free to keeps its screwy definition just like
>>>>> set theory until a superior alternative comes along,
>>>>> then it may be renamed naive formal systems.
>>>>>
>>>>> A consistent set of stipulated axioms combined with
>>>>> semantic logical entailment as the only inference step
>>>>> makes undecidability impossible.
>>>>
>>>> If semantic logical entaillment is allowed as an inference rule
>>>> the system is not formal. In order to be formal the system must
>>>> define "proof" as any string that satiisfies the syntactic rules
>>>> that the system specifies for proofs.
>>>>
>>>
>>> This "baffled" Richard
>>> https://en.wikipedia.org/wiki/Montague_grammar
>>> https://plato.stanford.edu/entries/montague-semantics/
>>> Semantics as rich as natural language fully formalized
>>> syntactically.
>>>
>>
>> WHich doesn't "baffle" me, but doesn't define the LOGIC that the 
>> system uses, a fact that seems to baffle you, because you just don't 
>> understand what logic actually is.
>>
>> Also note, this grammer doesn't remove the ambiguity inherent in the 
>> meaning of the words used, and especially can't handle the cases where 
>> the speaker was intentionally being vague to form a word play that 
>> extends the meaning of the word.
> 
> It provides a system such that the full expressiveness
> of natural language can be formalized thus enabling
> the only inference step that my formal system architecture
> requires: semantic logical entailment.
> 

Your problem is that "Semantic Logica; Entailment" is powerful enough to 
create the Natural Number system with enough of its properties to allow 
Godel's proof, and thus your system must be incomplete, and being 
incomplete, it can't have Truth Predicate.

Sorry, but you just don't understand what you are talking about.

Do you accept that the existance or non-existance of a number that 
satisfies some finite specification has a truth value. Goldbach 
Conjecture must be either True or False, as either there is or there is 
Not an even number (greater than 4) not expressible as the sum of two 
primes. (We might not know the answer, but the answer exists, and might 
be found)

Do you accept that for something to be a proof, we need to be able to 
verify the correctness of the proof in finte operations?

And thus we could write an algorithm for that procedure to verify the proof?

Do you agree that because such a proof is expressed as a finite string 
of symbols we can create a number that represents it, by suitably 
defining an encoding system.

And thus we could write an algorithm, that given that number verifies 
that the proof is valid.

Do you agree, that a statement that isn't true, can not be proven in a 
consistent system.

So, it is possible to create a program whose output is whether or not a 
given claimed "proof" actually proves a given statement.

And thus the question of if a number exists that the program will accept 
is a valid question (as said proggram either have or not have a number 
it will accept)

And thus the statement that no such number exists is a valid statement.

And thus it is reasonable that Godel could create the program that 
verifies if a number represents a proof of that statement.

And if such a program exists, it can't actually accept any number, as 
any number existing makes the statement false, but also represents a 
proof that makes the statement true.

And there can't be a proof of that statement, as any such proof would be 
convertable into a number which the program then MUST accept, since it 
is a valid proof, which makes the statement wrong.

Thus the statement must be true, but unprovable.