Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > sci.math > #641406 > unrolled thread
| Started by | olcott <polcott333@gmail.com> |
|---|---|
| First post | 2025-11-29 10:32 -0600 |
| Last post | 2025-11-29 15:08 -0500 |
| Articles | 20 on this page of 100 — 11 participants |
Back to article view | Back to sci.math
A new category of thought olcott <polcott333@gmail.com> - 2025-11-29 10:32 -0600
Re: A new category of thought Kaz Kylheku <046-301-5902@kylheku.com> - 2025-11-29 17:53 +0000
Re: A new category of thought olcott <polcott333@gmail.com> - 2025-11-29 12:07 -0600
Re: A new category of thought dbush <dbush.mobile@gmail.com> - 2025-11-29 13:19 -0500
Re: A new category of thought Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2025-12-01 16:55 +0000
Re: A new category of thought olcott <polcott333@gmail.com> - 2025-12-01 11:04 -0600
Re: A new category of thought Mikko <mikko.levanto@iki.fi> - 2025-12-02 11:49 +0200
Re: A new category of thought olcott <polcott333@gmail.com> - 2025-12-02 09:26 -0600
Re: A new category of thought olcott <polcott333@gmail.com> - 2025-12-04 08:46 -0600
Re: A new category of thought Mikko <mikko.levanto@iki.fi> - 2025-12-05 10:52 +0200
Re: A new category of thought olcott <polcott333@gmail.com> - 2025-12-05 11:21 -0600
Re: A new category of thought André G. Isaak <agisaak@gm.invalid> - 2025-12-05 19:57 -0700
Re: A new category of thought olcott <polcott333@gmail.com> - 2025-12-05 21:18 -0600
Re: A new category of thought Mikko <mikko.levanto@iki.fi> - 2025-12-06 11:01 +0200
Re: A new category of thought olcott <polcott333@gmail.com> - 2025-12-06 06:40 -0600
Re: A new category of thought Mikko <mikko.levanto@iki.fi> - 2025-12-07 12:47 +0200
Re: A new category of thought olcott <polcott333@gmail.com> - 2025-12-07 09:16 -0600
Re: A new category of thought Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2025-12-08 02:04 +0000
Re: A new category of thought olcott <polcott333@gmail.com> - 2025-12-07 21:21 -0600
Re: A new category of thought Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2025-12-08 09:55 +0000
Re: A new category of thought olcott <polcott333@gmail.com> - 2025-12-08 12:43 -0600
Re: A new category of thought Richard Damon <Richard@Damon-Family.org> - 2025-12-06 22:16 -0500
Re: A new category of thought polcott <polcott333@gmail.com> - 2025-12-06 21:50 -0600
Re: A new category of thought Python <python@cccp.invalid> - 2025-12-07 05:32 +0000
Re: A new category of thought Mike Terry <news.dead.person.stones@darjeeling.plus.com> - 2025-12-07 15:49 +0000
Re: A new category of thought olcott <polcott333@gmail.com> - 2025-12-07 11:38 -0600
Re: A new category of thought Richard Damon <Richard@Damon-Family.org> - 2025-12-07 07:32 -0500
Re: A new category of thought olcott <polcott333@gmail.com> - 2025-12-07 07:37 -0600
Re: A new category of thought Richard Damon <Richard@Damon-Family.org> - 2025-12-07 17:55 -0500
Re: A new category of thought polcott <polcott333@gmail.com> - 2025-12-07 17:15 -0600
Re: A new category of thought Richard Damon <Richard@Damon-Family.org> - 2025-12-07 21:50 -0500
Re: A new category of thought olcott <polcott333@gmail.com> - 2025-12-07 21:26 -0600
Re: A new category of thought Richard Damon <Richard@Damon-Family.org> - 2025-12-08 07:40 -0500
Re: A new category of thought olcott <polcott333@gmail.com> - 2025-12-08 12:47 -0600
Re: A new category of thought Richard Damon <Richard@Damon-Family.org> - 2025-12-08 19:18 -0500
Re: A new category of thought polcott <polcott333@gmail.com> - 2025-12-08 19:00 -0600
Re: A new category of thought Richard Damon <Richard@Damon-Family.org> - 2025-12-08 21:24 -0500
Key new insight into halting undecidability polcott <polcott333@gmail.com> - 2025-12-08 20:34 -0600
Re: Key new insight into halting undecidability Richard Damon <Richard@Damon-Family.org> - 2025-12-08 21:57 -0500
Re: Key new insight into halting undecidability polcott <polcott333@gmail.com> - 2025-12-08 21:16 -0600
Re: Key new insight into halting undecidability Richard Damon <Richard@Damon-Family.org> - 2025-12-08 22:22 -0500
Re: Key new insight into halting undecidability polcott <polcott333@gmail.com> - 2025-12-08 21:50 -0600
Re: Key new insight into halting undecidability Richard Damon <Richard@Damon-Family.org> - 2025-12-08 23:20 -0500
Re: Key new insight into halting undecidability polcott <polcott333@gmail.com> - 2025-12-08 22:30 -0600
Re: Key new insight into halting undecidability Richard Damon <Richard@Damon-Family.org> - 2025-12-09 07:42 -0500
Re: Key new insight into halting undecidability polcott <polcott333@gmail.com> - 2025-12-09 10:05 -0600
Re: Key new insight into halting undecidability Richard Damon <Richard@Damon-Family.org> - 2025-12-09 23:02 -0500
Re: A new category of thought Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2025-12-08 02:14 +0000
Re: A new category of thought olcott <polcott333@gmail.com> - 2025-12-07 21:21 -0600
Re: A new category of thought Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2025-12-08 07:07 +0000
Re: A new category of thought olcott <polcott333@gmail.com> - 2025-12-08 10:41 -0600
Re: A new category of thought Python <python@cccp.invalid> - 2025-12-08 19:39 +0000
Re: A new category of thought Mikko <mikko.levanto@iki.fi> - 2025-12-05 10:57 +0200
Re: A new category of thought olcott <polcott333@gmail.com> - 2025-12-05 11:30 -0600
Re: A new category of thought Mikko <mikko.levanto@iki.fi> - 2025-12-06 10:53 +0200
Re: A new category of thought olcott <polcott333@gmail.com> - 2025-12-06 06:33 -0600
Re: A new category of thought Mikko <mikko.levanto@iki.fi> - 2025-12-07 12:42 +0200
Re: A new category of thought olcott <polcott333@gmail.com> - 2025-12-07 09:03 -0600
Re: A new category of thought Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2025-12-08 06:12 +0000
Re: A new category of thought olcott <polcott333@gmail.com> - 2025-12-08 07:59 -0600
Re: A new category of thought olcott <polcott333@gmail.com> - 2025-12-08 10:18 -0600
Re: A new category of thought Kaz Kylheku <046-301-5902@kylheku.com> - 2025-11-29 20:23 +0000
Re: A new category of thought olcott <polcott333@gmail.com> - 2025-11-29 14:51 -0600
Re: A new category of thought Richard Damon <Richard@Damon-Family.org> - 2025-11-29 16:27 -0500
Re: A new category of thought "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2025-11-29 15:53 -0800
Re: A new category of thought Richard Damon <Richard@Damon-Family.org> - 2025-11-29 19:17 -0500
Re: A new category of thought "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2025-11-29 16:35 -0800
Re: A new category of thought Richard Damon <Richard@Damon-Family.org> - 2025-11-29 20:10 -0500
Re: A new category of thought "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2025-11-29 19:49 -0800
Re: A new category of thought "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2025-11-29 19:50 -0800
Re: A new category of thought Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2025-12-02 01:59 +0000
Re: A new category of thought Richard Damon <Richard@Damon-Family.org> - 2025-12-01 23:11 -0500
Re: A new category of thought Kaz Kylheku <046-301-5902@kylheku.com> - 2025-11-29 21:39 +0000
Re: A new category of thought olcott <polcott333@gmail.com> - 2025-11-29 15:59 -0600
Re: A new category of thought Kaz Kylheku <046-301-5902@kylheku.com> - 2025-11-29 22:44 +0000
Re: A new category of thought olcott <polcott333@gmail.com> - 2025-11-29 17:19 -0600
Re: A new category of thought Richard Damon <Richard@Damon-Family.org> - 2025-11-29 19:21 -0500
Re: A new category of thought Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2025-12-02 01:13 +0000
Re: A new category of thought olcott <polcott333@gmail.com> - 2025-12-01 19:50 -0600
Re: A new category of thought Mikko <mikko.levanto@iki.fi> - 2025-12-01 13:02 +0200
Re: A new category of thought olcott <polcott333@gmail.com> - 2025-12-01 11:15 -0600
Re: A new category of thought Mikko <mikko.levanto@iki.fi> - 2025-12-02 10:53 +0200
Re: A new category of thought olcott <polcott333@gmail.com> - 2025-12-02 08:00 -0600
Re: A new category of thought Mikko <mikko.levanto@iki.fi> - 2025-12-03 12:41 +0200
Re: A new category of thought olcott <polcott333@gmail.com> - 2025-12-03 09:59 -0600
Re: A new category of thought Mikko <mikko.levanto@iki.fi> - 2025-12-05 10:48 +0200
Re: A new category of thought Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2025-12-05 09:30 +0000
Re: A new category of thought olcott <polcott333@gmail.com> - 2025-12-05 10:41 -0600
Re: A new category of thought Mikko <mikko.levanto@iki.fi> - 2025-12-06 10:37 +0200
Re: A new category of thought olcott <polcott333@gmail.com> - 2025-12-06 06:24 -0600
Re: A new category of thought Mikko <mikko.levanto@iki.fi> - 2025-12-07 12:39 +0200
Re: A new category of thought olcott <polcott333@gmail.com> - 2025-12-07 08:59 -0600
Re: A new category of thought Mikko <mikko.levanto@iki.fi> - 2025-12-09 15:15 +0200
Re: A new category of thought polcott <polcott333@gmail.com> - 2025-12-09 12:04 -0600
Re: A new category of thought Mikko <mikko.levanto@iki.fi> - 2025-12-14 13:02 +0200
Re: A new category of thought Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2025-12-02 01:39 +0000
Re: A new category of thought olcott <polcott333@gmail.com> - 2025-12-01 20:01 -0600
Re: A new category of thought Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2025-12-01 17:37 +0000
Re: A new category of thought olcott <polcott333@gmail.com> - 2025-12-01 13:44 -0600
Re: A new category of thought Richard Damon <Richard@Damon-Family.org> - 2025-11-29 15:08 -0500
Page 5 of 5 — ← Prev page 1 2 3 4 [5]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2025-12-01 11:15 -0600 |
| Message-ID | <10gkiev$1h8eo$1@dont-email.me> |
| In reply to | #641505 |
On 12/1/2025 5:02 AM, Mikko wrote: > olcott kirjoitti 29.11.2025 klo 23.59: > > G := (F ⊬ G) // G says of itself that it is unprovable in F > > With a reasonable type system that is a type error: > - the symbol ⊬ requires a sentence on the right side > - the value of the ⊬ operation is a truth value > - the symbol := requires the same type on both sides > - thus G must be both a sentence and a truth value > > But G cannot be both. A sentence has a truth value but it isn't one. > % 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. It is an expression of language having no truth value because it is not a logic sentence. https://en.wikipedia.org/wiki/Sentence_(mathematical_logic) -- 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-02 10:53 +0200 |
| Message-ID | <10gm9do$24og8$1@dont-email.me> |
| In reply to | #641530 |
olcott kirjoitti 1.12.2025 klo 19.15: > On 12/1/2025 5:02 AM, Mikko wrote: >> olcott kirjoitti 29.11.2025 klo 23.59: >> >> G := (F ⊬ G) // G says of itself that it is unprovable in F >> >> With a reasonable type system that is a type error: >> - the symbol ⊬ requires a sentence on the right side >> - the value of the ⊬ operation is a truth value >> - the symbol := requires the same type on both sides >> - thus G must be both a sentence and a truth value >> >> But G cannot be both. A sentence has a truth value but it isn't one. >> > > % 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. > > It is an expression of language having no truth value > because it is not a logic sentence. > > https://en.wikipedia.org/wiki/Sentence_(mathematical_logic) Yes, that is the exxential difference between the two G's. The expession F ⊬ G has a truth value because it is either true or false that G is no provable in F, and the same truth value is given to G in the expression G := (F ⊬ G). The Prolog term not(provable(F, G)) does not have a truth value. After G = not(provable(F, G)) the value of G is that data structure, so it has no truth value, unlike the G in G := (F ⊬ G). -- Mikko
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2025-12-02 08:00 -0600 |
| Message-ID | <10gmre5$2blfd$1@dont-email.me> |
| In reply to | #641559 |
On 12/2/2025 2:53 AM, Mikko wrote: > olcott kirjoitti 1.12.2025 klo 19.15: >> On 12/1/2025 5:02 AM, Mikko wrote: >>> olcott kirjoitti 29.11.2025 klo 23.59: >>> >>> G := (F ⊬ G) // G says of itself that it is unprovable in F >>> >>> With a reasonable type system that is a type error: >>> - the symbol ⊬ requires a sentence on the right side >>> - the value of the ⊬ operation is a truth value >>> - the symbol := requires the same type on both sides >>> - thus G must be both a sentence and a truth value >>> >>> But G cannot be both. A sentence has a truth value but it isn't one. >>> >> >> % 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. >> >> It is an expression of language having no truth value >> because it is not a logic sentence. >> >> https://en.wikipedia.org/wiki/Sentence_(mathematical_logic) > > Yes, that is the exxential difference between the two G's. > The expession F ⊬ G has a truth value because it is either > true or false I propose that is a false assumption. G := (F ⊬ G) expands to (F ⊬ (F ⊬ (F ⊬ (F ⊬ (F ⊬ (F ⊬ ...)))))) and Prolog agrees G = not(provable(F, G)). expands to: not(provable(F, not(provable(F, not(provable(F, ...)))))) We completely bypass all of this by creating a formal language that fully integrates semantics directly in the syntax. In this case not provable in F simply means not true in F. Truthmaker Maximalism is an entire field of philosophy that deals with this. We can implement the notion of a Tarski theory / meta-theory in a single formal language implementing Gödel's 1944 "theory of simple types". "This sentence is not true" has a semantic type of ~truth_bearer. That is what makes this sentence true: This sentence is not true: "This sentence is not true" > that G is no provable in F, and the same truth > value is given to G in the expression G := (F ⊬ G). The > Prolog term not(provable(F, G)) does not have a truth value. Yes you are getting it now. > After G = not(provable(F, G)) the value of G is that data > structure, so it has no truth value, unlike the G in > G := (F ⊬ G). > Maybe we should stick with the Prolog then. I only created Minimal Type Theory because I didn't know that Prolog could to the same thing. Because I created Minimal Type Theory I know that pathological self-reference(Olcott 2004) creates cycles in the directed graph of evaluation sequence thus showing that evaluation gets stuck in an infinite loop never reaching a truth value. -- 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-03 12:41 +0200 |
| Message-ID | <10gp441$37f5l$1@dont-email.me> |
| In reply to | #641566 |
olcott kirjoitti 2.12.2025 klo 16.00: > On 12/2/2025 2:53 AM, Mikko wrote: >> olcott kirjoitti 1.12.2025 klo 19.15: >>> On 12/1/2025 5:02 AM, Mikko wrote: >>>> olcott kirjoitti 29.11.2025 klo 23.59: >>>> >>>> G := (F ⊬ G) // G says of itself that it is unprovable in F >>>> >>>> With a reasonable type system that is a type error: >>>> - the symbol ⊬ requires a sentence on the right side >>>> - the value of the ⊬ operation is a truth value >>>> - the symbol := requires the same type on both sides >>>> - thus G must be both a sentence and a truth value >>>> >>>> But G cannot be both. A sentence has a truth value but it isn't one. >>>> >>> >>> % 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. >>> >>> It is an expression of language having no truth value >>> because it is not a logic sentence. >>> >>> https://en.wikipedia.org/wiki/Sentence_(mathematical_logic) >> >> Yes, that is the exxential difference between the two G's. >> The expession F ⊬ G has a truth value because it is either >> true or false > > I propose that is a false assumption. If you want to propose anygthng like that you should (a) specify what is the assumption you want to propose as false (b) why should that assumption be considered false (c) what assumption would be true or at least less obviously false -- Mikko
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2025-12-03 09:59 -0600 |
| Message-ID | <10gpmpn$3emj7$1@dont-email.me> |
| In reply to | #641578 |
On 12/3/2025 4:41 AM, Mikko wrote: > olcott kirjoitti 2.12.2025 klo 16.00: >> On 12/2/2025 2:53 AM, Mikko wrote: >>> olcott kirjoitti 1.12.2025 klo 19.15: >>>> On 12/1/2025 5:02 AM, Mikko wrote: >>>>> olcott kirjoitti 29.11.2025 klo 23.59: >>>>> >>>>> G := (F ⊬ G) // G says of itself that it is unprovable in F >>>>> >>>>> With a reasonable type system that is a type error: >>>>> - the symbol ⊬ requires a sentence on the right side >>>>> - the value of the ⊬ operation is a truth value >>>>> - the symbol := requires the same type on both sides >>>>> - thus G must be both a sentence and a truth value >>>>> >>>>> But G cannot be both. A sentence has a truth value but it isn't one. >>>>> >>>> >>>> % 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. >>>> >>>> It is an expression of language having no truth value >>>> because it is not a logic sentence. >>>> >>>> https://en.wikipedia.org/wiki/Sentence_(mathematical_logic) >>> >>> Yes, that is the exxential difference between the two G's. >>> The expession F ⊬ G has a truth value because it is either >>> true or false >> >> I propose that is a false assumption. > > If you want to propose anygthng like that you should > (a) specify what is the assumption you want to propose as false > (b) why should that assumption be considered false > (c) what assumption would be true or at least less obviously false > ?- G = not(provable(F, G)). G = not(provable(F, G)). ?- unify_with_occurs_check(G, not(provable(F, G))). false. G is neither True nor False its resolution remains stuck in an infinite loop. 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. END:(Clocksin & Mellish 2003:254) -- 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-05 10:48 +0200 |
| Message-ID | <10gu68i$15ok0$1@dont-email.me> |
| In reply to | #641583 |
olcott kirjoitti 3.12.2025 klo 17.59: > On 12/3/2025 4:41 AM, Mikko wrote: >> olcott kirjoitti 2.12.2025 klo 16.00: >>> On 12/2/2025 2:53 AM, Mikko wrote: >>>> olcott kirjoitti 1.12.2025 klo 19.15: >>>>> On 12/1/2025 5:02 AM, Mikko wrote: >>>>>> olcott kirjoitti 29.11.2025 klo 23.59: >>>>>> >>>>>> G := (F ⊬ G) // G says of itself that it is unprovable in F >>>>>> >>>>>> With a reasonable type system that is a type error: >>>>>> - the symbol ⊬ requires a sentence on the right side >>>>>> - the value of the ⊬ operation is a truth value >>>>>> - the symbol := requires the same type on both sides >>>>>> - thus G must be both a sentence and a truth value >>>>>> >>>>>> But G cannot be both. A sentence has a truth value but it isn't one. >>>>>> >>>>> >>>>> % 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. >>>>> >>>>> It is an expression of language having no truth value >>>>> because it is not a logic sentence. >>>>> >>>>> https://en.wikipedia.org/wiki/Sentence_(mathematical_logic) >>>> >>>> Yes, that is the exxential difference between the two G's. >>>> The expession F ⊬ G has a truth value because it is either >>>> true or false >>> >>> I propose that is a false assumption. >> >> If you want to propose anygthng like that you should >> (a) specify what is the assumption you want to propose as false >> (b) why should that assumption be considered false >> (c) what assumption would be true or at least less obviously false > ?- G = not(provable(F, G)). > G = not(provable(F, G)). > ?- unify_with_occurs_check(G, not(provable(F, G))). > false. > > G is neither True nor False its resolution remains stuck > in an infinite loop. > > 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. > END:(Clocksin & Mellish 2003:254) As even (a) is not answered we must interprete the above to mean that you retracted your proposal. -- Mikko
[toc] | [prev] | [next] | [standalone]
| From | Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> |
|---|---|
| Date | 2025-12-05 09:30 +0000 |
| Message-ID | <10gu8mq$16dq8$1@dont-email.me> |
| In reply to | #641619 |
On 05/12/2025 08:48, Mikko wrote: > As even (a) is not answered we must interprete the above to mean > that you retracted your proposal. > false. -- 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 10:41 -0600 |
| Message-ID | <10gv20f$1iduf$2@dont-email.me> |
| In reply to | #641619 |
On 12/5/2025 2:48 AM, Mikko wrote: > olcott kirjoitti 3.12.2025 klo 17.59: >> On 12/3/2025 4:41 AM, Mikko wrote: >>> olcott kirjoitti 2.12.2025 klo 16.00: >>>> On 12/2/2025 2:53 AM, Mikko wrote: >>>>> olcott kirjoitti 1.12.2025 klo 19.15: >>>>>> On 12/1/2025 5:02 AM, Mikko wrote: >>>>>>> olcott kirjoitti 29.11.2025 klo 23.59: >>>>>>> >>>>>>> G := (F ⊬ G) // G says of itself that it is unprovable in F >>>>>>> >>>>>>> With a reasonable type system that is a type error: >>>>>>> - the symbol ⊬ requires a sentence on the right side >>>>>>> - the value of the ⊬ operation is a truth value >>>>>>> - the symbol := requires the same type on both sides >>>>>>> - thus G must be both a sentence and a truth value >>>>>>> >>>>>>> But G cannot be both. A sentence has a truth value but it isn't one. >>>>>>> >>>>>> >>>>>> % 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. >>>>>> >>>>>> It is an expression of language having no truth value >>>>>> because it is not a logic sentence. >>>>>> >>>>>> https://en.wikipedia.org/wiki/Sentence_(mathematical_logic) >>>>> >>>>> Yes, that is the exxential difference between the two G's. >>>>> The expession F ⊬ G has a truth value because it is either >>>>> true or false >>>> >>>> I propose that is a false assumption. >>> >>> If you want to propose anygthng like that you should >>> (a) specify what is the assumption you want to propose as false >>> (b) why should that assumption be considered false >>> (c) what assumption would be true or at least less obviously false > >> ?- G = not(provable(F, G)). >> G = not(provable(F, G)). >> ?- unify_with_occurs_check(G, not(provable(F, G))). >> false. >> >> G is neither True nor False its resolution remains stuck >> in an infinite loop. >> >> 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. >> END:(Clocksin & Mellish 2003:254) > > As even (a) is not answered we must interprete the above to mean > that you retracted your proposal. > If you understood the above you would understand that I already answered (a) in 100% complete detail. The assumption that is false is that G is not semantically incoherent. -- 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-06 10:37 +0200 |
| Message-ID | <10h0q1c$28ekd$1@dont-email.me> |
| In reply to | #641634 |
olcott kirjoitti 5.12.2025 klo 18.41: > On 12/5/2025 2:48 AM, Mikko wrote: >> olcott kirjoitti 3.12.2025 klo 17.59: >>> On 12/3/2025 4:41 AM, Mikko wrote: >>>> olcott kirjoitti 2.12.2025 klo 16.00: >>>>> On 12/2/2025 2:53 AM, Mikko wrote: >>>>>> olcott kirjoitti 1.12.2025 klo 19.15: >>>>>>> On 12/1/2025 5:02 AM, Mikko wrote: >>>>>>>> olcott kirjoitti 29.11.2025 klo 23.59: >>>>>>>> >>>>>>>> G := (F ⊬ G) // G says of itself that it is unprovable in F >>>>>>>> >>>>>>>> With a reasonable type system that is a type error: >>>>>>>> - the symbol ⊬ requires a sentence on the right side >>>>>>>> - the value of the ⊬ operation is a truth value >>>>>>>> - the symbol := requires the same type on both sides >>>>>>>> - thus G must be both a sentence and a truth value >>>>>>>> >>>>>>>> But G cannot be both. A sentence has a truth value but it isn't >>>>>>>> one. >>>>>>>> >>>>>>> >>>>>>> % 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. >>>>>>> >>>>>>> It is an expression of language having no truth value >>>>>>> because it is not a logic sentence. >>>>>>> >>>>>>> https://en.wikipedia.org/wiki/Sentence_(mathematical_logic) >>>>>> >>>>>> Yes, that is the exxential difference between the two G's. >>>>>> The expession F ⊬ G has a truth value because it is either >>>>>> true or false >>>>> >>>>> I propose that is a false assumption. >>>> >>>> If you want to propose anygthng like that you should >>>> (a) specify what is the assumption you want to propose as false >>>> (b) why should that assumption be considered false >>>> (c) what assumption would be true or at least less obviously false >> >>> ?- G = not(provable(F, G)). >>> G = not(provable(F, G)). >>> ?- unify_with_occurs_check(G, not(provable(F, G))). >>> false. >>> >>> G is neither True nor False its resolution remains stuck >>> in an infinite loop. >>> >>> 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. >>> END:(Clocksin & Mellish 2003:254) >> >> As even (a) is not answered we must interprete the above to mean >> that you retracted your proposal. > If you understood the above you would understand > that I already answered (a) in 100% complete detail. Apparently "that" in your "I propopose that is a false assumption" refers to my "yes" response to your previous posting. But that response does not oresent any assumption. As everyone can see, you did not indentify the assumption. > The assumption that is false is that G is not > semantically incoherent. That assumption is not present in any plase that the word "that" could refer to. -- Mikko
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2025-12-06 06:24 -0600 |
| Message-ID | <10h179h$2d17n$4@dont-email.me> |
| In reply to | #641657 |
On 12/6/2025 2:37 AM, Mikko wrote: > olcott kirjoitti 5.12.2025 klo 18.41: >> On 12/5/2025 2:48 AM, Mikko wrote: >>> olcott kirjoitti 3.12.2025 klo 17.59: >>>> On 12/3/2025 4:41 AM, Mikko wrote: >>>>> olcott kirjoitti 2.12.2025 klo 16.00: >>>>>> On 12/2/2025 2:53 AM, Mikko wrote: >>>>>>> olcott kirjoitti 1.12.2025 klo 19.15: >>>>>>>> On 12/1/2025 5:02 AM, Mikko wrote: >>>>>>>>> olcott kirjoitti 29.11.2025 klo 23.59: >>>>>>>>> >>>>>>>>> G := (F ⊬ G) // G says of itself that it is unprovable in F >>>>>>>>> >>>>>>>>> With a reasonable type system that is a type error: >>>>>>>>> - the symbol ⊬ requires a sentence on the right side >>>>>>>>> - the value of the ⊬ operation is a truth value >>>>>>>>> - the symbol := requires the same type on both sides >>>>>>>>> - thus G must be both a sentence and a truth value >>>>>>>>> >>>>>>>>> But G cannot be both. A sentence has a truth value but it isn't >>>>>>>>> one. >>>>>>>>> >>>>>>>> >>>>>>>> % 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. >>>>>>>> >>>>>>>> It is an expression of language having no truth value >>>>>>>> because it is not a logic sentence. >>>>>>>> >>>>>>>> https://en.wikipedia.org/wiki/Sentence_(mathematical_logic) >>>>>>> >>>>>>> Yes, that is the exxential difference between the two G's. >>>>>>> The expession F ⊬ G has a truth value because it is either >>>>>>> true or false >>>>>> >>>>>> I propose that is a false assumption. >>>>> >>>>> If you want to propose anygthng like that you should >>>>> (a) specify what is the assumption you want to propose as false >>>>> (b) why should that assumption be considered false >>>>> (c) what assumption would be true or at least less obviously false >>> >>>> ?- G = not(provable(F, G)). >>>> G = not(provable(F, G)). >>>> ?- unify_with_occurs_check(G, not(provable(F, G))). >>>> false. >>>> >>>> G is neither True nor False its resolution remains stuck >>>> in an infinite loop. >>>> >>>> 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. >>>> END:(Clocksin & Mellish 2003:254) >>> >>> As even (a) is not answered we must interprete the above to mean >>> that you retracted your proposal. > >> If you understood the above you would understand >> that I already answered (a) in 100% complete detail. > > Apparently "that" in your "I propopose that is a false assumption" > refers to my "yes" response to your previous posting. But that > response does not oresent any assumption. > > As everyone can see, you did not indentify the assumption. > >> The assumption that is false is that G is not >> semantically incoherent. > > That assumption is not present in any plase that the word "that" > could refer to. > I explained all of the details of how G is semantically incoherent and you understood none of it. -- 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-07 12:39 +0200 |
| Message-ID | <10h3lh6$3ci3p$1@dont-email.me> |
| In reply to | #641668 |
olcott kirjoitti 6.12.2025 klo 14.24: > On 12/6/2025 2:37 AM, Mikko wrote: >> olcott kirjoitti 5.12.2025 klo 18.41: >>> On 12/5/2025 2:48 AM, Mikko wrote: >>>> olcott kirjoitti 3.12.2025 klo 17.59: >>>>> On 12/3/2025 4:41 AM, Mikko wrote: >>>>>> olcott kirjoitti 2.12.2025 klo 16.00: >>>>>>> On 12/2/2025 2:53 AM, Mikko wrote: >>>>>>>> olcott kirjoitti 1.12.2025 klo 19.15: >>>>>>>>> On 12/1/2025 5:02 AM, Mikko wrote: >>>>>>>>>> olcott kirjoitti 29.11.2025 klo 23.59: >>>>>>>>>> >>>>>>>>>> G := (F ⊬ G) // G says of itself that it is unprovable in F >>>>>>>>>> >>>>>>>>>> With a reasonable type system that is a type error: >>>>>>>>>> - the symbol ⊬ requires a sentence on the right side >>>>>>>>>> - the value of the ⊬ operation is a truth value >>>>>>>>>> - the symbol := requires the same type on both sides >>>>>>>>>> - thus G must be both a sentence and a truth value >>>>>>>>>> >>>>>>>>>> But G cannot be both. A sentence has a truth value but it >>>>>>>>>> isn't one. >>>>>>>>>> >>>>>>>>> >>>>>>>>> % 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. >>>>>>>>> >>>>>>>>> It is an expression of language having no truth value >>>>>>>>> because it is not a logic sentence. >>>>>>>>> >>>>>>>>> https://en.wikipedia.org/wiki/Sentence_(mathematical_logic) >>>>>>>> >>>>>>>> Yes, that is the exxential difference between the two G's. >>>>>>>> The expession F ⊬ G has a truth value because it is either >>>>>>>> true or false >>>>>>> >>>>>>> I propose that is a false assumption. >>>>>> >>>>>> If you want to propose anygthng like that you should >>>>>> (a) specify what is the assumption you want to propose as false >>>>>> (b) why should that assumption be considered false >>>>>> (c) what assumption would be true or at least less obviously false >>>> >>>>> ?- G = not(provable(F, G)). >>>>> G = not(provable(F, G)). >>>>> ?- unify_with_occurs_check(G, not(provable(F, G))). >>>>> false. >>>>> >>>>> G is neither True nor False its resolution remains stuck >>>>> in an infinite loop. >>>>> >>>>> 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. >>>>> END:(Clocksin & Mellish 2003:254) >>>> >>>> As even (a) is not answered we must interprete the above to mean >>>> that you retracted your proposal. >> >>> If you understood the above you would understand >>> that I already answered (a) in 100% complete detail. >> >> Apparently "that" in your "I propopose that is a false assumption" >> refers to my "yes" response to your previous posting. But that >> response does not oresent any assumption. >> >> As everyone can see, you did not indentify the assumption. >> >>> The assumption that is false is that G is not >>> semantically incoherent. >> >> That assumption is not present in any plase that the word "that" >> could refer to. > > I explained all of the details of how G is > semantically incoherent and you understood none of it. The question (a) is still unanswered, apparently because the answer would reveal that your claim the equestion is about is false. -- Mikko
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2025-12-07 08:59 -0600 |
| Message-ID | <10h44ns$3gl41$1@dont-email.me> |
| In reply to | #641695 |
On 12/7/2025 4:39 AM, Mikko wrote: > olcott kirjoitti 6.12.2025 klo 14.24: >> On 12/6/2025 2:37 AM, Mikko wrote: >>> olcott kirjoitti 5.12.2025 klo 18.41: >>>> On 12/5/2025 2:48 AM, Mikko wrote: >>>>> olcott kirjoitti 3.12.2025 klo 17.59: >>>>>> On 12/3/2025 4:41 AM, Mikko wrote: >>>>>>> olcott kirjoitti 2.12.2025 klo 16.00: >>>>>>>> On 12/2/2025 2:53 AM, Mikko wrote: >>>>>>>>> olcott kirjoitti 1.12.2025 klo 19.15: >>>>>>>>>> On 12/1/2025 5:02 AM, Mikko wrote: >>>>>>>>>>> olcott kirjoitti 29.11.2025 klo 23.59: >>>>>>>>>>> >>>>>>>>>>> G := (F ⊬ G) // G says of itself that it is unprovable in F >>>>>>>>>>> >>>>>>>>>>> With a reasonable type system that is a type error: >>>>>>>>>>> - the symbol ⊬ requires a sentence on the right side >>>>>>>>>>> - the value of the ⊬ operation is a truth value >>>>>>>>>>> - the symbol := requires the same type on both sides >>>>>>>>>>> - thus G must be both a sentence and a truth value >>>>>>>>>>> >>>>>>>>>>> But G cannot be both. A sentence has a truth value but it >>>>>>>>>>> isn't one. >>>>>>>>>>> >>>>>>>>>> >>>>>>>>>> % 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. >>>>>>>>>> >>>>>>>>>> It is an expression of language having no truth value >>>>>>>>>> because it is not a logic sentence. >>>>>>>>>> >>>>>>>>>> https://en.wikipedia.org/wiki/Sentence_(mathematical_logic) >>>>>>>>> >>>>>>>>> Yes, that is the exxential difference between the two G's. >>>>>>>>> The expession F ⊬ G has a truth value because it is either >>>>>>>>> true or false >>>>>>>> >>>>>>>> I propose that is a false assumption. >>>>>>> >>>>>>> If you want to propose anygthng like that you should >>>>>>> (a) specify what is the assumption you want to propose as false >>>>>>> (b) why should that assumption be considered false >>>>>>> (c) what assumption would be true or at least less obviously false >>>>> >>>>>> ?- G = not(provable(F, G)). >>>>>> G = not(provable(F, G)). >>>>>> ?- unify_with_occurs_check(G, not(provable(F, G))). >>>>>> false. >>>>>> >>>>>> G is neither True nor False its resolution remains stuck >>>>>> in an infinite loop. >>>>>> >>>>>> 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. >>>>>> END:(Clocksin & Mellish 2003:254) >>>>> >>>>> As even (a) is not answered we must interprete the above to mean >>>>> that you retracted your proposal. >>> >>>> If you understood the above you would understand >>>> that I already answered (a) in 100% complete detail. >>> >>> Apparently "that" in your "I propopose that is a false assumption" >>> refers to my "yes" response to your previous posting. But that >>> response does not oresent any assumption. >>> >>> As everyone can see, you did not indentify the assumption. >>> >>>> The assumption that is false is that G is not >>>> semantically incoherent. >>> >>> That assumption is not present in any plase that the word "that" >>> could refer to. >> >> I explained all of the details of how G is >> semantically incoherent and you understood none of it. > > > The question (a) is still unanswered, apparently because the answer > would reveal that your claim the equestion is about is false. > (a) specify what is the assumption you want to propose as false That Gödel 1931 Incompleteness exists as anything besides a misconception. I thought that when I proved that it is a misconception that you would be able to infer the incorrect assumption on the basis of this proof. Also if you could not infer this then you lack the prerequisites to understand what I am saying. -- 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-09 15:15 +0200 |
| Message-ID | <10h97dr$r6sm$1@dont-email.me> |
| In reply to | #641708 |
> On 12/7/2025 4:39 AM, Mikko wrote: >> olcott kirjoitti 6.12.2025 klo 14.24: >>> On 12/6/2025 2:37 AM, Mikko wrote: >>>> olcott kirjoitti 5.12.2025 klo 18.41: >>>>> On 12/5/2025 2:48 AM, Mikko wrote: >>>>>> olcott kirjoitti 3.12.2025 klo 17.59: >>>>>>> On 12/3/2025 4:41 AM, Mikko wrote: >>>>>>>> olcott kirjoitti 2.12.2025 klo 16.00: >>>>>>>>>>> On 12/1/2025 5:02 AM, Mikko wrote: >>>>>>>>>> Yes, that is the exxential difference between the two G's. >>>>>>>>>> The expession F ⊬ G has a truth value because it is either >>>>>>>>>> true or false >>>>>>>>>> olcott kirjoitti 1.12.2025 klo 19.15: >>>>>>>>> I propose that is a false assumption. >>>>>>>>> On 12/2/2025 2:53 AM, Mikko wrote: >>>>>>>> If you want to propose anygthng like that you should >>>>>>>> (a) specify what is the assumption you want to propose as false >>>>>>>> (b) why should that assumption be considered false >>>>>>>> (c) what assumption would be true or at least less obviously false olcott kirjoitti 7.12.2025 klo 16.59: > (a) specify what is the assumption you want to propose as false > That Gödel 1931 Incompleteness exists as anything > besides a misconception. That does not make sense. Quite obviously Gödel's incompleteness is not mentioned in the scope where that can refer. > I thought that when I proved that it is a misconception > that you would be able to infer the incorrect assumption > on the basis of this proof. Also if you could not infer > this then you lack the prerequisites to understand what > I am saying. If you don't understand how pronouns refer you should not use them. -- Mikko
[toc] | [prev] | [next] | [standalone]
| From | polcott <polcott333@gmail.com> |
|---|---|
| Date | 2025-12-09 12:04 -0600 |
| Message-ID | <10h9obu$1d3h0$1@solani.org> |
| In reply to | #641775 |
On 12/9/2025 7:15 AM, Mikko wrote: >> On 12/7/2025 4:39 AM, Mikko wrote: >>> olcott kirjoitti 6.12.2025 klo 14.24: >>>> On 12/6/2025 2:37 AM, Mikko wrote: >>>>> olcott kirjoitti 5.12.2025 klo 18.41: >>>>>> On 12/5/2025 2:48 AM, Mikko wrote: >>>>>>> olcott kirjoitti 3.12.2025 klo 17.59: >>>>>>>> On 12/3/2025 4:41 AM, Mikko wrote: >>>>>>>>> olcott kirjoitti 2.12.2025 klo 16.00: >>>>>>>>>>>> On 12/1/2025 5:02 AM, Mikko wrote: > >>>>>>>>>>> Yes, that is the exxential difference between the two G's. >>>>>>>>>>> The expession F ⊬ G has a truth value because it is either >>>>>>>>>>> true or false > >>>>>>>>>>> olcott kirjoitti 1.12.2025 klo 19.15: > >>>>>>>>>> I propose that is a false assumption. > > >>>>>>>>> On 12/2/2025 2:53 AM, Mikko wrote: > >>>>>>>>> If you want to propose anygthng like that you should >>>>>>>>> (a) specify what is the assumption you want to propose as false >>>>>>>>> (b) why should that assumption be considered false >>>>>>>>> (c) what assumption would be true or at least less obviously false > > olcott kirjoitti 7.12.2025 klo 16.59: > >> (a) specify what is the assumption you want to propose as false > >> That Gödel 1931 Incompleteness exists as anything >> besides a misconception. > > That does not make sense. Quite obviously Gödel's incompleteness is not > mentioned in the scope where that can refer. > Actually I proved that every instance of pathological self-reference involves an incoherent decision problem instance. The only reason that you do not understand that this proof is correct is your own lack of sufficient understanding of unify_with_occurs_check(). >> I thought that when I proved that it is a misconception >> that you would be able to infer the incorrect assumption >> on the basis of this proof. Also if you could not infer >> this then you lack the prerequisites to understand what >> I am saying. > > If you don't understand how pronouns refer you should not use them. > -- 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-14 13:02 +0200 |
| Message-ID | <10hm5gi$v2o8$1@dont-email.me> |
| In reply to | #641779 |
On 09/12/2025 20:04, polcott wrote: > On 12/9/2025 7:15 AM, Mikko wrote: >>> On 12/7/2025 4:39 AM, Mikko wrote: >>>> olcott kirjoitti 6.12.2025 klo 14.24: >>>>> On 12/6/2025 2:37 AM, Mikko wrote: >>>>>> olcott kirjoitti 5.12.2025 klo 18.41: >>>>>>> On 12/5/2025 2:48 AM, Mikko wrote: >>>>>>>> olcott kirjoitti 3.12.2025 klo 17.59: >>>>>>>>> On 12/3/2025 4:41 AM, Mikko wrote: >>>>>>>>>> olcott kirjoitti 2.12.2025 klo 16.00: >>>>>>>>>>>>> On 12/1/2025 5:02 AM, Mikko wrote: >> >>>>>>>>>>>> Yes, that is the exxential difference between the two G's. >>>>>>>>>>>> The expession F ⊬ G has a truth value because it is either >>>>>>>>>>>> true or false >> >>>>>>>>>>>> olcott kirjoitti 1.12.2025 klo 19.15: >> >>>>>>>>>>> I propose that is a false assumption. >> >> >>>>>>>>> On 12/2/2025 2:53 AM, Mikko wrote: >> >>>>>>>>>> If you want to propose anygthng like that you should >>>>>>>>>> (a) specify what is the assumption you want to propose as false >>>>>>>>>> (b) why should that assumption be considered false >>>>>>>>>> (c) what assumption would be true or at least less obviously >>>>>>>>>> false >> >> olcott kirjoitti 7.12.2025 klo 16.59: >> >>> (a) specify what is the assumption you want to propose as false >> >>> That Gödel 1931 Incompleteness exists as anything >>> besides a misconception. >> >> That does not make sense. Quite obviously Gödel's incompleteness is not >> mentioned in the scope where that can refer. > > Actually I proved that every instance of pathological > self-reference involves an incoherent decision problem > instance. Your "involves" does not mean anything other than "can be associated with", or at least you havn't proven anything else about it. But everything can "involve" an incoherent problem instance. That does not mean that everything exists only as a misconceptions. -- Mikko
[toc] | [prev] | [next] | [standalone]
| From | Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> |
|---|---|
| Date | 2025-12-02 01:39 +0000 |
| Message-ID | <10glg06$1roie$2@dont-email.me> |
| In reply to | #641505 |
On 01/12/2025 11:02, Mikko wrote: > olcott kirjoitti 29.11.2025 klo 23.59: > > G := (F ⊬ G) // G says of itself that it is unprovable in F > > With a reasonable type system that is a type error: > - the symbol ⊬ requires a sentence on the right side If we're using it in its normal epitheoretic meaning. I think Olcott is using it as a predicative object of a logistic F so it requires a formula on the right? That's not unreasonable since we take A |- B as a shorthand for |-A => |-B leaving us with "B is a formula" to which the unary predicate |- may be applied to make a statement. It's the epitheoretic "=>" that takes a statement on the right, but clearly it's more complex because systems and lists of statements can be used on the left. Olcott's use of |- as a predicative object of F is clearly awkwardly ambiguous, as tempting as it may be. The extra awkward thing here is that F is capable of using |- in its own formulae, making its (normal) use as a unary predicate redundant and perhaps obstructive leaving us with a system whose statements are exactly its formulas unless we have a unary predicative with no visible elements, if it's not nonsense for any other reasons. I wonder if that may not be done for some reason. There are lots of reasons to be concerned about it. > - the value of the ⊬ operation is a truth value /Should/ we take ⊬ to be an operation here? or just a predicative object of F? > - the symbol := requires the same type on both sides Unless it's an operation (as in, an action to be done to generate sentences/formulas of the system being analysed). When G is an epitheoretic object rather than an object of a definition extension of F then I think it /must/ be such an operation. -- 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-01 20:01 -0600 |
| Message-ID | <10glh9f$1t33g$1@dont-email.me> |
| In reply to | #641554 |
On 12/1/2025 7:39 PM, Tristan Wibberley wrote: > On 01/12/2025 11:02, Mikko wrote: >> olcott kirjoitti 29.11.2025 klo 23.59: >> >> G := (F ⊬ G) // G says of itself that it is unprovable in F >> >> With a reasonable type system that is a type error: >> - the symbol ⊬ requires a sentence on the right side > > If we're using it in its normal epitheoretic meaning. I think Olcott is > using it as a predicative object of a logistic F so it requires a > formula on the right? That's not unreasonable since we take > > A |- B > > as a shorthand for > > |-A => |-B > > leaving us with "B is a formula" to which the unary predicate |- may be > applied to make a statement. > The first incompleteness theorem states that in any consistent formal system F within which a certain amount of arithmetic can be carried out, there are statements of the language of F which can neither be proved nor disproved in F. https://plato.stanford.edu/entries/goedel-incompleteness/ (G) F ⊢ GF ↔ ¬ProvF(┌GF┐) https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom G ↔ ¬Prov(⌜G⌝) Directed Graph of evaluation sequence 00 ↔ 01 02 01 G 02 ¬ 03 03 Prov 04 04 Gödel_Number_of 01 // cycle thus stuck in infinite evaluation loop *YACC Syntax of Olcott Minimal Type Theory* https://philarchive.org/archive/PETMTT-4v2 I used the "defined as" operator to allow direct self-reference. > It's the epitheoretic "=>" that takes a statement on the right, but > clearly it's more complex because systems and lists of statements can be > used on the left. Olcott's use of |- as a predicative object of F is > clearly awkwardly ambiguous, as tempting as it may be. > > The extra awkward thing here is that F is capable of using |- in its own > formulae, making its (normal) use as a unary predicate redundant and > perhaps obstructive leaving us with a system whose statements are > exactly its formulas unless we have a unary predicative with no visible > elements, if it's not nonsense for any other reasons. > > I wonder if that may not be done for some reason. There are lots of > reasons to be concerned about it. > >> - the value of the ⊬ operation is a truth value > > /Should/ we take ⊬ to be an operation here? or just a predicative object > of F? > >> - the symbol := requires the same type on both sides > > Unless it's an operation (as in, an action to be done to generate > sentences/formulas of the system being analysed). When G is an > epitheoretic object rather than an object of a definition extension of F > then I think it /must/ be such an operation. > > -- 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-01 17:37 +0000 |
| Message-ID | <10gkjo3$1hrmo$1@dont-email.me> |
| In reply to | #641430 |
On 29/11/2025 20:51, olcott wrote: > Try and show how Gödel incompleteness can be > specified in a language that can directly encode > self-reference and has its own provability operator > without hiding the actual semantics using Gödel numbers. An outline how I'd go about this kind of thing (not complete by far, and also not checked properly, though I have thought about it a bit). I've done this about Olcott's paraphrasing of Goedel's outline in PM rather than the challenge stated above because Goedel's system P is weird and I don't trust it at all. IMPORTANT! Goedels outline and Olcott's paraphrase use a self-referential definition rather than universal quantification! I'll have to cogitate more to waffle about that. Note, it involves a formal system /extension/ rather than an /episystem/ and that's how we may interpret the challenge to do our task "in [the] language". Thinking about it a touch more carefully than before, assuming Olcott very carefully formulated his G definition (I think F is nothing to do with Goedel's system P, but is more akin to a modernisation of PM which goedel used for his similar outline). Note I have this time interpreted F to refer to a basic system rather than the definition extension that I previously supposed. This way we have a few points in the space of systems to reason more clearly with. You have to take this all with a pinch of salt, we're using ":=" and it will take some formalisation which I'm not doing (and so will |/-). Then consider Olcott's paraphrasing G := (F |/- G) The above must be an axiom of a definition extension I'll call "I" that also adjoins G and I to the objects of F and we'll assume we've already formalised extension within F. I'll call the resulting extended system "I(F)" and suppose that's the form by which statements in F may name a system "F" extended by I. In that case I(F) is consistent: G is not derived of F. We'd have a problem if I use a definition extension "J" that adjoins, instead, objects G and J and an axiom G := (J(F) |/- G). "J(F)" names what I assumed Olcott had meant "F" to name previously. I kind-of-conjecture that J(F) is contradictory because it seems obvious that we can derive both |- G and |/- G which is how we'll recognise contradiction. I hesitate to use the term "inconsistent" because I don't trust the concept having found "indiscriminate" to be satisfactory and more general for simpler systems. Having drawn a very faint line on a block of stone before spending eons carving and polishing and looking up to see what it took to do so little, it is obvious why Olcott has not been swayed by the conversations in these newsgroups. -- 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-01 13:44 -0600 |
| Message-ID | <10gkr6f$1l2cr$1@dont-email.me> |
| In reply to | #641531 |
On 12/1/2025 11:37 AM, Tristan Wibberley wrote: > On 29/11/2025 20:51, olcott wrote: > >> Try and show how Gödel incompleteness can be >> specified in a language that can directly encode >> self-reference and has its own provability operator >> without hiding the actual semantics using Gödel numbers. > > An outline how I'd go about this kind of thing (not complete by far, and > also not checked properly, though I have thought about it a bit). I've > done this about Olcott's paraphrasing of Goedel's outline in PM rather > than the challenge stated above because Goedel's system P is weird and I > don't trust it at all. IMPORTANT! Goedels outline and Olcott's > paraphrase use a self-referential definition rather than universal > quantification! I'll have to cogitate more to waffle about that. > > Note, it involves a formal system /extension/ rather than an /episystem/ > and that's how we may interpret the challenge to do our task "in [the] > language". > > Thinking about it a touch more carefully than before, assuming Olcott > very carefully formulated his G definition (I think F is nothing to do > with Goedel's system P, but is more akin to a modernisation of PM which > goedel used for his similar outline). Note I have this time interpreted > F to refer to a basic system rather than the definition extension that I > previously supposed. This way we have a few points in the space of > systems to reason more clearly with. > > You have to take this all with a pinch of salt, we're using ":=" and it > will take some formalisation which I'm not doing (and so will |/-). > > > Then consider Olcott's paraphrasing > > G := (F |/- G) > > The above must be an axiom of a definition extension I'll call "I" that > also adjoins G and I to the objects of F and we'll assume we've already > formalised extension within F. I'll call the resulting extended system > "I(F)" and suppose that's the form by which statements in F may name a > system "F" extended by I. > > In that case I(F) is consistent: G is not derived of F. > > We'd have a problem if I use a definition extension "J" that adjoins, > instead, objects G and J and an axiom > > G := (J(F) |/- G). > > "J(F)" names what I assumed Olcott had meant "F" to name previously. I > kind-of-conjecture that J(F) is contradictory because it seems obvious > that we can derive both |- G and |/- G which is how we'll recognise > contradiction. I hesitate to use the term "inconsistent" because I don't > trust the concept having found "indiscriminate" to be satisfactory and > more general for simpler systems. > > > Having drawn a very faint line on a block of stone before spending eons > carving and polishing and looking up to see what it took to do so > little, it is obvious why Olcott has not been swayed by the > conversations in these newsgroups. > I have not been swayed because there have been no actual rebuttals on the basis of actual correct reasoning. Most all of the rebuttals have been some form of "we really really don't believe you". Here is Prolog directly showing how Pathological self-reference(Olcott 2004) make an expression semantically unsound. % This sentence is not true. ?- LP = not(true(LP)). LP = not(true(LP)). ?- unify_with_occurs_check(LP, not(true(LP))). false. % 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. 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. END:(Clocksin & Mellish 2003:254) This is the same as Olcott's Minimal Type Theory LP := ~True(LP) // LP is defined as ~True(LP) this expands to ~True(~True(~True(~True(~True(~True(...)))))) -- 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 | Richard Damon <Richard@Damon-Family.org> |
|---|---|
| Date | 2025-11-29 15:08 -0500 |
| Message-ID | <7pIWQ.9130$fEH6.3983@fx41.iad> |
| In reply to | #641406 |
On 11/29/25 11:32 AM, olcott wrote: > Any expression of language that is proven true entirely > on the basis of its meaning expressed in language is > a semantic tautology. > > I also call this Analytic(Olcott) > > https://plato.stanford.edu/entries/analytic-synthetic/ > > Two Dogmas of Empiricism > Willard Van Orman Quine > https://www.theologie.uzh.ch/dam/jcr:ffffffff- > fbd6-1538-0000-000070cf64bc/Quine51.pdf > > It overcomes Quine's objections by encoding basic facts > of the world as Rudolf Carnap Meaning Postulates organized > as a knowledge ontology inheritance hierarchy > > In information science, an ontology encompasses a > representation, formal naming, and definitions of > the categories, properties, and relations between > the concepts... > https://en.wikipedia.org/wiki/Ontology_(information_science) > > That is essentially Kurt Gödel's "theory of simple types" By > the theory of simple types I mean the doctrine which says > that the objects of thought ... are divided into types, > namely: individuals, properties of individuals, relations > between individuals, properties of such relations, etc. > https://en.wikipedia.org/wiki/History_of_type_theory#G%C3%B6del_1944 > Ib other words, you are claiming to have create a "logic system" that can only handle things that are tautologically true. Since most interesting statements are not tautologies, your system is just uninteresting at best, and generally worthless. Can you show an actually useful problem that you can actually SOLVE with your idea of a logic system.
[toc] | [prev] | [standalone]
Page 5 of 5 — ← Prev page 1 2 3 4 [5]
Back to top | Article view | sci.math
csiph-web