Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > sci.logic > #344098 > unrolled thread
| Started by | olcott <polcott333@gmail.com> |
|---|---|
| First post | 2026-01-06 22:44 -0600 |
| Last post | 2026-01-09 09:47 -0600 |
| Articles | 20 on this page of 211 — 8 participants |
Back to article view | Back to sci.logic
The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-06 22:44 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-07 13:49 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-07 05:54 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-08 12:22 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-08 08:22 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-09 11:59 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-09 09:52 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-10 10:23 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-10 09:47 -0600
Re: The Halting Problem asks for too much Richard Damon <news.x.richarddamon@xoxy.net> - 2026-01-10 18:19 -0500
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-10 18:13 -0600
Re: The Halting Problem asks for too much Richard Damon <news.x.richarddamon@xoxy.net> - 2026-01-10 19:35 -0500
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-10 18:52 -0600
Re: The Halting Problem asks for too much Richard Damon <news.x.richarddamon@xoxy.net> - 2026-01-10 21:03 -0500
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-10 20:22 -0600
Re: The Halting Problem asks for too much Richard Damon <news.x.richarddamon@xoxy.net> - 2026-01-10 21:34 -0500
Computation and Undecidability olcott <polcott333@gmail.com> - 2026-01-10 21:24 -0600
Re: Computation and Undecidability Richard Damon <news.x.richarddamon@xoxy.net> - 2026-01-10 22:32 -0500
Re: The Halting Problem asks for too much Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2026-01-11 07:09 +0000
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-11 12:13 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-11 08:18 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-12 12:44 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-12 08:29 -0600
Re: The Halting Problem asks for too much Richard Damon <Richard@Damon-Family.org> - 2026-01-12 22:19 -0500
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-14 19:25 -0600
Re: The Halting Problem asks for too much Richard Damon <Richard@Damon-Family.org> - 2026-01-14 22:51 -0500
Re: The Halting Problem asks for too much Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2026-01-15 15:57 +0000
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-15 10:54 -0600
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-15 11:34 -0600
Re: The Halting Problem asks for too much Richard Damon <Richard@Damon-Family.org> - 2026-01-15 22:27 -0500
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-15 22:03 -0600
Re: The Halting Problem asks for too much Richard Damon <Richard@Damon-Family.org> - 2026-01-16 11:46 -0500
Re: The Halting Problem asks for too much Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2026-01-31 01:47 +0000
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-30 20:10 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-13 11:11 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-13 08:27 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-14 09:40 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-14 11:28 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-15 11:48 +0200
Re: The Halting Problem asks for too much Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2026-01-15 15:04 +0000
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-17 12:00 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-15 17:38 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-16 11:17 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-16 08:12 -0600
Re: The Halting Problem asks for too much Richard Damon <Richard@Damon-Family.org> - 2026-01-16 11:48 -0500
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-16 09:12 -0600
Re: The Halting Problem asks for too much Richard Damon <Richard@Damon-Family.org> - 2026-01-16 11:53 -0500
Re: The Halting Problem asks for too much Richard Damon <Richard@Damon-Family.org> - 2026-01-16 12:08 -0500
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-17 12:25 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-13 08:34 -0600
Re: The Halting Problem asks for too much Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2026-01-13 18:23 +0000
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-13 12:50 -0600
Re: The Halting Problem asks for too much Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2026-01-14 14:52 +0000
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-14 10:24 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-14 10:53 +0200
Re: The Halting Problem asks for too much Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2026-01-14 14:55 +0000
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-15 11:26 +0200
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-14 10:39 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-12 08:32 -0600
Re: The Halting Problem asks for too much Richard Damon <Richard@Damon-Family.org> - 2026-01-12 22:20 -0500
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-13 11:13 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-13 08:31 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-14 11:01 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-14 13:32 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-15 11:34 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-15 14:30 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-16 11:32 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-16 09:38 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-17 11:53 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-17 08:47 -0600
Re: The Halting Problem asks for too much Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2026-01-17 22:21 +0000
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-18 13:27 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-18 07:28 -0600
Re: The Halting Problem asks for too much Richard Damon <Richard@Damon-Family.org> - 2026-01-18 12:55 -0500
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-19 10:19 +0200
Re: The Halting Problem asks for too much Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2026-01-19 15:00 +0000
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-20 11:48 +0200
Re: The Halting Problem asks for too much Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2026-01-21 13:46 +0000
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-22 10:30 +0200
Re: The Halting Problem asks for too much Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2026-01-22 12:40 +0000
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-23 11:31 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-19 09:03 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-20 11:58 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-20 12:35 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-21 11:03 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-21 09:22 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-22 10:21 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-22 10:40 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-23 11:13 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-23 04:22 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-24 10:20 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-24 08:01 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-25 13:19 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-25 07:24 -0600
Re: The Halting Problem asks for too much Richard Damon <Richard@Damon-Family.org> - 2026-01-25 13:27 -0500
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-25 12:33 -0600
Re: The Halting Problem asks for too much Richard Damon <Richard@Damon-Family.org> - 2026-01-25 13:40 -0500
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-25 13:10 -0600
Re: The Halting Problem asks for too much Richard Damon <Richard@Damon-Family.org> - 2026-01-25 14:57 -0500
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-25 14:09 -0600
Re: The Halting Problem asks for too much Richard Damon <Richard@Damon-Family.org> - 2026-01-25 15:47 -0500
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-22 10:47 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-24 10:23 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-24 08:18 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-25 13:24 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-25 07:30 -0600
Re: The Halting Problem asks for too much Richard Damon <Richard@Damon-Family.org> - 2026-01-25 13:31 -0500
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-25 13:05 -0600
Re: The Halting Problem asks for too much Richard Damon <Richard@Damon-Family.org> - 2026-01-25 14:59 -0500
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-25 14:21 -0600
Re: The Halting Problem asks for too much Richard Damon <Richard@Damon-Family.org> - 2026-01-25 15:54 -0500
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-26 14:55 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-26 09:22 -0600
Re: The Halting Problem asks for too much Richard Damon <Richard@Damon-Family.org> - 2026-01-26 11:45 -0500
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-26 10:58 -0600
Re: The Halting Problem asks for too much Richard Damon <Richard@Damon-Family.org> - 2026-01-26 12:13 -0500
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-26 11:28 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-27 10:17 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-27 09:32 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-28 11:54 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-28 07:49 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-29 11:12 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-29 07:57 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-30 11:34 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-30 08:35 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-31 10:41 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-31 09:23 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-02-01 12:28 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-02-01 09:18 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-02-02 09:39 +0200
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-31 10:56 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-31 09:26 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-02-01 12:17 +0200
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-27 10:15 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-27 09:29 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-28 11:45 +0200
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-27 10:05 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-27 08:48 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-28 11:40 +0200
Re: The Halting Problem asks for too much Richard Damon <Richard@Damon-Family.org> - 2026-01-24 09:51 -0500
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-24 09:44 -0600
Re: The Halting Problem asks for too much Richard Damon <Richard@Damon-Family.org> - 2026-01-24 12:10 -0500
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-24 11:54 -0600
Re: The Halting Problem asks for too much Richard Damon <Richard@Damon-Family.org> - 2026-01-24 14:23 -0500
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-24 13:25 -0600
Re: The Halting Problem asks for too much Richard Damon <Richard@Damon-Family.org> - 2026-01-24 14:52 -0500
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-24 14:38 -0600
Re: The Halting Problem asks for too much Richard Damon <Richard@Damon-Family.org> - 2026-01-24 17:25 -0500
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-24 16:31 -0600
Re: The Halting Problem asks for too much Richard Damon <Richard@Damon-Family.org> - 2026-01-24 19:52 -0500
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-24 19:44 -0600
Re: The Halting Problem asks for too much Richard Damon <Richard@Damon-Family.org> - 2026-01-25 13:36 -0500
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-25 13:09 -0600
Re: The Halting Problem asks for too much Richard Damon <Richard@Damon-Family.org> - 2026-01-25 14:54 -0500
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-25 14:07 -0600
Re: The Halting Problem asks for too much Richard Damon <Richard@Damon-Family.org> - 2026-01-25 15:44 -0500
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-25 20:31 -0600
Re: The Halting Problem asks for too much Richard Damon <Richard@Damon-Family.org> - 2026-01-26 11:49 -0500
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-26 11:23 -0600
Re: The Halting Problem asks for too much Richard Damon <Richard@Damon-Family.org> - 2026-01-26 13:24 -0500
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-26 12:43 -0600
Re: The Halting Problem asks for too much Richard Damon <Richard@Damon-Family.org> - 2026-01-26 16:58 -0500
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-26 16:08 -0600
Re: The Halting Problem asks for too much Richard Damon <Richard@Damon-Family.org> - 2026-01-26 17:36 -0500
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-26 16:44 -0600
Re: The Halting Problem asks for too much Richard Damon <Richard@Damon-Family.org> - 2026-01-26 21:51 -0500
"true on the basis of meaning expressed in language" olcott <NoOne@NoWhere.com> - 2026-01-26 21:28 -0600
Re: The Halting Problem asks for too much dart200 <user7160@newsgrouper.org.invalid> - 2026-01-24 18:28 -0800
Re: The Halting Problem asks for too much Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2026-01-29 04:39 +0000
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-11 12:22 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-11 08:23 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-12 12:51 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-12 08:43 -0600
Re: The Halting Problem asks for too much Richard Damon <Richard@Damon-Family.org> - 2026-01-12 22:22 -0500
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-13 10:46 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-13 08:17 -0600
Re: The Halting Problem asks for too much Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2026-01-13 14:31 +0000
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-14 09:58 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-14 13:14 -0600
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-14 13:19 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-15 11:38 +0200
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-14 11:04 +0200
Re: The Halting Problem asks for too much olcott <polcott333@gmail.com> - 2026-01-14 13:35 -0600
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-15 11:21 +0200
Re: The Halting Problem asks for too much Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2026-01-15 14:52 +0000
Re: The Halting Problem asks for too much Mikko <mikko.levanto@iki.fi> - 2026-01-16 11:21 +0200
Computation and Undecidability olcott <polcott333@gmail.com> - 2026-01-10 17:19 -0600
Re: Computation and Undecidability Richard Damon <news.x.richarddamon@xoxy.net> - 2026-01-10 19:35 -0500
Re: Computation and Undecidability olcott <polcott333@gmail.com> - 2026-01-10 19:03 -0600
Re: Computation and Undecidability Richard Damon <news.x.richarddamon@xoxy.net> - 2026-01-10 21:03 -0500
Re: Computation and Undecidability olcott <polcott333@gmail.com> - 2026-01-10 20:20 -0600
Re: Computation and Undecidability Richard Damon <news.x.richarddamon@xoxy.net> - 2026-01-10 21:33 -0500
Re: Computation and Undecidability olcott <polcott333@gmail.com> - 2026-01-10 21:18 -0600
Re: Computation and Undecidability Richard Damon <news.x.richarddamon@xoxy.net> - 2026-01-10 22:30 -0500
Re: Computation and Undecidability olcott <polcott333@gmail.com> - 2026-01-10 19:05 -0600
Re: Computation and Undecidability Richard Damon <news.x.richarddamon@xoxy.net> - 2026-01-10 21:03 -0500
Re: Computation and Undecidability olcott <polcott333@gmail.com> - 2026-01-10 20:09 -0600
Re: Computation and Undecidability Richard Damon <news.x.richarddamon@xoxy.net> - 2026-01-10 21:33 -0500
Re: Computation and Undecidability polcott <polcott333@gmail.com> - 2026-01-10 20:52 -0600
Re: Computation and Undecidability Richard Damon <news.x.richarddamon@xoxy.net> - 2026-01-10 22:28 -0500
Re: Computation and Undecidability olcott <polcott333@gmail.com> - 2026-01-10 21:16 -0600
Re: Computation and Undecidability Richard Damon <news.x.richarddamon@xoxy.net> - 2026-01-10 22:28 -0500
Re: Computation and Undecidability olcott <polcott333@gmail.com> - 2026-01-10 21:34 -0600
Re: Computation and Undecidability Richard Damon <news.x.richarddamon@xoxy.net> - 2026-01-11 06:31 -0500
Re: Computation and Undecidability olcott <polcott333@gmail.com> - 2026-01-11 08:03 -0600
Re: Computation and Undecidability Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2026-01-11 14:39 +0000
Re: Computation and Undecidability Richard Damon <news.x.richarddamon@xoxy.net> - 2026-01-11 12:52 -0500
Re: Computation and Undecidability olcott <polcott333@gmail.com> - 2026-01-11 12:12 -0600
Re: Computation and Undecidability Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk> - 2026-01-11 21:28 +0000
Re: Computation and Undecidability olcott <polcott333@gmail.com> - 2026-01-11 15:50 -0600
Haskell Curry Foundations of Mathematical Logic sense of true in the system olcott <polcott333@gmail.com> - 2026-01-09 09:47 -0600
Page 5 of 11 — ← Prev page 1 … 3 4 [5] 6 7 … 11 Next page →
| From | Mikko <mikko.levanto@iki.fi> |
|---|---|
| Date | 2026-01-23 11:31 +0200 |
| Message-ID | <10kvf5k$3p3q5$1@dont-email.me> |
| In reply to | #344445 |
On 22/01/2026 14:40, Tristan Wibberley wrote: > On 22/01/2026 08:30, Mikko wrote: > >> I don't any web site that I could trust to meet your >> requirement.However, as far as I know, all authors agree about its meaning >> for ordinary logic. > > Essentially boolean, with undefinedness when either argument is > undefined and no notion that it's true when exactly one argument "has no > content" and no notion that it has no content when both arguments have none? Boole used different symbols. the symbol ∨ is from Principia Mathematica by Russell and Whitehead. In any ordinary formal logic every one can from A always infer A ∨ B with any B. Some formulations of logic do not use ∨ as a primitive symbol. In these formulations it can be defined in terms of primitive symbols, e.g. as ¬A → B. -- Mikko
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2026-01-19 09:03 -0600 |
| Message-ID | <10klh4e$ecm9$1@dont-email.me> |
| In reply to | #344380 |
On 1/19/2026 2:19 AM, Mikko wrote: > On 18/01/2026 15:28, olcott wrote: >> On 1/18/2026 5:27 AM, Mikko wrote: >>> On 17/01/2026 16:47, olcott wrote: >>>> On 1/17/2026 3:53 AM, Mikko wrote: >>>>> On 16/01/2026 17:38, olcott wrote: >>>>>> On 1/16/2026 3:32 AM, Mikko wrote: >>>>>>> On 15/01/2026 22:30, olcott wrote: >>>>>>>> On 1/15/2026 3:34 AM, Mikko wrote: >>>>>>>>> On 14/01/2026 21:32, olcott wrote: >>>>>>>>>> On 1/14/2026 3:01 AM, Mikko wrote: >>>>>>>>>>> On 13/01/2026 16:31, olcott wrote: >>>>>>>>>>>> On 1/13/2026 3:13 AM, Mikko wrote: >>>>>>>>>>>>> On 12/01/2026 16:32, olcott wrote: >>>>>>>>>>>>>> On 1/12/2026 4:47 AM, Mikko wrote: >>>>>>>>>>>>>>> On 11/01/2026 16:24, Tristan Wibberley wrote: >>>>>>>>>>>>>>>> On 11/01/2026 10:13, Mikko wrote: >>>>>>>>>>>>>>>>> On 10/01/2026 17:47, olcott wrote: >>>>>>>>>>>>>>>>>> On 1/10/2026 2:23 AM, Mikko wrote: >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>> No, that does not follow. If a required result cannot >>>>>>>>>>>>>>>>>>> be derived by >>>>>>>>>>>>>>>>>>> appying a finite string transformation then the it it >>>>>>>>>>>>>>>>>>> is uncomputable. >>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>> Right. Outside the scope of computation. Requiring >>>>>>>>>>>>>>>>>> anything >>>>>>>>>>>>>>>>>> outside the scope of computation is an incorrect >>>>>>>>>>>>>>>>>> requirement. >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>> You can't determine whether the required result is >>>>>>>>>>>>>>>>> computable before >>>>>>>>>>>>>>>>> you have the requirement. >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> Right, it is /in/ scope for computer science... for >>>>>>>>>>>>>>>> the / ology/. Olcott >>>>>>>>>>>>>>>> here uses "computation" to refer to the practice. You >>>>>>>>>>>>>>>> give the >>>>>>>>>>>>>>>> requirement to the /ologist/ who correctly decides that >>>>>>>>>>>>>>>> it is not for >>>>>>>>>>>>>>>> computation because it is not computable. >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> You two so often violently agree; I find it warming to >>>>>>>>>>>>>>>> the heart. >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> For pracitcal programming it is useful to know what is >>>>>>>>>>>>>>> known to be >>>>>>>>>>>>>>> uncomputable in order to avoid wasting time in attemlpts >>>>>>>>>>>>>>> to do the >>>>>>>>>>>>>>> impossible. >>>>>>>>>>>>>> >>>>>>>>>>>>>> It f-cking nuts that after more than 2000 years >>>>>>>>>>>>>> people still don't understand that self-contradictory >>>>>>>>>>>>>> expressions: "This sentence is not true" have no >>>>>>>>>>>>>> truth value. A smart high school student should have >>>>>>>>>>>>>> figured this out 2000 years ago. >>>>>>>>>>>>> >>>>>>>>>>>>> Irrelevant. For practical programming that question needn't >>>>>>>>>>>>> be answered. >>>>>>>>>>>> >>>>>>>>>>>> The halting problem counter-example input is anchored >>>>>>>>>>>> in the Liar Paradox. Proof Theoretic Semantics rejects >>>>>>>>>>>> those two and Gödel's incompleteness and a bunch more >>>>>>>>>>>> as merely non-well-founded inputs. >>>>>>>>>>> >>>>>>>>>>> For every Turing machine the halting problem counter-example >>>>>>>>>>> provably >>>>>>>>>>> exists. >>>>>>>>>> >>>>>>>>>> Not when using Proof Theoretic Semantics grounded >>>>>>>>>> in the specification language. In this case the >>>>>>>>>> pathological input is simply rejected as ungrounded. >>>>>>>>> >>>>>>>>> Then your "Proof Theoretic Semantics" is not useful for >>>>>>>>> discussion of >>>>>>>>> Turing machines. For every Turing machine a counter example >>>>>>>>> exists. >>>>>>>>> And so exists a Turing machine that writes the counter example >>>>>>>>> when >>>>>>>>> given a Turing machine as input. >>>>>>>> >>>>>>>> It is "not useful" in the same way that ZFC was >>>>>>>> "not useful" for addressing Russell's Paradox. >>>>>>> >>>>>>> ZF or ZFC is to some extent useful for addressing Russell's paradox. >>>>>>> It is an example of a set theory where Russell's paradox is avoided. >>>>>>> If your "Proof Theretic Semantics" cannot handle the existence of >>>>>>> a counter example for every Turing decider then it is not usefule >>>>>>> for those who work on practical problems of program correctness. >>>>>> >>>>>> Proof theoretic semantics addresses Gödel Incompleteness >>>>>> for PA in a way similar to the way that ZFC addresses >>>>>> Russell's Paradox in set theory. >>>>> >>>>> Not really the same way. Your "Proof theoretic semantics" redefines >>>>> truth and replaces the logic. ZFC is another theory using ordinary >>>>> logic. The problem with the naive set theory is that it is not >>>>> sound for any semantics. >>>> >>>> ZFC redefines set theory such that Russell's Paradox cannot arise. >>> >>> No, it does not. It is just another exammle of the generic concept >>> of set theory. Essentially the same as ZF but has one additional >>> postulate. >> >> ZFC redefines set theory such that Russell's Paradox cannot arise >> and the original set theory is now referred to as naive set theory. > > ZF and ZFC are not redefinitions. ZF is another theory. It can be > called a "set theory" because its structure is similar to Cnator's > original informal set theory. Cantor did not specify whther a set > must be well-founded but ZF specifies that it must. A set theory > were all sets are well-founded does not have Russell's paradox. > ZF is a redefinition in the only sense that matters: it changes the foundational rules so that Russell’s paradox cannot arise. Naive set theory allowed unrestricted comprehension; ZF restricts it and adds Foundation. That’s exactly the same structural move I’m making. Classical semantics treats every formula as a truth‑bearer and gets Gödel’s paradox. Proof‑theoretic semantics restricts truth‑bearers to what PA can classify and the paradox disappears. Calling ZF “another theory” instead of a “redefinition” doesn’t change the fact that it avoids the paradox by changing the foundations. >>>> Proof theoretic semantics redefines formal systems such that >>>> Incompleteness cannot arise. Gödel did not do this himself because >>>> Proof theoretic semantics did not exist at the time. >>> >>> Gödel did not do that because his topic was Peano arithmetic and its >>> extensions, and more generally ordinary logic. >>> >>> Can you can you prove anyting analogous to Gödel's completeness >>> theorem for your "Proof theoretic semantics"? > > Note that the question is not answered (or otherwise addressed) below. > No, there is no model‑theoretic completeness theorem here, because there is no model‑theoretic semantics. The proof‑theoretic analogue is built into the framework: all valid inferences are derivable by definition. >> Gödel’s incompleteness arises only because >> “true in PA” was never an internal notion >> of PA at all, but a meta‑mathematical notion >> of truth about PA defined externally through >> models; > > You have proven neither "only" nor "because". > Gödel’s “true but unprovable” reading of incompleteness depends on a meta‑mathematical notion of truth about PA, defined externally via models. If we instead define truth in PA proof‑theoretically—as provability—then that specific incompleteness phenomenon does not arise. >> Once truth is defined internally—by extending >> PA with a truth predicate so that “true in PA” >> simply means “derivable from PA’s axioms”— >> the supposed gap between truth and provability >> disappears > > But the syntactic incompleteness is still there. Both G and ¬G are > well-formed formulas of Peano arithmetic but neither is provable. > The well-formed formula G ∨ ¬G is provable, and so is G → G. Yes, syntactic incompleteness remains: there are well‑formed formulas PA neither proves nor refutes. But Gödel’s semantic incompleteness—the claim that there are true but unprovable sentences—depends on an external notion of truth that PA does not contain. Once truth in PA is defined internally as provability, G and ¬G are simply not truth‑bearers. The syntactic fact that they are unprovable does not create a semantic gap, because “true in PA” no longer means “true in an external model.” >> With that disappearance PA no longer counts as >> incomplete, because the statements Gödel identified >> as “true but unprovable” were never internal truths >> of PA in the first place, only truths assigned from >> the outside by the meta‑system. > > It still is syntactically incomplete. > Yes, PA is syntactically incomplete — that’s just the fact that some formulas are undecided. But Gödel’s semantic incompleteness, the claim of “true but unprovable,” depends on an external notion of truth that PA does not contain. Once truth in PA is defined internally as provability, the semantic gap disappears. What remains is only syntactic incompleteness, which is not the Gödel phenomenon I’m rejecting. Thus semantically, G simply becomes not a truth‑bearer in PA. -- Copyright 2026 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 | 2026-01-20 11:58 +0200 |
| Message-ID | <10knjks$1426t$1@dont-email.me> |
| In reply to | #344387 |
On 19/01/2026 17:03, olcott wrote: > On 1/19/2026 2:19 AM, Mikko wrote: >> On 18/01/2026 15:28, olcott wrote: >>> On 1/18/2026 5:27 AM, Mikko wrote: >>>> On 17/01/2026 16:47, olcott wrote: >>>>> On 1/17/2026 3:53 AM, Mikko wrote: >>>>>> On 16/01/2026 17:38, olcott wrote: >>>>>>> On 1/16/2026 3:32 AM, Mikko wrote: >>>>>>>> On 15/01/2026 22:30, olcott wrote: >>>>>>>>> On 1/15/2026 3:34 AM, Mikko wrote: >>>>>>>>>> On 14/01/2026 21:32, olcott wrote: >>>>>>>>>>> On 1/14/2026 3:01 AM, Mikko wrote: >>>>>>>>>>>> On 13/01/2026 16:31, olcott wrote: >>>>>>>>>>>>> On 1/13/2026 3:13 AM, Mikko wrote: >>>>>>>>>>>>>> On 12/01/2026 16:32, olcott wrote: >>>>>>>>>>>>>>> On 1/12/2026 4:47 AM, Mikko wrote: >>>>>>>>>>>>>>>> On 11/01/2026 16:24, Tristan Wibberley wrote: >>>>>>>>>>>>>>>>> On 11/01/2026 10:13, Mikko wrote: >>>>>>>>>>>>>>>>>> On 10/01/2026 17:47, olcott wrote: >>>>>>>>>>>>>>>>>>> On 1/10/2026 2:23 AM, Mikko wrote: >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>> No, that does not follow. If a required result >>>>>>>>>>>>>>>>>>>> cannot be derived by >>>>>>>>>>>>>>>>>>>> appying a finite string transformation then the it >>>>>>>>>>>>>>>>>>>> it is uncomputable. >>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>> Right. Outside the scope of computation. Requiring >>>>>>>>>>>>>>>>>>> anything >>>>>>>>>>>>>>>>>>> outside the scope of computation is an incorrect >>>>>>>>>>>>>>>>>>> requirement. >>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>> You can't determine whether the required result is >>>>>>>>>>>>>>>>>> computable before >>>>>>>>>>>>>>>>>> you have the requirement. >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>> Right, it is /in/ scope for computer science... for >>>>>>>>>>>>>>>>> the / ology/. Olcott >>>>>>>>>>>>>>>>> here uses "computation" to refer to the practice. You >>>>>>>>>>>>>>>>> give the >>>>>>>>>>>>>>>>> requirement to the /ologist/ who correctly decides that >>>>>>>>>>>>>>>>> it is not for >>>>>>>>>>>>>>>>> computation because it is not computable. >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>> You two so often violently agree; I find it warming to >>>>>>>>>>>>>>>>> the heart. >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> For pracitcal programming it is useful to know what is >>>>>>>>>>>>>>>> known to be >>>>>>>>>>>>>>>> uncomputable in order to avoid wasting time in attemlpts >>>>>>>>>>>>>>>> to do the >>>>>>>>>>>>>>>> impossible. >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> It f-cking nuts that after more than 2000 years >>>>>>>>>>>>>>> people still don't understand that self-contradictory >>>>>>>>>>>>>>> expressions: "This sentence is not true" have no >>>>>>>>>>>>>>> truth value. A smart high school student should have >>>>>>>>>>>>>>> figured this out 2000 years ago. >>>>>>>>>>>>>> >>>>>>>>>>>>>> Irrelevant. For practical programming that question >>>>>>>>>>>>>> needn't be answered. >>>>>>>>>>>>> >>>>>>>>>>>>> The halting problem counter-example input is anchored >>>>>>>>>>>>> in the Liar Paradox. Proof Theoretic Semantics rejects >>>>>>>>>>>>> those two and Gödel's incompleteness and a bunch more >>>>>>>>>>>>> as merely non-well-founded inputs. >>>>>>>>>>>> >>>>>>>>>>>> For every Turing machine the halting problem counter-example >>>>>>>>>>>> provably >>>>>>>>>>>> exists. >>>>>>>>>>> >>>>>>>>>>> Not when using Proof Theoretic Semantics grounded >>>>>>>>>>> in the specification language. In this case the >>>>>>>>>>> pathological input is simply rejected as ungrounded. >>>>>>>>>> >>>>>>>>>> Then your "Proof Theoretic Semantics" is not useful for >>>>>>>>>> discussion of >>>>>>>>>> Turing machines. For every Turing machine a counter example >>>>>>>>>> exists. >>>>>>>>>> And so exists a Turing machine that writes the counter example >>>>>>>>>> when >>>>>>>>>> given a Turing machine as input. >>>>>>>>> >>>>>>>>> It is "not useful" in the same way that ZFC was >>>>>>>>> "not useful" for addressing Russell's Paradox. >>>>>>>> >>>>>>>> ZF or ZFC is to some extent useful for addressing Russell's >>>>>>>> paradox. >>>>>>>> It is an example of a set theory where Russell's paradox is >>>>>>>> avoided. >>>>>>>> If your "Proof Theretic Semantics" cannot handle the existence of >>>>>>>> a counter example for every Turing decider then it is not usefule >>>>>>>> for those who work on practical problems of program correctness. >>>>>>> >>>>>>> Proof theoretic semantics addresses Gödel Incompleteness >>>>>>> for PA in a way similar to the way that ZFC addresses >>>>>>> Russell's Paradox in set theory. >>>>>> >>>>>> Not really the same way. Your "Proof theoretic semantics" redefines >>>>>> truth and replaces the logic. ZFC is another theory using ordinary >>>>>> logic. The problem with the naive set theory is that it is not >>>>>> sound for any semantics. >>>>> >>>>> ZFC redefines set theory such that Russell's Paradox cannot arise. >>>> >>>> No, it does not. It is just another exammle of the generic concept >>>> of set theory. Essentially the same as ZF but has one additional >>>> postulate. >>> >>> ZFC redefines set theory such that Russell's Paradox cannot arise >>> and the original set theory is now referred to as naive set theory. >> >> ZF and ZFC are not redefinitions. ZF is another theory. It can be >> called a "set theory" because its structure is similar to Cnator's >> original informal set theory. Cantor did not specify whther a set >> must be well-founded but ZF specifies that it must. A set theory >> were all sets are well-founded does not have Russell's paradox. > > ZF is a redefinition in the only sense that matters: > it changes the foundational rules so that Russell’s > paradox cannot arise. The only sense that matters is: to give a new meaning to an exsisting term. That is OK when the new meaning is only used in a context where the old one does not make sense. What you are trying is to give a new meaning to "true" but preted that it still means 'true'. -- Mikko
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2026-01-20 12:35 -0600 |
| Message-ID | <10kohu3$1f51g$1@dont-email.me> |
| In reply to | #344405 |
On 1/20/2026 3:58 AM, Mikko wrote: > On 19/01/2026 17:03, olcott wrote: >> On 1/19/2026 2:19 AM, Mikko wrote: >>> On 18/01/2026 15:28, olcott wrote: >>>> On 1/18/2026 5:27 AM, Mikko wrote: >>>>> On 17/01/2026 16:47, olcott wrote: >>>>>> On 1/17/2026 3:53 AM, Mikko wrote: >>>>>>> On 16/01/2026 17:38, olcott wrote: >>>>>>>> On 1/16/2026 3:32 AM, Mikko wrote: >>>>>>>>> On 15/01/2026 22:30, olcott wrote: >>>>>>>>>> On 1/15/2026 3:34 AM, Mikko wrote: >>>>>>>>>>> On 14/01/2026 21:32, olcott wrote: >>>>>>>>>>>> On 1/14/2026 3:01 AM, Mikko wrote: >>>>>>>>>>>>> On 13/01/2026 16:31, olcott wrote: >>>>>>>>>>>>>> On 1/13/2026 3:13 AM, Mikko wrote: >>>>>>>>>>>>>>> On 12/01/2026 16:32, olcott wrote: >>>>>>>>>>>>>>>> On 1/12/2026 4:47 AM, Mikko wrote: >>>>>>>>>>>>>>>>> On 11/01/2026 16:24, Tristan Wibberley wrote: >>>>>>>>>>>>>>>>>> On 11/01/2026 10:13, Mikko wrote: >>>>>>>>>>>>>>>>>>> On 10/01/2026 17:47, olcott wrote: >>>>>>>>>>>>>>>>>>>> On 1/10/2026 2:23 AM, Mikko wrote: >>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>> No, that does not follow. If a required result >>>>>>>>>>>>>>>>>>>>> cannot be derived by >>>>>>>>>>>>>>>>>>>>> appying a finite string transformation then the it >>>>>>>>>>>>>>>>>>>>> it is uncomputable. >>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>> Right. Outside the scope of computation. Requiring >>>>>>>>>>>>>>>>>>>> anything >>>>>>>>>>>>>>>>>>>> outside the scope of computation is an incorrect >>>>>>>>>>>>>>>>>>>> requirement. >>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>> You can't determine whether the required result is >>>>>>>>>>>>>>>>>>> computable before >>>>>>>>>>>>>>>>>>> you have the requirement. >>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>> Right, it is /in/ scope for computer science... for >>>>>>>>>>>>>>>>>> the / ology/. Olcott >>>>>>>>>>>>>>>>>> here uses "computation" to refer to the practice. You >>>>>>>>>>>>>>>>>> give the >>>>>>>>>>>>>>>>>> requirement to the /ologist/ who correctly decides >>>>>>>>>>>>>>>>>> that it is not for >>>>>>>>>>>>>>>>>> computation because it is not computable. >>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>> You two so often violently agree; I find it warming to >>>>>>>>>>>>>>>>>> the heart. >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>> For pracitcal programming it is useful to know what is >>>>>>>>>>>>>>>>> known to be >>>>>>>>>>>>>>>>> uncomputable in order to avoid wasting time in >>>>>>>>>>>>>>>>> attemlpts to do the >>>>>>>>>>>>>>>>> impossible. >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> It f-cking nuts that after more than 2000 years >>>>>>>>>>>>>>>> people still don't understand that self-contradictory >>>>>>>>>>>>>>>> expressions: "This sentence is not true" have no >>>>>>>>>>>>>>>> truth value. A smart high school student should have >>>>>>>>>>>>>>>> figured this out 2000 years ago. >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> Irrelevant. For practical programming that question >>>>>>>>>>>>>>> needn't be answered. >>>>>>>>>>>>>> >>>>>>>>>>>>>> The halting problem counter-example input is anchored >>>>>>>>>>>>>> in the Liar Paradox. Proof Theoretic Semantics rejects >>>>>>>>>>>>>> those two and Gödel's incompleteness and a bunch more >>>>>>>>>>>>>> as merely non-well-founded inputs. >>>>>>>>>>>>> >>>>>>>>>>>>> For every Turing machine the halting problem counter- >>>>>>>>>>>>> example provably >>>>>>>>>>>>> exists. >>>>>>>>>>>> >>>>>>>>>>>> Not when using Proof Theoretic Semantics grounded >>>>>>>>>>>> in the specification language. In this case the >>>>>>>>>>>> pathological input is simply rejected as ungrounded. >>>>>>>>>>> >>>>>>>>>>> Then your "Proof Theoretic Semantics" is not useful for >>>>>>>>>>> discussion of >>>>>>>>>>> Turing machines. For every Turing machine a counter example >>>>>>>>>>> exists. >>>>>>>>>>> And so exists a Turing machine that writes the counter >>>>>>>>>>> example when >>>>>>>>>>> given a Turing machine as input. >>>>>>>>>> >>>>>>>>>> It is "not useful" in the same way that ZFC was >>>>>>>>>> "not useful" for addressing Russell's Paradox. >>>>>>>>> >>>>>>>>> ZF or ZFC is to some extent useful for addressing Russell's >>>>>>>>> paradox. >>>>>>>>> It is an example of a set theory where Russell's paradox is >>>>>>>>> avoided. >>>>>>>>> If your "Proof Theretic Semantics" cannot handle the existence of >>>>>>>>> a counter example for every Turing decider then it is not usefule >>>>>>>>> for those who work on practical problems of program correctness. >>>>>>>> >>>>>>>> Proof theoretic semantics addresses Gödel Incompleteness >>>>>>>> for PA in a way similar to the way that ZFC addresses >>>>>>>> Russell's Paradox in set theory. >>>>>>> >>>>>>> Not really the same way. Your "Proof theoretic semantics" redefines >>>>>>> truth and replaces the logic. ZFC is another theory using ordinary >>>>>>> logic. The problem with the naive set theory is that it is not >>>>>>> sound for any semantics. >>>>>> >>>>>> ZFC redefines set theory such that Russell's Paradox cannot arise. >>>>> >>>>> No, it does not. It is just another exammle of the generic concept >>>>> of set theory. Essentially the same as ZF but has one additional >>>>> postulate. >>>> >>>> ZFC redefines set theory such that Russell's Paradox cannot arise >>>> and the original set theory is now referred to as naive set theory. >>> >>> ZF and ZFC are not redefinitions. ZF is another theory. It can be >>> called a "set theory" because its structure is similar to Cnator's >>> original informal set theory. Cantor did not specify whther a set >>> must be well-founded but ZF specifies that it must. A set theory >>> were all sets are well-founded does not have Russell's paradox. >> >> ZF is a redefinition in the only sense that matters: >> it changes the foundational rules so that Russell’s >> paradox cannot arise. > > The only sense that matters is: to give a new meaning to an exsisting > term. That is OK when the new meaning is only used in a context where > the old one does not make sense. > > What you are trying is to give a new meaning to "true" but preted that > it still means 'true'. > True in the standard model of arithmetic using meta-math has always been misconstrued as true <in> arithmetic only because back then proof theoretic semantics did not exist. No one ever understood how a truth predicate could be directly added to PA. Now with Proof theoretic semantics and the Haskell Curry notion of true in the system it is easy to directly define a truth predicate <is> PA. Truth in the standard model is meta‑mathematical. Truth in PA is proof‑theoretic. These were historically conflated only because proof‑theoretic semantics did not exist. With Curry’s notion of internal truth, PA’s truth predicate is simply: ∀x ∈ PA ((True(PA, x) ≡ (PA ⊢ x)) ∀x ∈ PA ((False(PA, x) ≡ (PA ⊢ ~x)) -- Copyright 2026 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 | 2026-01-21 11:03 +0200 |
| Message-ID | <10kq4p9$1vmg3$1@dont-email.me> |
| In reply to | #344408 |
On 20/01/2026 20:35, olcott wrote: > On 1/20/2026 3:58 AM, Mikko wrote: >> On 19/01/2026 17:03, olcott wrote: >>> On 1/19/2026 2:19 AM, Mikko wrote: >>>> On 18/01/2026 15:28, olcott wrote: >>>>> On 1/18/2026 5:27 AM, Mikko wrote: >>>>>> On 17/01/2026 16:47, olcott wrote: >>>>>>> On 1/17/2026 3:53 AM, Mikko wrote: >>>>>>>> On 16/01/2026 17:38, olcott wrote: >>>>>>>>> On 1/16/2026 3:32 AM, Mikko wrote: >>>>>>>>>> On 15/01/2026 22:30, olcott wrote: >>>>>>>>>>> On 1/15/2026 3:34 AM, Mikko wrote: >>>>>>>>>>>> On 14/01/2026 21:32, olcott wrote: >>>>>>>>>>>>> On 1/14/2026 3:01 AM, Mikko wrote: >>>>>>>>>>>>>> On 13/01/2026 16:31, olcott wrote: >>>>>>>>>>>>>>> On 1/13/2026 3:13 AM, Mikko wrote: >>>>>>>>>>>>>>>> On 12/01/2026 16:32, olcott wrote: >>>>>>>>>>>>>>>>> On 1/12/2026 4:47 AM, Mikko wrote: >>>>>>>>>>>>>>>>>> On 11/01/2026 16:24, Tristan Wibberley wrote: >>>>>>>>>>>>>>>>>>> On 11/01/2026 10:13, Mikko wrote: >>>>>>>>>>>>>>>>>>>> On 10/01/2026 17:47, olcott wrote: >>>>>>>>>>>>>>>>>>>>> On 1/10/2026 2:23 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>> No, that does not follow. If a required result >>>>>>>>>>>>>>>>>>>>>> cannot be derived by >>>>>>>>>>>>>>>>>>>>>> appying a finite string transformation then the it >>>>>>>>>>>>>>>>>>>>>> it is uncomputable. >>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>> Right. Outside the scope of computation. Requiring >>>>>>>>>>>>>>>>>>>>> anything >>>>>>>>>>>>>>>>>>>>> outside the scope of computation is an incorrect >>>>>>>>>>>>>>>>>>>>> requirement. >>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>> You can't determine whether the required result is >>>>>>>>>>>>>>>>>>>> computable before >>>>>>>>>>>>>>>>>>>> you have the requirement. >>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>> Right, it is /in/ scope for computer science... for >>>>>>>>>>>>>>>>>>> the / ology/. Olcott >>>>>>>>>>>>>>>>>>> here uses "computation" to refer to the practice. You >>>>>>>>>>>>>>>>>>> give the >>>>>>>>>>>>>>>>>>> requirement to the /ologist/ who correctly decides >>>>>>>>>>>>>>>>>>> that it is not for >>>>>>>>>>>>>>>>>>> computation because it is not computable. >>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>> You two so often violently agree; I find it warming >>>>>>>>>>>>>>>>>>> to the heart. >>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>> For pracitcal programming it is useful to know what is >>>>>>>>>>>>>>>>>> known to be >>>>>>>>>>>>>>>>>> uncomputable in order to avoid wasting time in >>>>>>>>>>>>>>>>>> attemlpts to do the >>>>>>>>>>>>>>>>>> impossible. >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>> It f-cking nuts that after more than 2000 years >>>>>>>>>>>>>>>>> people still don't understand that self-contradictory >>>>>>>>>>>>>>>>> expressions: "This sentence is not true" have no >>>>>>>>>>>>>>>>> truth value. A smart high school student should have >>>>>>>>>>>>>>>>> figured this out 2000 years ago. >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> Irrelevant. For practical programming that question >>>>>>>>>>>>>>>> needn't be answered. >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> The halting problem counter-example input is anchored >>>>>>>>>>>>>>> in the Liar Paradox. Proof Theoretic Semantics rejects >>>>>>>>>>>>>>> those two and Gödel's incompleteness and a bunch more >>>>>>>>>>>>>>> as merely non-well-founded inputs. >>>>>>>>>>>>>> >>>>>>>>>>>>>> For every Turing machine the halting problem counter- >>>>>>>>>>>>>> example provably >>>>>>>>>>>>>> exists. >>>>>>>>>>>>> >>>>>>>>>>>>> Not when using Proof Theoretic Semantics grounded >>>>>>>>>>>>> in the specification language. In this case the >>>>>>>>>>>>> pathological input is simply rejected as ungrounded. >>>>>>>>>>>> >>>>>>>>>>>> Then your "Proof Theoretic Semantics" is not useful for >>>>>>>>>>>> discussion of >>>>>>>>>>>> Turing machines. For every Turing machine a counter example >>>>>>>>>>>> exists. >>>>>>>>>>>> And so exists a Turing machine that writes the counter >>>>>>>>>>>> example when >>>>>>>>>>>> given a Turing machine as input. >>>>>>>>>>> >>>>>>>>>>> It is "not useful" in the same way that ZFC was >>>>>>>>>>> "not useful" for addressing Russell's Paradox. >>>>>>>>>> >>>>>>>>>> ZF or ZFC is to some extent useful for addressing Russell's >>>>>>>>>> paradox. >>>>>>>>>> It is an example of a set theory where Russell's paradox is >>>>>>>>>> avoided. >>>>>>>>>> If your "Proof Theretic Semantics" cannot handle the existence of >>>>>>>>>> a counter example for every Turing decider then it is not usefule >>>>>>>>>> for those who work on practical problems of program correctness. >>>>>>>>> >>>>>>>>> Proof theoretic semantics addresses Gödel Incompleteness >>>>>>>>> for PA in a way similar to the way that ZFC addresses >>>>>>>>> Russell's Paradox in set theory. >>>>>>>> >>>>>>>> Not really the same way. Your "Proof theoretic semantics" redefines >>>>>>>> truth and replaces the logic. ZFC is another theory using ordinary >>>>>>>> logic. The problem with the naive set theory is that it is not >>>>>>>> sound for any semantics. >>>>>>> >>>>>>> ZFC redefines set theory such that Russell's Paradox cannot arise. >>>>>> >>>>>> No, it does not. It is just another exammle of the generic concept >>>>>> of set theory. Essentially the same as ZF but has one additional >>>>>> postulate. >>>>> >>>>> ZFC redefines set theory such that Russell's Paradox cannot arise >>>>> and the original set theory is now referred to as naive set theory. >>>> >>>> ZF and ZFC are not redefinitions. ZF is another theory. It can be >>>> called a "set theory" because its structure is similar to Cnator's >>>> original informal set theory. Cantor did not specify whther a set >>>> must be well-founded but ZF specifies that it must. A set theory >>>> were all sets are well-founded does not have Russell's paradox. >>> >>> ZF is a redefinition in the only sense that matters: >>> it changes the foundational rules so that Russell’s >>> paradox cannot arise. >> >> The only sense that matters is: to give a new meaning to an exsisting >> term. That is OK when the new meaning is only used in a context where >> the old one does not make sense. >> >> What you are trying is to give a new meaning to "true" but preted that >> it still means 'true'. > > True in the standard model of arithmetic using meta-math > has always been misconstrued as true <in> arithmetic No, it hasn't. In the way theories are usually discussed nothing is "ture in arithmetic". Every sentence of a first order theory that can be proven in the theory is true in every model theory. Every sentence of a theory that cannot be proven in the theory is false in some model of the theory. > only because back then proof theoretic semantics did > not exist. Every interpretation of the theory is a definition of semantics. -- Mikko
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2026-01-21 09:22 -0600 |
| Message-ID | <10kqr0g$27agi$1@dont-email.me> |
| In reply to | #344423 |
On 1/21/2026 3:03 AM, Mikko wrote: > On 20/01/2026 20:35, olcott wrote: >> On 1/20/2026 3:58 AM, Mikko wrote: >>> On 19/01/2026 17:03, olcott wrote: >>>> On 1/19/2026 2:19 AM, Mikko wrote: >>>>> On 18/01/2026 15:28, olcott wrote: >>>>>> On 1/18/2026 5:27 AM, Mikko wrote: >>>>>>> On 17/01/2026 16:47, olcott wrote: >>>>>>>> On 1/17/2026 3:53 AM, Mikko wrote: >>>>>>>>> On 16/01/2026 17:38, olcott wrote: >>>>>>>>>> On 1/16/2026 3:32 AM, Mikko wrote: >>>>>>>>>>> On 15/01/2026 22:30, olcott wrote: >>>>>>>>>>>> On 1/15/2026 3:34 AM, Mikko wrote: >>>>>>>>>>>>> On 14/01/2026 21:32, olcott wrote: >>>>>>>>>>>>>> On 1/14/2026 3:01 AM, Mikko wrote: >>>>>>>>>>>>>>> On 13/01/2026 16:31, olcott wrote: >>>>>>>>>>>>>>>> On 1/13/2026 3:13 AM, Mikko wrote: >>>>>>>>>>>>>>>>> On 12/01/2026 16:32, olcott wrote: >>>>>>>>>>>>>>>>>> On 1/12/2026 4:47 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>> On 11/01/2026 16:24, Tristan Wibberley wrote: >>>>>>>>>>>>>>>>>>>> On 11/01/2026 10:13, Mikko wrote: >>>>>>>>>>>>>>>>>>>>> On 10/01/2026 17:47, olcott wrote: >>>>>>>>>>>>>>>>>>>>>> On 1/10/2026 2:23 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>> No, that does not follow. If a required result >>>>>>>>>>>>>>>>>>>>>>> cannot be derived by >>>>>>>>>>>>>>>>>>>>>>> appying a finite string transformation then the >>>>>>>>>>>>>>>>>>>>>>> it it is uncomputable. >>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>> Right. Outside the scope of computation. Requiring >>>>>>>>>>>>>>>>>>>>>> anything >>>>>>>>>>>>>>>>>>>>>> outside the scope of computation is an incorrect >>>>>>>>>>>>>>>>>>>>>> requirement. >>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>> You can't determine whether the required result is >>>>>>>>>>>>>>>>>>>>> computable before >>>>>>>>>>>>>>>>>>>>> you have the requirement. >>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>> Right, it is /in/ scope for computer science... for >>>>>>>>>>>>>>>>>>>> the / ology/. Olcott >>>>>>>>>>>>>>>>>>>> here uses "computation" to refer to the practice. >>>>>>>>>>>>>>>>>>>> You give the >>>>>>>>>>>>>>>>>>>> requirement to the /ologist/ who correctly decides >>>>>>>>>>>>>>>>>>>> that it is not for >>>>>>>>>>>>>>>>>>>> computation because it is not computable. >>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>> You two so often violently agree; I find it warming >>>>>>>>>>>>>>>>>>>> to the heart. >>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>> For pracitcal programming it is useful to know what >>>>>>>>>>>>>>>>>>> is known to be >>>>>>>>>>>>>>>>>>> uncomputable in order to avoid wasting time in >>>>>>>>>>>>>>>>>>> attemlpts to do the >>>>>>>>>>>>>>>>>>> impossible. >>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>> It f-cking nuts that after more than 2000 years >>>>>>>>>>>>>>>>>> people still don't understand that self-contradictory >>>>>>>>>>>>>>>>>> expressions: "This sentence is not true" have no >>>>>>>>>>>>>>>>>> truth value. A smart high school student should have >>>>>>>>>>>>>>>>>> figured this out 2000 years ago. >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>> Irrelevant. For practical programming that question >>>>>>>>>>>>>>>>> needn't be answered. >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> The halting problem counter-example input is anchored >>>>>>>>>>>>>>>> in the Liar Paradox. Proof Theoretic Semantics rejects >>>>>>>>>>>>>>>> those two and Gödel's incompleteness and a bunch more >>>>>>>>>>>>>>>> as merely non-well-founded inputs. >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> For every Turing machine the halting problem counter- >>>>>>>>>>>>>>> example provably >>>>>>>>>>>>>>> exists. >>>>>>>>>>>>>> >>>>>>>>>>>>>> Not when using Proof Theoretic Semantics grounded >>>>>>>>>>>>>> in the specification language. In this case the >>>>>>>>>>>>>> pathological input is simply rejected as ungrounded. >>>>>>>>>>>>> >>>>>>>>>>>>> Then your "Proof Theoretic Semantics" is not useful for >>>>>>>>>>>>> discussion of >>>>>>>>>>>>> Turing machines. For every Turing machine a counter example >>>>>>>>>>>>> exists. >>>>>>>>>>>>> And so exists a Turing machine that writes the counter >>>>>>>>>>>>> example when >>>>>>>>>>>>> given a Turing machine as input. >>>>>>>>>>>> >>>>>>>>>>>> It is "not useful" in the same way that ZFC was >>>>>>>>>>>> "not useful" for addressing Russell's Paradox. >>>>>>>>>>> >>>>>>>>>>> ZF or ZFC is to some extent useful for addressing Russell's >>>>>>>>>>> paradox. >>>>>>>>>>> It is an example of a set theory where Russell's paradox is >>>>>>>>>>> avoided. >>>>>>>>>>> If your "Proof Theretic Semantics" cannot handle the >>>>>>>>>>> existence of >>>>>>>>>>> a counter example for every Turing decider then it is not >>>>>>>>>>> usefule >>>>>>>>>>> for those who work on practical problems of program correctness. >>>>>>>>>> >>>>>>>>>> Proof theoretic semantics addresses Gödel Incompleteness >>>>>>>>>> for PA in a way similar to the way that ZFC addresses >>>>>>>>>> Russell's Paradox in set theory. >>>>>>>>> >>>>>>>>> Not really the same way. Your "Proof theoretic semantics" >>>>>>>>> redefines >>>>>>>>> truth and replaces the logic. ZFC is another theory using ordinary >>>>>>>>> logic. The problem with the naive set theory is that it is not >>>>>>>>> sound for any semantics. >>>>>>>> >>>>>>>> ZFC redefines set theory such that Russell's Paradox cannot arise. >>>>>>> >>>>>>> No, it does not. It is just another exammle of the generic concept >>>>>>> of set theory. Essentially the same as ZF but has one additional >>>>>>> postulate. >>>>>> >>>>>> ZFC redefines set theory such that Russell's Paradox cannot arise >>>>>> and the original set theory is now referred to as naive set theory. >>>>> >>>>> ZF and ZFC are not redefinitions. ZF is another theory. It can be >>>>> called a "set theory" because its structure is similar to Cnator's >>>>> original informal set theory. Cantor did not specify whther a set >>>>> must be well-founded but ZF specifies that it must. A set theory >>>>> were all sets are well-founded does not have Russell's paradox. >>>> >>>> ZF is a redefinition in the only sense that matters: >>>> it changes the foundational rules so that Russell’s >>>> paradox cannot arise. >>> >>> The only sense that matters is: to give a new meaning to an exsisting >>> term. That is OK when the new meaning is only used in a context where >>> the old one does not make sense. >>> >>> What you are trying is to give a new meaning to "true" but preted that >>> it still means 'true'. >> >> True in the standard model of arithmetic using meta-math >> has always been misconstrued as true <in> arithmetic > > No, it hasn't. In the way theories are usually discussed nothing is > "ture in arithmetic". Every sentence of a first order theory that > can be proven in the theory is true in every model theory. Every > sentence of a theory that cannot be proven in the theory is false > in some model of the theory. > >> only because back then proof theoretic semantics did >> not exist. > > Every interpretation of the theory is a definition of semantics. > Meta‑math relations about numbers don’t exist in PA because PA only contains arithmetical relations—addition, multiplication, ordering, primitive‑recursive predicates about numbers themselves—while relations that talk about PA’s own proofs, syntax, or truth conditions live entirely in the meta‑theory; so when someone appeals to a Gödel‑style relation like “n encodes a proof of this very sentence,” they’re invoking a meta‑mathematical predicate that PA cannot internalize, which is exactly why your framework draws a clean boundary between internal proof‑theoretic truth and external model‑theoretic truth. -- Copyright 2026 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 | 2026-01-22 10:21 +0200 |
| Message-ID | <10ksmlt$2rf95$1@dont-email.me> |
| In reply to | #344428 |
On 21/01/2026 17:22, olcott wrote: > On 1/21/2026 3:03 AM, Mikko wrote: >> On 20/01/2026 20:35, olcott wrote: >>> On 1/20/2026 3:58 AM, Mikko wrote: >>>> On 19/01/2026 17:03, olcott wrote: >>>>> On 1/19/2026 2:19 AM, Mikko wrote: >>>>>> On 18/01/2026 15:28, olcott wrote: >>>>>>> On 1/18/2026 5:27 AM, Mikko wrote: >>>>>>>> On 17/01/2026 16:47, olcott wrote: >>>>>>>>> On 1/17/2026 3:53 AM, Mikko wrote: >>>>>>>>>> On 16/01/2026 17:38, olcott wrote: >>>>>>>>>>> On 1/16/2026 3:32 AM, Mikko wrote: >>>>>>>>>>>> On 15/01/2026 22:30, olcott wrote: >>>>>>>>>>>>> On 1/15/2026 3:34 AM, Mikko wrote: >>>>>>>>>>>>>> On 14/01/2026 21:32, olcott wrote: >>>>>>>>>>>>>>> On 1/14/2026 3:01 AM, Mikko wrote: >>>>>>>>>>>>>>>> On 13/01/2026 16:31, olcott wrote: >>>>>>>>>>>>>>>>> On 1/13/2026 3:13 AM, Mikko wrote: >>>>>>>>>>>>>>>>>> On 12/01/2026 16:32, olcott wrote: >>>>>>>>>>>>>>>>>>> On 1/12/2026 4:47 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>> On 11/01/2026 16:24, Tristan Wibberley wrote: >>>>>>>>>>>>>>>>>>>>> On 11/01/2026 10:13, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>> On 10/01/2026 17:47, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>> On 1/10/2026 2:23 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>> No, that does not follow. If a required result >>>>>>>>>>>>>>>>>>>>>>>> cannot be derived by >>>>>>>>>>>>>>>>>>>>>>>> appying a finite string transformation then the >>>>>>>>>>>>>>>>>>>>>>>> it it is uncomputable. >>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>> Right. Outside the scope of computation. >>>>>>>>>>>>>>>>>>>>>>> Requiring anything >>>>>>>>>>>>>>>>>>>>>>> outside the scope of computation is an incorrect >>>>>>>>>>>>>>>>>>>>>>> requirement. >>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>> You can't determine whether the required result is >>>>>>>>>>>>>>>>>>>>>> computable before >>>>>>>>>>>>>>>>>>>>>> you have the requirement. >>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>> Right, it is /in/ scope for computer science... for >>>>>>>>>>>>>>>>>>>>> the / ology/. Olcott >>>>>>>>>>>>>>>>>>>>> here uses "computation" to refer to the practice. >>>>>>>>>>>>>>>>>>>>> You give the >>>>>>>>>>>>>>>>>>>>> requirement to the /ologist/ who correctly decides >>>>>>>>>>>>>>>>>>>>> that it is not for >>>>>>>>>>>>>>>>>>>>> computation because it is not computable. >>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>> You two so often violently agree; I find it warming >>>>>>>>>>>>>>>>>>>>> to the heart. >>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>> For pracitcal programming it is useful to know what >>>>>>>>>>>>>>>>>>>> is known to be >>>>>>>>>>>>>>>>>>>> uncomputable in order to avoid wasting time in >>>>>>>>>>>>>>>>>>>> attemlpts to do the >>>>>>>>>>>>>>>>>>>> impossible. >>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>> It f-cking nuts that after more than 2000 years >>>>>>>>>>>>>>>>>>> people still don't understand that self-contradictory >>>>>>>>>>>>>>>>>>> expressions: "This sentence is not true" have no >>>>>>>>>>>>>>>>>>> truth value. A smart high school student should have >>>>>>>>>>>>>>>>>>> figured this out 2000 years ago. >>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>> Irrelevant. For practical programming that question >>>>>>>>>>>>>>>>>> needn't be answered. >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>> The halting problem counter-example input is anchored >>>>>>>>>>>>>>>>> in the Liar Paradox. Proof Theoretic Semantics rejects >>>>>>>>>>>>>>>>> those two and Gödel's incompleteness and a bunch more >>>>>>>>>>>>>>>>> as merely non-well-founded inputs. >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> For every Turing machine the halting problem counter- >>>>>>>>>>>>>>>> example provably >>>>>>>>>>>>>>>> exists. >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> Not when using Proof Theoretic Semantics grounded >>>>>>>>>>>>>>> in the specification language. In this case the >>>>>>>>>>>>>>> pathological input is simply rejected as ungrounded. >>>>>>>>>>>>>> >>>>>>>>>>>>>> Then your "Proof Theoretic Semantics" is not useful for >>>>>>>>>>>>>> discussion of >>>>>>>>>>>>>> Turing machines. For every Turing machine a counter >>>>>>>>>>>>>> example exists. >>>>>>>>>>>>>> And so exists a Turing machine that writes the counter >>>>>>>>>>>>>> example when >>>>>>>>>>>>>> given a Turing machine as input. >>>>>>>>>>>>> >>>>>>>>>>>>> It is "not useful" in the same way that ZFC was >>>>>>>>>>>>> "not useful" for addressing Russell's Paradox. >>>>>>>>>>>> >>>>>>>>>>>> ZF or ZFC is to some extent useful for addressing Russell's >>>>>>>>>>>> paradox. >>>>>>>>>>>> It is an example of a set theory where Russell's paradox is >>>>>>>>>>>> avoided. >>>>>>>>>>>> If your "Proof Theretic Semantics" cannot handle the >>>>>>>>>>>> existence of >>>>>>>>>>>> a counter example for every Turing decider then it is not >>>>>>>>>>>> usefule >>>>>>>>>>>> for those who work on practical problems of program >>>>>>>>>>>> correctness. >>>>>>>>>>> >>>>>>>>>>> Proof theoretic semantics addresses Gödel Incompleteness >>>>>>>>>>> for PA in a way similar to the way that ZFC addresses >>>>>>>>>>> Russell's Paradox in set theory. >>>>>>>>>> >>>>>>>>>> Not really the same way. Your "Proof theoretic semantics" >>>>>>>>>> redefines >>>>>>>>>> truth and replaces the logic. ZFC is another theory using >>>>>>>>>> ordinary >>>>>>>>>> logic. The problem with the naive set theory is that it is not >>>>>>>>>> sound for any semantics. >>>>>>>>> >>>>>>>>> ZFC redefines set theory such that Russell's Paradox cannot arise. >>>>>>>> >>>>>>>> No, it does not. It is just another exammle of the generic concept >>>>>>>> of set theory. Essentially the same as ZF but has one additional >>>>>>>> postulate. >>>>>>> >>>>>>> ZFC redefines set theory such that Russell's Paradox cannot arise >>>>>>> and the original set theory is now referred to as naive set theory. >>>>>> >>>>>> ZF and ZFC are not redefinitions. ZF is another theory. It can be >>>>>> called a "set theory" because its structure is similar to Cnator's >>>>>> original informal set theory. Cantor did not specify whther a set >>>>>> must be well-founded but ZF specifies that it must. A set theory >>>>>> were all sets are well-founded does not have Russell's paradox. >>>>> >>>>> ZF is a redefinition in the only sense that matters: >>>>> it changes the foundational rules so that Russell’s >>>>> paradox cannot arise. >>>> >>>> The only sense that matters is: to give a new meaning to an exsisting >>>> term. That is OK when the new meaning is only used in a context where >>>> the old one does not make sense. >>>> >>>> What you are trying is to give a new meaning to "true" but preted that >>>> it still means 'true'. >>> >>> True in the standard model of arithmetic using meta-math >>> has always been misconstrued as true <in> arithmetic >> >> No, it hasn't. In the way theories are usually discussed nothing is >> "ture in arithmetic". Every sentence of a first order theory that >> can be proven in the theory is true in every model theory. Every >> sentence of a theory that cannot be proven in the theory is false >> in some model of the theory. >> >>> only because back then proof theoretic semantics did >>> not exist. >> >> Every interpretation of the theory is a definition of semantics. >> > > Meta‑math relations about numbers don’t exist in PA > because PA only contains arithmetical relations—addition, > multiplication, ordering, primitive‑recursive predicates > about numbers themselves—while relations that talk about > PA’s own proofs, syntax, or truth conditions live entirely > in the meta‑theory; Methamathematics does not need any other relations between numbers than what PA has. But relations that map other things to numbers can be useful for methamathematical purposes. > so when someone appeals to a Gödel‑style relation like > “n encodes a proof of this very sentence,” they’re > invoking a meta‑mathematical predicate that PA cannot > internalize, which is exactly why your framework draws > a clean boundary between internal proof‑theoretic truth > and external model‑theoretic truth. Anyway, what can be provven that way is true aboout PA. You can deny the proof but you cannot perform what is meta-provably impossible. -- Mikko
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2026-01-22 10:40 -0600 |
| Message-ID | <10ktjtm$35tto$1@dont-email.me> |
| In reply to | #344443 |
On 1/22/2026 2:21 AM, Mikko wrote: > On 21/01/2026 17:22, olcott wrote: >> On 1/21/2026 3:03 AM, Mikko wrote: >>> >>> No, it hasn't. In the way theories are usually discussed nothing is >>> "ture in arithmetic". Every sentence of a first order theory that >>> can be proven in the theory is true in every model theory. Every >>> sentence of a theory that cannot be proven in the theory is false >>> in some model of the theory. >>> >>>> only because back then proof theoretic semantics did >>>> not exist. >>> >>> Every interpretation of the theory is a definition of semantics. >>> >> >> Meta‑math relations about numbers don’t exist in PA >> because PA only contains arithmetical relations—addition, >> multiplication, ordering, primitive‑recursive predicates >> about numbers themselves—while relations that talk about >> PA’s own proofs, syntax, or truth conditions live entirely >> in the meta‑theory; > > Methamathematics does not need any other relations between numbers > than what PA has. But relations that map other things to numbers > can be useful for methamathematical purposes. > >> so when someone appeals to a Gödel‑style relation like >> “n encodes a proof of this very sentence,” they’re >> invoking a meta‑mathematical predicate that PA cannot >> internalize, which is exactly why your framework draws >> a clean boundary between internal proof‑theoretic truth >> and external model‑theoretic truth. > > Anyway, what can be provven that way is true aboout PA. You can deny > the proof but you cannot perform what is meta-provably impossible. > Gödel’s sentence is not “true in arithmetic.” It is true only in the meta‑theory, under an external interpretation of PA (typically the standard model ℕ). Inside PA itself, the sentence is not a truth‑bearer at all. The conflation happens when people treat model‑theoretic truth—truth in ℕ—as if it were internal truth in PA. Proof theoretic semantics anchored in axioms as their basis of truth proves that I have always been correct about everything that I said. All five LLMs agree with this immediately after I force them to actually simulate DD by HHH according to the semantics if C: Thus within well-founded proof theoretic semantics anchored in the operational semantics of the c programming language HHH(DD) is correct to reject its input as non-well-founded? Any cycle in the directed graph of the evaluation sequence of an expression correctly rejects this expression as non-well-founded in any proof theoretic semantics where true is anchored in the axioms of the system. Here is the first time that I explicitly referred to the idea of non-well-founded expressions in proof theoretic semantics [True(X) and ~Provable(X) is Impossible] Feb 4, 2018 https://groups.google.com/g/sci.logic/c/7XihPDLDy9s/m/uD6biLdjAwAJ -- Copyright 2026 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 | 2026-01-23 11:13 +0200 |
| Message-ID | <10kve43$3op07$1@dont-email.me> |
| In reply to | #344447 |
On 22/01/2026 18:40, olcott wrote: > On 1/22/2026 2:21 AM, Mikko wrote: >> On 21/01/2026 17:22, olcott wrote: >>> On 1/21/2026 3:03 AM, Mikko wrote: >>>> >>>> No, it hasn't. In the way theories are usually discussed nothing is >>>> "ture in arithmetic". Every sentence of a first order theory that >>>> can be proven in the theory is true in every model theory. Every >>>> sentence of a theory that cannot be proven in the theory is false >>>> in some model of the theory. >>>> >>>>> only because back then proof theoretic semantics did >>>>> not exist. >>>> >>>> Every interpretation of the theory is a definition of semantics. >>>> >>> >>> Meta‑math relations about numbers don’t exist in PA >>> because PA only contains arithmetical relations—addition, >>> multiplication, ordering, primitive‑recursive predicates >>> about numbers themselves—while relations that talk about >>> PA’s own proofs, syntax, or truth conditions live entirely >>> in the meta‑theory; >> >> Methamathematics does not need any other relations between numbers >> than what PA has. But relations that map other things to numbers >> can be useful for methamathematical purposes. >> >>> so when someone appeals to a Gödel‑style relation like >>> “n encodes a proof of this very sentence,” they’re >>> invoking a meta‑mathematical predicate that PA cannot >>> internalize, which is exactly why your framework draws >>> a clean boundary between internal proof‑theoretic truth >>> and external model‑theoretic truth. >> >> Anyway, what can be provven that way is true aboout PA. You can deny >> the proof but you cannot perform what is meta-provably impossible. > > Gödel’s sentence is not “true in arithmetic.” > It is true only in the meta‑theory, under an > external interpretation of PA (typically the > standard model ℕ). Inside PA itself, the sentence > is not a truth‑bearer at all. There is no concept of "truth-bearer" in an uninterpreted theory because there is not concept of "truth". The relevant concept is "sell-formed- formula" and Gödels sentence is one. It may be true or false in an interpretation. Gädel's metatheory contains PA. In Gödel's interpretation PA is interpreted in the same way as the PA part of the metathoéory. Gödel proves that G of PA as interpreted in the metatheory is true but cannot be proven in PA. -- Mikko
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2026-01-23 04:22 -0600 |
| Message-ID | <10kvi5r$3q24q$2@dont-email.me> |
| In reply to | #344473 |
On 1/23/2026 3:13 AM, Mikko wrote: > On 22/01/2026 18:40, olcott wrote: >> On 1/22/2026 2:21 AM, Mikko wrote: >>> On 21/01/2026 17:22, olcott wrote: >>>> On 1/21/2026 3:03 AM, Mikko wrote: >>>>> >>>>> No, it hasn't. In the way theories are usually discussed nothing is >>>>> "ture in arithmetic". Every sentence of a first order theory that >>>>> can be proven in the theory is true in every model theory. Every >>>>> sentence of a theory that cannot be proven in the theory is false >>>>> in some model of the theory. >>>>> >>>>>> only because back then proof theoretic semantics did >>>>>> not exist. >>>>> >>>>> Every interpretation of the theory is a definition of semantics. >>>>> >>>> >>>> Meta‑math relations about numbers don’t exist in PA >>>> because PA only contains arithmetical relations—addition, >>>> multiplication, ordering, primitive‑recursive predicates >>>> about numbers themselves—while relations that talk about >>>> PA’s own proofs, syntax, or truth conditions live entirely >>>> in the meta‑theory; >>> >>> Methamathematics does not need any other relations between numbers >>> than what PA has. But relations that map other things to numbers >>> can be useful for methamathematical purposes. >>> >>>> so when someone appeals to a Gödel‑style relation like >>>> “n encodes a proof of this very sentence,” they’re >>>> invoking a meta‑mathematical predicate that PA cannot >>>> internalize, which is exactly why your framework draws >>>> a clean boundary between internal proof‑theoretic truth >>>> and external model‑theoretic truth. >>> >>> Anyway, what can be provven that way is true aboout PA. You can deny >>> the proof but you cannot perform what is meta-provably impossible. >> >> Gödel’s sentence is not “true in arithmetic.” >> It is true only in the meta‑theory, under an >> external interpretation of PA (typically the >> standard model ℕ). Inside PA itself, the sentence >> is not a truth‑bearer at all. > > There is no concept of "truth-bearer" in an uninterpreted theory because > there is not concept of "truth". The relevant concept is "sell-formed- > formula" and Gödels sentence is one. It may be true or false in an > interpretation. > There is a "true on the basis of meaning expressed in language" and I figured out how to make it computable over the body of knowledge. > Gädel's metatheory contains PA. In Gödel's interpretation PA is > interpreted in the same way as the PA part of the metathoéory. > Gödel proves that G of PA as interpreted in the metatheory is > true but cannot be proven in PA. > -- Copyright 2026 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 | 2026-01-24 10:20 +0200 |
| Message-ID | <10l1vdd$l5o9$1@dont-email.me> |
| In reply to | #344476 |
On 23/01/2026 12:22, olcott wrote: > On 1/23/2026 3:13 AM, Mikko wrote: >> On 22/01/2026 18:40, olcott wrote: >>> On 1/22/2026 2:21 AM, Mikko wrote: >>>> On 21/01/2026 17:22, olcott wrote: >>>>> On 1/21/2026 3:03 AM, Mikko wrote: >>>>>> >>>>>> No, it hasn't. In the way theories are usually discussed nothing is >>>>>> "ture in arithmetic". Every sentence of a first order theory that >>>>>> can be proven in the theory is true in every model theory. Every >>>>>> sentence of a theory that cannot be proven in the theory is false >>>>>> in some model of the theory. >>>>>> >>>>>>> only because back then proof theoretic semantics did >>>>>>> not exist. >>>>>> >>>>>> Every interpretation of the theory is a definition of semantics. >>>>>> >>>>> >>>>> Meta‑math relations about numbers don’t exist in PA >>>>> because PA only contains arithmetical relations—addition, >>>>> multiplication, ordering, primitive‑recursive predicates >>>>> about numbers themselves—while relations that talk about >>>>> PA’s own proofs, syntax, or truth conditions live entirely >>>>> in the meta‑theory; >>>> >>>> Methamathematics does not need any other relations between numbers >>>> than what PA has. But relations that map other things to numbers >>>> can be useful for methamathematical purposes. >>>> >>>>> so when someone appeals to a Gödel‑style relation like >>>>> “n encodes a proof of this very sentence,” they’re >>>>> invoking a meta‑mathematical predicate that PA cannot >>>>> internalize, which is exactly why your framework draws >>>>> a clean boundary between internal proof‑theoretic truth >>>>> and external model‑theoretic truth. >>>> >>>> Anyway, what can be provven that way is true aboout PA. You can deny >>>> the proof but you cannot perform what is meta-provably impossible. >>> >>> Gödel’s sentence is not “true in arithmetic.” >>> It is true only in the meta‑theory, under an >>> external interpretation of PA (typically the >>> standard model ℕ). Inside PA itself, the sentence >>> is not a truth‑bearer at all. >> >> There is no concept of "truth-bearer" in an uninterpreted theory because >> there is not concept of "truth". The relevant concept is "sell-formed- >> formula" and Gödels sentence is one. It may be true or false in an >> interpretation. > There is a > "true on the basis of meaning expressed in language" > and I figured out how to make it computable over the > body of knowledge. Except that "true on the basis of meaning expressed in language" is nmt computable and does not cover all of the body of knowldge. -- Mikko
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2026-01-24 08:01 -0600 |
| Message-ID | <10l2jci$rkbl$1@dont-email.me> |
| In reply to | #344487 |
On 1/24/2026 2:20 AM, Mikko wrote: > On 23/01/2026 12:22, olcott wrote: >> On 1/23/2026 3:13 AM, Mikko wrote: >>> On 22/01/2026 18:40, olcott wrote: >>>> On 1/22/2026 2:21 AM, Mikko wrote: >>>>> On 21/01/2026 17:22, olcott wrote: >>>>>> On 1/21/2026 3:03 AM, Mikko wrote: >>>>>>> >>>>>>> No, it hasn't. In the way theories are usually discussed nothing is >>>>>>> "ture in arithmetic". Every sentence of a first order theory that >>>>>>> can be proven in the theory is true in every model theory. Every >>>>>>> sentence of a theory that cannot be proven in the theory is false >>>>>>> in some model of the theory. >>>>>>> >>>>>>>> only because back then proof theoretic semantics did >>>>>>>> not exist. >>>>>>> >>>>>>> Every interpretation of the theory is a definition of semantics. >>>>>>> >>>>>> >>>>>> Meta‑math relations about numbers don’t exist in PA >>>>>> because PA only contains arithmetical relations—addition, >>>>>> multiplication, ordering, primitive‑recursive predicates >>>>>> about numbers themselves—while relations that talk about >>>>>> PA’s own proofs, syntax, or truth conditions live entirely >>>>>> in the meta‑theory; >>>>> >>>>> Methamathematics does not need any other relations between numbers >>>>> than what PA has. But relations that map other things to numbers >>>>> can be useful for methamathematical purposes. >>>>> >>>>>> so when someone appeals to a Gödel‑style relation like >>>>>> “n encodes a proof of this very sentence,” they’re >>>>>> invoking a meta‑mathematical predicate that PA cannot >>>>>> internalize, which is exactly why your framework draws >>>>>> a clean boundary between internal proof‑theoretic truth >>>>>> and external model‑theoretic truth. >>>>> >>>>> Anyway, what can be provven that way is true aboout PA. You can deny >>>>> the proof but you cannot perform what is meta-provably impossible. >>>> >>>> Gödel’s sentence is not “true in arithmetic.” >>>> It is true only in the meta‑theory, under an >>>> external interpretation of PA (typically the >>>> standard model ℕ). Inside PA itself, the sentence >>>> is not a truth‑bearer at all. >>> >>> There is no concept of "truth-bearer" in an uninterpreted theory because >>> there is not concept of "truth". The relevant concept is "sell-formed- >>> formula" and Gödels sentence is one. It may be true or false in an >>> interpretation. > >> There is a >> "true on the basis of meaning expressed in language" >> and I figured out how to make it computable over the >> body of knowledge. > > Except that "true on the basis of meaning expressed in language" is > nmt computable and does not cover all of the body of knowldge. > When the basis of "true" is proof theoretic semantics internal to the formal system relative to its own axioms and not truth conditional in a separate model outside of the system undecidability ceases to exist. -- Copyright 2026 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 | 2026-01-25 13:19 +0200 |
| Message-ID | <10l4u7q$1jgpb$1@dont-email.me> |
| In reply to | #344493 |
On 24/01/2026 16:01, olcott wrote: > On 1/24/2026 2:20 AM, Mikko wrote: >> On 23/01/2026 12:22, olcott wrote: >>> On 1/23/2026 3:13 AM, Mikko wrote: >>>> On 22/01/2026 18:40, olcott wrote: >>>>> On 1/22/2026 2:21 AM, Mikko wrote: >>>>>> On 21/01/2026 17:22, olcott wrote: >>>>>>> On 1/21/2026 3:03 AM, Mikko wrote: >>>>>>>> >>>>>>>> No, it hasn't. In the way theories are usually discussed nothing is >>>>>>>> "ture in arithmetic". Every sentence of a first order theory that >>>>>>>> can be proven in the theory is true in every model theory. Every >>>>>>>> sentence of a theory that cannot be proven in the theory is false >>>>>>>> in some model of the theory. >>>>>>>> >>>>>>>>> only because back then proof theoretic semantics did >>>>>>>>> not exist. >>>>>>>> >>>>>>>> Every interpretation of the theory is a definition of semantics. >>>>>>>> >>>>>>> >>>>>>> Meta‑math relations about numbers don’t exist in PA >>>>>>> because PA only contains arithmetical relations—addition, >>>>>>> multiplication, ordering, primitive‑recursive predicates >>>>>>> about numbers themselves—while relations that talk about >>>>>>> PA’s own proofs, syntax, or truth conditions live entirely >>>>>>> in the meta‑theory; >>>>>> >>>>>> Methamathematics does not need any other relations between numbers >>>>>> than what PA has. But relations that map other things to numbers >>>>>> can be useful for methamathematical purposes. >>>>>> >>>>>>> so when someone appeals to a Gödel‑style relation like >>>>>>> “n encodes a proof of this very sentence,” they’re >>>>>>> invoking a meta‑mathematical predicate that PA cannot >>>>>>> internalize, which is exactly why your framework draws >>>>>>> a clean boundary between internal proof‑theoretic truth >>>>>>> and external model‑theoretic truth. >>>>>> >>>>>> Anyway, what can be provven that way is true aboout PA. You can deny >>>>>> the proof but you cannot perform what is meta-provably impossible. >>>>> >>>>> Gödel’s sentence is not “true in arithmetic.” >>>>> It is true only in the meta‑theory, under an >>>>> external interpretation of PA (typically the >>>>> standard model ℕ). Inside PA itself, the sentence >>>>> is not a truth‑bearer at all. >>>> >>>> There is no concept of "truth-bearer" in an uninterpreted theory >>>> because >>>> there is not concept of "truth". The relevant concept is "sell-formed- >>>> formula" and Gödels sentence is one. It may be true or false in an >>>> interpretation. >> >>> There is a >>> "true on the basis of meaning expressed in language" >>> and I figured out how to make it computable over the >>> body of knowledge. >> >> Except that "true on the basis of meaning expressed in language" is >> nmt computable and does not cover all of the body of knowldge. > > When the basis of "true" is proof theoretic semantics > internal to the formal system relative to its own axioms > and not truth conditional in a separate model outside > of the system undecidability ceases to exist. No, it does not. It does not matter what you call it, a sentence that cannot be neither proven nor disproven is undecidable because that is what the word means. An example is Gödel's sentence in Peano arithmetics. -- Mikko
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2026-01-25 07:24 -0600 |
| Message-ID | <10l55hq$1lth6$1@dont-email.me> |
| In reply to | #344529 |
On 1/25/2026 5:19 AM, Mikko wrote: > On 24/01/2026 16:01, olcott wrote: >> On 1/24/2026 2:20 AM, Mikko wrote: >>> On 23/01/2026 12:22, olcott wrote: >>>> On 1/23/2026 3:13 AM, Mikko wrote: >>>>> On 22/01/2026 18:40, olcott wrote: >>>>>> On 1/22/2026 2:21 AM, Mikko wrote: >>>>>>> On 21/01/2026 17:22, olcott wrote: >>>>>>>> On 1/21/2026 3:03 AM, Mikko wrote: >>>>>>>>> >>>>>>>>> No, it hasn't. In the way theories are usually discussed >>>>>>>>> nothing is >>>>>>>>> "ture in arithmetic". Every sentence of a first order theory that >>>>>>>>> can be proven in the theory is true in every model theory. Every >>>>>>>>> sentence of a theory that cannot be proven in the theory is false >>>>>>>>> in some model of the theory. >>>>>>>>> >>>>>>>>>> only because back then proof theoretic semantics did >>>>>>>>>> not exist. >>>>>>>>> >>>>>>>>> Every interpretation of the theory is a definition of semantics. >>>>>>>>> >>>>>>>> >>>>>>>> Meta‑math relations about numbers don’t exist in PA >>>>>>>> because PA only contains arithmetical relations—addition, >>>>>>>> multiplication, ordering, primitive‑recursive predicates >>>>>>>> about numbers themselves—while relations that talk about >>>>>>>> PA’s own proofs, syntax, or truth conditions live entirely >>>>>>>> in the meta‑theory; >>>>>>> >>>>>>> Methamathematics does not need any other relations between numbers >>>>>>> than what PA has. But relations that map other things to numbers >>>>>>> can be useful for methamathematical purposes. >>>>>>> >>>>>>>> so when someone appeals to a Gödel‑style relation like >>>>>>>> “n encodes a proof of this very sentence,” they’re >>>>>>>> invoking a meta‑mathematical predicate that PA cannot >>>>>>>> internalize, which is exactly why your framework draws >>>>>>>> a clean boundary between internal proof‑theoretic truth >>>>>>>> and external model‑theoretic truth. >>>>>>> >>>>>>> Anyway, what can be provven that way is true aboout PA. You can deny >>>>>>> the proof but you cannot perform what is meta-provably impossible. >>>>>> >>>>>> Gödel’s sentence is not “true in arithmetic.” >>>>>> It is true only in the meta‑theory, under an >>>>>> external interpretation of PA (typically the >>>>>> standard model ℕ). Inside PA itself, the sentence >>>>>> is not a truth‑bearer at all. >>>>> >>>>> There is no concept of "truth-bearer" in an uninterpreted theory >>>>> because >>>>> there is not concept of "truth". The relevant concept is "sell-formed- >>>>> formula" and Gödels sentence is one. It may be true or false in an >>>>> interpretation. >>> >>>> There is a >>>> "true on the basis of meaning expressed in language" >>>> and I figured out how to make it computable over the >>>> body of knowledge. >>> >>> Except that "true on the basis of meaning expressed in language" is >>> nmt computable and does not cover all of the body of knowldge. >> >> When the basis of "true" is proof theoretic semantics >> internal to the formal system relative to its own axioms >> and not truth conditional in a separate model outside >> of the system undecidability ceases to exist. > > No, it does not. It does not matter what you call it, a sentence > that cannot be neither proven nor disproven is undecidable because > that is what the word means. An example is Gödel's sentence in > Peano arithmetics. > When a truth predicate gets the input "What time is?" this input is rejected as not truth-apt. When PA gets an expression that cannot be proven or refuted using its own axioms then this expression is not within its domain. -- Copyright 2026 Olcott<br><br> My 28 year goal has been to make <br> "true on the basis of meaning expressed in language"<br> reliably computable for the entire body of knowledge.<br><br> This required establishing a new foundation<br>
[toc] | [prev] | [next] | [standalone]
| From | Richard Damon <Richard@Damon-Family.org> |
|---|---|
| Date | 2026-01-25 13:27 -0500 |
| Message-ID | <xgtdR.98062$4e1.48518@fx20.iad> |
| In reply to | #344531 |
On 1/25/26 8:24 AM, olcott wrote: > On 1/25/2026 5:19 AM, Mikko wrote: >> On 24/01/2026 16:01, olcott wrote: >>> On 1/24/2026 2:20 AM, Mikko wrote: >>>> On 23/01/2026 12:22, olcott wrote: >>>>> On 1/23/2026 3:13 AM, Mikko wrote: >>>>>> On 22/01/2026 18:40, olcott wrote: >>>>>>> On 1/22/2026 2:21 AM, Mikko wrote: >>>>>>>> On 21/01/2026 17:22, olcott wrote: >>>>>>>>> On 1/21/2026 3:03 AM, Mikko wrote: >>>>>>>>>> >>>>>>>>>> No, it hasn't. In the way theories are usually discussed >>>>>>>>>> nothing is >>>>>>>>>> "ture in arithmetic". Every sentence of a first order theory that >>>>>>>>>> can be proven in the theory is true in every model theory. Every >>>>>>>>>> sentence of a theory that cannot be proven in the theory is false >>>>>>>>>> in some model of the theory. >>>>>>>>>> >>>>>>>>>>> only because back then proof theoretic semantics did >>>>>>>>>>> not exist. >>>>>>>>>> >>>>>>>>>> Every interpretation of the theory is a definition of semantics. >>>>>>>>>> >>>>>>>>> >>>>>>>>> Meta‑math relations about numbers don’t exist in PA >>>>>>>>> because PA only contains arithmetical relations—addition, >>>>>>>>> multiplication, ordering, primitive‑recursive predicates >>>>>>>>> about numbers themselves—while relations that talk about >>>>>>>>> PA’s own proofs, syntax, or truth conditions live entirely >>>>>>>>> in the meta‑theory; >>>>>>>> >>>>>>>> Methamathematics does not need any other relations between numbers >>>>>>>> than what PA has. But relations that map other things to numbers >>>>>>>> can be useful for methamathematical purposes. >>>>>>>> >>>>>>>>> so when someone appeals to a Gödel‑style relation like >>>>>>>>> “n encodes a proof of this very sentence,” they’re >>>>>>>>> invoking a meta‑mathematical predicate that PA cannot >>>>>>>>> internalize, which is exactly why your framework draws >>>>>>>>> a clean boundary between internal proof‑theoretic truth >>>>>>>>> and external model‑theoretic truth. >>>>>>>> >>>>>>>> Anyway, what can be provven that way is true aboout PA. You can >>>>>>>> deny >>>>>>>> the proof but you cannot perform what is meta-provably impossible. >>>>>>> >>>>>>> Gödel’s sentence is not “true in arithmetic.” >>>>>>> It is true only in the meta‑theory, under an >>>>>>> external interpretation of PA (typically the >>>>>>> standard model ℕ). Inside PA itself, the sentence >>>>>>> is not a truth‑bearer at all. >>>>>> >>>>>> There is no concept of "truth-bearer" in an uninterpreted theory >>>>>> because >>>>>> there is not concept of "truth". The relevant concept is "sell- >>>>>> formed- >>>>>> formula" and Gödels sentence is one. It may be true or false in an >>>>>> interpretation. >>>> >>>>> There is a >>>>> "true on the basis of meaning expressed in language" >>>>> and I figured out how to make it computable over the >>>>> body of knowledge. >>>> >>>> Except that "true on the basis of meaning expressed in language" is >>>> nmt computable and does not cover all of the body of knowldge. >>> >>> When the basis of "true" is proof theoretic semantics >>> internal to the formal system relative to its own axioms >>> and not truth conditional in a separate model outside >>> of the system undecidability ceases to exist. >> >> No, it does not. It does not matter what you call it, a sentence >> that cannot be neither proven nor disproven is undecidable because >> that is what the word means. An example is Gödel's sentence in >> Peano arithmetics. >> > > When a truth predicate gets the input "What time is?" > this input is rejected as not truth-apt. That fine. > > When PA gets an expression that cannot be proven or > refuted using its own axioms then this expression is > not within its domain. > Then most of Natural Number mathematics is isn't in its domain, And, you can't KNOW if somehting is a valid question to ask until you know the answer. This makes a fairly worthless domain to learn things in. By your definition, a question like can every even number, greater than 2, be the sum of two prime numbers MIGHT not be within its domain, even though it is purely a question about the capability of numbers.
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2026-01-25 12:33 -0600 |
| Message-ID | <10l5nls$1sfs5$1@dont-email.me> |
| In reply to | #344534 |
On 1/25/2026 12:27 PM, Richard Damon wrote: > On 1/25/26 8:24 AM, olcott wrote: >> On 1/25/2026 5:19 AM, Mikko wrote: >>> On 24/01/2026 16:01, olcott wrote: >>>> On 1/24/2026 2:20 AM, Mikko wrote: >>>>> On 23/01/2026 12:22, olcott wrote: >>>>>> On 1/23/2026 3:13 AM, Mikko wrote: >>>>>>> On 22/01/2026 18:40, olcott wrote: >>>>>>>> On 1/22/2026 2:21 AM, Mikko wrote: >>>>>>>>> On 21/01/2026 17:22, olcott wrote: >>>>>>>>>> On 1/21/2026 3:03 AM, Mikko wrote: >>>>>>>>>>> >>>>>>>>>>> No, it hasn't. In the way theories are usually discussed >>>>>>>>>>> nothing is >>>>>>>>>>> "ture in arithmetic". Every sentence of a first order theory >>>>>>>>>>> that >>>>>>>>>>> can be proven in the theory is true in every model theory. Every >>>>>>>>>>> sentence of a theory that cannot be proven in the theory is >>>>>>>>>>> false >>>>>>>>>>> in some model of the theory. >>>>>>>>>>> >>>>>>>>>>>> only because back then proof theoretic semantics did >>>>>>>>>>>> not exist. >>>>>>>>>>> >>>>>>>>>>> Every interpretation of the theory is a definition of semantics. >>>>>>>>>>> >>>>>>>>>> >>>>>>>>>> Meta‑math relations about numbers don’t exist in PA >>>>>>>>>> because PA only contains arithmetical relations—addition, >>>>>>>>>> multiplication, ordering, primitive‑recursive predicates >>>>>>>>>> about numbers themselves—while relations that talk about >>>>>>>>>> PA’s own proofs, syntax, or truth conditions live entirely >>>>>>>>>> in the meta‑theory; >>>>>>>>> >>>>>>>>> Methamathematics does not need any other relations between numbers >>>>>>>>> than what PA has. But relations that map other things to numbers >>>>>>>>> can be useful for methamathematical purposes. >>>>>>>>> >>>>>>>>>> so when someone appeals to a Gödel‑style relation like >>>>>>>>>> “n encodes a proof of this very sentence,” they’re >>>>>>>>>> invoking a meta‑mathematical predicate that PA cannot >>>>>>>>>> internalize, which is exactly why your framework draws >>>>>>>>>> a clean boundary between internal proof‑theoretic truth >>>>>>>>>> and external model‑theoretic truth. >>>>>>>>> >>>>>>>>> Anyway, what can be provven that way is true aboout PA. You can >>>>>>>>> deny >>>>>>>>> the proof but you cannot perform what is meta-provably impossible. >>>>>>>> >>>>>>>> Gödel’s sentence is not “true in arithmetic.” >>>>>>>> It is true only in the meta‑theory, under an >>>>>>>> external interpretation of PA (typically the >>>>>>>> standard model ℕ). Inside PA itself, the sentence >>>>>>>> is not a truth‑bearer at all. >>>>>>> >>>>>>> There is no concept of "truth-bearer" in an uninterpreted theory >>>>>>> because >>>>>>> there is not concept of "truth". The relevant concept is "sell- >>>>>>> formed- >>>>>>> formula" and Gödels sentence is one. It may be true or false in an >>>>>>> interpretation. >>>>> >>>>>> There is a >>>>>> "true on the basis of meaning expressed in language" >>>>>> and I figured out how to make it computable over the >>>>>> body of knowledge. >>>>> >>>>> Except that "true on the basis of meaning expressed in language" is >>>>> nmt computable and does not cover all of the body of knowldge. >>>> >>>> When the basis of "true" is proof theoretic semantics >>>> internal to the formal system relative to its own axioms >>>> and not truth conditional in a separate model outside >>>> of the system undecidability ceases to exist. >>> >>> No, it does not. It does not matter what you call it, a sentence >>> that cannot be neither proven nor disproven is undecidable because >>> that is what the word means. An example is Gödel's sentence in >>> Peano arithmetics. >>> >> >> When a truth predicate gets the input "What time is?" >> this input is rejected as not truth-apt. > > > That fine. >> >> When PA gets an expression that cannot be proven or >> refuted using its own axioms then this expression is >> not within its domain. >> > > Then most of Natural Number mathematics is isn't in its domain, > It is what it is. PA doesn't even know PA until you add a truth predicate. When you do add a truth predicate then PA knows PA. If you want more than that then meta-math can know "about" PA. This is one level of indirect reference away from knowing PA. > And, you can't KNOW if somehting is a valid question to ask until you > know the answer. > > This makes a fairly worthless domain to learn things in. > > By your definition, a question like can every even number, greater than > 2, be the sum of two prime numbers MIGHT not be within its domain, even > though it is purely a question about the capability of numbers. > -- Copyright 2026 Olcott<br><br> My 28 year goal has been to make <br> "true on the basis of meaning expressed in language"<br> reliably computable for the entire body of knowledge.<br><br> This required establishing a new foundation<br>
[toc] | [prev] | [next] | [standalone]
| From | Richard Damon <Richard@Damon-Family.org> |
|---|---|
| Date | 2026-01-25 13:40 -0500 |
| Message-ID | <DstdR.98065$4e1.52878@fx20.iad> |
| In reply to | #344536 |
On 1/25/26 1:33 PM, olcott wrote: > On 1/25/2026 12:27 PM, Richard Damon wrote: >> On 1/25/26 8:24 AM, olcott wrote: >>> On 1/25/2026 5:19 AM, Mikko wrote: >>>> On 24/01/2026 16:01, olcott wrote: >>>>> On 1/24/2026 2:20 AM, Mikko wrote: >>>>>> On 23/01/2026 12:22, olcott wrote: >>>>>>> On 1/23/2026 3:13 AM, Mikko wrote: >>>>>>>> On 22/01/2026 18:40, olcott wrote: >>>>>>>>> On 1/22/2026 2:21 AM, Mikko wrote: >>>>>>>>>> On 21/01/2026 17:22, olcott wrote: >>>>>>>>>>> On 1/21/2026 3:03 AM, Mikko wrote: >>>>>>>>>>>> >>>>>>>>>>>> No, it hasn't. In the way theories are usually discussed >>>>>>>>>>>> nothing is >>>>>>>>>>>> "ture in arithmetic". Every sentence of a first order theory >>>>>>>>>>>> that >>>>>>>>>>>> can be proven in the theory is true in every model theory. >>>>>>>>>>>> Every >>>>>>>>>>>> sentence of a theory that cannot be proven in the theory is >>>>>>>>>>>> false >>>>>>>>>>>> in some model of the theory. >>>>>>>>>>>> >>>>>>>>>>>>> only because back then proof theoretic semantics did >>>>>>>>>>>>> not exist. >>>>>>>>>>>> >>>>>>>>>>>> Every interpretation of the theory is a definition of >>>>>>>>>>>> semantics. >>>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> Meta‑math relations about numbers don’t exist in PA >>>>>>>>>>> because PA only contains arithmetical relations—addition, >>>>>>>>>>> multiplication, ordering, primitive‑recursive predicates >>>>>>>>>>> about numbers themselves—while relations that talk about >>>>>>>>>>> PA’s own proofs, syntax, or truth conditions live entirely >>>>>>>>>>> in the meta‑theory; >>>>>>>>>> >>>>>>>>>> Methamathematics does not need any other relations between >>>>>>>>>> numbers >>>>>>>>>> than what PA has. But relations that map other things to numbers >>>>>>>>>> can be useful for methamathematical purposes. >>>>>>>>>> >>>>>>>>>>> so when someone appeals to a Gödel‑style relation like >>>>>>>>>>> “n encodes a proof of this very sentence,” they’re >>>>>>>>>>> invoking a meta‑mathematical predicate that PA cannot >>>>>>>>>>> internalize, which is exactly why your framework draws >>>>>>>>>>> a clean boundary between internal proof‑theoretic truth >>>>>>>>>>> and external model‑theoretic truth. >>>>>>>>>> >>>>>>>>>> Anyway, what can be provven that way is true aboout PA. You >>>>>>>>>> can deny >>>>>>>>>> the proof but you cannot perform what is meta-provably >>>>>>>>>> impossible. >>>>>>>>> >>>>>>>>> Gödel’s sentence is not “true in arithmetic.” >>>>>>>>> It is true only in the meta‑theory, under an >>>>>>>>> external interpretation of PA (typically the >>>>>>>>> standard model ℕ). Inside PA itself, the sentence >>>>>>>>> is not a truth‑bearer at all. >>>>>>>> >>>>>>>> There is no concept of "truth-bearer" in an uninterpreted theory >>>>>>>> because >>>>>>>> there is not concept of "truth". The relevant concept is "sell- >>>>>>>> formed- >>>>>>>> formula" and Gödels sentence is one. It may be true or false in an >>>>>>>> interpretation. >>>>>> >>>>>>> There is a >>>>>>> "true on the basis of meaning expressed in language" >>>>>>> and I figured out how to make it computable over the >>>>>>> body of knowledge. >>>>>> >>>>>> Except that "true on the basis of meaning expressed in language" is >>>>>> nmt computable and does not cover all of the body of knowldge. >>>>> >>>>> When the basis of "true" is proof theoretic semantics >>>>> internal to the formal system relative to its own axioms >>>>> and not truth conditional in a separate model outside >>>>> of the system undecidability ceases to exist. >>>> >>>> No, it does not. It does not matter what you call it, a sentence >>>> that cannot be neither proven nor disproven is undecidable because >>>> that is what the word means. An example is Gödel's sentence in >>>> Peano arithmetics. >>>> >>> >>> When a truth predicate gets the input "What time is?" >>> this input is rejected as not truth-apt. >> >> >> That fine. >>> >>> When PA gets an expression that cannot be proven or >>> refuted using its own axioms then this expression is >>> not within its domain. >>> >> >> Then most of Natural Number mathematics is isn't in its domain, >> > > It is what it is. But PA was CREATED to allow us to define the Natural Numbers in an axiomatic way. > PA doesn't even know PA until you add a truth predicate. > When you do add a truth predicate then PA knows PA. If > you want more than that then meta-math can know "about" PA. > This is one level of indirect reference away from knowing PA. In other words, you world is just inconsistant because it can't handle itself. You just build your logic on equivocations and lies. But since PA doesn't have a truth predicate, you can't add it. What PA has, if you actually understand it, is that it was built on a definition of logic that defines truth based on what flows out of the possible infinite application of its axioms. When you try to build with a lessor logic, you don't get a PA that can do what it needs to, and thus isn't actually an arithmatic. > >> And, you can't KNOW if somehting is a valid question to ask until you >> know the answer. >> >> This makes a fairly worthless domain to learn things in. >> >> By your definition, a question like can every even number, greater >> than 2, be the sum of two prime numbers MIGHT not be within its >> domain, even though it is purely a question about the capability of >> numbers. >> > >
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2026-01-25 13:10 -0600 |
| Message-ID | <10l5ps0$1t9k0$2@dont-email.me> |
| In reply to | #344538 |
On 1/25/2026 12:40 PM, Richard Damon wrote: > On 1/25/26 1:33 PM, olcott wrote: >> On 1/25/2026 12:27 PM, Richard Damon wrote: >>> On 1/25/26 8:24 AM, olcott wrote: >>>> On 1/25/2026 5:19 AM, Mikko wrote: >>>>> On 24/01/2026 16:01, olcott wrote: >>>>>> On 1/24/2026 2:20 AM, Mikko wrote: >>>>>>> On 23/01/2026 12:22, olcott wrote: >>>>>>>> On 1/23/2026 3:13 AM, Mikko wrote: >>>>>>>>> On 22/01/2026 18:40, olcott wrote: >>>>>>>>>> On 1/22/2026 2:21 AM, Mikko wrote: >>>>>>>>>>> On 21/01/2026 17:22, olcott wrote: >>>>>>>>>>>> On 1/21/2026 3:03 AM, Mikko wrote: >>>>>>>>>>>>> >>>>>>>>>>>>> No, it hasn't. In the way theories are usually discussed >>>>>>>>>>>>> nothing is >>>>>>>>>>>>> "ture in arithmetic". Every sentence of a first order >>>>>>>>>>>>> theory that >>>>>>>>>>>>> can be proven in the theory is true in every model theory. >>>>>>>>>>>>> Every >>>>>>>>>>>>> sentence of a theory that cannot be proven in the theory is >>>>>>>>>>>>> false >>>>>>>>>>>>> in some model of the theory. >>>>>>>>>>>>> >>>>>>>>>>>>>> only because back then proof theoretic semantics did >>>>>>>>>>>>>> not exist. >>>>>>>>>>>>> >>>>>>>>>>>>> Every interpretation of the theory is a definition of >>>>>>>>>>>>> semantics. >>>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> Meta‑math relations about numbers don’t exist in PA >>>>>>>>>>>> because PA only contains arithmetical relations—addition, >>>>>>>>>>>> multiplication, ordering, primitive‑recursive predicates >>>>>>>>>>>> about numbers themselves—while relations that talk about >>>>>>>>>>>> PA’s own proofs, syntax, or truth conditions live entirely >>>>>>>>>>>> in the meta‑theory; >>>>>>>>>>> >>>>>>>>>>> Methamathematics does not need any other relations between >>>>>>>>>>> numbers >>>>>>>>>>> than what PA has. But relations that map other things to numbers >>>>>>>>>>> can be useful for methamathematical purposes. >>>>>>>>>>> >>>>>>>>>>>> so when someone appeals to a Gödel‑style relation like >>>>>>>>>>>> “n encodes a proof of this very sentence,” they’re >>>>>>>>>>>> invoking a meta‑mathematical predicate that PA cannot >>>>>>>>>>>> internalize, which is exactly why your framework draws >>>>>>>>>>>> a clean boundary between internal proof‑theoretic truth >>>>>>>>>>>> and external model‑theoretic truth. >>>>>>>>>>> >>>>>>>>>>> Anyway, what can be provven that way is true aboout PA. You >>>>>>>>>>> can deny >>>>>>>>>>> the proof but you cannot perform what is meta-provably >>>>>>>>>>> impossible. >>>>>>>>>> >>>>>>>>>> Gödel’s sentence is not “true in arithmetic.” >>>>>>>>>> It is true only in the meta‑theory, under an >>>>>>>>>> external interpretation of PA (typically the >>>>>>>>>> standard model ℕ). Inside PA itself, the sentence >>>>>>>>>> is not a truth‑bearer at all. >>>>>>>>> >>>>>>>>> There is no concept of "truth-bearer" in an uninterpreted >>>>>>>>> theory because >>>>>>>>> there is not concept of "truth". The relevant concept is "sell- >>>>>>>>> formed- >>>>>>>>> formula" and Gödels sentence is one. It may be true or false in an >>>>>>>>> interpretation. >>>>>>> >>>>>>>> There is a >>>>>>>> "true on the basis of meaning expressed in language" >>>>>>>> and I figured out how to make it computable over the >>>>>>>> body of knowledge. >>>>>>> >>>>>>> Except that "true on the basis of meaning expressed in language" is >>>>>>> nmt computable and does not cover all of the body of knowldge. >>>>>> >>>>>> When the basis of "true" is proof theoretic semantics >>>>>> internal to the formal system relative to its own axioms >>>>>> and not truth conditional in a separate model outside >>>>>> of the system undecidability ceases to exist. >>>>> >>>>> No, it does not. It does not matter what you call it, a sentence >>>>> that cannot be neither proven nor disproven is undecidable because >>>>> that is what the word means. An example is Gödel's sentence in >>>>> Peano arithmetics. >>>>> >>>> >>>> When a truth predicate gets the input "What time is?" >>>> this input is rejected as not truth-apt. >>> >>> >>> That fine. >>>> >>>> When PA gets an expression that cannot be proven or >>>> refuted using its own axioms then this expression is >>>> not within its domain. >>>> >>> >>> Then most of Natural Number mathematics is isn't in its domain, >>> >> >> It is what it is. > > But PA was CREATED to allow us to define the Natural Numbers in an > axiomatic way. > Yet only within the actual axioms of PA. >> PA doesn't even know PA until you add a truth predicate. >> When you do add a truth predicate then PA knows PA. If >> you want more than that then meta-math can know "about" PA. >> This is one level of indirect reference away from knowing PA. > > In other words, you world is just inconsistant because it can't handle > itself. > > You just build your logic on equivocations and lies. > > But since PA doesn't have a truth predicate, you can't add it. > > What PA has, if you actually understand it, is that it was built on a > definition of logic that defines truth based on what flows out of the > possible infinite application of its axioms. > > When you try to build with a lessor logic, you don't get a PA that can > do what it needs to, and thus isn't actually an arithmatic. > >> >>> And, you can't KNOW if somehting is a valid question to ask until you >>> know the answer. >>> >>> This makes a fairly worthless domain to learn things in. >>> >>> By your definition, a question like can every even number, greater >>> than 2, be the sum of two prime numbers MIGHT not be within its >>> domain, even though it is purely a question about the capability of >>> numbers. >>> >> >> > -- Copyright 2026 Olcott<br><br> My 28 year goal has been to make <br> "true on the basis of meaning expressed in language"<br> reliably computable for the entire body of knowledge.<br><br> This required establishing a new foundation<br>
[toc] | [prev] | [next] | [standalone]
| From | Richard Damon <Richard@Damon-Family.org> |
|---|---|
| Date | 2026-01-25 14:57 -0500 |
| Message-ID | <rAudR.98067$4e1.42181@fx20.iad> |
| In reply to | #344541 |
On 1/25/26 2:10 PM, olcott wrote: > On 1/25/2026 12:40 PM, Richard Damon wrote: >> On 1/25/26 1:33 PM, olcott wrote: >>> On 1/25/2026 12:27 PM, Richard Damon wrote: >>>> On 1/25/26 8:24 AM, olcott wrote: >>>>> On 1/25/2026 5:19 AM, Mikko wrote: >>>>>> On 24/01/2026 16:01, olcott wrote: >>>>>>> On 1/24/2026 2:20 AM, Mikko wrote: >>>>>>>> On 23/01/2026 12:22, olcott wrote: >>>>>>>>> On 1/23/2026 3:13 AM, Mikko wrote: >>>>>>>>>> On 22/01/2026 18:40, olcott wrote: >>>>>>>>>>> On 1/22/2026 2:21 AM, Mikko wrote: >>>>>>>>>>>> On 21/01/2026 17:22, olcott wrote: >>>>>>>>>>>>> On 1/21/2026 3:03 AM, Mikko wrote: >>>>>>>>>>>>>> >>>>>>>>>>>>>> No, it hasn't. In the way theories are usually discussed >>>>>>>>>>>>>> nothing is >>>>>>>>>>>>>> "ture in arithmetic". Every sentence of a first order >>>>>>>>>>>>>> theory that >>>>>>>>>>>>>> can be proven in the theory is true in every model theory. >>>>>>>>>>>>>> Every >>>>>>>>>>>>>> sentence of a theory that cannot be proven in the theory >>>>>>>>>>>>>> is false >>>>>>>>>>>>>> in some model of the theory. >>>>>>>>>>>>>> >>>>>>>>>>>>>>> only because back then proof theoretic semantics did >>>>>>>>>>>>>>> not exist. >>>>>>>>>>>>>> >>>>>>>>>>>>>> Every interpretation of the theory is a definition of >>>>>>>>>>>>>> semantics. >>>>>>>>>>>>>> >>>>>>>>>>>>> >>>>>>>>>>>>> Meta‑math relations about numbers don’t exist in PA >>>>>>>>>>>>> because PA only contains arithmetical relations—addition, >>>>>>>>>>>>> multiplication, ordering, primitive‑recursive predicates >>>>>>>>>>>>> about numbers themselves—while relations that talk about >>>>>>>>>>>>> PA’s own proofs, syntax, or truth conditions live entirely >>>>>>>>>>>>> in the meta‑theory; >>>>>>>>>>>> >>>>>>>>>>>> Methamathematics does not need any other relations between >>>>>>>>>>>> numbers >>>>>>>>>>>> than what PA has. But relations that map other things to >>>>>>>>>>>> numbers >>>>>>>>>>>> can be useful for methamathematical purposes. >>>>>>>>>>>> >>>>>>>>>>>>> so when someone appeals to a Gödel‑style relation like >>>>>>>>>>>>> “n encodes a proof of this very sentence,” they’re >>>>>>>>>>>>> invoking a meta‑mathematical predicate that PA cannot >>>>>>>>>>>>> internalize, which is exactly why your framework draws >>>>>>>>>>>>> a clean boundary between internal proof‑theoretic truth >>>>>>>>>>>>> and external model‑theoretic truth. >>>>>>>>>>>> >>>>>>>>>>>> Anyway, what can be provven that way is true aboout PA. You >>>>>>>>>>>> can deny >>>>>>>>>>>> the proof but you cannot perform what is meta-provably >>>>>>>>>>>> impossible. >>>>>>>>>>> >>>>>>>>>>> Gödel’s sentence is not “true in arithmetic.” >>>>>>>>>>> It is true only in the meta‑theory, under an >>>>>>>>>>> external interpretation of PA (typically the >>>>>>>>>>> standard model ℕ). Inside PA itself, the sentence >>>>>>>>>>> is not a truth‑bearer at all. >>>>>>>>>> >>>>>>>>>> There is no concept of "truth-bearer" in an uninterpreted >>>>>>>>>> theory because >>>>>>>>>> there is not concept of "truth". The relevant concept is >>>>>>>>>> "sell- formed- >>>>>>>>>> formula" and Gödels sentence is one. It may be true or false >>>>>>>>>> in an >>>>>>>>>> interpretation. >>>>>>>> >>>>>>>>> There is a >>>>>>>>> "true on the basis of meaning expressed in language" >>>>>>>>> and I figured out how to make it computable over the >>>>>>>>> body of knowledge. >>>>>>>> >>>>>>>> Except that "true on the basis of meaning expressed in language" is >>>>>>>> nmt computable and does not cover all of the body of knowldge. >>>>>>> >>>>>>> When the basis of "true" is proof theoretic semantics >>>>>>> internal to the formal system relative to its own axioms >>>>>>> and not truth conditional in a separate model outside >>>>>>> of the system undecidability ceases to exist. >>>>>> >>>>>> No, it does not. It does not matter what you call it, a sentence >>>>>> that cannot be neither proven nor disproven is undecidable because >>>>>> that is what the word means. An example is Gödel's sentence in >>>>>> Peano arithmetics. >>>>>> >>>>> >>>>> When a truth predicate gets the input "What time is?" >>>>> this input is rejected as not truth-apt. >>>> >>>> >>>> That fine. >>>>> >>>>> When PA gets an expression that cannot be proven or >>>>> refuted using its own axioms then this expression is >>>>> not within its domain. >>>>> >>>> >>>> Then most of Natural Number mathematics is isn't in its domain, >>>> >>> >>> It is what it is. >> >> But PA was CREATED to allow us to define the Natural Numbers in an >> axiomatic way. >> > > Yet only within the actual axioms of PA. Yes, the Natural Numbers are object created within the formal system of Peano Arithmetic (as one way to define them) and in that system there are a lot of properties of them that are True (or False). If there is a property of them that PA Created that it can't talk about, that sounds very much like PA is just incomplete in its understanding of what it does, just by the basic normal definition of incomplete. > >>> PA doesn't even know PA until you add a truth predicate. >>> When you do add a truth predicate then PA knows PA. If >>> you want more than that then meta-math can know "about" PA. >>> This is one level of indirect reference away from knowing PA. >> >> In other words, you world is just inconsistant because it can't handle >> itself. >> >> You just build your logic on equivocations and lies. >> >> But since PA doesn't have a truth predicate, you can't add it. >> >> What PA has, if you actually understand it, is that it was built on a >> definition of logic that defines truth based on what flows out of the >> possible infinite application of its axioms. >> >> When you try to build with a lessor logic, you don't get a PA that can >> do what it needs to, and thus isn't actually an arithmatic. >> >>> >>>> And, you can't KNOW if somehting is a valid question to ask until >>>> you know the answer. >>>> >>>> This makes a fairly worthless domain to learn things in. >>>> >>>> By your definition, a question like can every even number, greater >>>> than 2, be the sum of two prime numbers MIGHT not be within its >>>> domain, even though it is purely a question about the capability of >>>> numbers. >>>> >>> >>> >> > >
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2026-01-25 14:09 -0600 |
| Message-ID | <10l5t9e$1ui63$2@dont-email.me> |
| In reply to | #344543 |
On 1/25/2026 1:57 PM, Richard Damon wrote: > On 1/25/26 2:10 PM, olcott wrote: >> On 1/25/2026 12:40 PM, Richard Damon wrote: >>> On 1/25/26 1:33 PM, olcott wrote: >>>> On 1/25/2026 12:27 PM, Richard Damon wrote: >>>>> On 1/25/26 8:24 AM, olcott wrote: >>>>>> On 1/25/2026 5:19 AM, Mikko wrote: >>>>>>> On 24/01/2026 16:01, olcott wrote: >>>>>>>> On 1/24/2026 2:20 AM, Mikko wrote: >>>>>>>>> On 23/01/2026 12:22, olcott wrote: >>>>>>>>>> On 1/23/2026 3:13 AM, Mikko wrote: >>>>>>>>>>> On 22/01/2026 18:40, olcott wrote: >>>>>>>>>>>> On 1/22/2026 2:21 AM, Mikko wrote: >>>>>>>>>>>>> On 21/01/2026 17:22, olcott wrote: >>>>>>>>>>>>>> On 1/21/2026 3:03 AM, Mikko wrote: >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> No, it hasn't. In the way theories are usually discussed >>>>>>>>>>>>>>> nothing is >>>>>>>>>>>>>>> "ture in arithmetic". Every sentence of a first order >>>>>>>>>>>>>>> theory that >>>>>>>>>>>>>>> can be proven in the theory is true in every model >>>>>>>>>>>>>>> theory. Every >>>>>>>>>>>>>>> sentence of a theory that cannot be proven in the theory >>>>>>>>>>>>>>> is false >>>>>>>>>>>>>>> in some model of the theory. >>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> only because back then proof theoretic semantics did >>>>>>>>>>>>>>>> not exist. >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> Every interpretation of the theory is a definition of >>>>>>>>>>>>>>> semantics. >>>>>>>>>>>>>>> >>>>>>>>>>>>>> >>>>>>>>>>>>>> Meta‑math relations about numbers don’t exist in PA >>>>>>>>>>>>>> because PA only contains arithmetical relations—addition, >>>>>>>>>>>>>> multiplication, ordering, primitive‑recursive predicates >>>>>>>>>>>>>> about numbers themselves—while relations that talk about >>>>>>>>>>>>>> PA’s own proofs, syntax, or truth conditions live entirely >>>>>>>>>>>>>> in the meta‑theory; >>>>>>>>>>>>> >>>>>>>>>>>>> Methamathematics does not need any other relations between >>>>>>>>>>>>> numbers >>>>>>>>>>>>> than what PA has. But relations that map other things to >>>>>>>>>>>>> numbers >>>>>>>>>>>>> can be useful for methamathematical purposes. >>>>>>>>>>>>> >>>>>>>>>>>>>> so when someone appeals to a Gödel‑style relation like >>>>>>>>>>>>>> “n encodes a proof of this very sentence,” they’re >>>>>>>>>>>>>> invoking a meta‑mathematical predicate that PA cannot >>>>>>>>>>>>>> internalize, which is exactly why your framework draws >>>>>>>>>>>>>> a clean boundary between internal proof‑theoretic truth >>>>>>>>>>>>>> and external model‑theoretic truth. >>>>>>>>>>>>> >>>>>>>>>>>>> Anyway, what can be provven that way is true aboout PA. You >>>>>>>>>>>>> can deny >>>>>>>>>>>>> the proof but you cannot perform what is meta-provably >>>>>>>>>>>>> impossible. >>>>>>>>>>>> >>>>>>>>>>>> Gödel’s sentence is not “true in arithmetic.” >>>>>>>>>>>> It is true only in the meta‑theory, under an >>>>>>>>>>>> external interpretation of PA (typically the >>>>>>>>>>>> standard model ℕ). Inside PA itself, the sentence >>>>>>>>>>>> is not a truth‑bearer at all. >>>>>>>>>>> >>>>>>>>>>> There is no concept of "truth-bearer" in an uninterpreted >>>>>>>>>>> theory because >>>>>>>>>>> there is not concept of "truth". The relevant concept is >>>>>>>>>>> "sell- formed- >>>>>>>>>>> formula" and Gödels sentence is one. It may be true or false >>>>>>>>>>> in an >>>>>>>>>>> interpretation. >>>>>>>>> >>>>>>>>>> There is a >>>>>>>>>> "true on the basis of meaning expressed in language" >>>>>>>>>> and I figured out how to make it computable over the >>>>>>>>>> body of knowledge. >>>>>>>>> >>>>>>>>> Except that "true on the basis of meaning expressed in >>>>>>>>> language" is >>>>>>>>> nmt computable and does not cover all of the body of knowldge. >>>>>>>> >>>>>>>> When the basis of "true" is proof theoretic semantics >>>>>>>> internal to the formal system relative to its own axioms >>>>>>>> and not truth conditional in a separate model outside >>>>>>>> of the system undecidability ceases to exist. >>>>>>> >>>>>>> No, it does not. It does not matter what you call it, a sentence >>>>>>> that cannot be neither proven nor disproven is undecidable because >>>>>>> that is what the word means. An example is Gödel's sentence in >>>>>>> Peano arithmetics. >>>>>>> >>>>>> >>>>>> When a truth predicate gets the input "What time is?" >>>>>> this input is rejected as not truth-apt. >>>>> >>>>> >>>>> That fine. >>>>>> >>>>>> When PA gets an expression that cannot be proven or >>>>>> refuted using its own axioms then this expression is >>>>>> not within its domain. >>>>>> >>>>> >>>>> Then most of Natural Number mathematics is isn't in its domain, >>>>> >>>> >>>> It is what it is. >>> >>> But PA was CREATED to allow us to define the Natural Numbers in an >>> axiomatic way. >>> >> >> Yet only within the actual axioms of PA. > > Yes, the Natural Numbers are object created within the formal system of > Peano Arithmetic (as one way to define them) and in that system there > are a lot of properties of them that are True (or False). > > If there is a property of them that PA Created that it can't talk about, > that sounds very much like PA is just incomplete in its understanding of > what it does, just by the basic normal definition of incomplete. > > Gödel’s sentence is not “true in arithmetic.” It is true only in the meta‑theory, under an external interpretation of PA (typically the standard model ℕ). Inside PA itself, the sentence is not a truth‑bearer at all. -- Copyright 2026 Olcott<br><br> My 28 year goal has been to make <br> "true on the basis of meaning expressed in language"<br> reliably computable for the entire body of knowledge.<br><br> This required establishing a new foundation<br>
[toc] | [prev] | [next] | [standalone]
Page 5 of 11 — ← Prev page 1 … 3 4 [5] 6 7 … 11 Next page →
Back to top | Article view | sci.logic
csiph-web