Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  newsreader  groups  login

Message-ID:  

Why won't sharks eat lawyers? Professional courtesy.


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

Re: Is this correct Prolog?

<t4stef$djo$1@dont-email.me>

  copy mid

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

  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 21:54:53 -0600
Organization: Christians and Atheists United Against Creeping Agnosticism
Lines: 322
Message-ID: <t4stef$djo$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>
<t4srko$445$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:54:55 -0000 (UTC)
Injection-Info: reader02.eternal-september.org; posting-host="ab2835e1a019a70ccf6aefd886b80f45";
logging-data="13944"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18r0G9DooeQbnGcMNXdocZ7"
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.14; rv:91.0)
Gecko/20100101 Thunderbird/91.8.1
Cancel-Lock: sha1:SMzTmQrARCcZwgXbouilkQx5zvY=
In-Reply-To: <t4srko$445$1@dont-email.me>
Content-Language: en-US
 by: André G. Isaak - Wed, 4 May 2022 03:54 UTC

On 2022-05-03 21:24, olcott wrote:
> 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.

Neither 'impossibly true' nor 'impossibly false' are meaningful English.
I really wish you would stop using this adverb as if it somehow made
sense. It doesn't.

G is definitely a truth bearer. It states that a specific polynomial
equation has at least one integer solution. Any statement of that form
is either true or false. It is not possible for it to be both. It is not
possible for it to be neither.

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

Maybe you should read the actual proof. We proof in some higher order
system T' that G is unprovable in T and that G is true in T.

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

Again, try reading the actual proof. I mean the math part, not the text
part.

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

Yes. It can. That is the entire point of the proof which you have not
actually read. The problem is that you seem to have a personal
definition of 'true' which essentially is the same as 'provable'. Yes,
it can't be both provable in T and unprovable in T, but that's a truism.
Not Gödel's theorem.

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

No one besides you recognizes this whole 'semantic incorrectness'
notion. Until you can get people to accept that there is such a thing,
there is no point bringing it up.

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

So then what is it? In the case of The Liar I am willing to accept your
claim that it is not a truth-bearer on the grounds that The Liar
effectively has no actual content apart from its own self-referential
claim. That's about the only case I can see it being legitimate to refer
to a declarative sentence as a non-truth bearer (under standard
definitions, truth-bearer and declarative sentence are simply synonyms).

Gödel's G is not like that. It is not self-referential and it does have
actual content.

>>
>>>> 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 ⊬ ¬φ)).

There are no such semantically erroneous expressions. Claiming that they
are 'erroneous' doesn't actually demonstrate an error. It's just an
empty assertion on your part.

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

When I say that LP doesn't fit into the above I am referring to the fact
that unlike G, LP is a *contradiction*. A contradiction is a statement
which can be *both* proven to be true and proven to be false.
Contradictions lead to inconsistency.

G is definitely not a contradiction; it is a statement which can
*neither* be proven to be true nor proven to be false. That's
incompleteness. G and LP are not analogous statements despite the fact
that you continuously conflate the two.

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

That doesn't answer my question.

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

133olcott
server_pubkey.txt

rocksolid light 0.9.8
clearnet tor