Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  newsreader  groups  login

Message-ID:  

Put no trust in cryptic comments.


computers / comp.theory / Re: Is this correct Prolog?

Re: Is this correct Prolog?

<t4s1r5$n2b$1@dont-email.me>

  copy mid

https://www.novabbs.com/computers/article-flat.php?id=31514&group=comp.theory#31514

  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: agis...@gm.invalid (André G. Isaak)
Newsgroups: comp.theory,comp.lang.prolog,comp.ai.philosophy
Subject: Re: Is this correct Prolog?
Date: Tue, 3 May 2022 14:03:47 -0600
Organization: Christians and Atheists United Against Creeping Agnosticism
Lines: 241
Message-ID: <t4s1r5$n2b$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>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Tue, 3 May 2022 20:03:49 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="7f071c55a4f6bdb2e9a846aebe0c1a13";
logging-data="23627"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18Kblez7h5lWh6z/qkHdV9h"
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.14; rv:91.0)
Gecko/20100101 Thunderbird/91.8.1
Cancel-Lock: sha1:v0ahb78LXW1dNid+xGOuU7ncov8=
In-Reply-To: <t4ru1s$mre$1@dont-email.me>
Content-Language: en-US
 by: André G. Isaak - Tue, 3 May 2022 20:03 UTC

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.

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

> 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.

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:

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.

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.

>> 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.

> 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.

>>
>>>> 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.

>>> 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 are letting weasel words leak semantic meaning.

What does 'leak semantic meaning' even mean?

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é
>>
>
>

--
To email remove 'invalid' & replace 'gm' with well known Google mail
service.

SubjectRepliesAuthor
o Is this correct Prolog?

By: olcott on Sat, 30 Apr 2022

195olcott
server_pubkey.txt

rocksolid light 0.9.81
clearnet tor