Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > sci.math > #641055 > unrolled thread
| Started by | olcott <polcott333@gmail.com> |
|---|---|
| First post | 2025-11-24 18:53 -0600 |
| Last post | 2025-12-05 17:45 -0600 |
| Articles | 20 on this page of 115 — 9 participants |
Back to article view | Back to sci.math
A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-11-24 18:53 -0600
Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-11-25 11:40 +0200
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-11-25 08:21 -0600
Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-11-26 13:37 +0200
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-11-26 09:39 -0600
Re: A new foundation for correct reasoning Richard Damon <Richard@Damon-Family.org> - 2025-11-26 12:44 -0500
Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-11-27 09:56 +0200
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-11-27 09:31 -0600
Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-11-28 10:58 +0200
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-11-28 09:51 -0600
Re: A new foundation for correct reasoning Richard Damon <Richard@Damon-Family.org> - 2025-11-28 11:04 -0500
Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-11-29 12:17 +0200
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-11-29 11:54 -0600
Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-11-30 11:22 +0200
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-11-26 09:54 -0600
Re: A new foundation for correct reasoning Richard Damon <Richard@Damon-Family.org> - 2025-11-26 12:49 -0500
Re: A new foundation for correct reasoning Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2025-11-26 19:43 +0000
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-11-26 14:04 -0600
Re: A new foundation for correct reasoning Kaz Kylheku <643-408-1753@kylheku.com> - 2025-11-26 21:42 +0000
Re: A new foundation for correct reasoning Kaz Kylheku <643-408-1753@kylheku.com> - 2025-11-26 21:49 +0000
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-11-26 15:54 -0600
Re: A new foundation for correct reasoning "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2025-11-26 22:33 -0800
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-11-26 15:50 -0600
Re: A new foundation for correct reasoning Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2025-12-02 11:26 +0000
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-02 07:22 -0600
Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-11-27 10:00 +0200
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-11-27 09:43 -0600
Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-11-28 11:01 +0200
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-11-28 09:54 -0600
Re: A new foundation for correct reasoning Alan Mackenzie <acm@muc.de> - 2025-11-28 17:32 +0000
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-11-28 12:40 -0600
Re: A new foundation for correct reasoning Alan Mackenzie <acm@muc.de> - 2025-11-28 18:51 +0000
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-11-28 13:21 -0600
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-11-29 08:43 -0600
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-03 19:59 -0600
Re: A new foundation for correct reasoning Richard Damon <Richard@Damon-Family.org> - 2025-11-28 16:49 -0500
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-03 20:07 -0600
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-03 20:30 -0600
Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-11-29 12:20 +0200
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-11-29 11:57 -0600
Re: A new foundation for correct reasoning Ross Finlayson <ross.a.finlayson@gmail.com> - 2025-11-29 11:27 -0800
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-11-29 13:33 -0600
Re: A new foundation for correct reasoning Ross Finlayson <ross.a.finlayson@gmail.com> - 2025-11-30 10:33 -0800
Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-11-30 11:58 +0200
Re: A new foundation for correct reasoning Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2025-12-04 02:32 +0000
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-03 20:39 -0600
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-04 08:06 -0600
Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-12-05 11:38 +0200
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 Python <python@cccp.invalid> - 2025-12-10 15:03 +0000
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-10 10:14 -0600
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
Re: A new foundation for correct reasoning Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2025-12-05 10:49 +0000
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-05 11:05 -0600
Re: A new foundation for correct reasoning Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2025-12-06 08:24 +0000
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-06 06:08 -0600
Re: A new foundation for correct reasoning Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2025-12-06 13:03 +0000
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-06 07:14 -0600
Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-12-08 11:18 +0200
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-08 13:12 -0600
Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-12-10 12:10 +0200
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-10 10:29 -0600
Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-12-11 10:40 +0200
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-11 08:15 -0600
Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-12-12 10:46 +0200
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-12 08:16 -0600
Re: A new foundation for correct reasoning Richard Damon <Richard@Damon-Family.org> - 2025-12-12 09:22 -0500
Re: A new foundation for correct reasoning Mikko <mikko.levanto@iki.fi> - 2025-12-13 12:42 +0200
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-13 09:37 -0600
Re: A new foundation for correct reasoning Python <python@cccp.invalid> - 2025-12-13 15:42 +0000
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-05 11:00 -0600
Re: A new foundation for correct reasoning Python <python@cccp.invalid> - 2025-12-05 22:17 +0000
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-05 16:24 -0600
Re: A new foundation for correct reasoning Python <python@cccp.invalid> - 2025-12-05 22:45 +0000
Re: A new foundation for correct reasoning Ross Finlayson <ross.a.finlayson@gmail.com> - 2025-12-05 15:16 -0800
Re: A new foundation for correct reasoning olcott <polcott333@gmail.com> - 2025-12-05 17:45 -0600
Page 5 of 6 — ← Prev page 1 2 3 4 [5] 6 Next page →
| From | Richard Damon <Richard@Damon-Family.org> |
|---|---|
| Date | 2025-12-14 20:46 -0500 |
| Message-ID | <LLJ%Q.152592$8Vc1.57935@fx14.iad> |
| In reply to | #641929 |
On 12/14/25 8:08 PM, olcott wrote: > On 12/14/2025 6:53 PM, Richard Damon wrote: >> On 12/14/25 7:46 PM, olcott wrote: >>> On 12/14/2025 6:13 PM, Richard Damon wrote: >>>> On 12/14/25 6:14 PM, olcott wrote: >>>>> On 12/14/2025 4:05 AM, Mikko wrote: >>>>>> On 13/12/2025 16:43, olcott wrote: >>>>>>> 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. >>>>> >>>>> Also every other decision problem instance >>>>> with pathological self reference is isomorphic >>>>> to the Liar Paradox. >>>>> >>>> >>>> But no one (except maybe you) didn't understand that the liar >>>> paradox wasn't a truth bearer. >>> >>> It sure would seem that way wouldn't it? >> >> Yep >> >>> >>> It turns out that the Liar Paradox as not >>> a truth bearer has never been accepted. >> >> Sure it has. It is you who just don't understand what people are >> talking about. >> >>> >>> It remains one of the great unresolved >>> paradoxes of the world. >>> >> >> Nope. Care to docuement that claim? >> > > I know exactly how ridiculous it sounds. > None-the-less that the Liar Paradox has > no accepted resolutions remains a verified fact. Can you show where someone didn't consider it a non-truth-bearing statement? > > This guy is one of the greatest experts in > the field of Truthmaker Maximalism > > I do not mean to commit myself to the claim that > denying that the Liar expresses a proposition is the > best solution to the Liar paradox, nor do I want > to commit Truthmaker Maximalism to that claim. > So, you don't understand the difference between it being a proposition or not, and having a truth value? Just shows your stupidity. > Published in Analysis 2006 > Truthmaker Maximalism defended > GONZALO RODRIGUEZ-PEREYRA > https://philarchive.org/archive/RODTMD > > I have owned LiarParadox.org for many years > as the repository for my word. It used > to be a WordPress size before it was hacked. So, you couldn't fix the hacked site?
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2025-12-14 20:05 -0600 |
| Message-ID | <10hnqdh$1ivc2$1@dont-email.me> |
| In reply to | #641932 |
On 12/14/2025 7:46 PM, Richard Damon wrote: > On 12/14/25 8:08 PM, olcott wrote: >> On 12/14/2025 6:53 PM, Richard Damon wrote: >>> On 12/14/25 7:46 PM, olcott wrote: >>>> On 12/14/2025 6:13 PM, Richard Damon wrote: >>>>> On 12/14/25 6:14 PM, olcott wrote: >>>>>> On 12/14/2025 4:05 AM, Mikko wrote: >>>>>>> On 13/12/2025 16:43, olcott wrote: >>>>>>>> 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. >>>>>> >>>>>> Also every other decision problem instance >>>>>> with pathological self reference is isomorphic >>>>>> to the Liar Paradox. >>>>>> >>>>> >>>>> But no one (except maybe you) didn't understand that the liar >>>>> paradox wasn't a truth bearer. >>>> >>>> It sure would seem that way wouldn't it? >>> >>> Yep >>> >>>> >>>> It turns out that the Liar Paradox as not >>>> a truth bearer has never been accepted. >>> >>> Sure it has. It is you who just don't understand what people are >>> talking about. >>> >>>> >>>> It remains one of the great unresolved >>>> paradoxes of the world. >>>> >>> >>> Nope. Care to docuement that claim? >>> >> >> I know exactly how ridiculous it sounds. >> None-the-less that the Liar Paradox has >> no accepted resolutions remains a verified fact. > > Can you show where someone didn't consider it a non-truth-bearing > statement? > There are all kinds of screwy views including that it is both true and false. There are no accepted final resolutions. >> >> This guy is one of the greatest experts in >> the field of Truthmaker Maximalism >> >> I do not mean to commit myself to the claim that >> denying that the Liar expresses a proposition is the >> best solution to the Liar paradox, nor do I want >> to commit Truthmaker Maximalism to that claim. >> > > So, you don't understand the difference between it being a proposition > or not, and having a truth value? > > Just shows your stupidity. > > >> Published in Analysis 2006 >> Truthmaker Maximalism defended >> GONZALO RODRIGUEZ-PEREYRA >> https://philarchive.org/archive/RODTMD >> >> I have owned LiarParadox.org for many years >> as the repository for my word. It used >> to be a WordPress size before it was hacked. > > So, you couldn't fix the hacked site? -- 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>
[toc] | [prev] | [next] | [standalone]
| From | Richard Damon <Richard@Damon-Family.org> |
|---|---|
| Date | 2025-12-14 21:23 -0500 |
| Message-ID | <WiK%Q.1359$qKWd.531@fx42.iad> |
| In reply to | #641936 |
On 12/14/25 9:05 PM, olcott wrote:
> On 12/14/2025 7:46 PM, Richard Damon wrote:
>> On 12/14/25 8:08 PM, olcott wrote:
>>> On 12/14/2025 6:53 PM, Richard Damon wrote:
>>>> On 12/14/25 7:46 PM, olcott wrote:
>>>>> On 12/14/2025 6:13 PM, Richard Damon wrote:
>>>>>> On 12/14/25 6:14 PM, olcott wrote:
>>>>>>> On 12/14/2025 4:05 AM, Mikko wrote:
>>>>>>>> On 13/12/2025 16:43, olcott wrote:
>>>>>>>>> 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.
>>>>>>>
>>>>>>> Also every other decision problem instance
>>>>>>> with pathological self reference is isomorphic
>>>>>>> to the Liar Paradox.
>>>>>>>
>>>>>>
>>>>>> But no one (except maybe you) didn't understand that the liar
>>>>>> paradox wasn't a truth bearer.
>>>>>
>>>>> It sure would seem that way wouldn't it?
>>>>
>>>> Yep
>>>>
>>>>>
>>>>> It turns out that the Liar Paradox as not
>>>>> a truth bearer has never been accepted.
>>>>
>>>> Sure it has. It is you who just don't understand what people are
>>>> talking about.
>>>>
>>>>>
>>>>> It remains one of the great unresolved
>>>>> paradoxes of the world.
>>>>>
>>>>
>>>> Nope. Care to docuement that claim?
>>>>
>>>
>>> I know exactly how ridiculous it sounds.
>>> None-the-less that the Liar Paradox has
>>> no accepted resolutions remains a verified fact.
>>
>> Can you show where someone didn't consider it a non-truth-bearing
>> statement?
>>
>
> There are all kinds of screwy views including
> that it is both true and false. There are no
> accepted final resolutions.
Sure there is, in conventional logic, it just doesn't have a truth value.
Only in your strange field of "Truthmaker Maximilization" do you get the
problem, because you intertain the concept that a statement can be true
without a truth maker based on the meaning of the words.
Formal Logic doesn't allow for that. A statement is only true if it
derives from a (possibly infinite) sequence of logical derivation steps
from the axioms ("truthmakers") of the system.
It is only in fuzzy philosophy that doesn't have as rigid of a
definition do you get into that issue.
If THAT is what you are talking about, then you are in the wrong area,
as none of the proofs you tried to use that on allow for that fuzzy logic.
M: This sentence has no truthmaker
is just a statement without a Truth Value in formal logic systems.
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2025-12-14 20:09 -0600 |
| Message-ID | <10hnqkj$1j13b$1@dont-email.me> |
| In reply to | #641932 |
On 12/14/2025 7:46 PM, Richard Damon wrote: > On 12/14/25 8:08 PM, olcott wrote: >> On 12/14/2025 6:53 PM, Richard Damon wrote: >>> On 12/14/25 7:46 PM, olcott wrote: >>>> On 12/14/2025 6:13 PM, Richard Damon wrote: >>>>> On 12/14/25 6:14 PM, olcott wrote: >>>>>> On 12/14/2025 4:05 AM, Mikko wrote: >>>>>>> On 13/12/2025 16:43, olcott wrote: >>>>>>>> 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. >>>>>> >>>>>> Also every other decision problem instance >>>>>> with pathological self reference is isomorphic >>>>>> to the Liar Paradox. >>>>>> >>>>> >>>>> But no one (except maybe you) didn't understand that the liar >>>>> paradox wasn't a truth bearer. >>>> >>>> It sure would seem that way wouldn't it? >>> >>> Yep >>> >>>> >>>> It turns out that the Liar Paradox as not >>>> a truth bearer has never been accepted. >>> >>> Sure it has. It is you who just don't understand what people are >>> talking about. >>> >>>> >>>> It remains one of the great unresolved >>>> paradoxes of the world. >>>> >>> >>> Nope. Care to docuement that claim? >>> >> >> I know exactly how ridiculous it sounds. >> None-the-less that the Liar Paradox has >> no accepted resolutions remains a verified fact. > > Can you show where someone didn't consider it a non-truth-bearing > statement? > There isn't an accepted final resolution to the Liar Paradox—it remains one of the most debated open problems in logic and philosophy! The Liar Paradox (sentences like "This sentence is false") has generated numerous proposed solutions, but none has achieved consensus. Here are the main approaches: 1. Tarski's Hierarchy of Languages Truth predicates apply only to sentences in lower-level languages. The liar sentence is blocked because it tries to apply a truth predicate to itself within the same language level. This "solves" it but many find it restrictive for natural language. 2. Paraconsistent Logic Accept that some contradictions can exist without everything becoming provable. The liar sentence can be both true and false without the logical system exploding. 3. Dialetheism (Graham Priest) Accept that the liar sentence is actually both true and false—a "true contradiction" or dialetheia. Challenges the law of non-contradiction. 4. Semantic Approaches Various theories argue the liar sentence is meaningless, lacks a truth value, or is semantically defective in some way. 5. Contextualism The truth value shifts depending on context or level of evaluation. 6. Revision Theories Truth values can be revised over time through iterative processes. Each approach has its defenders and critics, and philosophers continue to debate which (if any) is correct. The paradox remains philosophically live—it's not "solved" in the way mathematical problems get solved with accepted proofs. -- 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>
[toc] | [prev] | [next] | [standalone]
| From | Richard Damon <Richard@Damon-Family.org> |
|---|---|
| Date | 2025-12-14 21:27 -0500 |
| Message-ID | <LmK%Q.152594$8Vc1.60183@fx14.iad> |
| In reply to | #641937 |
On 12/14/25 9:09 PM, olcott wrote: > On 12/14/2025 7:46 PM, Richard Damon wrote: >> On 12/14/25 8:08 PM, olcott wrote: >>> On 12/14/2025 6:53 PM, Richard Damon wrote: >>>> On 12/14/25 7:46 PM, olcott wrote: >>>>> On 12/14/2025 6:13 PM, Richard Damon wrote: >>>>>> On 12/14/25 6:14 PM, olcott wrote: >>>>>>> On 12/14/2025 4:05 AM, Mikko wrote: >>>>>>>> On 13/12/2025 16:43, olcott wrote: >>>>>>>>> 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. >>>>>>> >>>>>>> Also every other decision problem instance >>>>>>> with pathological self reference is isomorphic >>>>>>> to the Liar Paradox. >>>>>>> >>>>>> >>>>>> But no one (except maybe you) didn't understand that the liar >>>>>> paradox wasn't a truth bearer. >>>>> >>>>> It sure would seem that way wouldn't it? >>>> >>>> Yep >>>> >>>>> >>>>> It turns out that the Liar Paradox as not >>>>> a truth bearer has never been accepted. >>>> >>>> Sure it has. It is you who just don't understand what people are >>>> talking about. >>>> >>>>> >>>>> It remains one of the great unresolved >>>>> paradoxes of the world. >>>>> >>>> >>>> Nope. Care to docuement that claim? >>>> >>> >>> I know exactly how ridiculous it sounds. >>> None-the-less that the Liar Paradox has >>> no accepted resolutions remains a verified fact. >> >> Can you show where someone didn't consider it a non-truth-bearing >> statement? >> > > There isn't an accepted final resolution to the Liar Paradox—it remains > one of the most debated open problems in logic and philosophy! Nope, it is well resolved in formal logic, it just doesn't have a truth value. > > The Liar Paradox (sentences like "This sentence is false") has generated > numerous proposed solutions, but none has achieved consensus. Here are > the main approaches: > > 1. Tarski's Hierarchy of Languages > Truth predicates apply only to sentences in lower-level languages. The > liar sentence is blocked because it tries to apply a truth predicate to > itself within the same language level. This "solves" it but many find it > restrictive for natural language. And what is wrong with that rule? Note, this rule also resolves to there is no truth predicate that can be defined in its own language. And none of the following seem to be defined in normal FORMAL LOGIC systems. > > 2. Paraconsistent Logic > Accept that some contradictions can exist without everything becoming > provable. The liar sentence can be both true and false without the > logical system exploding. > > 3. Dialetheism (Graham Priest) > Accept that the liar sentence is actually both true and false—a "true > contradiction" or dialetheia. Challenges the law of non-contradiction. > > 4. Semantic Approaches > Various theories argue the liar sentence is meaningless, lacks a truth > value, or is semantically defective in some way. > > 5. Contextualism > The truth value shifts depending on context or level of evaluation. > > 6. Revision Theories > Truth values can be revised over time through iterative processes. > Each approach has its defenders and critics, and philosophers continue > to debate which (if any) is correct. The paradox remains philosophically > live—it's not "solved" in the way mathematical problems get solved with > accepted proofs. > >
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2025-12-14 21:22 -0600 |
| Message-ID | <10hnuss$1k71a$1@dont-email.me> |
| In reply to | #641939 |
On 12/14/2025 8:27 PM, Richard Damon wrote: > On 12/14/25 9:09 PM, olcott wrote: >> On 12/14/2025 7:46 PM, Richard Damon wrote: >>> On 12/14/25 8:08 PM, olcott wrote: >>>> On 12/14/2025 6:53 PM, Richard Damon wrote: >>>>> On 12/14/25 7:46 PM, olcott wrote: >>>>>> On 12/14/2025 6:13 PM, Richard Damon wrote: >>>>>>> On 12/14/25 6:14 PM, olcott wrote: >>>>>>>> On 12/14/2025 4:05 AM, Mikko wrote: >>>>>>>>> On 13/12/2025 16:43, olcott wrote: >>>>>>>>>> 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. >>>>>>>> >>>>>>>> Also every other decision problem instance >>>>>>>> with pathological self reference is isomorphic >>>>>>>> to the Liar Paradox. >>>>>>>> >>>>>>> >>>>>>> But no one (except maybe you) didn't understand that the liar >>>>>>> paradox wasn't a truth bearer. >>>>>> >>>>>> It sure would seem that way wouldn't it? >>>>> >>>>> Yep >>>>> >>>>>> >>>>>> It turns out that the Liar Paradox as not >>>>>> a truth bearer has never been accepted. >>>>> >>>>> Sure it has. It is you who just don't understand what people are >>>>> talking about. >>>>> >>>>>> >>>>>> It remains one of the great unresolved >>>>>> paradoxes of the world. >>>>>> >>>>> >>>>> Nope. Care to docuement that claim? >>>>> >>>> >>>> I know exactly how ridiculous it sounds. >>>> None-the-less that the Liar Paradox has >>>> no accepted resolutions remains a verified fact. >>> >>> Can you show where someone didn't consider it a non-truth-bearing >>> statement? >>> >> >> There isn't an accepted final resolution to the Liar Paradox—it >> remains one of the most debated open problems in logic and philosophy! > > Nope, it is well resolved in formal logic, it just doesn't have a truth > value. > >> >> The Liar Paradox (sentences like "This sentence is false") has >> generated numerous proposed solutions, but none has achieved >> consensus. Here are the main approaches: >> >> 1. Tarski's Hierarchy of Languages >> Truth predicates apply only to sentences in lower-level languages. The >> liar sentence is blocked because it tries to apply a truth predicate >> to itself within the same language level. This "solves" it but many >> find it restrictive for natural language. > > And what is wrong with that rule? Note, this rule also resolves to there > is no truth predicate that can be defined in its own language. > > And none of the following seem to be defined in normal FORMAL LOGIC > systems. > None of them (above or below) has ever been accepted as the final resolution. >> >> 2. Paraconsistent Logic >> Accept that some contradictions can exist without everything becoming >> provable. The liar sentence can be both true and false without the >> logical system exploding. >> >> 3. Dialetheism (Graham Priest) >> Accept that the liar sentence is actually both true and false—a "true >> contradiction" or dialetheia. Challenges the law of non-contradiction. >> >> 4. Semantic Approaches >> Various theories argue the liar sentence is meaningless, lacks a truth >> value, or is semantically defective in some way. >> >> 5. Contextualism >> The truth value shifts depending on context or level of evaluation. >> >> 6. Revision Theories >> Truth values can be revised over time through iterative processes. >> Each approach has its defenders and critics, and philosophers continue >> to debate which (if any) is correct. The paradox remains >> philosophically live—it's not "solved" in the way mathematical >> problems get solved with accepted proofs. >> >> > -- 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>
[toc] | [prev] | [next] | [standalone]
| From | Richard Damon <Richard@Damon-Family.org> |
|---|---|
| Date | 2025-12-15 07:33 -0500 |
| Message-ID | <SeT%Q.1362$qKWd.1045@fx42.iad> |
| In reply to | #641941 |
On 12/14/25 10:22 PM, olcott wrote: > On 12/14/2025 8:27 PM, Richard Damon wrote: >> On 12/14/25 9:09 PM, olcott wrote: >>> On 12/14/2025 7:46 PM, Richard Damon wrote: >>>> On 12/14/25 8:08 PM, olcott wrote: >>>>> On 12/14/2025 6:53 PM, Richard Damon wrote: >>>>>> On 12/14/25 7:46 PM, olcott wrote: >>>>>>> On 12/14/2025 6:13 PM, Richard Damon wrote: >>>>>>>> On 12/14/25 6:14 PM, olcott wrote: >>>>>>>>> On 12/14/2025 4:05 AM, Mikko wrote: >>>>>>>>>> On 13/12/2025 16:43, olcott wrote: >>>>>>>>>>> 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. >>>>>>>>> >>>>>>>>> Also every other decision problem instance >>>>>>>>> with pathological self reference is isomorphic >>>>>>>>> to the Liar Paradox. >>>>>>>>> >>>>>>>> >>>>>>>> But no one (except maybe you) didn't understand that the liar >>>>>>>> paradox wasn't a truth bearer. >>>>>>> >>>>>>> It sure would seem that way wouldn't it? >>>>>> >>>>>> Yep >>>>>> >>>>>>> >>>>>>> It turns out that the Liar Paradox as not >>>>>>> a truth bearer has never been accepted. >>>>>> >>>>>> Sure it has. It is you who just don't understand what people are >>>>>> talking about. >>>>>> >>>>>>> >>>>>>> It remains one of the great unresolved >>>>>>> paradoxes of the world. >>>>>>> >>>>>> >>>>>> Nope. Care to docuement that claim? >>>>>> >>>>> >>>>> I know exactly how ridiculous it sounds. >>>>> None-the-less that the Liar Paradox has >>>>> no accepted resolutions remains a verified fact. >>>> >>>> Can you show where someone didn't consider it a non-truth-bearing >>>> statement? >>>> >>> >>> There isn't an accepted final resolution to the Liar Paradox—it >>> remains one of the most debated open problems in logic and philosophy! >> >> Nope, it is well resolved in formal logic, it just doesn't have a >> truth value. >> >>> >>> The Liar Paradox (sentences like "This sentence is false") has >>> generated numerous proposed solutions, but none has achieved >>> consensus. Here are the main approaches: >>> >>> 1. Tarski's Hierarchy of Languages >>> Truth predicates apply only to sentences in lower-level languages. >>> The liar sentence is blocked because it tries to apply a truth >>> predicate to itself within the same language level. This "solves" it >>> but many find it restrictive for natural language. >> >> And what is wrong with that rule? Note, this rule also resolves to >> there is no truth predicate that can be defined in its own language. >> >> And none of the following seem to be defined in normal FORMAL LOGIC >> systems. >> > > None of them (above or below) has ever been > accepted as the final resolution. Sure they have (at least for the first few) as the fields that use them accept them. The field that doesn't is general philosophy which has the problem that it has no firm definition of truth, and thus NOTHING can actually be proven in it, it is all just a debating society based on subjective agreement (or disagreement). It is an essentially a rule-less domain, which is likely why you like to work in it. It has no bearing on the more formal theories that you try to applies is indecision too. At best it can try to argue that the fields are based on bad assumptions, but that is just the pot calling the kettle black, as it is based purely on baseless assumptions. Your problem boils down to not undertanding the importance of context, so you aren't even good at handling the fussy realm of philosophy, as you miss the meanings that come out of context. > >>> >>> 2. Paraconsistent Logic >>> Accept that some contradictions can exist without everything becoming >>> provable. The liar sentence can be both true and false without the >>> logical system exploding. >>> >>> 3. Dialetheism (Graham Priest) >>> Accept that the liar sentence is actually both true and false—a "true >>> contradiction" or dialetheia. Challenges the law of non-contradiction. >>> >>> 4. Semantic Approaches >>> Various theories argue the liar sentence is meaningless, lacks a >>> truth value, or is semantically defective in some way. >>> >>> 5. Contextualism >>> The truth value shifts depending on context or level of evaluation. >>> >>> 6. Revision Theories >>> Truth values can be revised over time through iterative processes. >>> Each approach has its defenders and critics, and philosophers >>> continue to debate which (if any) is correct. The paradox remains >>> philosophically live—it's not "solved" in the way mathematical >>> problems get solved with accepted proofs. >>> >>> >> > >
[toc] | [prev] | [next] | [standalone]
| From | Mikko <mikko.levanto@iki.fi> |
|---|---|
| Date | 2025-12-15 11:04 +0200 |
| Message-ID | <10hoive$1p2m3$2@dont-email.me> |
| In reply to | #641916 |
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. -- Mikko
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2025-12-15 08:03 -0600 |
| Message-ID | <10hp4eo$1uh6i$2@dont-email.me> |
| In reply to | #641950 |
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>
[toc] | [prev] | [next] | [standalone]
| From | Mikko <mikko.levanto@iki.fi> |
|---|---|
| Date | 2025-12-16 11:44 +0200 |
| Message-ID | <10hr9m8$2i2de$1@dont-email.me> |
| In reply to | #641962 |
On 15/12/2025 16:03, olcott wrote: > 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. It makes as much sense as "in other words" in your messages. -- Mikko
[toc] | [prev] | [next] | [standalone]
| From | Mikko <mikko.levanto@iki.fi> |
|---|---|
| Date | 2025-12-16 11:48 +0200 |
| Message-ID | <10hr9tt$2i2de$2@dont-email.me> |
| In reply to | #641916 |
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. > > Also every other decision problem instance > with pathological self reference is isomorphic > to the Liar Paradox. That doesn't support your claim, either. -- Mikko
[toc] | [prev] | [next] | [standalone]
| From | Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> |
|---|---|
| Date | 2025-12-05 10:49 +0000 |
| Message-ID | <10gudb4$186tf$2@dont-email.me> |
| In reply to | #641609 |
On 04/12/2025 14:06, olcott wrote: > % 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" No. I think I showed in one of my recent posts (using definition extensions) that you need to formalise the mathematicians notion of "proof /in/ [system]" vis-a-vis "let" and its stronger sibling "suppose". That's a bigger job than you've done. I need a new quotation convention for referring to things whose name has an existing meaning in my U-language, I quoted "let" and "suppose" as if I were using their names; I mean to use the things themselves, but they have to be quoted in some way to distinguish the objects of mathematical language from the verbs of ordinary language without introducing such incidental new names as I would otherwise need. -- Tristan Wibberley The message body is Copyright (C) 2025 Tristan Wibberley except citations and quotations noted. All Rights Reserved except that you may, of course, cite it academically giving credit to me, distribute it verbatim as part of a usenet system or its archives, and use it to promote my greatness and general superiority without misrepresentation of my opinions other than my opinion of my greatness and general superiority which you _may_ misrepresent. You definitely MAY NOT train any production AI system with it but you may train experimental AI that will only be used for evaluation of the AI methods it implements.
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2025-12-05 11:05 -0600 |
| Message-ID | <10gv3ck$1j4e9$1@dont-email.me> |
| In reply to | #641628 |
On 12/5/2025 4:49 AM, Tristan Wibberley wrote: > On 04/12/2025 14:06, olcott wrote: > >> % 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" > > No. I think I showed in one of my recent posts (using definition > extensions) that you need to formalise the mathematicians notion of > "proof /in/ [system]" vis-a-vis "let" and its stronger sibling > "suppose". That's a bigger job than you've done. > If an expression of language cannot be proven at all because it is semantically incoherent then it seems quite stupid to say that it cannot be proved in a specific formal system. > I need a new quotation convention for referring to things whose name has > an existing meaning in my U-language, I quoted "let" and "suppose" as if > I were using their names; I mean to use the things themselves, but they > have to be quoted in some way to distinguish the objects of mathematical > language from the verbs of ordinary language without introducing such > incidental new names as I would otherwise need. > Halting Problem Proof Counter-Example is Isomorphic to the Liar Paradox https://www.researchgate.net/publication/398375553_Halting_Problem_Proof_Counter-Example_is_Isomorphic_to_the_Liar_Paradox Gödel's 1931 Incompleteness is also comprehensively covered. -- Copyright 2025 Olcott My 28 year goal has been to make "true on the basis of meaning" computable. This required establishing a new foundation for correct reasoning.
[toc] | [prev] | [next] | [standalone]
| From | Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> |
|---|---|
| Date | 2025-12-06 08:24 +0000 |
| Message-ID | <10h0p8o$27ulm$1@dont-email.me> |
| In reply to | #641636 |
On 05/12/2025 17:05, olcott wrote: > On 12/5/2025 4:49 AM, Tristan Wibberley wrote: >> No. I think I showed in one of my recent posts (using definition >> extensions) that you need to formalise the mathematicians notion of >> "proof /in/ [system]" vis-a-vis "let" and its stronger sibling >> "suppose". That's a bigger job than you've done. >> > > If an expression of language cannot be proven at > all because it is semantically incoherent then it > seems quite stupid to say that it cannot be proved > in a specific formal system. See if you find my message in your newsreader in which I describe some definition extensions and systems related by them. There is critical matter of the precise meaning of "prove in a system" (mathematicians) and "derive of a system" (logicians). And the matter of whether your "F" refers to the system of which your definition of G is an axiom, to its related basic system of which your G is not, or to something else. -- Tristan Wibberley The message body is Copyright (C) 2025 Tristan Wibberley except citations and quotations noted. All Rights Reserved except that you may, of course, cite it academically giving credit to me, distribute it verbatim as part of a usenet system or its archives, and use it to promote my greatness and general superiority without misrepresentation of my opinions other than my opinion of my greatness and general superiority which you _may_ misrepresent. You definitely MAY NOT train any production AI system with it but you may train experimental AI that will only be used for evaluation of the AI methods it implements.
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2025-12-06 06:08 -0600 |
| Message-ID | <10h16cl$2crbn$1@dont-email.me> |
| In reply to | #641656 |
On 12/6/2025 2:24 AM, Tristan Wibberley wrote: > On 05/12/2025 17:05, olcott wrote: >> On 12/5/2025 4:49 AM, Tristan Wibberley wrote: > >>> No. I think I showed in one of my recent posts (using definition >>> extensions) that you need to formalise the mathematicians notion of >>> "proof /in/ [system]" vis-a-vis "let" and its stronger sibling >>> "suppose". That's a bigger job than you've done. >>> >> >> If an expression of language cannot be proven at >> all because it is semantically incoherent then it >> seems quite stupid to say that it cannot be proved >> in a specific formal system. > > See if you find my message in your newsreader in which I describe some > definition extensions and systems related by them. There is critical > matter of the precise meaning of "prove in a system" (mathematicians) > and "derive of a system" (logicians). And the matter of whether your "F" > refers to the system of which your definition of G is an axiom, to its > related basic system of which your G is not, or to something else. > > I just made the system have a large enough scope such that unprovable in the system means not a member of the body of general knowledge. https://www.researchgate.net/publication/398375553_Halting_Problem_Proof_Counter-Example_is_Isomorphic_to_the_Liar_Paradox I refute the halting problem then I refute Gödel's 1931 Incompleteness. -- Copyright 2025 Olcott My 28 year goal has been to make "true on the basis of meaning" computable. This required establishing a new foundation for correct reasoning.
[toc] | [prev] | [next] | [standalone]
| From | Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> |
|---|---|
| Date | 2025-12-06 13:03 +0000 |
| Message-ID | <10h19ie$2du4c$1@dont-email.me> |
| In reply to | #641665 |
On 06/12/2025 12:08, olcott wrote: > On 12/6/2025 2:24 AM, Tristan Wibberley wrote: >> See if you find my message in your newsreader in which I describe some >> definition extensions and systems related by them. There is critical >> matter of the precise meaning of "prove in a system" (mathematicians) >> and "derive of a system" (logicians). And the matter of whether your "F" >> refers to the system of which your definition of G is an axiom, to its >> related basic system of which your G is not, or to something else. >> >> > > I just made the system have a large enough scope > such that unprovable in the system means not a member > of the body of general knowledge. I think you're talking about the logicians "derivable of a system" (ie, "is among the theorems of a formal system"). I think you should read my more detailed message about definition extension. I'm super sleepy so I can't make myself find the message id, maybe later. -- Tristan Wibberley The message body is Copyright (C) 2025 Tristan Wibberley except citations and quotations noted. All Rights Reserved except that you may, of course, cite it academically giving credit to me, distribute it verbatim as part of a usenet system or its archives, and use it to promote my greatness and general superiority without misrepresentation of my opinions other than my opinion of my greatness and general superiority which you _may_ misrepresent. You definitely MAY NOT train any production AI system with it but you may train experimental AI that will only be used for evaluation of the AI methods it implements.
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2025-12-06 07:14 -0600 |
| Message-ID | <10h1a7o$2ebfq$1@dont-email.me> |
| In reply to | #641676 |
On 12/6/2025 7:03 AM, Tristan Wibberley wrote: > On 06/12/2025 12:08, olcott wrote: >> On 12/6/2025 2:24 AM, Tristan Wibberley wrote: > >>> See if you find my message in your newsreader in which I describe some >>> definition extensions and systems related by them. There is critical >>> matter of the precise meaning of "prove in a system" (mathematicians) >>> and "derive of a system" (logicians). And the matter of whether your "F" >>> refers to the system of which your definition of G is an axiom, to its >>> related basic system of which your G is not, or to something else. >>> >>> >> >> I just made the system have a large enough scope >> such that unprovable in the system means not a member >> of the body of general knowledge. > > I think you're talking about the logicians "derivable of a system" (ie, > "is among the theorems of a formal system"). > Semantically entailed on the basis of a complete finite set of basic facts of general knowledge encoded in formalized natural language. This last part is crucial because then provable means true and unprovable means not a member of the body of general knowledge. You never ever get true and unprovable. > I think you should read my more detailed message about definition > extension. I'm super sleepy so I can't make myself find the message id, > maybe later. > > -- Copyright 2025 Olcott My 28 year goal has been to make "true on the basis of meaning" computable. This required establishing a new foundation for correct reasoning.
[toc] | [prev] | [next] | [standalone]
| From | Mikko <mikko.levanto@iki.fi> |
|---|---|
| Date | 2025-12-08 11:18 +0200 |
| Message-ID | <10h655e$1hmk$1@dont-email.me> |
| In reply to | #641628 |
Tristan Wibberley kirjoitti 5.12.2025 klo 12.49: > I need a new quotation convention for referring to things whose name has > an existing meaning in my U-language, In ASCII text you can use quotes, apostrophes, and grave accents. If you need more quotes you can use any characters you don't need for other purposes. -- Mikko
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2025-12-08 13:12 -0600 |
| Message-ID | <10h77vb$bfof$2@dont-email.me> |
| In reply to | #641628 |
On 12/5/2025 4:49 AM, Tristan Wibberley wrote: > On 04/12/2025 14:06, olcott wrote: > >> % 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" > > No. I think I showed in one of my recent posts (using definition > extensions) that you need to formalise the mathematicians notion of > "proof /in/ [system]" vis-a-vis "let" and its stronger sibling > "suppose". That's a bigger job than you've done. > > I need a new quotation convention for referring to things whose name has > an existing meaning in my U-language, I quoted "let" and "suppose" as if > I were using their names; I mean to use the things themselves, but they > have to be quoted in some way to distinguish the objects of mathematical > language from the verbs of ordinary language without introducing such > incidental new names as I would otherwise need. > Semantics tautologies that define finite strings in terms of other finite strings to give the LHS its semantic meaning on the basis of the RHS. -- Copyright 2025 Olcott<br><br> My 28 year goal has been to make <br> "true on the basis of meaning" computable.<br><br> This required establishing a new foundation<br>
[toc] | [prev] | [next] | [standalone]
| From | Mikko <mikko.levanto@iki.fi> |
|---|---|
| Date | 2025-12-10 12:10 +0200 |
| Message-ID | <10hbgva$1e1qs$1@dont-email.me> |
| In reply to | #641751 |
olcott kirjoitti 8.12.2025 klo 21.12: > On 12/5/2025 4:49 AM, Tristan Wibberley wrote: >> On 04/12/2025 14:06, olcott wrote: >> >>> % 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" >> >> No. I think I showed in one of my recent posts (using definition >> extensions) that you need to formalise the mathematicians notion of >> "proof /in/ [system]" vis-a-vis "let" and its stronger sibling >> "suppose". That's a bigger job than you've done. >> >> I need a new quotation convention for referring to things whose name has >> an existing meaning in my U-language, I quoted "let" and "suppose" as if >> I were using their names; I mean to use the things themselves, but they >> have to be quoted in some way to distinguish the objects of mathematical >> language from the verbs of ordinary language without introducing such >> incidental new names as I would otherwise need. > Semantics tautologies that define finite strings in > terms of other finite strings to give the LHS its > semantic meaning on the basis of the RHS. You havn't given a single example of a smenatic tautology that can be interpreted as a definition nor a single example of defintion that is a semantic tautology. Perhaps it is possible if you define "semantic taultology" so that it needn't be anything like a tautology. -- Mikko
[toc] | [prev] | [next] | [standalone]
Page 5 of 6 — ← Prev page 1 2 3 4 [5] 6 Next page →
Back to top | Article view | sci.math
csiph-web