Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.lang.prolog > #15172

Re: A new foundation for correct reasoning

From olcott <polcott333@gmail.com>
Newsgroups comp.lang.prolog, comp.theory, sci.logic, sci.math
Subject Re: A new foundation for correct reasoning
Date 2025-12-15 08:03 -0600
Organization A noiseless patient Spider
Message-ID <10hp4eo$1uh6i$2@dont-email.me> (permalink)
References (25 earlier) <10hjejt$3u3sm$1@dont-email.me> <10hju2h$4hat$1@dont-email.me> <10hm25a$tpc7$1@dont-email.me> <10hngct$1gbn9$1@dont-email.me> <10hoive$1p2m3$2@dont-email.me>

Cross-posted to 4 groups.

Show all headers | View raw

On 12/15/2025 3:04 AM, Mikko wrote:
> On 15/12/2025 01:14, olcott wrote:
>> On 12/14/2025 4:05 AM, Mikko wrote:
>>> On 13/12/2025 16:43, olcott wrote:
>>>> On 12/13/2025 4:19 AM, Mikko wrote:
>>>>> olcott kirjoitti 12.12.2025 klo 16.19:
>>>>>> On 12/12/2025 2:50 AM, Mikko wrote:
>>>>>>> olcott kirjoitti 11.12.2025 klo 16.17:
>>>>>>>> On 12/11/2025 2:42 AM, Mikko wrote:
>>>>>>>>> olcott kirjoitti 10.12.2025 klo 16.10:
>>>>>>>>>> On 12/10/2025 4:04 AM, Mikko wrote:
>>>>>>>>>>> olcott kirjoitti 8.12.2025 klo 21.09:
>>>>>>>>>>>> On 12/8/2025 3:13 AM, Mikko wrote:
>>>>>>>>>>>>> olcott kirjoitti 5.12.2025 klo 19.43:
>>>>>>>>>>>>>> On 12/5/2025 3:38 AM, Mikko wrote:
>>>>>>>>>>>>>>> olcott kirjoitti 4.12.2025 klo 16.06:
>>>>>>>>>>>>>>>> On 12/4/2025 2:58 AM, Mikko wrote:
>>>>>>>>>>>>>>>>> Tristan Wibberley kirjoitti 4.12.2025 klo 4.32:
>>>>>>>>>>>>>>>>>> On 30/11/2025 09:58, Mikko wrote:
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> Note that the meanings of
>>>>>>>>>>>>>>>>>>>   ?- G = not(provable(F, G)).
>>>>>>>>>>>>>>>>>>> and
>>>>>>>>>>>>>>>>>>>   ?- unify_with_occurs_check(G, not(provable(F, G))).
>>>>>>>>>>>>>>>>>>> are different. The former assigns a value to G, the 
>>>>>>>>>>>>>>>>>>> latter does not.
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> For sufficiently informal definitions of "value".
>>>>>>>>>>>>>>>>>> And for sufficiently wrong ones too!
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> It is sufficiently clear what "value" of a Prolog 
>>>>>>>>>>>>>>>>> variable means.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> % This sentence cannot be proven in F
>>>>>>>>>>>>>>>> ?- G = not(provable(F, G)).
>>>>>>>>>>>>>>>> G = not(provable(F, G)).
>>>>>>>>>>>>>>>> ?- unify_with_occurs_check(G, not(provable(F, G))).
>>>>>>>>>>>>>>>> false.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> I would say that the above Prolog is the 100%
>>>>>>>>>>>>>>>> complete formal specification of:
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> "This sentence cannot be proven in F"
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> The first query can be regarded as a question whether "G 
>>>>>>>>>>>>>>> = not(provable(
>>>>>>>>>>>>>>> F, G))" can be proven for some F and some G. The answer 
>>>>>>>>>>>>>>> is that it can
>>>>>>>>>>>>>>> for every F and for (at least) one G, which is 
>>>>>>>>>>>>>>> not(provable(G)).
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> The second query can be regarded as a question whether "G 
>>>>>>>>>>>>>>> = not(provable
>>>>>>>>>>>>>>> (F, G))" can be proven for some F and some G that do not 
>>>>>>>>>>>>>>> contain cycles.
>>>>>>>>>>>>>>> The answer is that in the proof system of Prolog it 
>>>>>>>>>>>>>>> cannot be.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> No that it flatly incorrect. The second question is this:
>>>>>>>>>>>>>> Is "G = not(provable(F, G))." semantically sound?
>>>>>>>>>>>>>
>>>>>>>>>>>>> Where is the definition of Prolog semantics is that said?
>>>>>>>>>>>>
>>>>>>>>>>>> Any expression of Prolog that cannot be evaluated to
>>>>>>>>>>>> a truth value because it specifies non-terminating
>>>>>>>>>>>> infinite recursion is "semantically unsound" by the
>>>>>>>>>>>> definition of those terms even if Prolog only specifies
>>>>>>>>>>>> that cannot be evaluated to a truth value because it
>>>>>>>>>>>> specifies non-terminating infinite recursion.
>>>>>>>>>>>
>>>>>>>>>>> Your Prolog implementation has evaluated G = not(provablel(F, 
>>>>>>>>>>> G))
>>>>>>>>>>> to a truth value true. When doing so it evaluated each side of =
>>>>>>>>>>> to a value that is not a truth value.
>>>>>>>>>>
>>>>>>>>>> ?- unify_with_occurs_check(G, not(provable(F, G))).
>>>>>>>>>> false.
>>>>>>>>>>
>>>>>>>>>> Proves that
>>>>>>>>>> G = not(provable(F, G)).
>>>>>>>>>> would remain stuck in infinite recursion.
>>>>>>>>>>
>>>>>>>>>> unify_with_occurs_check() examines the directed
>>>>>>>>>> graph of the evaluation sequence of an expression.
>>>>>>>>>> When it detects a cycle that indicates that an
>>>>>>>>>> expression would remain stuck in recursive
>>>>>>>>>> evaluation never to be resolved to a truth value.
>>>>>>>>>>
>>>>>>>>>> BEGIN:(Clocksin & Mellish 2003:254)
>>>>>>>>>> Finally, a note about how Prolog matching sometimes differs
>>>>>>>>>> from the unification used in Resolution. Most Prolog systems
>>>>>>>>>> will allow you to satisfy goals like:
>>>>>>>>>>
>>>>>>>>>> equal(X, X).
>>>>>>>>>> ?- equal(foo(Y), Y).
>>>>>>>>>>
>>>>>>>>>> that is, they will allow you to match a term against an
>>>>>>>>>> uninstantiated subterm of itself. In this example, foo(Y)
>>>>>>>>>> is matched against Y, which appears within it. As a result,
>>>>>>>>>> Y will stand for foo(Y), which is foo(foo(Y)) (because of
>>>>>>>>>> what Y stands for), which is foo(foo(foo(Y))), and so on.
>>>>>>>>>> So Y ends up standing for some kind of infinite structure.
>>>>>>>>>>
>>>>>>>>>> Note that, whereas they may allow you to construct something
>>>>>>>>>> like this, most Prolog systems will not be able to write it
>>>>>>>>>> out at the end. According to the formal definition of
>>>>>>>>>> Unification, this kind of “infinite term” should never come
>>>>>>>>>> to exist. Thus Prolog systems that allow a term to match an
>>>>>>>>>> uninstantiated subterm of itself do not act correctly as
>>>>>>>>>> Resolution theorem provers. In order to make them do so, we
>>>>>>>>>> would have to add a check that a variable cannot be
>>>>>>>>>> instantiated to something containing itself. Such a check,
>>>>>>>>>> an occurs check, would be straightforward to implement, but
>>>>>>>>>> would slow down the execution of Prolog programs considerably.
>>>>>>>>>> Since it would only affect very few programs, most implementors
>>>>>>>>>> have simply left it out 1.
>>>>>>>>>>
>>>>>>>>>> 1 The Prolog standard states that the result is undefined if
>>>>>>>>>> a Prolog system attempts to match a term against an 
>>>>>>>>>> uninstantiated subterm of itself, which means that programs 
>>>>>>>>>> which cause this to
>>>>>>>>>> happen will not be portable. A portable program should ensure 
>>>>>>>>>> that wherever an occurs check might be applicable the built-in 
>>>>>>>>>> predicate
>>>>>>>>>> unify_with_occurs_check/2 is used explicitly instead of the 
>>>>>>>>>> normal
>>>>>>>>>> unification operation of the Prolog implementation. As its 
>>>>>>>>>> name suggests, this predicate acts like =/2 except that it 
>>>>>>>>>> fails if an
>>>>>>>>>> occurs check detects an illegal attempt to instantiate a 
>>>>>>>>>> variable.
>>>>>>>>>> END:(Clocksin & Mellish 2003:254)
>>>>>>>>>>
>>>>>>>>>> Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog
>>>>>>>>>> Using the ISO Standard Fifth Edition, 254. Berlin Heidelberg:
>>>>>>>>>> Springer-Verlag.
>>>>>>>>>
>>>>>>>>> Thank you for the confirmation of my explanation of your error.
>>>>>>>>
>>>>>>>>  >> Y will stand for foo(Y), which is foo(foo(Y)) (because of
>>>>>>>>  >> what Y stands for), which is foo(foo(foo(Y))), and so on.
>>>>>>>> As I say non-terminating, thus never resolves to a truth value.
>>>>>>>
>>>>>>> As according to Prolog rules foo(Y) isn't a truth value for any Y
>>>>>>> the above is obviously just an attempt to deive with a distraction.
>>>>>>
>>>>>> That was a quote from the most definitive source
>>>>>> for the Prolog Language.
>>>>>
>>>>> As I already said, that source agrees with what I said above.
>>>>>
>>>>>> Prolog only has Facts and Rules thus the only
>>>>>> derivation is to a truth value.
>>>>>
>>>>
>>>> You just don't seem to understand:
>>>> ?- G = not(provable(F, G)).
>>>> G = not(provable(F, G)).
>>>> ?- unify_with_occurs_check(G, not(provable(F, G))).
>>>> false.
>>>>
>>>> The first statement creates a cyclic term, also called
>>>> a rational tree. The second executes logically sound
>>>> unification and thus fails.
>>>> https://www.swi-prolog.org/pldoc/man? 
>>>> predicate=unify_with_occurs_check/2
>>>
>>> Saying the same as I said does not support a claim of non-understanding.
>>
>> It finally resolves the Liar Paradox
>> as not a truth bearer or proposition.
> 
> In other words you admit you were lying about me.
> 

I have no idea what you are referring to.

-- 
Copyright 2025 Olcott<br><br>

My 28 year goal has been to make <br>
"true on the basis of meaning expressed in language"<br>
reliably computable.<br><br>

This required establishing a new foundation<br>

Back to comp.lang.prolog | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread

Thread

Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-05 11:43 -0600
  Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-12-06 11:30 +0200
    Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-06 06:50 -0600
      Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-12-07 13:02 +0200
        Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-08 13:49 -0600
  Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-12-08 11:13 +0200
    Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-08 13:09 -0600
      Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-12-10 12:04 +0200
        Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-10 08:10 -0600
          Re: A new foundation for correct reasoning Python <python@cccp.invalid> - 2025-12-10 15:01 +0000
          Re: A new foundation for correct reasoning Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2025-12-10 18:10 +0000
            Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-10 14:01 -0600
          Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-12-11 10:42 +0200
            Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-11 08:17 -0600
              Re: A new foundation for correct reasoning Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2025-12-11 23:28 +0000
                Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-11 17:49 -0600
                Re: A new foundation for correct reasoning Richard Damon <Richard@Damon-Family.org> - 2025-12-11 19:52 -0500
              Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-12-12 10:50 +0200
                Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-12 08:19 -0600
                Re: A new foundation for correct reasoning Richard Damon <Richard@Damon-Family.org> - 2025-12-12 09:24 -0500
                Re: A new foundation for correct reasoning Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2025-12-14 19:03 +0000
                Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-12-13 12:19 +0200
                Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-13 08:43 -0600
                Re: A new foundation for correct reasoning Richard Damon <Richard@Damon-Family.org> - 2025-12-13 13:36 -0500
                Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-12-14 12:05 +0200
                Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-14 17:14 -0600
                Re: A new foundation for correct reasoning Richard Damon <Richard@Damon-Family.org> - 2025-12-14 19:13 -0500
                Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-14 18:46 -0600
                Re: A new foundation for correct reasoning Richard Damon <Richard@Damon-Family.org> - 2025-12-14 19:53 -0500
                Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-14 19:08 -0600
                Re: A new foundation for correct reasoning Richard Damon <Richard@Damon-Family.org> - 2025-12-14 20:46 -0500
                Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-14 20:05 -0600
                Re: A new foundation for correct reasoning Richard Damon <Richard@Damon-Family.org> - 2025-12-14 21:23 -0500
                Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-14 20:09 -0600
                Re: A new foundation for correct reasoning Richard Damon <Richard@Damon-Family.org> - 2025-12-14 21:27 -0500
                Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-14 21:22 -0600
                Re: A new foundation for correct reasoning Richard Damon <Richard@Damon-Family.org> - 2025-12-15 07:33 -0500
                Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-12-15 11:04 +0200
                Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-15 08:03 -0600
                Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-12-16 11:44 +0200
                Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-12-16 11:48 +0200

csiph-web