Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  newsreader  groups  login

Message-ID:  

"It is easier to fight for principles than to live up to them." -- Alfred Adler


computers / comp.ai.philosophy / Re: Is this correct Prolog?

Re: Is this correct Prolog?

<t4srko$445$1@dont-email.me>

 copy mid

https://www.novabbs.com/computers/article-flat.php?id=8649&group=comp.ai.philosophy#8649

 copy link   Newsgroups: comp.theory comp.lang.prolog comp.ai.philosophy
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: polco...@gmail.com (olcott)
Newsgroups: comp.theory,comp.lang.prolog,comp.ai.philosophy
Subject: Re: Is this correct Prolog?
Date: Tue, 3 May 2022 22:24:05 -0500
Organization: A noiseless patient Spider
Lines: 288
Message-ID: <t4srko$445$1@dont-email.me>
References: <qcOdndRse-RjQ_H_nZ2dnUU7_83NnZ2d@giganews.com>
<t4ivm8$c4v$1@dont-email.me> <t4jubn$r31$1@dont-email.me>
<rcadndtC6vGrOPD_nZ2dnUU7_83NnZ2d@giganews.com> <t4ljnn$5k0$1@dont-email.me>
<KtadnUFsIcTQ9fP_nZ2dnUU7_8xh4p2d@giganews.com> <t4ogft$8dt$1@dont-email.me>
<t4ol6v$hpr$1@dont-email.me> <t4ommc$8dt$2@dont-email.me>
<t4ontc$93n$1@dont-email.me> <t4opqo$g2g$1@dont-email.me>
<t4ot2r$o65$1@dont-email.me> <t4p4br$b81$1@dont-email.me>
<t4pbl5$g28$1@dont-email.me> <pWYbK.48$UWx1.17@fx41.iad>
<t4pmmd$4f6$3@dont-email.me> <87a6bzfqkz.fsf@bsb.me.uk>
<t4pulq$bci$1@dont-email.me> <t4rh4c$t51$1@dont-email.me>
<t4rk2m$rei$1@dont-email.me> <t4rmkb$jrt$1@dont-email.me>
<t4rncl$qtf$1@dont-email.me> <t4ro31$1kc$1@dont-email.me>
<t4rp26$a70$1@dont-email.me> <t4rruh$557$1@dont-email.me>
<t4ru1s$mre$1@dont-email.me> <t4s1r5$n2b$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Wed, 4 May 2022 03:24:08 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="3f069846940d953f06eba1973f7ebc89";
logging-data="4229"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+zuvRxhFkR/Wcs8XgceYRN"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
Thunderbird/91.9.0
Cancel-Lock: sha1:3593X6aGCdFLIYCB5y/AhifUfRY=
In-Reply-To: <t4s1r5$n2b$1@dont-email.me>
Content-Language: en-US
 by: olcott - Wed, 4 May 2022 03:24 UTC

On 5/3/2022 3:03 PM, André G. Isaak wrote:
> On 2022-05-03 12:59, olcott wrote:
>> On 5/3/2022 1:23 PM, André G. Isaak wrote:
>>> On 2022-05-03 11:33, olcott wrote:
>>>> On 5/3/2022 12:17 PM, André G. Isaak wrote:
>>>>> On 2022-05-03 11:05, olcott wrote:
>>>>>> On 5/3/2022 11:52 AM, André G. Isaak wrote:
>>>
>>> <snippage>
>>>
>>>>>>> G is very clearly a truth-bearer. Go back and reread my original
>>>>>>> explanation.
>>>>>>>
>>>>>>
>>>>>> When G is not provable in PA, how is it shown to be true?
>>>>>> If it is not shown to be true in PA then we have the strawman error.
>>>>>
>>>>> Here you're simply begging the question by assuming your own
>>>>> conclusion: that being true and being provable are the same.
>>>>
>>>> This is not any mere assumption.
>>>>
>>>> The only way that any analytic expressions of language are correctly
>>>> determined to be true is:
>>>
>>> 'True' and 'Correctly determined to be true' mean different things.
>>>
>>
>> Yes that seems to be correct.
>> On the other hand calling an expression of language true that has not
>> be 'Correctly determined to be true' is an error.
>
> But calling it a "non-truth bearer" simply because it has not been
> determined to be true would equally be an error.
>

That if correct. If is is impossibly true or false then it is not a
truth bearer.

> And it can be shown (i.e. correctly determined) that G is true, just not
> within the system for which it was constructed.
>

unprovable in the system entails untrue in the system.

>> If G is claimed to be true then this assertion must be supported by:
>> 'Correctly determined to be true' otherwise the assessment of its
>> truth is no more than a wild guess.
>>
>>>> (a) They are defined to be true.
>>>> (b) They are derived from applying truth preserving operations to
>>>> (a) or (b). Prolog knows this on the basis of its facts and rules.
>>>> Facts are (a) and rules are (b). This is also known as sound
>>>> deductive inference.
>>>
>>> These are YOUR assumptions. They have not been demonstrated. And they
>>> are not consistent with the way in which the rest of the world talks
>>> about truth. You are talking about provability, not truth.
>>>
>>
>> If G is claimed to be true then this assertion must be supported by:
>> 'Correctly determined to be true' otherwise the assessment of its
>> truth is no more than a wild guess.
>>
>>>>> The whole point of Gödel's proof is that they cannot be the same
>>>>> (at least not for non-trivial systems).
>>>>>
>>>>
>>>> When G is not provable in PA, how is it shown to be true (wild guess)?
>>>> What is the precise basis for assessing that G is true? please
>>>> provide ALL the steps.
>>>
>>> "True" and "Known to be true" are entirely different things.
>>>
>>
>> Yes, however:
>> If G is claimed to be true then this assertion must be supported by:
>> 'Correctly determined to be true' otherwise the assessment of its
>> truth is no more than a wild guess.
>
> As I said, it can be shown in a higher order system.

Sure, yet it is only true in this system which also makes it provable in
that system.

> But even if it could not be, if we can show that G can only be true in
> cases where it is not provable in T, then there are only two possible
> conclusions:
>

It can't be true in T and unprovable in T.

> Either G is true and unprovable in T, in which case T is incomplete.
> Or G is false and provable in T, in which case T is inconsistent.
>

If G is provable in U then it is true in U.
If G is unprovable in T then it is untrue in T.
G is unprovable in T because it is semantically incorrect.

> Which is exactly what Gödel's theorem states: A system can be consistent
> or it can be complete but it cannot be both. An incomplete system is
> still useful. An inconsistent system is not. Ergo he phrases this as an
> consistent system must be incomplete [with the usual caveats about
> meeting some minimum threshold of expressive power].
>
>>> Consider the equation Srt((2748 + 87)^3) = 150,948.776 (to 3 decimal
>>> places)
>>>
>>
>> (2748 + 87)^3 = 22,785,532,875
>> What are you sorting with Srt()?
>
> That was obviously a type. Sqrt().
>
>>> That equation is true but it is unlikely anyone knew this to be true
>>> until now since I very much doubt anyone had previously considered
>>> that specific equation. That's doesn't mean it wasn't true all along.
>>> Just that no one knew it was true.
>>>
>>> There are all sorts of cases where we know one thing without knowing
>>> all things. I can know with certainty that (A ∨ B) is true meaning
>>> that I know that *at least* one of A or B must be true while still
>>> not knowing the truth value of either. These sorts of things occur
>>> all the time.
>>>
>>
>> That is not true. If A and B are syntactically correct expressions of
>> a formal language yet neither one is semantically correct then we have
>> the same case as the Liar Paradox not being a truth bearer, thus (A ∨
>> B) is neither true nor false.
>
> But your whole notion of 'semantically correct' is recognized by no one
> but you and is antithetical to the entire notion of a formal system. And
> what I describe above is a situation which *very* commonly arises in
> proofs. They're called proofs by dilemma and take the form:
>
> A → C
> B → C
> (A ∨ B)
>
> Therefore C
>
> We draw a conclusion from A or B without knowing the truth value of
> either. This strategy, for example, was used by Euclid in his proof that
> no largest prime exists.
>
> If you declare A and B to be 'non-truth bearers' simply because you
> don't know whether they are true or false, then this and many other
> proofs completely fall apart.

It is not because they have unknown truth values.

>
>>> And not being provable in PA and not being provable are also two
>>> different things.
>>>
>>
>> I know that. Yet not being provable in PA also means that G cannot be
>> derived in PA by applying truth preserving operations to the axioms Z
>> of PA or other expressions Y derived from Z or Y.
>>
>> If G is correctly determined to be true then there must be some
>> process detailing the steps of how it is 'Correctly determined to be
>> true'.
>
> Just not in PA.

OK great this is great progress!

>> Lacking these steps one cannot correctly assert that G is true, only
>> that G might possibly be true.
>>
>>>>> The question is not whether it is true but whether it is a truth
>>>>> *bearer*.
>>>>>
>>>>> You make the claim that The Liar is not a truth bearer (a plausible
>>>>> claim depending on one's definitions).
>>>>>
>>>>> You then jump to the conclusion that G is not a truth bearer based
>>>>> on your assertion that it is "equivalent" to The Liar. But it is
>>>>> *NOT* equivalent. It merely bears a close relationship. But you
>>>>> refuse to actually consider what the nature of that relationship;
>>>>> there are both similiarites and differences.
>>>>>
>>>>
>>>> Precise equivalence is defined by this:
>>>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>>>>
>>>> The Liar Paradox can be neither proven nor refuted where T is the
>>>> entire body of analytic knowledge and φ is LP.
>>>
>>> The Liar Paradox is a self-contradiction. The Gödel sentence is not.
>>
>> Until you understand that G can only be correctly asserted to be true
>> in X if G is provable in X. G may be true in X without a proof in X,
>> yet it cannot be correctly asserted to be true in X without such a proof.
>
> This is your confusion, not mine. We can assert that G is not provable
> and that ¬G is also not provable without asserting anything at all about
> whether G is true and still conclude that X is incomplete.

Yes, but, only because the mathematical definition of Incomplete does
not screen out semantically erroneous expression of the language of X:
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).

>>>
>>>>> Whereas the Liar has no content other than to assert its own
>>>>> falsity, Gödel's G has definite content. It does not assert its own
>>>>> unprovability, it asserts a very specific mathematical claim, one
>>>>> which must by its nature be either true or false. Therefore G *is*
>>>>> a truth bearer.
>>>>>
>>>>> The formulation that G asserts its own unprovability is the
>>>>> Cliff-Notes version of the proof. It's not the substance of the
>>>>> actual proof.
>>>>>
>>>>> André
>>>>
>>>> It is isomorphic to the substance of the actual proof.
>>>
>>> No. It is not. G asserts a claim about mathematics. It does not
>>> assert anything about itself. However, within the metalanguage we can
>>> prove that G can only be true if it is not provable within the system
>>> under consideration.
>>>
>>
>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>> When both G and the LP exactly meet the official mathematical
>> definition of incompleteness then G and LP are proven to be isomorphic.
>
> LP doesn't meet said definition. LP is a paradox of natural language.
> There is no 'isomorphism' between G and LP. And if you claim there is,
> you must state what that isomorphism actually is.

It is a little iffy to say that the LP fits into the above formula
making it isomorphic to Gödel's G unless we can at least specify the
formal system that LP is a member of. Tarski seemed to have provided a
very clean basis to formalize the Liar Paradox. I am working on deriving
it.

>>>> Gödel says:
>>>> since the undecidable proposition [R(q); q] states precisely that q
>>>> belongs to K, i.e. according to (1), that [R(q); q] is not provable.
>>>> We are therefore confronted with a proposition which asserts its own
>>>> unprovability.
>>>
>>> We are confronted *in our analysis* with such a situation. But there
>>> is no proposition which directly asserts such a thing.
>>>
>>

You have to pay attention to this
since the undecidable proposition [R(q); q] states precisely that q
belongs to K, i.e. according to (1), that [R(q); q] is not provable.
It is the English language version of a formal logic sentence.

>> You are letting weasel words leak semantic meaning.
>
> What does 'leak semantic meaning' even mean?

You were simply looking at the wrong lines of the Gödel quote.

>
> André
>
>> My analysis pertaining to the official mathematical definition of
>> incompleteness cuts through these weasel words.
>>
>> This proves that G the LP and the following sentence are all isomorphic:
>> "This sentence is unprovable".
>>
>>> The problem is you refuse to look at the actual math and instead look
>>> only at the text commentary which is merely a guide to, not the
>>> actual substance of, the proof.
>>>
>>> André
>>>
>>
>>
>
>

--
Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
Genius hits a target no one else can see." Arthur Schopenhauer

SubjectRepliesAuthor
o Is this correct Prolog?

By: olcott on Sat, 30 Apr 2022

133olcott
server_pubkey.txt

rocksolid light 0.9.7
clearnet tor