Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > sci.logic > #333908 > unrolled thread
| Started by | olcott <polcott333@gmail.com> |
|---|---|
| First post | 2024-05-10 21:36 -0500 |
| Last post | 2024-05-14 10:26 -0500 |
| Articles | 20 on this page of 209 — 5 participants |
Back to article view | Back to sci.logic
True on the basis of meaning olcott <polcott333@gmail.com> - 2024-05-10 21:36 -0500
Re: True on the basis of meaning Richard Damon <richard@damon-family.org> - 2024-05-10 23:16 -0400
Re: True on the basis of meaning olcott <polcott333@gmail.com> - 2024-05-10 22:35 -0500
Re: True on the basis of meaning Richard Damon <richard@damon-family.org> - 2024-05-10 23:49 -0400
Re: True on the basis of meaning olcott <polcott333@gmail.com> - 2024-05-10 23:27 -0500
Re: True on the basis of meaning Richard Damon <richard@damon-family.org> - 2024-05-11 11:36 -0400
Re: True on the basis of meaning Mikko <mikko.levanto@iki.fi> - 2024-05-12 10:42 +0300
Re: True on the basis of meaning olcott <polcott333@gmail.com> - 2024-05-12 09:22 -0500
Re: True on the basis of meaning Mikko <mikko.levanto@iki.fi> - 2024-05-12 18:33 +0300
Re: True on the basis of meaning olcott <polcott333@gmail.com> - 2024-05-12 12:19 -0500
Re: True on the basis of meaning Richard Damon <richard@damon-family.org> - 2024-05-12 13:52 -0400
Re: True on the basis of meaning olcott <polcott333@gmail.com> - 2024-05-12 13:06 -0500
Re: True on the basis of meaning Richard Damon <richard@damon-family.org> - 2024-05-12 14:22 -0400
Re: True on the basis of meaning olcott <polcott333@gmail.com> - 2024-05-12 13:36 -0500
Re: True on the basis of meaning Richard Damon <richard@damon-family.org> - 2024-05-12 16:33 -0400
Re: True on the basis of meaning olcott <polcott333@gmail.com> - 2024-05-12 16:54 -0500
Re: True on the basis of meaning Richard Damon <richard@damon-family.org> - 2024-05-12 18:40 -0400
Re: True on the basis of meaning olcott <polcott333@gmail.com> - 2024-05-12 17:56 -0500
Re: True on the basis of meaning Richard Damon <richard@damon-family.org> - 2024-05-12 19:02 -0400
Re: True on the basis of meaning olcott <polcott333@gmail.com> - 2024-05-12 18:22 -0500
Re: True on the basis of meaning olcott <polcott333@gmail.com> - 2024-05-12 18:53 -0500
Re: True on the basis of meaning Richard Damon <richard@damon-family.org> - 2024-05-12 20:06 -0400
Re: True on the basis of meaning Richard Damon <richard@damon-family.org> - 2024-05-12 19:55 -0400
Re: True on the basis of meaning olcott <polcott333@gmail.com> - 2024-05-12 19:07 -0500
Re: True on the basis of meaning Richard Damon <richard@damon-family.org> - 2024-05-12 20:35 -0400
Re: True on the basis of meaning olcott <polcott333@gmail.com> - 2024-05-12 22:41 -0500
Re: True on the basis of meaning Richard Damon <richard@damon-family.org> - 2024-05-13 07:18 -0400
Re: True on the basis of meaning --- Good job Richard ! olcott <polcott333@gmail.com> - 2024-05-13 10:04 -0500
Re: True on the basis of meaning --- Good job Richard ! Richard Damon <richard@damon-family.org> - 2024-05-13 20:29 -0400
Re: True on the basis of meaning --- Good job Richard ! olcott <polcott333@gmail.com> - 2024-05-13 19:48 -0500
Re: True on the basis of meaning --- Good job Richard ! Richard Damon <richard@damon-family.org> - 2024-05-13 21:52 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-13 21:03 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-13 22:31 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-13 21:49 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-13 23:16 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-13 22:36 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-14 07:31 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-14 08:53 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-14 22:16 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-14 21:59 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-14 23:44 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-14 23:11 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-15 07:16 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-15 08:48 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-15 20:26 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-15 19:36 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-15 20:52 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method immibis <news@immibis.com> - 2024-05-16 05:38 +0200
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-15 22:58 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-15 20:20 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-15 21:39 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-15 20:57 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-15 22:07 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-15 21:17 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-15 22:33 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-15 21:42 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-15 23:17 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-15 22:33 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-16 07:29 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-16 08:37 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-16 22:29 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-16 21:38 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-15 23:44 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-16 07:32 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-16 08:59 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-16 22:29 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-16 21:44 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-16 22:54 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-16 22:20 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-16 23:29 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-16 22:51 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-17 07:41 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-17 09:32 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-17 21:07 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-17 20:22 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-17 21:33 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-17 21:19 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-17 22:40 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-17 22:35 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-18 08:43 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-18 09:15 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-18 10:32 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-18 11:48 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-18 12:56 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-18 12:26 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-18 13:38 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-18 14:35 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-18 15:54 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-18 14:46 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-18 15:57 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-18 15:00 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-18 18:22 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-18 17:47 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-18 19:04 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-18 22:47 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-19 07:55 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-19 08:41 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Mikko <mikko.levanto@iki.fi> - 2024-05-19 17:03 +0300
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-19 09:15 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Mikko <mikko.levanto@iki.fi> - 2024-05-20 10:55 +0300
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-20 12:48 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Mikko <mikko.levanto@iki.fi> - 2024-05-21 11:05 +0300
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) olcott <polcott333@gmail.com> - 2024-05-21 09:36 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) Mikko <mikko.levanto@iki.fi> - 2024-05-22 19:58 +0300
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) olcott <polcott333@gmail.com> - 2024-05-22 14:52 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) Richard Damon <richard@damon-family.org> - 2024-05-22 19:01 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) olcott <polcott333@gmail.com> - 2024-05-22 18:55 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) Richard Damon <richard@damon-family.org> - 2024-05-22 21:03 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) olcott <polcott333@gmail.com> - 2024-05-22 20:36 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) Richard Damon <richard@damon-family.org> - 2024-05-22 22:31 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) olcott <polcott333@gmail.com> - 2024-05-22 22:45 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) Richard Damon <richard@damon-family.org> - 2024-05-23 07:29 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) olcott <polcott333@gmail.com> - 2024-05-23 08:46 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) Richard Damon <richard@damon-family.org> - 2024-05-23 21:44 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) olcott <polcott333@gmail.com> - 2024-05-23 08:32 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) Mikko <mikko.levanto@iki.fi> - 2024-05-24 11:18 +0300
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) olcott <polcott333@gmail.com> - 2024-05-24 14:16 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) Mikko <mikko.levanto@iki.fi> - 2024-05-25 11:01 +0300
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) olcott <polcott333@gmail.com> - 2024-05-25 13:13 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) Mikko <mikko.levanto@iki.fi> - 2024-05-26 11:38 +0300
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) olcott <polcott333@gmail.com> - 2024-05-26 08:52 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) Mikko <mikko.levanto@iki.fi> - 2024-05-27 11:00 +0300
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) olcott <polcott333@gmail.com> - 2024-05-27 09:15 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) Mikko <mikko.levanto@iki.fi> - 2024-05-27 17:19 +0300
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT olcott <polcott333@gmail.com> - 2024-05-27 09:34 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT Mikko <mikko.levanto@iki.fi> - 2024-05-28 09:59 +0300
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT olcott <polcott333@gmail.com> - 2024-05-28 09:59 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT Richard Damon <richard@damon-family.org> - 2024-05-28 22:04 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT olcott <polcott333@gmail.com> - 2024-05-28 21:39 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT Richard Damon <richard@damon-family.org> - 2024-05-28 23:38 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT olcott <polcott333@gmail.com> - 2024-05-28 22:54 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT Richard Damon <richard@damon-family.org> - 2024-05-29 07:31 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT olcott <polcott333@gmail.com> - 2024-05-29 09:00 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT Richard Damon <richard@damon-family.org> - 2024-05-29 19:47 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT Python <python@invalid.org> - 2024-05-29 09:01 +0200
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT olcott <polcott333@gmail.com> - 2024-05-29 08:11 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT Richard Damon <richard@damon-family.org> - 2024-05-29 19:47 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT Mikko <mikko.levanto@iki.fi> - 2024-05-29 11:25 +0300
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT olcott <polcott333@gmail.com> - 2024-05-29 08:31 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT Mikko <mikko.levanto@iki.fi> - 2024-05-30 09:52 +0300
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT olcott <polcott333@gmail.com> - 2024-05-30 08:43 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT Mikko <mikko.levanto@iki.fi> - 2024-05-31 10:17 +0300
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT olcott <polcott333@gmail.com> - 2024-05-31 10:47 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT Mikko <mikko.levanto@iki.fi> - 2024-06-01 10:32 +0300
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT olcott <polcott333@gmail.com> - 2024-06-01 10:41 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT Mikko <mikko.levanto@iki.fi> - 2024-06-02 10:29 +0300
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT olcott <polcott333@gmail.com> - 2024-06-02 08:01 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT Mikko <mikko.levanto@iki.fi> - 2024-06-03 10:19 +0300
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT olcott <polcott333@gmail.com> - 2024-06-03 07:56 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT Mikko <mikko.levanto@iki.fi> - 2024-06-03 17:14 +0300
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) Mikko <mikko.levanto@iki.fi> - 2024-05-23 11:09 +0300
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) olcott <polcott333@gmail.com> - 2024-05-22 20:07 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) olcott <polcott333@gmail.com> - 2024-05-23 08:27 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) Mikko <mikko.levanto@iki.fi> - 2024-05-24 12:15 +0300
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) Mikko <mikko.levanto@iki.fi> - 2024-05-23 11:05 +0300
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) olcott <polcott333@gmail.com> - 2024-05-23 08:23 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) Mikko <mikko.levanto@iki.fi> - 2024-05-24 12:25 +0300
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) Mikko <mikko.levanto@iki.fi> - 2024-05-23 10:54 +0300
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) Mikko <mikko.levanto@iki.fi> - 2024-05-22 10:57 +0300
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) olcott <polcott333@gmail.com> - 2024-05-22 10:55 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-19 13:17 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-19 15:12 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-19 19:30 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-20 13:59 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-20 20:57 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-20 20:54 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-20 22:24 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-20 21:56 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-20 23:37 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-21 00:52 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-21 07:50 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-21 10:00 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method immibis <news@immibis.com> - 2024-05-21 18:08 +0200
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-21 21:46 -0400
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method immibis <news@immibis.com> - 2024-05-20 13:29 +0200
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method olcott <polcott333@gmail.com> - 2024-05-17 00:28 -0500
Re: True on the basis of meaning --- Good job Richard ! ---Socratic method Richard Damon <richard@damon-family.org> - 2024-05-17 07:41 -0400
Re: True on the basis of meaning Mikko <mikko.levanto@iki.fi> - 2024-05-13 12:23 +0300
Re: True on the basis of meaning olcott <polcott333@gmail.com> - 2024-05-13 09:48 -0500
Re: True on the basis of meaning Richard Damon <richard@damon-family.org> - 2024-05-13 20:29 -0400
Re: True on the basis of meaning Mikko <mikko.levanto@iki.fi> - 2024-05-14 12:08 +0300
Re: True on the basis of meaning olcott <polcott333@gmail.com> - 2024-05-14 09:42 -0500
Re: True on the basis of meaning Richard Damon <richard@damon-family.org> - 2024-05-14 22:16 -0400
Re: True on the basis of meaning Mikko <mikko.levanto@iki.fi> - 2024-05-15 11:39 +0300
Re: True on the basis of meaning olcott <polcott333@gmail.com> - 2024-05-15 09:27 -0500
Re: True on the basis of meaning Richard Damon <richard@damon-family.org> - 2024-05-15 20:25 -0400
Re: True on the basis of meaning Mikko <mikko.levanto@iki.fi> - 2024-05-16 11:44 +0300
Re: True on the basis of meaning olcott <polcott333@gmail.com> - 2024-05-16 10:05 -0500
Re: True on the basis of meaning Mikko <mikko.levanto@iki.fi> - 2024-05-17 18:49 +0300
Re: True on the basis of meaning olcott <polcott333@gmail.com> - 2024-05-17 12:23 -0500
Re: True on the basis of meaning Richard Damon <richard@damon-family.org> - 2024-05-17 21:07 -0400
Re: True on the basis of meaning Mikko <mikko.levanto@iki.fi> - 2024-05-18 12:21 +0300
Re: True on the basis of meaning Richard Damon <richard@damon-family.org> - 2024-05-14 22:24 -0400
Re: True on the basis of meaning --- Tarski olcott <polcott333@gmail.com> - 2024-05-13 09:34 -0500
Re: True on the basis of meaning --- Tarski Mikko <mikko.levanto@iki.fi> - 2024-05-14 12:16 +0300
Re: True on the basis of meaning --- Tarski olcott <polcott333@gmail.com> - 2024-05-14 10:18 -0500
Re: True on the basis of meaning --- Tarski Richard Damon <richard@damon-family.org> - 2024-05-14 22:16 -0400
Re: True on the basis of meaning --- Tarski Mikko <mikko.levanto@iki.fi> - 2024-05-15 11:43 +0300
Re: True on the basis of meaning --- Tarski olcott <polcott333@gmail.com> - 2024-05-15 09:31 -0500
Re: True on the basis of meaning --- Tarski Richard Damon <richard@damon-family.org> - 2024-05-15 20:26 -0400
Re: True on the basis of meaning --- Tarski Mikko <mikko.levanto@iki.fi> - 2024-05-16 11:59 +0300
Re: True on the basis of meaning --- Tarski olcott <polcott333@gmail.com> - 2024-05-16 11:00 -0500
Re: True on the basis of meaning --- Tarski Mikko <mikko.levanto@iki.fi> - 2024-05-17 18:56 +0300
Re: True on the basis of meaning --- Tarski olcott <polcott333@gmail.com> - 2024-05-17 12:28 -0500
Re: True on the basis of meaning --- Tarski Richard Damon <richard@damon-family.org> - 2024-05-17 21:07 -0400
Re: True on the basis of meaning --- Tarski Mikko <mikko.levanto@iki.fi> - 2024-05-18 10:46 +0300
Re: True on the basis of meaning --- Tarski olcott <polcott333@gmail.com> - 2024-05-18 11:59 -0500
Re: True on the basis of meaning --- Tarski Mikko <mikko.levanto@iki.fi> - 2024-05-14 13:09 +0300
Re: True on the basis of meaning --- Tarski olcott <polcott333@gmail.com> - 2024-05-14 10:26 -0500
Page 7 of 11 — ← Prev page 1 … 5 6 [7] 8 9 … 11 Next page →
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2024-05-26 08:52 -0500 |
| Subject | Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) |
| Message-ID | <v2veqj$3e8pb$1@dont-email.me> |
| In reply to | #334571 |
On 5/26/2024 3:38 AM, Mikko wrote: > On 2024-05-25 18:13:02 +0000, olcott said: > >> On 5/25/2024 3:01 AM, Mikko wrote: >>> On 2024-05-24 19:16:47 +0000, olcott said: >>> >>>> On 5/24/2024 3:18 AM, Mikko wrote: >>>>> On 2024-05-23 13:32:51 +0000, olcott said: >>>>> >>>>>> On 5/23/2024 3:09 AM, Mikko wrote: >>>>>>> On 2024-05-23 01:03:44 +0000, Richard Damon said: >>>>>>> >>>>>>>> On 5/22/24 7:55 PM, olcott wrote: >>>>>>>>> On 5/22/2024 6:01 PM, Richard Damon wrote: >>>>>>>>>> On 5/22/24 3:52 PM, olcott wrote: >>>>>>>>>>> On 5/22/2024 11:58 AM, Mikko wrote: >>>>>>>>>>>> On 2024-05-22 15:55:39 +0000, olcott said: >>>>>>>>>>>> >>>>>>>>>>>>> On 5/22/2024 2:57 AM, Mikko wrote: >>>>>>>>>>>>>> On 2024-05-21 14:36:29 +0000, olcott said: >>>>>>>>>>>>>> >>>>>>>>>>>>>>> On 5/21/2024 3:05 AM, Mikko wrote: >>>>>>>>>>>>>>>> On 2024-05-20 17:48:40 +0000, olcott said: >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>> On 5/20/2024 2:55 AM, Mikko wrote: >>>>>>>>>>>>>>>>>> On 2024-05-19 14:15:51 +0000, olcott said: >>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>> On 5/19/2024 9:03 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>> On 2024-05-19 13:41:56 +0000, olcott said: >>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>> On 5/19/2024 6:55 AM, Richard Damon wrote: >>>>>>>>>>>>>>>>>>>>>> On 5/18/24 11:47 PM, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>> On 5/18/2024 6:04 PM, Richard Damon wrote: >>>>>>>>>>>>>>>>>>>>>>>> On 5/18/24 6:47 PM, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/2024 5:22 PM, Richard Damon wrote: >>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/24 4:00 PM, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/2024 2:57 PM, Richard Damon wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/24 3:46 PM, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/2024 12:38 PM, Richard Damon wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/24 1:26 PM, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/2024 11:56 AM, Richard Damon wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/24 12:48 PM, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/2024 9:32 AM, Richard Damon wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/24 10:15 AM, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/2024 7:43 AM, Richard Damon >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> No, your system contradicts itself. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> You have never shown this. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> The most you have shown is a lack of >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> understanding of the >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> Truth Teller Paradox. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> No, I have, but you don't understand >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> the proof, it seems because you don't >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> know what a "Truth Predicate" has been >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> defined to be. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> My True(L,x) predicate is defined to >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> return true or false for every >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> finite string x on the basis of the >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> existence of a sequence of truth >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> preserving operations that derive x from >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> And thus, When True(L, p) established a >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> sequence of truth preserving operations >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> eminationg from ~True(L, p) by returning >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> false, it contradicts itself. The >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> problem is that True, in making an >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> answer of false, has asserted that such >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> a sequence exists. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/13/2024 9:31 PM, Richard Damon wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> > On 5/13/24 10:03 PM, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >> On 5/13/2024 7:29 PM, Richard Damon >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>> Remember, p defined as ~True(L, p) ... >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >> Can a sequence of true preserving >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> operations applied >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >> to expressions that are stipulated to >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> be true derive p? >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> > No, so True(L, p) is false >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >> Can a sequence of true preserving >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> operations applied >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >> to expressions that are stipulated to >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> be true derive ~p? >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> > >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> > No, so False(L, p) is false, >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> > >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> *To help you concentrate I repeated this* >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> The Liar Paradox and your formalized Liar >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> Paradox both >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> contradict themselves that is why they >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> must be screened >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> out as type mismatch error >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> non-truth-bearers *BEFORE THAT OCCURS* >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> And the Truth Predicate isn't allowed to >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> "filter" out expressions. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>> YOU ALREADY KNOW THAT IT DOESN'T >>>>>>>>>>>>>>>>>>>>>>>>>>>>> WE HAVE BEEN OVER THIS AGAIN AND AGAIN >>>>>>>>>>>>>>>>>>>>>>>>>>>>> THE FORMAL SYSTEM USES THE TRUE AND FALSE >>>>>>>>>>>>>>>>>>>>>>>>>>>>> PREDICATE >>>>>>>>>>>>>>>>>>>>>>>>>>>>> TO FILTER OUT TYPE MISMATCH ERROR >>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>> The first thing that the formal system does >>>>>>>>>>>>>>>>>>>>>>>>>>>>> with any >>>>>>>>>>>>>>>>>>>>>>>>>>>>> arbitrary finite string input is see if it >>>>>>>>>>>>>>>>>>>>>>>>>>>>> is a Truth-bearer: >>>>>>>>>>>>>>>>>>>>>>>>>>>>> Truthbearer(L,x) ≡ (True(L,x) ∨ True(L,~x)) >>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>> No, we can ask True(L, x) for any expression >>>>>>>>>>>>>>>>>>>>>>>>>>>> x and get an answer. >>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>> The system is designed so you can ask this, >>>>>>>>>>>>>>>>>>>>>>>>>>> yet non-truth-bearers >>>>>>>>>>>>>>>>>>>>>>>>>>> are rejected before True(L, x) is allowed to >>>>>>>>>>>>>>>>>>>>>>>>>>> be called. >>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>> Not allowed. >>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>> My True(L,x) predicate is defined to return >>>>>>>>>>>>>>>>>>>>>>>>> true or false for every >>>>>>>>>>>>>>>>>>>>>>>>> finite string x on the basis of the existence >>>>>>>>>>>>>>>>>>>>>>>>> of a sequence of truth >>>>>>>>>>>>>>>>>>>>>>>>> preserving operations that derive x from >>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>> A set of finite string semantic meanings that >>>>>>>>>>>>>>>>>>>>>>>>> form an accurate >>>>>>>>>>>>>>>>>>>>>>>>> verbal model of the general knowledge of the >>>>>>>>>>>>>>>>>>>>>>>>> actual world that >>>>>>>>>>>>>>>>>>>>>>>>> form a finite set of finite strings that are >>>>>>>>>>>>>>>>>>>>>>>>> stipulated to have >>>>>>>>>>>>>>>>>>>>>>>>> the semantic value of Boolean true. >>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>> *This is computable* Truthbearer(L,x) ≡ >>>>>>>>>>>>>>>>>>>>>>>>> (True(L,x) ∨ True(L,~x)) >>>>>>>>>>>>>>>>>>>>>>>>> *This is computable* Truthbearer(L,x) ≡ >>>>>>>>>>>>>>>>>>>>>>>>> (True(L,x) ∨ True(L,~x)) >>>>>>>>>>>>>>>>>>>>>>>>> *This is computable* Truthbearer(L,x) ≡ >>>>>>>>>>>>>>>>>>>>>>>>> (True(L,x) ∨ True(L,~x)) >>>>>>>>>>>>>>>>>>>>>>>>> *This is computable* Truthbearer(L,x) ≡ >>>>>>>>>>>>>>>>>>>>>>>>> (True(L,x) ∨ True(L,~x)) >>>>>>>>>>>>>>>>>>>>>>>>> *This is computable* Truthbearer(L,x) ≡ >>>>>>>>>>>>>>>>>>>>>>>>> (True(L,x) ∨ True(L,~x)) >>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>> So, for a statement x to be false, it says that >>>>>>>>>>>>>>>>>>>>>>>> there must be a sequence of truth perserving >>>>>>>>>>>>>>>>>>>>>>>> operations that derive ~x from, right? >>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>> Yes we must build from mutual agreement, good. >>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>> So do you still say that for p defined in L as >>>>>>>>>>>>>>>>>>>>>>>> ~True(L, p) that your definition will say that >>>>>>>>>>>>>>>>>>>>>>>> True(L, p) will return false? >>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>> It is the perfectly isomorphic to this: >>>>>>>>>>>>>>>>>>>>>>> True(English, "This sentence is not true") >>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>> Nope, Because "This sentece is not true" can be a >>>>>>>>>>>>>>>>>>>>>> non-truth-bearer, but by its definition, True(L, >>>>>>>>>>>>>>>>>>>>>> x) can not. >>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>> True(L,x) is always a truth bearer. >>>>>>>>>>>>>>>>>>>>> when x is defined as True(L,x) then x is not a >>>>>>>>>>>>>>>>>>>>> truth bearer. >>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>> When x is defined as True(L,x) then x is what >>>>>>>>>>>>>>>>>>>> True(L,x) is, >>>>>>>>>>>>>>>>>>>> in this case a truth bearer. >>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>> This is known as the Truth Teller Paradox >>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>> Doesn't matter. But ir you say that "x is not a truth >>>>>>>>>>>>>>>>>> bearer" then, >>>>>>>>>>>>>>>>>> by a truth preserving transformation, you imply that >>>>>>>>>>>>>>>>>> True(L,x) is >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>> True(English, "a cat is an animal) is true >>>>>>>>>>>>>>>>> LP := ~True(L, LP) expands to >>>>>>>>>>>>>>>>> ~True(~True(~True(~True(...)))) >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> No, it doesn't. It is a syntax error to have the same >>>>>>>>>>>>>>>> symbol on >>>>>>>>>>>>>>>> both sides ":=" so the expansion is not justified. >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> ϕ(x) there is a sentence ψ such that S ⊢ ψ ↔ ϕ⟨ψ⟩. >>>>>>>>>>>>>>> *The sentence ψ is of course not self-referential in a >>>>>>>>>>>>>>> strict sense*, >>>>>>>>>>>>>>> but mathematically it behaves like one. >>>>>>>>>>>>>>> https://plato.stanford.edu/entries/self-reference/#ConSemPar >>>>>>>>>>>>>> >>>>>>>>>>>>>> Your quote omitted important details. One is that the >>>>>>>>>>>>>> claim is not >>>>>>>>>>>>>> true about every theory but is about first order >>>>>>>>>>>>>> arithmetic and its >>>>>>>>>>>>>> extension. Another one is that ϕ(x) is that the claim is >>>>>>>>>>>>>> about >>>>>>>>>>>>>> every formula ϕ(x). >>>>>>>>>>>>>> >>>>>>>>>>>>> >>>>>>>>>>>>> *The whole article is about self-reference* >>>>>>>>>>>>> The ONLY detail that I am referring to is that it is >>>>>>>>>>>>> conventional to formalize self-reference incorrectly. >>>>>>>>>>>>> >>>>>>>>>>>>> *Richard and both fixed that* >>>>>>>>>>>>> >>>>>>>>>>>>> On 5/13/2024 9:31 PM, Richard Damon wrote: >>>>>>>>>>>>> > On 5/13/24 10:03 PM, olcott wrote: >>>>>>>>>>>>> >> On 5/13/2024 7:29 PM, Richard Damon wrote: >>>>>>>>>>>>> >>> >>>>>>>>>>>>> >>> Remember, p defined as ~True(L, p) ... >>>>>>>>>>>>> >>>>>>>>>>>>> x := y means x is defined to be another name for y >>>>>>>>>>>> >>>>>>>>>>>> Another name for the meaning of y. Therefore any pair of >>>>>>>>>>>> sentences that >>>>>>>>>>>> are otherwise equal but one contains x where rhe other >>>>>>>>>>>> contains y is a pair >>>>>>>>>>>> of equally true sentences. For example, if p defined as >>>>>>>>>>>> ~True(L, ⟨p⟩) >>>>>>>>>>> >>>>>>>>>>> I have no idea what you mean by the weird ⟨p⟩ quotes. >>>>>>>>>>> I AM ABSOLUTELY NOT TALKING ABOUT ANY FREAKING Gödel NUMBERS >>>>>>>>>>> I AM ABSOLUTELY NOT TALKING ABOUT ANY FREAKING Gödel NUMBERS >>>>>>>>>>> I AM ABSOLUTELY NOT TALKING ABOUT ANY FREAKING Gödel NUMBERS >>>>>>>>>>> >>>>>>>>>>> I AM TALKING ABOUT THE EXISTENCE OR NON-EXISTENCE OF >>>>>>>>>>> AN ACTUAL SEQUENCE OF TRUTH PRESERVING OPERATIONS FROM >>>>>>>>>>> EXPRESSIONS OF LANGUAGE KNOWN TO BE TRUE >>>>>>>>>> >>>>>>>>>> So, you aren't talking about Tarski's proof of the >>>>>>>>>> impossibility to define a Truth Predicate per his definition? >>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>>> then Truthbearer(L,p) has the same truth value as >>>>>>>>>>>> Truthbearer(L,~True(L, ⟨p⟩)). >>>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> When p defined as ~True(L, p) >>>>>>>>>>> Then ~True(L, p) is true, thus a truth-bearer. >>>>>>>>>> >>>>>>>>>> Which means that True(L, p) is false, so your True just erred >>>>>>>>>> in describing a true statement as false. >>>>>>>>>> >>>>>>>>>> Remeber, you just said that ~True(L, p) which has been given >>>>>>>>>> the name of p IS a truth-bearer. >>>>>>>>>> >>>>>>>>> >>>>>>>>> *You are just not paying close enough attention again* >>>>>>>>> >>>>>>>>> When p defined as ~True(L, p) >>>>>>>>> True(L,p) is false >>>>>>>>> True(L,~p) is false >>>>>>>>> ~True(L,~p) is true >>>>>>>>> >>>>>>>>> x := y means x is defined to be another name for y >>>>>>>>> https://en.wikipedia.org/wiki/List_of_logic_symbols >>>>>>>> >>>>>>>> Right, so since p is DEFINED to be ~True(L, p), which since >>>>>>>> True(L, p) is false, must be true, that means that you are >>>>>>>> claiming that >>>>>>>> T(L, <a statement that has been shown to be true>) is false. >>>>>>>> >>>>>>>> Thus your True predicat is just broken. >>>>>>>> >>>>>>>>> >>>>>>>>> You ignored the part where Mikko agreed that >>>>>>>>> p defined as ~True(L, p) >>>>>>>>> is a syntax error: >>>>>>>> >>>>>>>> So, what it the "Syntax Error"? >>>>>>>> >>>>>>>> Are we not allowed to negate an expression >>>>>>>> >>>>>>>> Or are we not allowed to assign an expression to a name. >>>>>>>> >>>>>>>> Note, "Syntax Error", by its definition doesn't look at Semantics, >>>>>>>> >>>>>>>>> >>>>>>>>> On 5/21/2024 3:05 AM, Mikko wrote: >>>>>>>>>> On 2024-05-20 17:48:40 +0000, olcott said: >>>>>>>>>>> True(English, "a cat is an animal) is true >>>>>>>>>>> LP := ~True(L, LP) expands to ~True(~True(~True(~True(...)))) >>>>>>>>>> >>>>>>>>>> No, it doesn't. It is a syntax error to have the same symbol on >>>>>>>>>> both sides ":=" so the expansion is not justified. >>>>>>>> >>>>>>>> But it isn't. >>>>>>> >>>>>>> By the usual rules a definition of a symbol in terms of itself is >>>>>>> not >>>>>>> an acceptable definition. >>>>>>> >>>>>> >>>>>> One can either reject it as a syntax error or let it go ahead >>>>>> and infinitely expand and reject it as a semantic error. >>>>> >>>>> It is a syntax error by the usual rules. If you want to use a >>>>> different >>>>> syntax then you should specify one, preferably using a different >>>>> symbol >>>>> instead of ":=". It is OK to extend the syntax but one should avoid >>>>> any >>>>> conflict with the usual conventions. Also, if you change the syntax >>>>> rules you should not call it a "definition". >>>>> >>>> >>>> LP := ~True(L, LP) is required to refer to itself on both sides >>>> that is what actual self-reference means. >>>> >>>> *THE ACTUAL Stanford ARTICLE ON SELF-REFERENCE SAYS* >>>> *THAT THEY MAKE SURE TO ENCODE IS INCORRECTLY* >>>> ϕ(x) there is a sentence ψ such that S ⊢ ψ ↔ ϕ⟨ψ⟩. >>>> *The sentence ψ is of course not self-referential in a strict sense*, >>>> but mathematically it behaves like one. >>>> https://plato.stanford.edu/entries/self-reference/#ConSemPar >>>> >>>> It is the standard convention throughout the literature to encode >>>> self-reference incorrectly. When the standard convention is to do >>>> these things incorrectly then the standard convention must be >>>> superseded and replaced. >>>> >>>> That is one of the reasons what correctly analyzing these this is >>>> so difficult. >>>> >>>> If you are correct that this is incorrect syntax >>>> LP := ~True(L, LP) >>>> that is yet another reason to reject the Liar Paradox >>>> (and every other self-reference paradox) as ill-formed. >>>> >>>>>> Or one can reject is as a self-contradictory epistemological antinomy >>>>>> having no truth value thus a type mismatch error for any formal >>>>>> system of bivalent logic. >>>>> >>>>> If that can be formulated as a syntax rule. Being an epistemological >>>>> antinomy is semantics as is being true or false but type mismach can >>>>> be handled as syntax error if the syntax rules have a type system. >>>>> >>>> >>>> The formalized Liar Paradox >>>> LP := ~True(L, LP) <is> an epistemological antinomy because assuming >>>> that it is true makes it false and assuming that it is false makes it >>>> true. >>>> >>>> That you want to also call it a syntax error seems reasonable to me. >>>> >>>> If it is not rejected as a syntax error then it does recursively >>>> expand ~True(~True(~True(~True(~True(...))))) as Clocksin & Mellish >>>> point out. >>>> >>>> BEGIN:(Clocksin & Mellish 2003:254) >>>> equal(X, X). >>>> ?- equal(foo(Y), Y). >>>> >>>> that is, they will allow you to match a term against an >>>> uninstantiated >>>> subterm of itself. In this example, foo(Y) is matched against Y, >>>> which >>>> appears within it. As a result, Y will stand for foo(Y), which is >>>> foo(foo(Y)) (because of what Y stands for), which is >>>> foo(foo(foo(Y))), >>>> and so on. So Y ends up standing for some kind of infinite >>>> structure. >>>> END:(Clocksin & Mellish 2003:254) >>>> >>>> >>>>>> Most of the greatest experts in the field are not even sure >>>>>> that there is anything wrong with it. >>>>> >>>>> Nothing is inherently wrong in an uninterpreted formal system. >>>>> Something may be unsuitable for some purpose but still useful >>>>> for another purpose. >>>>> >>>> >>>> You already said that this is a syntax error: >>>> LP := ~True(L, LP) >>>> please at least be consistent with yourself. >>> >>> I don't. Because of a syntax error "LP := ~True(L, LP)" is not an >>> expression in the formal system and not in contradiction that there >>> is nothing wrong in the formal system. >>> >> >> This is where Tarski says that his proof is anchored in the Liar Paradox >> https://liarparadox.org/Tarski_247_248.pdf > > Nothing to that page contradicts anything I have said above. > >> When you look at my new thread (and completely understand what it says) >> You will see when we correctly formalize Tarski's clumsy formalization >> of the Liar Paradox > > You don't formalize it correctly with a string that is not in the > language of the formnal system. A syntax error excludes all meaning > and in prticular the meaning that Tarksi's expressions have. > Back in 2019 I created a formal system for this purpose: https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF Initially it took any MTT expression and output the directed graph of the evaluation sequence of this expression. The current system only outputs the XML of the expression yet the directed graph can still be derived manually. It turns out the Prolog can also detect cycles in the directed graph of the evaluation sequence of an expression. The SWI-Prolog implementation of unify_with_occurs_check/2 is cycle-safe and only guards against creating cycles, not against cycles that may already be present in one of the arguments. https://www.swi-prolog.org/pldoc/man?predicate=unify_with_occurs_check/2 ?- LP = not(true(LP)). LP = not(true(LP)). ?- unify_with_occurs_check(LP, not(true(LP))). false. In other words Prolog has detected a cycle in the directed graph of the evaluation sequence of the structure of the Liar Paradox. Experts seem to think that Prolog is taking "not" and "true" as meaningless and is only evaluating the structure of the expression. -- Copyright 2024 Olcott "Talent hits a target no one else can hit; Genius hits a target no one else can see." Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | Mikko <mikko.levanto@iki.fi> |
|---|---|
| Date | 2024-05-27 11:00 +0300 |
| Subject | Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) |
| Message-ID | <v31eit$3ugn4$1@dont-email.me> |
| In reply to | #334577 |
On 2024-05-26 13:52:17 +0000, olcott said: > On 5/26/2024 3:38 AM, Mikko wrote: >> On 2024-05-25 18:13:02 +0000, olcott said: >> >>> On 5/25/2024 3:01 AM, Mikko wrote: >>>> On 2024-05-24 19:16:47 +0000, olcott said: >>>> >>>>> On 5/24/2024 3:18 AM, Mikko wrote: >>>>>> On 2024-05-23 13:32:51 +0000, olcott said: >>>>>> >>>>>>> On 5/23/2024 3:09 AM, Mikko wrote: >>>>>>>> On 2024-05-23 01:03:44 +0000, Richard Damon said: >>>>>>>> >>>>>>>>> On 5/22/24 7:55 PM, olcott wrote: >>>>>>>>>> On 5/22/2024 6:01 PM, Richard Damon wrote: >>>>>>>>>>> On 5/22/24 3:52 PM, olcott wrote: >>>>>>>>>>>> On 5/22/2024 11:58 AM, Mikko wrote: >>>>>>>>>>>>> On 2024-05-22 15:55:39 +0000, olcott said: >>>>>>>>>>>>> >>>>>>>>>>>>>> On 5/22/2024 2:57 AM, Mikko wrote: >>>>>>>>>>>>>>> On 2024-05-21 14:36:29 +0000, olcott said: >>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> On 5/21/2024 3:05 AM, Mikko wrote: >>>>>>>>>>>>>>>>> On 2024-05-20 17:48:40 +0000, olcott said: >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>> On 5/20/2024 2:55 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>> On 2024-05-19 14:15:51 +0000, olcott said: >>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>> On 5/19/2024 9:03 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>> On 2024-05-19 13:41:56 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>> On 5/19/2024 6:55 AM, Richard Damon wrote: >>>>>>>>>>>>>>>>>>>>>>> On 5/18/24 11:47 PM, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>>> On 5/18/2024 6:04 PM, Richard Damon wrote: >>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/24 6:47 PM, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/2024 5:22 PM, Richard Damon wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/24 4:00 PM, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/2024 2:57 PM, Richard Damon wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/24 3:46 PM, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/2024 12:38 PM, Richard Damon wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/24 1:26 PM, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/2024 11:56 AM, Richard Damon wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/24 12:48 PM, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/2024 9:32 AM, Richard Damon wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/24 10:15 AM, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/2024 7:43 AM, Richard Damon wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> No, your system contradicts itself. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> You have never shown this. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> The most you have shown is a lack of understanding of the >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> Truth Teller Paradox. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> No, I have, but you don't understand the proof, it seems because you >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> don't know what a "Truth Predicate" has been defined to be. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> My True(L,x) predicate is defined to return true or false for every >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> finite string x on the basis of the existence of a sequence of truth >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> preserving operations that derive x from >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> And thus, When True(L, p) established a sequence of truth preserving >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> operations eminationg from ~True(L, p) by returning false, it >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> contradicts itself. The problem is that True, in making an answer of >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> false, has asserted that such a sequence exists. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/13/2024 9:31 PM, Richard Damon wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> > On 5/13/24 10:03 PM, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >> On 5/13/2024 7:29 PM, Richard Damon wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>> Remember, p defined as ~True(L, p) ... >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >> Can a sequence of true preserving operations applied >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >> to expressions that are stipulated to be true derive p? >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> > No, so True(L, p) is false >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >> Can a sequence of true preserving operations applied >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >> to expressions that are stipulated to be true derive ~p? >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> > >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> > No, so False(L, p) is false, >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> > >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> *To help you concentrate I repeated this* >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> The Liar Paradox and your formalized Liar Paradox both >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> contradict themselves that is why they must be screened >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> out as type mismatch error non-truth-bearers *BEFORE THAT OCCURS* >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> And the Truth Predicate isn't allowed to "filter" out expressions. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> YOU ALREADY KNOW THAT IT DOESN'T >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> WE HAVE BEEN OVER THIS AGAIN AND AGAIN >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> THE FORMAL SYSTEM USES THE TRUE AND FALSE PREDICATE >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> TO FILTER OUT TYPE MISMATCH ERROR >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> The first thing that the formal system does with any >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> arbitrary finite string input is see if it is a Truth-bearer: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> Truthbearer(L,x) ≡ (True(L,x) ∨ True(L,~x)) >>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>> No, we can ask True(L, x) for any expression x and get an answer. >>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>> The system is designed so you can ask this, yet non-truth-bearers >>>>>>>>>>>>>>>>>>>>>>>>>>>> are rejected before True(L, x) is allowed to be called. >>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>> Not allowed. >>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>> My True(L,x) predicate is defined to return true or false for every >>>>>>>>>>>>>>>>>>>>>>>>>> finite string x on the basis of the existence of a sequence of truth >>>>>>>>>>>>>>>>>>>>>>>>>> preserving operations that derive x from >>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>> A set of finite string semantic meanings that form an accurate >>>>>>>>>>>>>>>>>>>>>>>>>> verbal model of the general knowledge of the actual world that >>>>>>>>>>>>>>>>>>>>>>>>>> form a finite set of finite strings that are stipulated to have >>>>>>>>>>>>>>>>>>>>>>>>>> the semantic value of Boolean true. >>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>> *This is computable* Truthbearer(L,x) ≡ (True(L,x) ∨ True(L,~x)) >>>>>>>>>>>>>>>>>>>>>>>>>> *This is computable* Truthbearer(L,x) ≡ (True(L,x) ∨ True(L,~x)) >>>>>>>>>>>>>>>>>>>>>>>>>> *This is computable* Truthbearer(L,x) ≡ (True(L,x) ∨ True(L,~x)) >>>>>>>>>>>>>>>>>>>>>>>>>> *This is computable* Truthbearer(L,x) ≡ (True(L,x) ∨ True(L,~x)) >>>>>>>>>>>>>>>>>>>>>>>>>> *This is computable* Truthbearer(L,x) ≡ (True(L,x) ∨ True(L,~x)) >>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>> So, for a statement x to be false, it says that there must be a >>>>>>>>>>>>>>>>>>>>>>>>> sequence of truth perserving operations that derive ~x from, right? >>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>> Yes we must build from mutual agreement, good. >>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>> So do you still say that for p defined in L as ~True(L, p) that your >>>>>>>>>>>>>>>>>>>>>>>>> definition will say that True(L, p) will return false? >>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>> It is the perfectly isomorphic to this: >>>>>>>>>>>>>>>>>>>>>>>> True(English, "This sentence is not true") >>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>> Nope, Because "This sentece is not true" can be a non-truth-bearer, but >>>>>>>>>>>>>>>>>>>>>>> by its definition, True(L, x) can not. >>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>> True(L,x) is always a truth bearer. >>>>>>>>>>>>>>>>>>>>>> when x is defined as True(L,x) then x is not a truth bearer. >>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>> When x is defined as True(L,x) then x is what True(L,x) is, >>>>>>>>>>>>>>>>>>>>> in this case a truth bearer. >>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>> This is known as the Truth Teller Paradox >>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>> Doesn't matter. But ir you say that "x is not a truth bearer" then, >>>>>>>>>>>>>>>>>>> by a truth preserving transformation, you imply that True(L,x) is >>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>> True(English, "a cat is an animal) is true >>>>>>>>>>>>>>>>>> LP := ~True(L, LP) expands to ~True(~True(~True(~True(...)))) >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>> No, it doesn't. It is a syntax error to have the same symbol on >>>>>>>>>>>>>>>>> both sides ":=" so the expansion is not justified. >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> ϕ(x) there is a sentence ψ such that S ⊢ ψ ↔ ϕ⟨ψ⟩. >>>>>>>>>>>>>>>> *The sentence ψ is of course not self-referential in a strict sense*, >>>>>>>>>>>>>>>> but mathematically it behaves like one. >>>>>>>>>>>>>>>> https://plato.stanford.edu/entries/self-reference/#ConSemPar >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> Your quote omitted important details. One is that the claim is not >>>>>>>>>>>>>>> true about every theory but is about first order arithmetic and its >>>>>>>>>>>>>>> extension. Another one is that ϕ(x) is that the claim is about >>>>>>>>>>>>>>> every formula ϕ(x). >>>>>>>>>>>>>>> >>>>>>>>>>>>>> >>>>>>>>>>>>>> *The whole article is about self-reference* >>>>>>>>>>>>>> The ONLY detail that I am referring to is that it is conventional to >>>>>>>>>>>>>> formalize self-reference incorrectly. >>>>>>>>>>>>>> >>>>>>>>>>>>>> *Richard and both fixed that* >>>>>>>>>>>>>> >>>>>>>>>>>>>> On 5/13/2024 9:31 PM, Richard Damon wrote: >>>>>>>>>>>>>> > On 5/13/24 10:03 PM, olcott wrote: >>>>>>>>>>>>>> >> On 5/13/2024 7:29 PM, Richard Damon wrote: >>>>>>>>>>>>>> >>> >>>>>>>>>>>>>> >>> Remember, p defined as ~True(L, p) ... >>>>>>>>>>>>>> >>>>>>>>>>>>>> x := y means x is defined to be another name for y >>>>>>>>>>>>> >>>>>>>>>>>>> Another name for the meaning of y. Therefore any pair of sentences that >>>>>>>>>>>>> are otherwise equal but one contains x where rhe other contains y is a pair >>>>>>>>>>>>> of equally true sentences. For example, if p defined as ~True(L, ⟨p⟩) >>>>>>>>>>>> >>>>>>>>>>>> I have no idea what you mean by the weird ⟨p⟩ quotes. >>>>>>>>>>>> I AM ABSOLUTELY NOT TALKING ABOUT ANY FREAKING Gödel NUMBERS >>>>>>>>>>>> I AM ABSOLUTELY NOT TALKING ABOUT ANY FREAKING Gödel NUMBERS >>>>>>>>>>>> I AM ABSOLUTELY NOT TALKING ABOUT ANY FREAKING Gödel NUMBERS >>>>>>>>>>>> >>>>>>>>>>>> I AM TALKING ABOUT THE EXISTENCE OR NON-EXISTENCE OF >>>>>>>>>>>> AN ACTUAL SEQUENCE OF TRUTH PRESERVING OPERATIONS FROM >>>>>>>>>>>> EXPRESSIONS OF LANGUAGE KNOWN TO BE TRUE >>>>>>>>>>> >>>>>>>>>>> So, you aren't talking about Tarski's proof of the impossibility to >>>>>>>>>>> define a Truth Predicate per his definition? >>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>>> then Truthbearer(L,p) has the same truth value as Truthbearer(L,~True(L, ⟨p⟩)). >>>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> When p defined as ~True(L, p) >>>>>>>>>>>> Then ~True(L, p) is true, thus a truth-bearer. >>>>>>>>>>> >>>>>>>>>>> Which means that True(L, p) is false, so your True just erred in >>>>>>>>>>> describing a true statement as false. >>>>>>>>>>> >>>>>>>>>>> Remeber, you just said that ~True(L, p) which has been given the name >>>>>>>>>>> of p IS a truth-bearer. >>>>>>>>>>> >>>>>>>>>> >>>>>>>>>> *You are just not paying close enough attention again* >>>>>>>>>> >>>>>>>>>> When p defined as ~True(L, p) >>>>>>>>>> True(L,p) is false >>>>>>>>>> True(L,~p) is false >>>>>>>>>> ~True(L,~p) is true >>>>>>>>>> >>>>>>>>>> x := y means x is defined to be another name for y >>>>>>>>>> https://en.wikipedia.org/wiki/List_of_logic_symbols >>>>>>>>> >>>>>>>>> Right, so since p is DEFINED to be ~True(L, p), which since True(L, p) >>>>>>>>> is false, must be true, that means that you are claiming that >>>>>>>>> T(L, <a statement that has been shown to be true>) is false. >>>>>>>>> >>>>>>>>> Thus your True predicat is just broken. >>>>>>>>> >>>>>>>>>> >>>>>>>>>> You ignored the part where Mikko agreed that >>>>>>>>>> p defined as ~True(L, p) >>>>>>>>>> is a syntax error: >>>>>>>>> >>>>>>>>> So, what it the "Syntax Error"? >>>>>>>>> >>>>>>>>> Are we not allowed to negate an expression >>>>>>>>> >>>>>>>>> Or are we not allowed to assign an expression to a name. >>>>>>>>> >>>>>>>>> Note, "Syntax Error", by its definition doesn't look at Semantics, >>>>>>>>> >>>>>>>>>> >>>>>>>>>> On 5/21/2024 3:05 AM, Mikko wrote: >>>>>>>>>>> On 2024-05-20 17:48:40 +0000, olcott said: >>>>>>>>>>>> True(English, "a cat is an animal) is true >>>>>>>>>>>> LP := ~True(L, LP) expands to ~True(~True(~True(~True(...)))) >>>>>>>>>>> >>>>>>>>>>> No, it doesn't. It is a syntax error to have the same symbol on >>>>>>>>>>> both sides ":=" so the expansion is not justified. >>>>>>>>> >>>>>>>>> But it isn't. >>>>>>>> >>>>>>>> By the usual rules a definition of a symbol in terms of itself is not >>>>>>>> an acceptable definition. >>>>>>>> >>>>>>> >>>>>>> One can either reject it as a syntax error or let it go ahead >>>>>>> and infinitely expand and reject it as a semantic error. >>>>>> >>>>>> It is a syntax error by the usual rules. If you want to use a different >>>>>> syntax then you should specify one, preferably using a different symbol >>>>>> instead of ":=". It is OK to extend the syntax but one should avoid any >>>>>> conflict with the usual conventions. Also, if you change the syntax >>>>>> rules you should not call it a "definition". >>>>>> >>>>> >>>>> LP := ~True(L, LP) is required to refer to itself on both sides >>>>> that is what actual self-reference means. >>>>> >>>>> *THE ACTUAL Stanford ARTICLE ON SELF-REFERENCE SAYS* >>>>> *THAT THEY MAKE SURE TO ENCODE IS INCORRECTLY* >>>>> ϕ(x) there is a sentence ψ such that S ⊢ ψ ↔ ϕ⟨ψ⟩. >>>>> *The sentence ψ is of course not self-referential in a strict sense*, >>>>> but mathematically it behaves like one. >>>>> https://plato.stanford.edu/entries/self-reference/#ConSemPar >>>>> >>>>> It is the standard convention throughout the literature to encode >>>>> self-reference incorrectly. When the standard convention is to do >>>>> these things incorrectly then the standard convention must be >>>>> superseded and replaced. >>>>> >>>>> That is one of the reasons what correctly analyzing these this is >>>>> so difficult. >>>>> >>>>> If you are correct that this is incorrect syntax >>>>> LP := ~True(L, LP) >>>>> that is yet another reason to reject the Liar Paradox >>>>> (and every other self-reference paradox) as ill-formed. >>>>> >>>>>>> Or one can reject is as a self-contradictory epistemological antinomy >>>>>>> having no truth value thus a type mismatch error for any formal >>>>>>> system of bivalent logic. >>>>>> >>>>>> If that can be formulated as a syntax rule. Being an epistemological >>>>>> antinomy is semantics as is being true or false but type mismach can >>>>>> be handled as syntax error if the syntax rules have a type system. >>>>>> >>>>> >>>>> The formalized Liar Paradox >>>>> LP := ~True(L, LP) <is> an epistemological antinomy because assuming >>>>> that it is true makes it false and assuming that it is false makes it >>>>> true. >>>>> >>>>> That you want to also call it a syntax error seems reasonable to me. >>>>> >>>>> If it is not rejected as a syntax error then it does recursively >>>>> expand ~True(~True(~True(~True(~True(...))))) as Clocksin & Mellish >>>>> point out. >>>>> >>>>> BEGIN:(Clocksin & Mellish 2003:254) >>>>> equal(X, X). >>>>> ?- equal(foo(Y), Y). >>>>> >>>>> that is, they will allow you to match a term against an uninstantiated >>>>> subterm of itself. In this example, foo(Y) is matched against Y, which >>>>> appears within it. As a result, Y will stand for foo(Y), which is >>>>> foo(foo(Y)) (because of what Y stands for), which is foo(foo(foo(Y))), >>>>> and so on. So Y ends up standing for some kind of infinite structure. >>>>> END:(Clocksin & Mellish 2003:254) >>>>> >>>>> >>>>>>> Most of the greatest experts in the field are not even sure >>>>>>> that there is anything wrong with it. >>>>>> >>>>>> Nothing is inherently wrong in an uninterpreted formal system. >>>>>> Something may be unsuitable for some purpose but still useful >>>>>> for another purpose. >>>>>> >>>>> >>>>> You already said that this is a syntax error: >>>>> LP := ~True(L, LP) >>>>> please at least be consistent with yourself. >>>> >>>> I don't. Because of a syntax error "LP := ~True(L, LP)" is not an >>>> expression in the formal system and not in contradiction that there >>>> is nothing wrong in the formal system. >>>> >>> >>> This is where Tarski says that his proof is anchored in the Liar Paradox >>> https://liarparadox.org/Tarski_247_248.pdf >> >> Nothing to that page contradicts anything I have said above. >> >>> When you look at my new thread (and completely understand what it says) >>> You will see when we correctly formalize Tarski's clumsy formalization >>> of the Liar Paradox >> >> You don't formalize it correctly with a string that is not in the >> language of the formnal system. A syntax error excludes all meaning >> and in prticular the meaning that Tarksi's expressions have. >> > > Back in 2019 I created a formal system for this purpose: > https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF > > Initially it took any MTT expression and output the directed graph > of the evaluation sequence of this expression. The current system > only outputs the XML of the expression yet the directed graph can > still be derived manually. Users of your MTT basically need two programs: one that checks whether the input is syntactiaclly correct and identifies at least one error if it is not, and one that checks whether a proof (that may but need not have unproven premises) is valid and identifies at least one error if it is not. -- Mikko
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2024-05-27 09:15 -0500 |
| Subject | Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) |
| Message-ID | <v324iu$2pkb$1@dont-email.me> |
| In reply to | #334610 |
On 5/27/2024 3:00 AM, Mikko wrote:
> On 2024-05-26 13:52:17 +0000, olcott said:
>
>> On 5/26/2024 3:38 AM, Mikko wrote:
>>> On 2024-05-25 18:13:02 +0000, olcott said:
>>>
>>>> On 5/25/2024 3:01 AM, Mikko wrote:
>>>>> On 2024-05-24 19:16:47 +0000, olcott said:
>>>>>
>>>>>> On 5/24/2024 3:18 AM, Mikko wrote:
>>>>>>> On 2024-05-23 13:32:51 +0000, olcott said:
>>>>>>>
>>>>>>>> On 5/23/2024 3:09 AM, Mikko wrote:
>>>>>>>>> On 2024-05-23 01:03:44 +0000, Richard Damon said:
>>>>>>>>>
>>>>>>>>>> On 5/22/24 7:55 PM, olcott wrote:
>>>>>>>>>>> On 5/22/2024 6:01 PM, Richard Damon wrote:
>>>>>>>>>>>> On 5/22/24 3:52 PM, olcott wrote:
>>>>>>>>>>>>> On 5/22/2024 11:58 AM, Mikko wrote:
>>>>>>>>>>>>>> On 2024-05-22 15:55:39 +0000, olcott said:
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> On 5/22/2024 2:57 AM, Mikko wrote:
>>>>>>>>>>>>>>>> On 2024-05-21 14:36:29 +0000, olcott said:
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> On 5/21/2024 3:05 AM, Mikko wrote:
>>>>>>>>>>>>>>>>>> On 2024-05-20 17:48:40 +0000, olcott said:
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> On 5/20/2024 2:55 AM, Mikko wrote:
>>>>>>>>>>>>>>>>>>>> On 2024-05-19 14:15:51 +0000, olcott said:
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> On 5/19/2024 9:03 AM, Mikko wrote:
>>>>>>>>>>>>>>>>>>>>>> On 2024-05-19 13:41:56 +0000, olcott said:
>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>> On 5/19/2024 6:55 AM, Richard Damon wrote:
>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/24 11:47 PM, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/2024 6:04 PM, Richard Damon wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/24 6:47 PM, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/2024 5:22 PM, Richard Damon wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/24 4:00 PM, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/2024 2:57 PM, Richard Damon wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/24 3:46 PM, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/2024 12:38 PM, Richard Damon wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/24 1:26 PM, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/2024 11:56 AM, Richard Damon
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/24 12:48 PM, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/2024 9:32 AM, Richard Damon
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/24 10:15 AM, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/2024 7:43 AM, Richard Damon
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> No, your system contradicts itself.
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> You have never shown this.
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> The most you have shown is a lack
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> of understanding of the
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> Truth Teller Paradox.
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> No, I have, but you don't understand
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> the proof, it seems because you
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> don't know what a "Truth Predicate"
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> has been defined to be.
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> My True(L,x) predicate is defined to
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> return true or false for every
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> finite string x on the basis of the
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> existence of a sequence of truth
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> preserving operations that derive x from
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> And thus, When True(L, p) established
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> a sequence of truth preserving
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> operations eminationg from ~True(L, p)
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> by returning false, it contradicts
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> itself. The problem is that True, in
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> making an answer of false, has
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> asserted that such a sequence exists.
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/13/2024 9:31 PM, Richard Damon wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> > On 5/13/24 10:03 PM, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >> On 5/13/2024 7:29 PM, Richard Damon
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>> Remember, p defined as ~True(L, p)
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> ...
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >> Can a sequence of true preserving
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> operations applied
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >> to expressions that are stipulated
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> to be true derive p?
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> > No, so True(L, p) is false
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >> Can a sequence of true preserving
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> operations applied
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >> to expressions that are stipulated
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> to be true derive ~p?
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> > No, so False(L, p) is false,
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> *To help you concentrate I repeated this*
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> The Liar Paradox and your formalized
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> Liar Paradox both
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> contradict themselves that is why they
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> must be screened
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> out as type mismatch error
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> non-truth-bearers *BEFORE THAT OCCURS*
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> And the Truth Predicate isn't allowed to
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> "filter" out expressions.
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> YOU ALREADY KNOW THAT IT DOESN'T
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> WE HAVE BEEN OVER THIS AGAIN AND AGAIN
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> THE FORMAL SYSTEM USES THE TRUE AND FALSE
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> PREDICATE
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> TO FILTER OUT TYPE MISMATCH ERROR
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> The first thing that the formal system
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> does with any
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> arbitrary finite string input is see if
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> it is a Truth-bearer:
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> Truthbearer(L,x) ≡ (True(L,x) ∨ True(L,~x))
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> No, we can ask True(L, x) for any
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> expression x and get an answer.
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>> The system is designed so you can ask this,
>>>>>>>>>>>>>>>>>>>>>>>>>>>>> yet non-truth-bearers
>>>>>>>>>>>>>>>>>>>>>>>>>>>>> are rejected before True(L, x) is allowed
>>>>>>>>>>>>>>>>>>>>>>>>>>>>> to be called.
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>> Not allowed.
>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>> My True(L,x) predicate is defined to return
>>>>>>>>>>>>>>>>>>>>>>>>>>> true or false for every
>>>>>>>>>>>>>>>>>>>>>>>>>>> finite string x on the basis of the existence
>>>>>>>>>>>>>>>>>>>>>>>>>>> of a sequence of truth
>>>>>>>>>>>>>>>>>>>>>>>>>>> preserving operations that derive x from
>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>> A set of finite string semantic meanings that
>>>>>>>>>>>>>>>>>>>>>>>>>>> form an accurate
>>>>>>>>>>>>>>>>>>>>>>>>>>> verbal model of the general knowledge of the
>>>>>>>>>>>>>>>>>>>>>>>>>>> actual world that
>>>>>>>>>>>>>>>>>>>>>>>>>>> form a finite set of finite strings that are
>>>>>>>>>>>>>>>>>>>>>>>>>>> stipulated to have
>>>>>>>>>>>>>>>>>>>>>>>>>>> the semantic value of Boolean true.
>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>> *This is computable* Truthbearer(L,x) ≡
>>>>>>>>>>>>>>>>>>>>>>>>>>> (True(L,x) ∨ True(L,~x))
>>>>>>>>>>>>>>>>>>>>>>>>>>> *This is computable* Truthbearer(L,x) ≡
>>>>>>>>>>>>>>>>>>>>>>>>>>> (True(L,x) ∨ True(L,~x))
>>>>>>>>>>>>>>>>>>>>>>>>>>> *This is computable* Truthbearer(L,x) ≡
>>>>>>>>>>>>>>>>>>>>>>>>>>> (True(L,x) ∨ True(L,~x))
>>>>>>>>>>>>>>>>>>>>>>>>>>> *This is computable* Truthbearer(L,x) ≡
>>>>>>>>>>>>>>>>>>>>>>>>>>> (True(L,x) ∨ True(L,~x))
>>>>>>>>>>>>>>>>>>>>>>>>>>> *This is computable* Truthbearer(L,x) ≡
>>>>>>>>>>>>>>>>>>>>>>>>>>> (True(L,x) ∨ True(L,~x))
>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>> So, for a statement x to be false, it says
>>>>>>>>>>>>>>>>>>>>>>>>>> that there must be a sequence of truth
>>>>>>>>>>>>>>>>>>>>>>>>>> perserving operations that derive ~x from, right?
>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>> Yes we must build from mutual agreement, good.
>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>> So do you still say that for p defined in L as
>>>>>>>>>>>>>>>>>>>>>>>>>> ~True(L, p) that your definition will say that
>>>>>>>>>>>>>>>>>>>>>>>>>> True(L, p) will return false?
>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>> It is the perfectly isomorphic to this:
>>>>>>>>>>>>>>>>>>>>>>>>> True(English, "This sentence is not true")
>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>> Nope, Because "This sentece is not true" can be
>>>>>>>>>>>>>>>>>>>>>>>> a non-truth-bearer, but by its definition,
>>>>>>>>>>>>>>>>>>>>>>>> True(L, x) can not.
>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>> True(L,x) is always a truth bearer.
>>>>>>>>>>>>>>>>>>>>>>> when x is defined as True(L,x) then x is not a
>>>>>>>>>>>>>>>>>>>>>>> truth bearer.
>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>> When x is defined as True(L,x) then x is what
>>>>>>>>>>>>>>>>>>>>>> True(L,x) is,
>>>>>>>>>>>>>>>>>>>>>> in this case a truth bearer.
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> This is known as the Truth Teller Paradox
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> Doesn't matter. But ir you say that "x is not a
>>>>>>>>>>>>>>>>>>>> truth bearer" then,
>>>>>>>>>>>>>>>>>>>> by a truth preserving transformation, you imply that
>>>>>>>>>>>>>>>>>>>> True(L,x) is
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> True(English, "a cat is an animal) is true
>>>>>>>>>>>>>>>>>>> LP := ~True(L, LP) expands to
>>>>>>>>>>>>>>>>>>> ~True(~True(~True(~True(...))))
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> No, it doesn't. It is a syntax error to have the same
>>>>>>>>>>>>>>>>>> symbol on
>>>>>>>>>>>>>>>>>> both sides ":=" so the expansion is not justified.
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> ϕ(x) there is a sentence ψ such that S ⊢ ψ ↔ ϕ⟨ψ⟩.
>>>>>>>>>>>>>>>>> *The sentence ψ is of course not self-referential in a
>>>>>>>>>>>>>>>>> strict sense*,
>>>>>>>>>>>>>>>>> but mathematically it behaves like one.
>>>>>>>>>>>>>>>>> https://plato.stanford.edu/entries/self-reference/#ConSemPar
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> Your quote omitted important details. One is that the
>>>>>>>>>>>>>>>> claim is not
>>>>>>>>>>>>>>>> true about every theory but is about first order
>>>>>>>>>>>>>>>> arithmetic and its
>>>>>>>>>>>>>>>> extension. Another one is that ϕ(x) is that the claim is
>>>>>>>>>>>>>>>> about
>>>>>>>>>>>>>>>> every formula ϕ(x).
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> *The whole article is about self-reference*
>>>>>>>>>>>>>>> The ONLY detail that I am referring to is that it is
>>>>>>>>>>>>>>> conventional to formalize self-reference incorrectly.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> *Richard and both fixed that*
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> On 5/13/2024 9:31 PM, Richard Damon wrote:
>>>>>>>>>>>>>>> > On 5/13/24 10:03 PM, olcott wrote:
>>>>>>>>>>>>>>> >> On 5/13/2024 7:29 PM, Richard Damon wrote:
>>>>>>>>>>>>>>> >>>
>>>>>>>>>>>>>>> >>> Remember, p defined as ~True(L, p) ...
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> x := y means x is defined to be another name for y
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> Another name for the meaning of y. Therefore any pair of
>>>>>>>>>>>>>> sentences that
>>>>>>>>>>>>>> are otherwise equal but one contains x where rhe other
>>>>>>>>>>>>>> contains y is a pair
>>>>>>>>>>>>>> of equally true sentences. For example, if p defined as
>>>>>>>>>>>>>> ~True(L, ⟨p⟩)
>>>>>>>>>>>>>
>>>>>>>>>>>>> I have no idea what you mean by the weird ⟨p⟩ quotes.
>>>>>>>>>>>>> I AM ABSOLUTELY NOT TALKING ABOUT ANY FREAKING Gödel NUMBERS
>>>>>>>>>>>>> I AM ABSOLUTELY NOT TALKING ABOUT ANY FREAKING Gödel NUMBERS
>>>>>>>>>>>>> I AM ABSOLUTELY NOT TALKING ABOUT ANY FREAKING Gödel NUMBERS
>>>>>>>>>>>>>
>>>>>>>>>>>>> I AM TALKING ABOUT THE EXISTENCE OR NON-EXISTENCE OF
>>>>>>>>>>>>> AN ACTUAL SEQUENCE OF TRUTH PRESERVING OPERATIONS FROM
>>>>>>>>>>>>> EXPRESSIONS OF LANGUAGE KNOWN TO BE TRUE
>>>>>>>>>>>>
>>>>>>>>>>>> So, you aren't talking about Tarski's proof of the
>>>>>>>>>>>> impossibility to define a Truth Predicate per his definition?
>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>> then Truthbearer(L,p) has the same truth value as
>>>>>>>>>>>>>> Truthbearer(L,~True(L, ⟨p⟩)).
>>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>> When p defined as ~True(L, p)
>>>>>>>>>>>>> Then ~True(L, p) is true, thus a truth-bearer.
>>>>>>>>>>>>
>>>>>>>>>>>> Which means that True(L, p) is false, so your True just
>>>>>>>>>>>> erred in describing a true statement as false.
>>>>>>>>>>>>
>>>>>>>>>>>> Remeber, you just said that ~True(L, p) which has been given
>>>>>>>>>>>> the name of p IS a truth-bearer.
>>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>> *You are just not paying close enough attention again*
>>>>>>>>>>>
>>>>>>>>>>> When p defined as ~True(L, p)
>>>>>>>>>>> True(L,p) is false
>>>>>>>>>>> True(L,~p) is false
>>>>>>>>>>> ~True(L,~p) is true
>>>>>>>>>>>
>>>>>>>>>>> x := y means x is defined to be another name for y
>>>>>>>>>>> https://en.wikipedia.org/wiki/List_of_logic_symbols
>>>>>>>>>>
>>>>>>>>>> Right, so since p is DEFINED to be ~True(L, p), which since
>>>>>>>>>> True(L, p) is false, must be true, that means that you are
>>>>>>>>>> claiming that
>>>>>>>>>> T(L, <a statement that has been shown to be true>) is false.
>>>>>>>>>>
>>>>>>>>>> Thus your True predicat is just broken.
>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>> You ignored the part where Mikko agreed that
>>>>>>>>>>> p defined as ~True(L, p)
>>>>>>>>>>> is a syntax error:
>>>>>>>>>>
>>>>>>>>>> So, what it the "Syntax Error"?
>>>>>>>>>>
>>>>>>>>>> Are we not allowed to negate an expression
>>>>>>>>>>
>>>>>>>>>> Or are we not allowed to assign an expression to a name.
>>>>>>>>>>
>>>>>>>>>> Note, "Syntax Error", by its definition doesn't look at
>>>>>>>>>> Semantics,
>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>> On 5/21/2024 3:05 AM, Mikko wrote:
>>>>>>>>>>>> On 2024-05-20 17:48:40 +0000, olcott said:
>>>>>>>>>>>>> True(English, "a cat is an animal) is true
>>>>>>>>>>>>> LP := ~True(L, LP) expands to ~True(~True(~True(~True(...))))
>>>>>>>>>>>>
>>>>>>>>>>>> No, it doesn't. It is a syntax error to have the same symbol on
>>>>>>>>>>>> both sides ":=" so the expansion is not justified.
>>>>>>>>>>
>>>>>>>>>> But it isn't.
>>>>>>>>>
>>>>>>>>> By the usual rules a definition of a symbol in terms of itself
>>>>>>>>> is not
>>>>>>>>> an acceptable definition.
>>>>>>>>>
>>>>>>>>
>>>>>>>> One can either reject it as a syntax error or let it go ahead
>>>>>>>> and infinitely expand and reject it as a semantic error.
>>>>>>>
>>>>>>> It is a syntax error by the usual rules. If you want to use a
>>>>>>> different
>>>>>>> syntax then you should specify one, preferably using a different
>>>>>>> symbol
>>>>>>> instead of ":=". It is OK to extend the syntax but one should
>>>>>>> avoid any
>>>>>>> conflict with the usual conventions. Also, if you change the syntax
>>>>>>> rules you should not call it a "definition".
>>>>>>>
>>>>>>
>>>>>> LP := ~True(L, LP) is required to refer to itself on both sides
>>>>>> that is what actual self-reference means.
>>>>>>
>>>>>> *THE ACTUAL Stanford ARTICLE ON SELF-REFERENCE SAYS*
>>>>>> *THAT THEY MAKE SURE TO ENCODE IS INCORRECTLY*
>>>>>> ϕ(x) there is a sentence ψ such that S ⊢ ψ ↔ ϕ⟨ψ⟩.
>>>>>> *The sentence ψ is of course not self-referential in a strict sense*,
>>>>>> but mathematically it behaves like one.
>>>>>> https://plato.stanford.edu/entries/self-reference/#ConSemPar
>>>>>>
>>>>>> It is the standard convention throughout the literature to encode
>>>>>> self-reference incorrectly. When the standard convention is to do
>>>>>> these things incorrectly then the standard convention must be
>>>>>> superseded and replaced.
>>>>>>
>>>>>> That is one of the reasons what correctly analyzing these this is
>>>>>> so difficult.
>>>>>>
>>>>>> If you are correct that this is incorrect syntax
>>>>>> LP := ~True(L, LP)
>>>>>> that is yet another reason to reject the Liar Paradox
>>>>>> (and every other self-reference paradox) as ill-formed.
>>>>>>
>>>>>>>> Or one can reject is as a self-contradictory epistemological
>>>>>>>> antinomy
>>>>>>>> having no truth value thus a type mismatch error for any formal
>>>>>>>> system of bivalent logic.
>>>>>>>
>>>>>>> If that can be formulated as a syntax rule. Being an epistemological
>>>>>>> antinomy is semantics as is being true or false but type mismach can
>>>>>>> be handled as syntax error if the syntax rules have a type system.
>>>>>>>
>>>>>>
>>>>>> The formalized Liar Paradox
>>>>>> LP := ~True(L, LP) <is> an epistemological antinomy because assuming
>>>>>> that it is true makes it false and assuming that it is false makes it
>>>>>> true.
>>>>>>
>>>>>> That you want to also call it a syntax error seems reasonable to me.
>>>>>>
>>>>>> If it is not rejected as a syntax error then it does recursively
>>>>>> expand ~True(~True(~True(~True(~True(...))))) as Clocksin & Mellish
>>>>>> point out.
>>>>>>
>>>>>> BEGIN:(Clocksin & Mellish 2003:254)
>>>>>> equal(X, X).
>>>>>> ?- equal(foo(Y), Y).
>>>>>>
>>>>>> that is, they will allow you to match a term against an
>>>>>> uninstantiated
>>>>>> subterm of itself. In this example, foo(Y) is matched against
>>>>>> Y, which
>>>>>> appears within it. As a result, Y will stand for foo(Y), which is
>>>>>> foo(foo(Y)) (because of what Y stands for), which is
>>>>>> foo(foo(foo(Y))),
>>>>>> and so on. So Y ends up standing for some kind of infinite
>>>>>> structure.
>>>>>> END:(Clocksin & Mellish 2003:254)
>>>>>>
>>>>>>
>>>>>>>> Most of the greatest experts in the field are not even sure
>>>>>>>> that there is anything wrong with it.
>>>>>>>
>>>>>>> Nothing is inherently wrong in an uninterpreted formal system.
>>>>>>> Something may be unsuitable for some purpose but still useful
>>>>>>> for another purpose.
>>>>>>>
>>>>>>
>>>>>> You already said that this is a syntax error:
>>>>>> LP := ~True(L, LP)
>>>>>> please at least be consistent with yourself.
>>>>>
>>>>> I don't. Because of a syntax error "LP := ~True(L, LP)" is not an
>>>>> expression in the formal system and not in contradiction that there
>>>>> is nothing wrong in the formal system.
>>>>>
>>>>
>>>> This is where Tarski says that his proof is anchored in the Liar
>>>> Paradox
>>>> https://liarparadox.org/Tarski_247_248.pdf
>>>
>>> Nothing to that page contradicts anything I have said above.
>>>
>>>> When you look at my new thread (and completely understand what it says)
>>>> You will see when we correctly formalize Tarski's clumsy formalization
>>>> of the Liar Paradox
>>>
>>> You don't formalize it correctly with a string that is not in the
>>> language of the formnal system. A syntax error excludes all meaning
>>> and in prticular the meaning that Tarksi's expressions have.
>>>
>>
>> Back in 2019 I created a formal system for this purpose:
>> https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
>>
>> Initially it took any MTT expression and output the directed graph
>> of the evaluation sequence of this expression. The current system
>> only outputs the XML of the expression yet the directed graph can
>> still be derived manually.
>
> Users of your MTT basically need two programs: one that checks whether
> the input is syntactiaclly correct and identifies at least one error
> if it is not, and one that checks whether a proof (that may but need
> not have unproven premises) is valid and identifies at least one error
> if it is not.
>
MTT is build with YACC and LEX and outputs the XML of the
input expression.
LP := ~True(L, LP)
definition_2 token="ASSIGN_ALIAS"
| definition_2 token="IDENTIFIER" value="LP"
| sentence_2 token="NOT"
| | atomic_sentence_1 token="IDENTIFIER" value="True"
| | | term_list_1
| | | | term_2 token="IDENTIFIER" value="L"
| | | | term_2 token="IDENTIFIER" value="LP"
Directed graph of evaulation sequence of LP
Nodes on the left edges on the right
00 NOT 01
01 True 02, 00 // cycle
02 L
<definition_2 token="ASSIGN_ALIAS">
<definition_2 token="IDENTIFIER" value="LP"/>
<sentence_2 token="NOT">
<atomic_sentence_1 token="IDENTIFIER" value="True">
<term_list_1>
<term_2 token="IDENTIFIER" value="L"/>
<term_2 token="IDENTIFIER" value="LP"/>
</term_list_1>
</atomic_sentence_1>
</sentence_2>
</definition_2>
--
Copyright 2024 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | Mikko <mikko.levanto@iki.fi> |
|---|---|
| Date | 2024-05-27 17:19 +0300 |
| Subject | Re: True on the basis of meaning --- Good job Richard ! ---Socratic method (agreement) |
| Message-ID | <v324pa$2rt4$1@dont-email.me> |
| In reply to | #334614 |
On 2024-05-27 14:15:57 +0000, olcott said: > On 5/27/2024 3:00 AM, Mikko wrote: >> On 2024-05-26 13:52:17 +0000, olcott said: >> >>> On 5/26/2024 3:38 AM, Mikko wrote: >>>> On 2024-05-25 18:13:02 +0000, olcott said: >>>> >>>>> On 5/25/2024 3:01 AM, Mikko wrote: >>>>>> On 2024-05-24 19:16:47 +0000, olcott said: >>>>>> >>>>>>> On 5/24/2024 3:18 AM, Mikko wrote: >>>>>>>> On 2024-05-23 13:32:51 +0000, olcott said: >>>>>>>> >>>>>>>>> On 5/23/2024 3:09 AM, Mikko wrote: >>>>>>>>>> On 2024-05-23 01:03:44 +0000, Richard Damon said: >>>>>>>>>> >>>>>>>>>>> On 5/22/24 7:55 PM, olcott wrote: >>>>>>>>>>>> On 5/22/2024 6:01 PM, Richard Damon wrote: >>>>>>>>>>>>> On 5/22/24 3:52 PM, olcott wrote: >>>>>>>>>>>>>> On 5/22/2024 11:58 AM, Mikko wrote: >>>>>>>>>>>>>>> On 2024-05-22 15:55:39 +0000, olcott said: >>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> On 5/22/2024 2:57 AM, Mikko wrote: >>>>>>>>>>>>>>>>> On 2024-05-21 14:36:29 +0000, olcott said: >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>> On 5/21/2024 3:05 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>> On 2024-05-20 17:48:40 +0000, olcott said: >>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>> On 5/20/2024 2:55 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>> On 2024-05-19 14:15:51 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>> On 5/19/2024 9:03 AM, Mikko wrote: >>>>>>>>>>>>>>>>>>>>>>> On 2024-05-19 13:41:56 +0000, olcott said: >>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>> On 5/19/2024 6:55 AM, Richard Damon wrote: >>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/24 11:47 PM, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/2024 6:04 PM, Richard Damon wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/24 6:47 PM, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/2024 5:22 PM, Richard Damon wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/24 4:00 PM, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/2024 2:57 PM, Richard Damon wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/24 3:46 PM, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/2024 12:38 PM, Richard Damon wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/24 1:26 PM, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/2024 11:56 AM, Richard Damon wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/24 12:48 PM, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/2024 9:32 AM, Richard Damon wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/24 10:15 AM, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/18/2024 7:43 AM, Richard Damon wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> No, your system contradicts itself. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> You have never shown this. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> The most you have shown is a lack of understanding of the >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> Truth Teller Paradox. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> No, I have, but you don't understand the proof, it seems because you >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> don't know what a "Truth Predicate" has been defined to be. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> My True(L,x) predicate is defined to return true or false for every >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> finite string x on the basis of the existence of a sequence of truth >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> preserving operations that derive x from >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> And thus, When True(L, p) established a sequence of truth preserving >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> operations eminationg from ~True(L, p) by returning false, it >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> contradicts itself. The problem is that True, in making an answer of >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> false, has asserted that such a sequence exists. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 5/13/2024 9:31 PM, Richard Damon wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> > On 5/13/24 10:03 PM, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >> On 5/13/2024 7:29 PM, Richard Damon wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>> Remember, p defined as ~True(L, p) ... >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >> Can a sequence of true preserving operations applied >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >> to expressions that are stipulated to be true derive p? >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> > No, so True(L, p) is false >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >> Can a sequence of true preserving operations applied >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >> to expressions that are stipulated to be true derive ~p? >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> > >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> > No, so False(L, p) is false, >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> > >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> *To help you concentrate I repeated this* >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> The Liar Paradox and your formalized Liar Paradox both >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> contradict themselves that is why they must be screened >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> out as type mismatch error non-truth-bearers *BEFORE THAT OCCURS* >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> And the Truth Predicate isn't allowed to "filter" out expressions. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> YOU ALREADY KNOW THAT IT DOESN'T >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> WE HAVE BEEN OVER THIS AGAIN AND AGAIN >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> THE FORMAL SYSTEM USES THE TRUE AND FALSE PREDICATE >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> TO FILTER OUT TYPE MISMATCH ERROR >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> The first thing that the formal system does with any >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> arbitrary finite string input is see if it is a Truth-bearer: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> Truthbearer(L,x) ≡ (True(L,x) ∨ True(L,~x)) >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> No, we can ask True(L, x) for any expression x and get an answer. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> The system is designed so you can ask this, yet non-truth-bearers >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> are rejected before True(L, x) is allowed to be called. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>>> Not allowed. >>>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>> My True(L,x) predicate is defined to return true or false for every >>>>>>>>>>>>>>>>>>>>>>>>>>>> finite string x on the basis of the existence of a sequence of truth >>>>>>>>>>>>>>>>>>>>>>>>>>>> preserving operations that derive x from >>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>> A set of finite string semantic meanings that form an accurate >>>>>>>>>>>>>>>>>>>>>>>>>>>> verbal model of the general knowledge of the actual world that >>>>>>>>>>>>>>>>>>>>>>>>>>>> form a finite set of finite strings that are stipulated to have >>>>>>>>>>>>>>>>>>>>>>>>>>>> the semantic value of Boolean true. >>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>> *This is computable* Truthbearer(L,x) ≡ (True(L,x) ∨ True(L,~x)) >>>>>>>>>>>>>>>>>>>>>>>>>>>> *This is computable* Truthbearer(L,x) ≡ (True(L,x) ∨ True(L,~x)) >>>>>>>>>>>>>>>>>>>>>>>>>>>> *This is computable* Truthbearer(L,x) ≡ (True(L,x) ∨ True(L,~x)) >>>>>>>>>>>>>>>>>>>>>>>>>>>> *This is computable* Truthbearer(L,x) ≡ (True(L,x) ∨ True(L,~x)) >>>>>>>>>>>>>>>>>>>>>>>>>>>> *This is computable* Truthbearer(L,x) ≡ (True(L,x) ∨ True(L,~x)) >>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>> So, for a statement x to be false, it says that there must be a >>>>>>>>>>>>>>>>>>>>>>>>>>> sequence of truth perserving operations that derive ~x from, right? >>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>> Yes we must build from mutual agreement, good. >>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>>> So do you still say that for p defined in L as ~True(L, p) that your >>>>>>>>>>>>>>>>>>>>>>>>>>> definition will say that True(L, p) will return false? >>>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>>> It is the perfectly isomorphic to this: >>>>>>>>>>>>>>>>>>>>>>>>>> True(English, "This sentence is not true") >>>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>>> Nope, Because "This sentece is not true" can be a non-truth-bearer, but >>>>>>>>>>>>>>>>>>>>>>>>> by its definition, True(L, x) can not. >>>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>>> True(L,x) is always a truth bearer. >>>>>>>>>>>>>>>>>>>>>>>> when x is defined as True(L,x) then x is not a truth bearer. >>>>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>>> When x is defined as True(L,x) then x is what True(L,x) is, >>>>>>>>>>>>>>>>>>>>>>> in this case a truth bearer. >>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>> This is known as the Truth Teller Paradox >>>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>> Doesn't matter. But ir you say that "x is not a truth bearer" then, >>>>>>>>>>>>>>>>>>>>> by a truth preserving transformation, you imply that True(L,x) is >>>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>> True(English, "a cat is an animal) is true >>>>>>>>>>>>>>>>>>>> LP := ~True(L, LP) expands to ~True(~True(~True(~True(...)))) >>>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>> No, it doesn't. It is a syntax error to have the same symbol on >>>>>>>>>>>>>>>>>>> both sides ":=" so the expansion is not justified. >>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>> ϕ(x) there is a sentence ψ such that S ⊢ ψ ↔ ϕ⟨ψ⟩. >>>>>>>>>>>>>>>>>> *The sentence ψ is of course not self-referential in a strict sense*, >>>>>>>>>>>>>>>>>> but mathematically it behaves like one. >>>>>>>>>>>>>>>>>> https://plato.stanford.edu/entries/self-reference/#ConSemPar >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>> Your quote omitted important details. One is that the claim is not >>>>>>>>>>>>>>>>> true about every theory but is about first order arithmetic and its >>>>>>>>>>>>>>>>> extension. Another one is that ϕ(x) is that the claim is about >>>>>>>>>>>>>>>>> every formula ϕ(x). >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> *The whole article is about self-reference* >>>>>>>>>>>>>>>> The ONLY detail that I am referring to is that it is conventional to >>>>>>>>>>>>>>>> formalize self-reference incorrectly. >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> *Richard and both fixed that* >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> On 5/13/2024 9:31 PM, Richard Damon wrote: >>>>>>>>>>>>>>>> > On 5/13/24 10:03 PM, olcott wrote: >>>>>>>>>>>>>>>> >> On 5/13/2024 7:29 PM, Richard Damon wrote: >>>>>>>>>>>>>>>> >>> >>>>>>>>>>>>>>>> >>> Remember, p defined as ~True(L, p) ... >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> x := y means x is defined to be another name for y >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> Another name for the meaning of y. Therefore any pair of sentences that >>>>>>>>>>>>>>> are otherwise equal but one contains x where rhe other contains y is a pair >>>>>>>>>>>>>>> of equally true sentences. For example, if p defined as ~True(L, ⟨p⟩) >>>>>>>>>>>>>> >>>>>>>>>>>>>> I have no idea what you mean by the weird ⟨p⟩ quotes. >>>>>>>>>>>>>> I AM ABSOLUTELY NOT TALKING ABOUT ANY FREAKING Gödel NUMBERS >>>>>>>>>>>>>> I AM ABSOLUTELY NOT TALKING ABOUT ANY FREAKING Gödel NUMBERS >>>>>>>>>>>>>> I AM ABSOLUTELY NOT TALKING ABOUT ANY FREAKING Gödel NUMBERS >>>>>>>>>>>>>> >>>>>>>>>>>>>> I AM TALKING ABOUT THE EXISTENCE OR NON-EXISTENCE OF >>>>>>>>>>>>>> AN ACTUAL SEQUENCE OF TRUTH PRESERVING OPERATIONS FROM >>>>>>>>>>>>>> EXPRESSIONS OF LANGUAGE KNOWN TO BE TRUE >>>>>>>>>>>>> >>>>>>>>>>>>> So, you aren't talking about Tarski's proof of the impossibility to >>>>>>>>>>>>> define a Truth Predicate per his definition? >>>>>>>>>>>>> >>>>>>>>>>>>>> >>>>>>>>>>>>>>> then Truthbearer(L,p) has the same truth value as Truthbearer(L,~True(L, ⟨p⟩)). >>>>>>>>>>>>>>> >>>>>>>>>>>>>> >>>>>>>>>>>>>> When p defined as ~True(L, p) >>>>>>>>>>>>>> Then ~True(L, p) is true, thus a truth-bearer. >>>>>>>>>>>>> >>>>>>>>>>>>> Which means that True(L, p) is false, so your True just erred in >>>>>>>>>>>>> describing a true statement as false. >>>>>>>>>>>>> >>>>>>>>>>>>> Remeber, you just said that ~True(L, p) which has been given the name >>>>>>>>>>>>> of p IS a truth-bearer. >>>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> *You are just not paying close enough attention again* >>>>>>>>>>>> >>>>>>>>>>>> When p defined as ~True(L, p) >>>>>>>>>>>> True(L,p) is false >>>>>>>>>>>> True(L,~p) is false >>>>>>>>>>>> ~True(L,~p) is true >>>>>>>>>>>> >>>>>>>>>>>> x := y means x is defined to be another name for y >>>>>>>>>>>> https://en.wikipedia.org/wiki/List_of_logic_symbols >>>>>>>>>>> >>>>>>>>>>> Right, so since p is DEFINED to be ~True(L, p), which since True(L, p) >>>>>>>>>>> is false, must be true, that means that you are claiming that >>>>>>>>>>> T(L, <a statement that has been shown to be true>) is false. >>>>>>>>>>> >>>>>>>>>>> Thus your True predicat is just broken. >>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> You ignored the part where Mikko agreed that >>>>>>>>>>>> p defined as ~True(L, p) >>>>>>>>>>>> is a syntax error: >>>>>>>>>>> >>>>>>>>>>> So, what it the "Syntax Error"? >>>>>>>>>>> >>>>>>>>>>> Are we not allowed to negate an expression >>>>>>>>>>> >>>>>>>>>>> Or are we not allowed to assign an expression to a name. >>>>>>>>>>> >>>>>>>>>>> Note, "Syntax Error", by its definition doesn't look at Semantics, >>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> On 5/21/2024 3:05 AM, Mikko wrote: >>>>>>>>>>>>> On 2024-05-20 17:48:40 +0000, olcott said: >>>>>>>>>>>>>> True(English, "a cat is an animal) is true >>>>>>>>>>>>>> LP := ~True(L, LP) expands to ~True(~True(~True(~True(...)))) >>>>>>>>>>>>> >>>>>>>>>>>>> No, it doesn't. It is a syntax error to have the same symbol on >>>>>>>>>>>>> both sides ":=" so the expansion is not justified. >>>>>>>>>>> >>>>>>>>>>> But it isn't. >>>>>>>>>> >>>>>>>>>> By the usual rules a definition of a symbol in terms of itself is not >>>>>>>>>> an acceptable definition. >>>>>>>>>> >>>>>>>>> >>>>>>>>> One can either reject it as a syntax error or let it go ahead >>>>>>>>> and infinitely expand and reject it as a semantic error. >>>>>>>> >>>>>>>> It is a syntax error by the usual rules. If you want to use a different >>>>>>>> syntax then you should specify one, preferably using a different symbol >>>>>>>> instead of ":=". It is OK to extend the syntax but one should avoid any >>>>>>>> conflict with the usual conventions. Also, if you change the syntax >>>>>>>> rules you should not call it a "definition". >>>>>>>> >>>>>>> >>>>>>> LP := ~True(L, LP) is required to refer to itself on both sides >>>>>>> that is what actual self-reference means. >>>>>>> >>>>>>> *THE ACTUAL Stanford ARTICLE ON SELF-REFERENCE SAYS* >>>>>>> *THAT THEY MAKE SURE TO ENCODE IS INCORRECTLY* >>>>>>> ϕ(x) there is a sentence ψ such that S ⊢ ψ ↔ ϕ⟨ψ⟩. >>>>>>> *The sentence ψ is of course not self-referential in a strict sense*, >>>>>>> but mathematically it behaves like one. >>>>>>> https://plato.stanford.edu/entries/self-reference/#ConSemPar >>>>>>> >>>>>>> It is the standard convention throughout the literature to encode >>>>>>> self-reference incorrectly. When the standard convention is to do >>>>>>> these things incorrectly then the standard convention must be >>>>>>> superseded and replaced. >>>>>>> >>>>>>> That is one of the reasons what correctly analyzing these this is >>>>>>> so difficult. >>>>>>> >>>>>>> If you are correct that this is incorrect syntax >>>>>>> LP := ~True(L, LP) >>>>>>> that is yet another reason to reject the Liar Paradox >>>>>>> (and every other self-reference paradox) as ill-formed. >>>>>>> >>>>>>>>> Or one can reject is as a self-contradictory epistemological antinomy >>>>>>>>> having no truth value thus a type mismatch error for any formal >>>>>>>>> system of bivalent logic. >>>>>>>> >>>>>>>> If that can be formulated as a syntax rule. Being an epistemological >>>>>>>> antinomy is semantics as is being true or false but type mismach can >>>>>>>> be handled as syntax error if the syntax rules have a type system. >>>>>>>> >>>>>>> >>>>>>> The formalized Liar Paradox >>>>>>> LP := ~True(L, LP) <is> an epistemological antinomy because assuming >>>>>>> that it is true makes it false and assuming that it is false makes it >>>>>>> true. >>>>>>> >>>>>>> That you want to also call it a syntax error seems reasonable to me. >>>>>>> >>>>>>> If it is not rejected as a syntax error then it does recursively >>>>>>> expand ~True(~True(~True(~True(~True(...))))) as Clocksin & Mellish >>>>>>> point out. >>>>>>> >>>>>>> BEGIN:(Clocksin & Mellish 2003:254) >>>>>>> equal(X, X). >>>>>>> ?- equal(foo(Y), Y). >>>>>>> >>>>>>> that is, they will allow you to match a term against an uninstantiated >>>>>>> subterm of itself. In this example, foo(Y) is matched against Y, which >>>>>>> appears within it. As a result, Y will stand for foo(Y), which is >>>>>>> foo(foo(Y)) (because of what Y stands for), which is foo(foo(foo(Y))), >>>>>>> and so on. So Y ends up standing for some kind of infinite structure. >>>>>>> END:(Clocksin & Mellish 2003:254) >>>>>>> >>>>>>> >>>>>>>>> Most of the greatest experts in the field are not even sure >>>>>>>>> that there is anything wrong with it. >>>>>>>> >>>>>>>> Nothing is inherently wrong in an uninterpreted formal system. >>>>>>>> Something may be unsuitable for some purpose but still useful >>>>>>>> for another purpose. >>>>>>>> >>>>>>> >>>>>>> You already said that this is a syntax error: >>>>>>> LP := ~True(L, LP) >>>>>>> please at least be consistent with yourself. >>>>>> >>>>>> I don't. Because of a syntax error "LP := ~True(L, LP)" is not an >>>>>> expression in the formal system and not in contradiction that there >>>>>> is nothing wrong in the formal system. >>>>>> >>>>> >>>>> This is where Tarski says that his proof is anchored in the Liar Paradox >>>>> https://liarparadox.org/Tarski_247_248.pdf >>>> >>>> Nothing to that page contradicts anything I have said above. >>>> >>>>> When you look at my new thread (and completely understand what it says) >>>>> You will see when we correctly formalize Tarski's clumsy formalization >>>>> of the Liar Paradox >>>> >>>> You don't formalize it correctly with a string that is not in the >>>> language of the formnal system. A syntax error excludes all meaning >>>> and in prticular the meaning that Tarksi's expressions have. >>>> >>> >>> Back in 2019 I created a formal system for this purpose: >>> https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF >>> >>> Initially it took any MTT expression and output the directed graph >>> of the evaluation sequence of this expression. The current system >>> only outputs the XML of the expression yet the directed graph can >>> still be derived manually. >> >> Users of your MTT basically need two programs: one that checks whether >> the input is syntactiaclly correct and identifies at least one error >> if it is not, and one that checks whether a proof (that may but need >> not have unproven premises) is valid and identifies at least one error >> if it is not. >> > > MTT is build with YACC and LEX and outputs the XML of the > input expression. > > LP := ~True(L, LP) > > definition_2 token="ASSIGN_ALIAS" > | definition_2 token="IDENTIFIER" value="LP" > | sentence_2 token="NOT" > | | atomic_sentence_1 token="IDENTIFIER" value="True" > | | | term_list_1 > | | | | term_2 token="IDENTIFIER" value="L" > | | | | term_2 token="IDENTIFIER" value="LP" > > Directed graph of evaulation sequence of LP > Nodes on the left edges on the right > 00 NOT 01 > 01 True 02, 00 // cycle > 02 L > > <definition_2 token="ASSIGN_ALIAS"> > <definition_2 token="IDENTIFIER" value="LP"/> > <sentence_2 token="NOT"> > <atomic_sentence_1 token="IDENTIFIER" value="True"> > <term_list_1> > <term_2 token="IDENTIFIER" value="L"/> > <term_2 token="IDENTIFIER" value="LP"/> > </term_list_1> > </atomic_sentence_1> > </sentence_2> > </definition_2> That is not far from useful. Much of the code could be reused for the more useful programs mentioned above. -- Mikko
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2024-05-27 09:34 -0500 |
| Subject | Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT |
| Message-ID | <v325l6$2pkb$3@dont-email.me> |
| In reply to | #334615 |
On 5/27/2024 9:19 AM, Mikko wrote: > On 2024-05-27 14:15:57 +0000, olcott said: > >> On 5/27/2024 3:00 AM, Mikko wrote: <snip> >>> Users of your MTT basically need two programs: one that checks whether >>> the input is syntactiaclly correct and identifies at least one error >>> if it is not, and one that checks whether a proof (that may but need >>> not have unproven premises) is valid and identifies at least one error >>> if it is not. >>> >> >> MTT is build with YACC and LEX and outputs the XML of the >> input expression. >> >> LP := ~True(L, LP) >> >> definition_2 token="ASSIGN_ALIAS" >> | definition_2 token="IDENTIFIER" value="LP" >> | sentence_2 token="NOT" >> | | atomic_sentence_1 token="IDENTIFIER" value="True" >> | | | term_list_1 >> | | | | term_2 token="IDENTIFIER" value="L" >> | | | | term_2 token="IDENTIFIER" value="LP" >> >> Directed graph of evaulation sequence of LP >> Nodes on the left edges on the right >> 00 NOT 01 >> 01 True 02, 00 // cycle >> 02 L >> >> <definition_2 token="ASSIGN_ALIAS"> >> <definition_2 token="IDENTIFIER" value="LP"/> >> <sentence_2 token="NOT"> >> <atomic_sentence_1 token="IDENTIFIER" value="True"> >> <term_list_1> >> <term_2 token="IDENTIFIER" value="L"/> >> <term_2 token="IDENTIFIER" value="LP"/> >> </term_list_1> >> </atomic_sentence_1> >> </sentence_2> >> </definition_2> > > That is not far from useful. Much of the code could be reused for > the more useful programs mentioned above. > Minimal Type Theory (YACC BNF) https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF It correctly parses every MTT expression and translates it into XML. The directed graph shown above does the same thing as unify_with_occurs_check/2 in Prolog The SWI-Prolog implementation of unify_with_occurs_check/2 is cycle-safe and only guards against creating cycles, not against cycles that may already be present in one of the arguments. https://www.swi-prolog.org/pldoc/man?predicate=unify_with_occurs_check/2 ?- LP = not(true(LP)). LP = not(true(LP)). ?- unify_with_occurs_check(LP, not(true(LP))). false. In other words Prolog has detected a cycle in the directed graph of the evaluation sequence of the structure of the Liar Paradox. Experts seem to think that Prolog is taking "not" and "true" as meaningless and is only evaluating the structure of the expression. -- Copyright 2024 Olcott "Talent hits a target no one else can hit; Genius hits a target no one else can see." Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | Mikko <mikko.levanto@iki.fi> |
|---|---|
| Date | 2024-05-28 09:59 +0300 |
| Subject | Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT |
| Message-ID | <v33vc1$g5n4$1@dont-email.me> |
| In reply to | #334617 |
On 2024-05-27 14:34:14 +0000, olcott said: > ?- LP = not(true(LP)). > LP = not(true(LP)). > > ?- unify_with_occurs_check(LP, not(true(LP))). > false. > > In other words Prolog has detected a cycle in the directed graph of the > evaluation sequence of the structure of the Liar Paradox. Experts seem > to think that Prolog is taking "not" and "true" as meaningless and is > only evaluating the structure of the expression. The words "not" and "true" of Prolog are meaningful in some contexts but not above. The word "true" is meaningful only when it has no arguments. You could try ?- LP = not(true(LP), true(LP). or ?- LP = not(true(LP), not(true(LP)). The predicate unify_with_occurs_check checks whether the resulting sructure is acyclic because that is its purpose. Whether a simple unification like LP = not(true(LP)) does same is implementation dependent as Prolog rules permit but do not require that. In a typical implementation a simple unification does not check for cycles. Anyway, none of this is relevant to the topic of this thread or topics of sci.logic. -- Mikko
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2024-05-28 09:59 -0500 |
| Subject | Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT |
| Message-ID | <v34rgj$l2fc$1@dont-email.me> |
| In reply to | #334653 |
On 5/28/2024 1:59 AM, Mikko wrote:
> On 2024-05-27 14:34:14 +0000, olcott said:
>
>> ?- LP = not(true(LP)).
>> LP = not(true(LP)).
>>
>> ?- unify_with_occurs_check(LP, not(true(LP))).
>> false.
>>
>> In other words Prolog has detected a cycle in the directed graph of the
>> evaluation sequence of the structure of the Liar Paradox. Experts seem
>> to think that Prolog is taking "not" and "true" as meaningless and is
>> only evaluating the structure of the expression.
>
> The words "not" and "true" of Prolog are meaningful in some contexts
> but not above. The word "true" is meaningful only when it has no arguments.
>
That Prolog construes any expression having the same structure as the
Liar Paradox as having a cycle in the directed graph of its evaluation
sequence already completely proves my point. In other words Prolog
is saying that there is something wrong with the expression and it must
be rejected.
> You could try
> ?- LP = not(true(LP), true(LP).
>
> or
> ?- LP = not(true(LP), not(true(LP)).
>
> The predicate unify_with_occurs_check checks whether the resulting
> sructure is acyclic because that is its purpose. Whether a simple
Yes exactly. If I knew that Prolog did this then I would not have
created Minimal Type Theory that does this same thing. That I did
create MTT that does do this same thing makes my understanding much
deeper.
> unification like LP = not(true(LP)) does same is implementation
> dependent as Prolog rules permit but do not require that. In a
> typical implementation a simple unification does not check for
> cycles.
>
ISO Prolog implementations have the built-in predicate
unify_with_occurs_check/2 for sound unification
https://en.wikipedia.org/wiki/Occurs_check#Sound_unification
Alternatively such expressions crash or remain stuck in infinite loops.
> Anyway, none of this is relevant to the topic of this thread or
> topics of sci.logic.
>
...14 Every epistemological antinomy can likewise be used for
a similar undecidability proof...(Gödel 1931:40)
Gödel, Kurt 1931.
On Formally Undecidable Propositions of Principia Mathematica And
Related Systems
https://monoskop.org/images/9/93/Kurt_G%C3%B6del_On_Formally_Undecidable_Propositions_of_Principia_Mathematica_and_Related_Systems_1992.pdf
It would
then be possible to reconstruct the *antinomy of the liar* in the
metalanguage, by forming in the language itself a sentence x
such that the sentence of the metalanguage which is correlated
with x asserts that x is not a true sentence.
CONCEPT OF TRUTH IN FORMALIZED LANGUAGES, Tarski
https://liarparadox.org/Tarski_247_248.pdf
The Liar Paradox and other such {epistemological antinomies} must be
rejected as type mismatch errors for any system of bivalent logic thus
cannot be correctly used for any undecidability or undefinability proof.
--
Copyright 2024 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | Richard Damon <richard@damon-family.org> |
|---|---|
| Date | 2024-05-28 22:04 -0400 |
| Subject | Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT |
| Message-ID | <v362er$2d367$1@i2pn2.org> |
| In reply to | #334658 |
On 5/28/24 10:59 AM, olcott wrote:
> On 5/28/2024 1:59 AM, Mikko wrote:
>> On 2024-05-27 14:34:14 +0000, olcott said:
>>
>>> ?- LP = not(true(LP)).
>>> LP = not(true(LP)).
>>>
>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>> false.
>>>
>>> In other words Prolog has detected a cycle in the directed graph of the
>>> evaluation sequence of the structure of the Liar Paradox. Experts seem
>>> to think that Prolog is taking "not" and "true" as meaningless and is
>>> only evaluating the structure of the expression.
>>
>> The words "not" and "true" of Prolog are meaningful in some contexts
>> but not above. The word "true" is meaningful only when it has no
>> arguments.
>>
>
> That Prolog construes any expression having the same structure as the
> Liar Paradox as having a cycle in the directed graph of its evaluation
> sequence already completely proves my point. In other words Prolog
> is saying that there is something wrong with the expression and it must
> be rejected.
But Prolog doesn't support powerful enough logic to handle the system
like Tarski and Godel are talking about.
The fact that Prolog just rejects it shows that.
>
>> You could try
>> ?- LP = not(true(LP), true(LP).
>>
>> or
>> ?- LP = not(true(LP), not(true(LP)).
>>
>> The predicate unify_with_occurs_check checks whether the resulting
>> sructure is acyclic because that is its purpose. Whether a simple
>
> Yes exactly. If I knew that Prolog did this then I would not have
> created Minimal Type Theory that does this same thing. That I did
> create MTT that does do this same thing makes my understanding much
> deeper.
>
>> unification like LP = not(true(LP)) does same is implementation
>> dependent as Prolog rules permit but do not require that. In a
>> typical implementation a simple unification does not check for
>> cycles.
>>
>
> ISO Prolog implementations have the built-in predicate
> unify_with_occurs_check/2 for sound unification
> https://en.wikipedia.org/wiki/Occurs_check#Sound_unification
>
> Alternatively such expressions crash or remain stuck in infinite loops.
>
>
>> Anyway, none of this is relevant to the topic of this thread or
>> topics of sci.logic.
>>
>
> ...14 Every epistemological antinomy can likewise be used for
> a similar undecidability proof...(Gödel 1931:40)
>
> Gödel, Kurt 1931.
> On Formally Undecidable Propositions of Principia Mathematica And
> Related Systems
>
> https://monoskop.org/images/9/93/Kurt_G%C3%B6del_On_Formally_Undecidable_Propositions_of_Principia_Mathematica_and_Related_Systems_1992.pdf
>
> It would
> then be possible to reconstruct the *antinomy of the liar* in the
> metalanguage, by forming in the language itself a sentence x
> such that the sentence of the metalanguage which is correlated
> with x asserts that x is not a true sentence.
>
> CONCEPT OF TRUTH IN FORMALIZED LANGUAGES, Tarski
> https://liarparadox.org/Tarski_247_248.pdf
>
> The Liar Paradox and other such {epistemological antinomies} must be
> rejected as type mismatch errors for any system of bivalent logic thus
> cannot be correctly used for any undecidability or undefinability proof.
>
But you just don't don't understand what was done in those proofs.
Neither of them assumed the Liar's paradox had a truth value. Only
statements formed from VALID logical sequences in the field.
Please try to show what step in Godel's or Tarski's proof where they
made a logical error (not just came up with a statement you think can't
be valid).
You can't, as shown by the fact that you never have even come close to
that, and that would be the actual nail in the coffin for the proofs.
All you are showing is that trying to add your rules to conventional
logic makes the system inconsistant, or requires removing some major
capability of the logic. Most people will prefer to live with the
limitations that some true statements can not be proven, which is sort
of what the lack of a Truth Predicate also says.
it seems you just want a world where no one can use logic too
complicated for you to understand, (which isn't very much logic).
It ain't going to happen.
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2024-05-28 21:39 -0500 |
| Subject | Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT |
| Message-ID | <v364hp$vl7m$1@dont-email.me> |
| In reply to | #334664 |
On 5/28/2024 9:04 PM, Richard Damon wrote:
> On 5/28/24 10:59 AM, olcott wrote:
>> On 5/28/2024 1:59 AM, Mikko wrote:
>>> On 2024-05-27 14:34:14 +0000, olcott said:
>>>
>>>> ?- LP = not(true(LP)).
>>>> LP = not(true(LP)).
>>>>
>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>> false.
>>>>
>>>> In other words Prolog has detected a cycle in the directed graph of the
>>>> evaluation sequence of the structure of the Liar Paradox. Experts seem
>>>> to think that Prolog is taking "not" and "true" as meaningless and is
>>>> only evaluating the structure of the expression.
>>>
>>> The words "not" and "true" of Prolog are meaningful in some contexts
>>> but not above. The word "true" is meaningful only when it has no
>>> arguments.
>>>
>>
>> That Prolog construes any expression having the same structure as the
>> Liar Paradox as having a cycle in the directed graph of its evaluation
>> sequence already completely proves my point. In other words Prolog
>> is saying that there is something wrong with the expression and it must
>> be rejected.
>
> But Prolog doesn't support powerful enough logic to handle the system
> like Tarski and Godel are talking about.
>
> The fact that Prolog just rejects it shows that.
>
Your ignorance is no excuse.
>>
>>> You could try
>>> ?- LP = not(true(LP), true(LP).
>>>
>>> or
>>> ?- LP = not(true(LP), not(true(LP)).
>>>
>>> The predicate unify_with_occurs_check checks whether the resulting
>>> sructure is acyclic because that is its purpose. Whether a simple
>>
>> Yes exactly. If I knew that Prolog did this then I would not have
>> created Minimal Type Theory that does this same thing. That I did
>> create MTT that does do this same thing makes my understanding much
>> deeper.
>>
>>> unification like LP = not(true(LP)) does same is implementation
>>> dependent as Prolog rules permit but do not require that. In a
>>> typical implementation a simple unification does not check for
>>> cycles.
>>>
>>
>> ISO Prolog implementations have the built-in predicate
>> unify_with_occurs_check/2 for sound unification
>> https://en.wikipedia.org/wiki/Occurs_check#Sound_unification
>>
>> Alternatively such expressions crash or remain stuck in infinite loops.
>>
>>
>>> Anyway, none of this is relevant to the topic of this thread or
>>> topics of sci.logic.
>>>
>>
>> ...14 Every epistemological antinomy can likewise be used for
>> a similar undecidability proof...(Gödel 1931:40)
>>
>> Gödel, Kurt 1931.
>> On Formally Undecidable Propositions of Principia Mathematica And
>> Related Systems
>>
>> https://monoskop.org/images/9/93/Kurt_G%C3%B6del_On_Formally_Undecidable_Propositions_of_Principia_Mathematica_and_Related_Systems_1992.pdf
>>
>> It would
>> then be possible to reconstruct the *antinomy of the liar* in the
>> metalanguage, by forming in the language itself a sentence x
>> such that the sentence of the metalanguage which is correlated
>> with x asserts that x is not a true sentence.
>>
>> CONCEPT OF TRUTH IN FORMALIZED LANGUAGES, Tarski
>> https://liarparadox.org/Tarski_247_248.pdf
>>
>> The Liar Paradox and other such {epistemological antinomies} must be
>> rejected as type mismatch errors for any system of bivalent logic thus
>> cannot be correctly used for any undecidability or undefinability proof.
>>
>
> But you just don't don't understand what was done in those proofs.
>
> Neither of them assumed the Liar's paradox had a truth value. Only
> statements formed from VALID logical sequences in the field.
>
> Please try to show what step in Godel's or Tarski's proof where they
> made a logical error (not just came up with a statement you think can't
> be valid).
>
Tarski's Liar Paradox from page 248
It would then be possible to reconstruct the antinomy of the liar
in the metalanguage, by forming in the language itself a sentence
x such that the sentence of the metalanguage which is correlated
with x asserts that x is not a true sentence.
https://liarparadox.org/Tarski_247_248.pdf
Formalized as:
x ∉ True if and only if p
where the symbol 'p' represents the whole sentence x
https://liarparadox.org/Tarski_275_276.pdf
adapted to become the first line of his proof
x ∉ Pr if and only if p
--
Copyright 2024 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | Richard Damon <richard@damon-family.org> |
|---|---|
| Date | 2024-05-28 23:38 -0400 |
| Subject | Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT |
| Message-ID | <v36801$2d368$2@i2pn2.org> |
| In reply to | #334670 |
On 5/28/24 10:39 PM, olcott wrote:
> On 5/28/2024 9:04 PM, Richard Damon wrote:
>> On 5/28/24 10:59 AM, olcott wrote:
>>> On 5/28/2024 1:59 AM, Mikko wrote:
>>>> On 2024-05-27 14:34:14 +0000, olcott said:
>>>>
>>>>> ?- LP = not(true(LP)).
>>>>> LP = not(true(LP)).
>>>>>
>>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>>> false.
>>>>>
>>>>> In other words Prolog has detected a cycle in the directed graph of
>>>>> the
>>>>> evaluation sequence of the structure of the Liar Paradox. Experts seem
>>>>> to think that Prolog is taking "not" and "true" as meaningless and is
>>>>> only evaluating the structure of the expression.
>>>>
>>>> The words "not" and "true" of Prolog are meaningful in some contexts
>>>> but not above. The word "true" is meaningful only when it has no
>>>> arguments.
>>>>
>>>
>>> That Prolog construes any expression having the same structure as the
>>> Liar Paradox as having a cycle in the directed graph of its evaluation
>>> sequence already completely proves my point. In other words Prolog
>>> is saying that there is something wrong with the expression and it must
>>> be rejected.
>>
>> But Prolog doesn't support powerful enough logic to handle the system
>> like Tarski and Godel are talking about.
>>
>> The fact that Prolog just rejects it shows that.
>>
>
> Your ignorance is no excuse.
What ignorance?
The fact that I understand the limitation of Prolog and what forms of
logic it can do, which seems to be beyond your understanding?
Claiming that Prolog rejects a statement because it doesn't fit its
grammer is meaningless for more complicated logics that don't have that
same grammer restricition.
IF you want to limit the logic you use to what Prolog can handle, go
ahead, the rest of the world likes its mathematics.
>
>>>
>>>> You could try
>>>> ?- LP = not(true(LP), true(LP).
>>>>
>>>> or
>>>> ?- LP = not(true(LP), not(true(LP)).
>>>>
>>>> The predicate unify_with_occurs_check checks whether the resulting
>>>> sructure is acyclic because that is its purpose. Whether a simple
>>>
>>> Yes exactly. If I knew that Prolog did this then I would not have
>>> created Minimal Type Theory that does this same thing. That I did
>>> create MTT that does do this same thing makes my understanding much
>>> deeper.
>>>
>>>> unification like LP = not(true(LP)) does same is implementation
>>>> dependent as Prolog rules permit but do not require that. In a
>>>> typical implementation a simple unification does not check for
>>>> cycles.
>>>>
>>>
>>> ISO Prolog implementations have the built-in predicate
>>> unify_with_occurs_check/2 for sound unification
>>> https://en.wikipedia.org/wiki/Occurs_check#Sound_unification
>>>
>>> Alternatively such expressions crash or remain stuck in infinite loops.
>>>
>>>
>>>> Anyway, none of this is relevant to the topic of this thread or
>>>> topics of sci.logic.
>>>>
>>>
>>> ...14 Every epistemological antinomy can likewise be used for
>>> a similar undecidability proof...(Gödel 1931:40)
>>>
>>> Gödel, Kurt 1931.
>>> On Formally Undecidable Propositions of Principia Mathematica And
>>> Related Systems
>>>
>>> https://monoskop.org/images/9/93/Kurt_G%C3%B6del_On_Formally_Undecidable_Propositions_of_Principia_Mathematica_and_Related_Systems_1992.pdf
>>>
>>> It would
>>> then be possible to reconstruct the *antinomy of the liar* in the
>>> metalanguage, by forming in the language itself a sentence x
>>> such that the sentence of the metalanguage which is correlated
>>> with x asserts that x is not a true sentence.
>>>
>>> CONCEPT OF TRUTH IN FORMALIZED LANGUAGES, Tarski
>>> https://liarparadox.org/Tarski_247_248.pdf
>>>
>>> The Liar Paradox and other such {epistemological antinomies} must be
>>> rejected as type mismatch errors for any system of bivalent logic thus
>>> cannot be correctly used for any undecidability or undefinability proof.
>>>
>>
>> But you just don't don't understand what was done in those proofs.
>>
>> Neither of them assumed the Liar's paradox had a truth value. Only
>> statements formed from VALID logical sequences in the field.
>>
>> Please try to show what step in Godel's or Tarski's proof where they
>> made a logical error (not just came up with a statement you think
>> can't be valid).
>>
>
> Tarski's Liar Paradox from page 248
> It would then be possible to reconstruct the antinomy of the liar
> in the metalanguage, by forming in the language itself a sentence
> x such that the sentence of the metalanguage which is correlated
> with x asserts that x is not a true sentence.
> https://liarparadox.org/Tarski_247_248.pdf
Right, He has SHOWN that the logic system, when given the assumption of
the existance of the Truth Predicate, can construct the liar as a
truth-bearing statement.
That means the logic system must be inconsistant.
The ONLY added assumption to the system, that was initially required to
be conssistant, was the existance of the Truth Predicate, so that
assumption must be incorrect.
If you try your idea that the statement somehow gets intercepted as a
type error, then all you have done is shown that you can, by your
detecting the type error, is prove the new system with the truth
predicate is inconsistant, so we STILL get to the assumption of a truth
predicate can't be correct, and your traps must reject THAT statement as
the source of the problem.
>
> Formalized as:
> x ∉ True if and only if p
> where the symbol 'p' represents the whole sentence x
> https://liarparadox.org/Tarski_275_276.pdf
>
> adapted to become the first line of his proof
> x ∉ Pr if and only if p
>
But that isn't the first line of the full proof, but a consequence from
his previous logic.
A system that can prove a non-truth-bearer (or a 'syntax error') is an
inconsistent system.
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2024-05-28 22:54 -0500 |
| Subject | Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT |
| Message-ID | <v368su$100kd$4@dont-email.me> |
| In reply to | #334672 |
On 5/28/2024 10:38 PM, Richard Damon wrote:
> On 5/28/24 10:39 PM, olcott wrote:
>> On 5/28/2024 9:04 PM, Richard Damon wrote:
>>> On 5/28/24 10:59 AM, olcott wrote:
>>>> On 5/28/2024 1:59 AM, Mikko wrote:
>>>>> On 2024-05-27 14:34:14 +0000, olcott said:
>>>>>
>>>>>> ?- LP = not(true(LP)).
>>>>>> LP = not(true(LP)).
>>>>>>
>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>>>> false.
>>>>>>
>>>>>> In other words Prolog has detected a cycle in the directed graph
>>>>>> of the
>>>>>> evaluation sequence of the structure of the Liar Paradox. Experts
>>>>>> seem
>>>>>> to think that Prolog is taking "not" and "true" as meaningless and is
>>>>>> only evaluating the structure of the expression.
>>>>>
>>>>> The words "not" and "true" of Prolog are meaningful in some contexts
>>>>> but not above. The word "true" is meaningful only when it has no
>>>>> arguments.
>>>>>
>>>>
>>>> That Prolog construes any expression having the same structure as the
>>>> Liar Paradox as having a cycle in the directed graph of its evaluation
>>>> sequence already completely proves my point. In other words Prolog
>>>> is saying that there is something wrong with the expression and it must
>>>> be rejected.
>>>
>>> But Prolog doesn't support powerful enough logic to handle the system
>>> like Tarski and Godel are talking about.
>>>
>>> The fact that Prolog just rejects it shows that.
>>>
>>
>> Your ignorance is no excuse.
>
> What ignorance?
>
The fact that you assert that you know the underlying details of
https://www.swi-prolog.org/pldoc/man?predicate=unify_with_occurs_check/2
without even glancing at the documentation and write-up in Clocksin and
Mellish seems to be willful ignorance.
> The fact that I understand the limitation of Prolog and what forms of
> logic it can do, which seems to be beyond your understanding?
>
> Claiming that Prolog rejects a statement because it doesn't fit its
> grammer is meaningless for more complicated logics that don't have that
> same grammer restricition.
>
> IF you want to limit the logic you use to what Prolog can handle, go
> ahead, the rest of the world likes its mathematics.
>
>>
>>>>
>>>>> You could try
>>>>> ?- LP = not(true(LP), true(LP).
>>>>>
>>>>> or
>>>>> ?- LP = not(true(LP), not(true(LP)).
>>>>>
>>>>> The predicate unify_with_occurs_check checks whether the resulting
>>>>> sructure is acyclic because that is its purpose. Whether a simple
>>>>
>>>> Yes exactly. If I knew that Prolog did this then I would not have
>>>> created Minimal Type Theory that does this same thing. That I did
>>>> create MTT that does do this same thing makes my understanding much
>>>> deeper.
>>>>
>>>>> unification like LP = not(true(LP)) does same is implementation
>>>>> dependent as Prolog rules permit but do not require that. In a
>>>>> typical implementation a simple unification does not check for
>>>>> cycles.
>>>>>
>>>>
>>>> ISO Prolog implementations have the built-in predicate
>>>> unify_with_occurs_check/2 for sound unification
>>>> https://en.wikipedia.org/wiki/Occurs_check#Sound_unification
>>>>
>>>> Alternatively such expressions crash or remain stuck in infinite loops.
>>>>
>>>>
>>>>> Anyway, none of this is relevant to the topic of this thread or
>>>>> topics of sci.logic.
>>>>>
>>>>
>>>> ...14 Every epistemological antinomy can likewise be used for
>>>> a similar undecidability proof...(Gödel 1931:40)
>>>>
>>>> Gödel, Kurt 1931.
>>>> On Formally Undecidable Propositions of Principia Mathematica And
>>>> Related Systems
>>>>
>>>> https://monoskop.org/images/9/93/Kurt_G%C3%B6del_On_Formally_Undecidable_Propositions_of_Principia_Mathematica_and_Related_Systems_1992.pdf
>>>>
>>>> It would
>>>> then be possible to reconstruct the *antinomy of the liar* in the
>>>> metalanguage, by forming in the language itself a sentence x
>>>> such that the sentence of the metalanguage which is correlated
>>>> with x asserts that x is not a true sentence.
>>>>
>>>> CONCEPT OF TRUTH IN FORMALIZED LANGUAGES, Tarski
>>>> https://liarparadox.org/Tarski_247_248.pdf
>>>>
>>>> The Liar Paradox and other such {epistemological antinomies} must be
>>>> rejected as type mismatch errors for any system of bivalent logic thus
>>>> cannot be correctly used for any undecidability or undefinability
>>>> proof.
>>>>
>>>
>>> But you just don't don't understand what was done in those proofs.
>>>
>>> Neither of them assumed the Liar's paradox had a truth value. Only
>>> statements formed from VALID logical sequences in the field.
>>>
>>> Please try to show what step in Godel's or Tarski's proof where they
>>> made a logical error (not just came up with a statement you think
>>> can't be valid).
>>>
>>
>> Tarski's Liar Paradox from page 248
>> It would then be possible to reconstruct the antinomy of the liar
>> in the metalanguage, by forming in the language itself a sentence
>> x such that the sentence of the metalanguage which is correlated
>> with x asserts that x is not a true sentence.
>> https://liarparadox.org/Tarski_247_248.pdf
>
> Right, He has SHOWN that the logic system, when given the assumption of
> the existance of the Truth Predicate, can construct the liar as a
> truth-bearing statement.
>
Utterly Ridiculous (and you probably don't know it).
--
Copyright 2024 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | Richard Damon <richard@damon-family.org> |
|---|---|
| Date | 2024-05-29 07:31 -0400 |
| Subject | Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT |
| Message-ID | <v373mu$2d367$6@i2pn2.org> |
| In reply to | #334675 |
On 5/28/24 11:54 PM, olcott wrote:
> On 5/28/2024 10:38 PM, Richard Damon wrote:
>> On 5/28/24 10:39 PM, olcott wrote:
>>> On 5/28/2024 9:04 PM, Richard Damon wrote:
>>>> On 5/28/24 10:59 AM, olcott wrote:
>>>>> On 5/28/2024 1:59 AM, Mikko wrote:
>>>>>> On 2024-05-27 14:34:14 +0000, olcott said:
>>>>>>
>>>>>>> ?- LP = not(true(LP)).
>>>>>>> LP = not(true(LP)).
>>>>>>>
>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>>>>> false.
>>>>>>>
>>>>>>> In other words Prolog has detected a cycle in the directed graph
>>>>>>> of the
>>>>>>> evaluation sequence of the structure of the Liar Paradox. Experts
>>>>>>> seem
>>>>>>> to think that Prolog is taking "not" and "true" as meaningless
>>>>>>> and is
>>>>>>> only evaluating the structure of the expression.
>>>>>>
>>>>>> The words "not" and "true" of Prolog are meaningful in some contexts
>>>>>> but not above. The word "true" is meaningful only when it has no
>>>>>> arguments.
>>>>>>
>>>>>
>>>>> That Prolog construes any expression having the same structure as the
>>>>> Liar Paradox as having a cycle in the directed graph of its evaluation
>>>>> sequence already completely proves my point. In other words Prolog
>>>>> is saying that there is something wrong with the expression and it
>>>>> must
>>>>> be rejected.
>>>>
>>>> But Prolog doesn't support powerful enough logic to handle the
>>>> system like Tarski and Godel are talking about.
>>>>
>>>> The fact that Prolog just rejects it shows that.
>>>>
>>>
>>> Your ignorance is no excuse.
>>
>> What ignorance?
>>
>
> The fact that you assert that you know the underlying details of
> https://www.swi-prolog.org/pldoc/man?predicate=unify_with_occurs_check/2
> without even glancing at the documentation and write-up in Clocksin and
> Mellish seems to be willful ignorance.
What makes you think that? I understand how Prolog works, and why it
only models relatively simple logic systems, because it just can't
handle the higher order logical primitives. It can't even handle full
first order logic.
>
>> The fact that I understand the limitation of Prolog and what forms of
>> logic it can do, which seems to be beyond your understanding?
>>
>> Claiming that Prolog rejects a statement because it doesn't fit its
>> grammer is meaningless for more complicated logics that don't have
>> that same grammer restricition.
>>
>> IF you want to limit the logic you use to what Prolog can handle, go
>> ahead, the rest of the world likes its mathematics.
>>
>>>
>>>>>
>>>>>> You could try
>>>>>> ?- LP = not(true(LP), true(LP).
>>>>>>
>>>>>> or
>>>>>> ?- LP = not(true(LP), not(true(LP)).
>>>>>>
>>>>>> The predicate unify_with_occurs_check checks whether the resulting
>>>>>> sructure is acyclic because that is its purpose. Whether a simple
>>>>>
>>>>> Yes exactly. If I knew that Prolog did this then I would not have
>>>>> created Minimal Type Theory that does this same thing. That I did
>>>>> create MTT that does do this same thing makes my understanding much
>>>>> deeper.
>>>>>
>>>>>> unification like LP = not(true(LP)) does same is implementation
>>>>>> dependent as Prolog rules permit but do not require that. In a
>>>>>> typical implementation a simple unification does not check for
>>>>>> cycles.
>>>>>>
>>>>>
>>>>> ISO Prolog implementations have the built-in predicate
>>>>> unify_with_occurs_check/2 for sound unification
>>>>> https://en.wikipedia.org/wiki/Occurs_check#Sound_unification
>>>>>
>>>>> Alternatively such expressions crash or remain stuck in infinite
>>>>> loops.
>>>>>
>>>>>
>>>>>> Anyway, none of this is relevant to the topic of this thread or
>>>>>> topics of sci.logic.
>>>>>>
>>>>>
>>>>> ...14 Every epistemological antinomy can likewise be used for
>>>>> a similar undecidability proof...(Gödel 1931:40)
>>>>>
>>>>> Gödel, Kurt 1931.
>>>>> On Formally Undecidable Propositions of Principia Mathematica And
>>>>> Related Systems
>>>>>
>>>>> https://monoskop.org/images/9/93/Kurt_G%C3%B6del_On_Formally_Undecidable_Propositions_of_Principia_Mathematica_and_Related_Systems_1992.pdf
>>>>>
>>>>> It would
>>>>> then be possible to reconstruct the *antinomy of the liar* in the
>>>>> metalanguage, by forming in the language itself a sentence x
>>>>> such that the sentence of the metalanguage which is correlated
>>>>> with x asserts that x is not a true sentence.
>>>>>
>>>>> CONCEPT OF TRUTH IN FORMALIZED LANGUAGES, Tarski
>>>>> https://liarparadox.org/Tarski_247_248.pdf
>>>>>
>>>>> The Liar Paradox and other such {epistemological antinomies} must be
>>>>> rejected as type mismatch errors for any system of bivalent logic thus
>>>>> cannot be correctly used for any undecidability or undefinability
>>>>> proof.
>>>>>
>>>>
>>>> But you just don't don't understand what was done in those proofs.
>>>>
>>>> Neither of them assumed the Liar's paradox had a truth value. Only
>>>> statements formed from VALID logical sequences in the field.
>>>>
>>>> Please try to show what step in Godel's or Tarski's proof where they
>>>> made a logical error (not just came up with a statement you think
>>>> can't be valid).
>>>>
>>>
>>> Tarski's Liar Paradox from page 248
>>> It would then be possible to reconstruct the antinomy of the liar
>>> in the metalanguage, by forming in the language itself a sentence
>>> x such that the sentence of the metalanguage which is correlated
>>> with x asserts that x is not a true sentence.
>>> https://liarparadox.org/Tarski_247_248.pdf
>>
>> Right, He has SHOWN that the logic system, when given the assumption
>> of the existance of the Truth Predicate, can construct the liar as a
>> truth-bearing statement.
>>
>
> Utterly Ridiculous (and you probably don't know it).
>
Why is it ridiculous?
I think you ard just proving you just don't understand any of the
details of what he is saying, and thus are just trying to match snippets
of words to things you think you know.
Just like a poorly trained Artificial Intelligence.
And this shows that you are not a very well trained intelligence of any
form.
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2024-05-29 09:00 -0500 |
| Subject | Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT |
| Message-ID | <v37ced$15rjf$1@dont-email.me> |
| In reply to | #334679 |
On 5/29/2024 6:31 AM, Richard Damon wrote:
> On 5/28/24 11:54 PM, olcott wrote:
>> On 5/28/2024 10:38 PM, Richard Damon wrote:
>>> On 5/28/24 10:39 PM, olcott wrote:
>>>> On 5/28/2024 9:04 PM, Richard Damon wrote:
>>>>> On 5/28/24 10:59 AM, olcott wrote:
>>>>>> On 5/28/2024 1:59 AM, Mikko wrote:
>>>>>>> On 2024-05-27 14:34:14 +0000, olcott said:
>>>>>>>
>>>>>>>> ?- LP = not(true(LP)).
>>>>>>>> LP = not(true(LP)).
>>>>>>>>
>>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>> false.
>>>>>>>>
>>>>>>>> In other words Prolog has detected a cycle in the directed graph
>>>>>>>> of the
>>>>>>>> evaluation sequence of the structure of the Liar Paradox.
>>>>>>>> Experts seem
>>>>>>>> to think that Prolog is taking "not" and "true" as meaningless
>>>>>>>> and is
>>>>>>>> only evaluating the structure of the expression.
>>>>>>>
>>>>>>> The words "not" and "true" of Prolog are meaningful in some contexts
>>>>>>> but not above. The word "true" is meaningful only when it has no
>>>>>>> arguments.
>>>>>>>
>>>>>>
>>>>>> That Prolog construes any expression having the same structure as the
>>>>>> Liar Paradox as having a cycle in the directed graph of its
>>>>>> evaluation
>>>>>> sequence already completely proves my point. In other words Prolog
>>>>>> is saying that there is something wrong with the expression and it
>>>>>> must
>>>>>> be rejected.
>>>>>
>>>>> But Prolog doesn't support powerful enough logic to handle the
>>>>> system like Tarski and Godel are talking about.
>>>>>
>>>>> The fact that Prolog just rejects it shows that.
>>>>>
>>>>
>>>> Your ignorance is no excuse.
>>>
>>> What ignorance?
>>>
>>
>> The fact that you assert that you know the underlying details of
>> https://www.swi-prolog.org/pldoc/man?predicate=unify_with_occurs_check/2
>> without even glancing at the documentation and write-up in Clocksin and
>> Mellish seems to be willful ignorance.
>
> What makes you think that? I understand how Prolog works, and why it
> only models relatively simple logic systems, because it just can't
> handle the higher order logical primitives. It can't even handle full
> first order logic.
>
Your explanation of
https://www.swi-prolog.org/pldoc/man?predicate=unify_with_occurs_check/2
was ridiculous.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs from the
unification used in Resolution. Most Prolog systems will allow you to
satisfy goals like:
equal(X, X).
?- equal(foo(Y), Y).
that is, they will allow you to match a term against an uninstantiated
subterm of itself. In this example, foo(Y) is matched against Y, which
appears within it. As a result, Y will stand for foo(Y), which is
foo(foo(Y)) (because of what Y stands for), which is foo(foo(foo(Y))),
and so on. So Y ends up standing for some kind of infinite structure.
Note that, whereas they may allow you to construct something like this,
most Prolog systems will not be able to write it out at the end.
According to the formal definition of Unification, this kind of
“infinite term” should never come to exist. Thus Prolog systems that
allow a term to match an uninstantiated subterm of itself do not act
correctly as Resolution theorem provers. In order to make them do so, we
would have to add a check that a variable cannot be instantiated to
something containing itself. Such a check, an occurs check, would be
straightforward to implement, but would slow down the execution of
Prolog programs considerably. Since it would only affect very few
programs, most implementors have simply left it out 1.
1 The Prolog standard states that the result is undefined if a Prolog
system attempts to match a term against an uninstantiated subterm of
itself, which means that programs which cause tills to happen will
not be portable. A portable program should ensure that wherever an
occurs check might be applicable the built-in predicate
unify_with_occurs_check/2 is used explicitly instead of the normal
unification operation of the Prolog implementation. As its
name suggests, this predicate acts like =/2 except that it fails if
an occurs check detects an illegal attempt to instantiate a variable.
END:(Clocksin & Mellish 2003:254)
Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog Using the
ISO Standard Fifth Edition, 254. Berlin Heidelberg: Springer-Verlag.
--
Copyright 2024 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | Richard Damon <richard@damon-family.org> |
|---|---|
| Date | 2024-05-29 19:47 -0400 |
| Subject | Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT |
| Message-ID | <v38eq6$2foi0$2@i2pn2.org> |
| In reply to | #334683 |
On 5/29/24 10:00 AM, olcott wrote: > On 5/29/2024 6:31 AM, Richard Damon wrote: >> On 5/28/24 11:54 PM, olcott wrote: >>> On 5/28/2024 10:38 PM, Richard Damon wrote: >>>> On 5/28/24 10:39 PM, olcott wrote: >>>>> On 5/28/2024 9:04 PM, Richard Damon wrote: >>>>>> On 5/28/24 10:59 AM, olcott wrote: >>>>>>> On 5/28/2024 1:59 AM, Mikko wrote: >>>>>>>> On 2024-05-27 14:34:14 +0000, olcott said: >>>>>>>> >>>>>>>>> ?- LP = not(true(LP)). >>>>>>>>> LP = not(true(LP)). >>>>>>>>> >>>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))). >>>>>>>>> false. >>>>>>>>> >>>>>>>>> In other words Prolog has detected a cycle in the directed >>>>>>>>> graph of the >>>>>>>>> evaluation sequence of the structure of the Liar Paradox. >>>>>>>>> Experts seem >>>>>>>>> to think that Prolog is taking "not" and "true" as meaningless >>>>>>>>> and is >>>>>>>>> only evaluating the structure of the expression. >>>>>>>> >>>>>>>> The words "not" and "true" of Prolog are meaningful in some >>>>>>>> contexts >>>>>>>> but not above. The word "true" is meaningful only when it has no >>>>>>>> arguments. >>>>>>>> >>>>>>> >>>>>>> That Prolog construes any expression having the same structure as >>>>>>> the >>>>>>> Liar Paradox as having a cycle in the directed graph of its >>>>>>> evaluation >>>>>>> sequence already completely proves my point. In other words Prolog >>>>>>> is saying that there is something wrong with the expression and >>>>>>> it must >>>>>>> be rejected. >>>>>> >>>>>> But Prolog doesn't support powerful enough logic to handle the >>>>>> system like Tarski and Godel are talking about. >>>>>> >>>>>> The fact that Prolog just rejects it shows that. >>>>>> >>>>> >>>>> Your ignorance is no excuse. >>>> >>>> What ignorance? >>>> >>> >>> The fact that you assert that you know the underlying details of >>> https://www.swi-prolog.org/pldoc/man?predicate=unify_with_occurs_check/2 >>> without even glancing at the documentation and write-up in Clocksin and >>> Mellish seems to be willful ignorance. >> >> What makes you think that? I understand how Prolog works, and why it >> only models relatively simple logic systems, because it just can't >> handle the higher order logical primitives. It can't even handle full >> first order logic. >> > > Your explanation of > https://www.swi-prolog.org/pldoc/man?predicate=unify_with_occurs_check/2 > was ridiculous. I didn't say anything about except that it Prolog only handles a simple set of logic forms. The makers of Proog freely admit that, so it isn't disparaging of them. It is a good tool for the problems it was designed for, and (as most tools) lousy at things that are outside its design parameters. A bit like using a fine screwdriver to try to cut your lumber. > > BEGIN:(Clocksin & Mellish 2003:254) > Finally, a note about how Prolog matching sometimes differs from the > unification used in Resolution. Most Prolog systems will allow you to > satisfy goals like: > equal(X, X). > ?- equal(foo(Y), Y). > > that is, they will allow you to match a term against an uninstantiated > subterm of itself. In this example, foo(Y) is matched against Y, which > appears within it. As a result, Y will stand for foo(Y), which is > foo(foo(Y)) (because of what Y stands for), which is foo(foo(foo(Y))), > and so on. So Y ends up standing for some kind of infinite structure. > > Note that, whereas they may allow you to construct something like this, > most Prolog systems will not be able to write it out at the end. > According to the formal definition of Unification, this kind of > “infinite term” should never come to exist. Thus Prolog systems that > allow a term to match an uninstantiated subterm of itself do not act > correctly as Resolution theorem provers. In order to make them do so, we > would have to add a check that a variable cannot be instantiated to > something containing itself. Such a check, an occurs check, would be > straightforward to implement, but would slow down the execution of > Prolog programs considerably. Since it would only affect very few > programs, most implementors have simply left it out 1. > > 1 The Prolog standard states that the result is undefined if a Prolog > system attempts to match a term against an uninstantiated subterm of > itself, which means that programs which cause tills to happen will > not be portable. A portable program should ensure that wherever an > occurs check might be applicable the built-in predicate > unify_with_occurs_check/2 is used explicitly instead of the normal > unification operation of the Prolog implementation. As its > name suggests, this predicate acts like =/2 except that it fails if > an occurs check detects an illegal attempt to instantiate a variable. > END:(Clocksin & Mellish 2003:254) > > Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog Using the > ISO Standard Fifth Edition, 254. Berlin Heidelberg: Springer-Verlag. >
[toc] | [prev] | [next] | [standalone]
| From | Python <python@invalid.org> |
|---|---|
| Date | 2024-05-29 09:01 +0200 |
| Subject | Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT |
| Message-ID | <v36js8$11o1h$1@dont-email.me> |
| In reply to | #334670 |
Le 29/05/2024 à 04:39, olcott a écrit : ... >>> That Prolog construes any expression having the same structure as the >>> Liar Paradox as having a cycle in the directed graph of its evaluation >>> sequence already completely proves my point. In other words Prolog >>> is saying that there is something wrong with the expression and it must >>> be rejected. >> >> But Prolog doesn't support powerful enough logic to handle the system >> like Tarski and Godel are talking about. >> >> The fact that Prolog just rejects it shows that. >> > > Your ignorance is no excuse. You, Peter Olcott, are actually the one showing one's ignorance here. Gödel theorems can be handled by more powerful proving systems such as COQ : http://r6.ca/Goedel/goedel1.html
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2024-05-29 08:11 -0500 |
| Subject | Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT |
| Message-ID | <v379h7$159q4$1@dont-email.me> |
| In reply to | #334676 |
On 5/29/2024 2:01 AM, Python wrote:
> Le 29/05/2024 à 04:39, olcott a écrit :
> ...
>>>> That Prolog construes any expression having the same structure as the
>>>> Liar Paradox as having a cycle in the directed graph of its evaluation
>>>> sequence already completely proves my point. In other words Prolog
>>>> is saying that there is something wrong with the expression and it must
>>>> be rejected.
>>>
>>> But Prolog doesn't support powerful enough logic to handle the system
>>> like Tarski and Godel are talking about.
>>>
>>> The fact that Prolog just rejects it shows that.
>>>
>>
>> Your ignorance is no excuse.
>
> You, Peter Olcott, are actually the one showing one's ignorance here.
>
> Gödel theorems can be handled by more powerful proving systems such
> as COQ : http://r6.ca/Goedel/goedel1.html
?- LP = not(true(L, LP)).
LP = not(true(L, LP)).
?- unify_with_occurs_check(LP, not(true(L, LP))).
false.
Richard explained this incorrectly.
let's see if you can do better.
I created Minimal Type Theory that does the same thing as
https://www.swi-prolog.org/pldoc/man?predicate=unify_with_occurs_check/2
Minimal Type Theory (YACC BNF)
https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
LP := ~True(L, LP)
definition_2 token="ASSIGN_ALIAS"
| definition_2 token="IDENTIFIER" value="LP"
| sentence_2 token="NOT"
| | atomic_sentence_1 token="IDENTIFIER" value="True"
| | | term_list_1
| | | | term_2 token="IDENTIFIER" value="L"
| | | | term_2 token="IDENTIFIER" value="LP"
<definition_2 token="ASSIGN_ALIAS">
<definition_2 token="IDENTIFIER" value="LP"/>
<sentence_2 token="NOT">
<atomic_sentence_1 token="IDENTIFIER" value="True">
<term_list_1>
<term_2 token="IDENTIFIER" value="L"/>
<term_2 token="IDENTIFIER" value="LP"/>
</term_list_1>
</atomic_sentence_1>
</sentence_2>
</definition_2>
Directed graph of evaluation sequence of LP
Nodes on the left edges on the right
00 NOT 01
01 True 02, 00 // cycle
02 L
--
Copyright 2024 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | Richard Damon <richard@damon-family.org> |
|---|---|
| Date | 2024-05-29 19:47 -0400 |
| Subject | Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT |
| Message-ID | <v38eq8$2foi0$3@i2pn2.org> |
| In reply to | #334680 |
On 5/29/24 9:11 AM, olcott wrote: > On 5/29/2024 2:01 AM, Python wrote: >> Le 29/05/2024 à 04:39, olcott a écrit : >> ... >>>>> That Prolog construes any expression having the same structure as the >>>>> Liar Paradox as having a cycle in the directed graph of its evaluation >>>>> sequence already completely proves my point. In other words Prolog >>>>> is saying that there is something wrong with the expression and it >>>>> must >>>>> be rejected. >>>> >>>> But Prolog doesn't support powerful enough logic to handle the >>>> system like Tarski and Godel are talking about. >>>> >>>> The fact that Prolog just rejects it shows that. >>>> >>> >>> Your ignorance is no excuse. >> >> You, Peter Olcott, are actually the one showing one's ignorance here. >> >> Gödel theorems can be handled by more powerful proving systems such >> as COQ : http://r6.ca/Goedel/goedel1.html > > ?- LP = not(true(L, LP)). > LP = not(true(L, LP)). > > ?- unify_with_occurs_check(LP, not(true(L, LP))). > false. > > Richard explained this incorrectly. > let's see if you can do better. > > I created Minimal Type Theory that does the same thing as > https://www.swi-prolog.org/pldoc/man?predicate=unify_with_occurs_check/2 > > Minimal Type Theory (YACC BNF) > https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF > > LP := ~True(L, LP) > > definition_2 token="ASSIGN_ALIAS" > | definition_2 token="IDENTIFIER" value="LP" > | sentence_2 token="NOT" > | | atomic_sentence_1 token="IDENTIFIER" value="True" > | | | term_list_1 > | | | | term_2 token="IDENTIFIER" value="L" > | | | | term_2 token="IDENTIFIER" value="LP" > > <definition_2 token="ASSIGN_ALIAS"> > <definition_2 token="IDENTIFIER" value="LP"/> > <sentence_2 token="NOT"> > <atomic_sentence_1 token="IDENTIFIER" value="True"> > <term_list_1> > <term_2 token="IDENTIFIER" value="L"/> > <term_2 token="IDENTIFIER" value="LP"/> > </term_list_1> > </atomic_sentence_1> > </sentence_2> > </definition_2> > > Directed graph of evaluation sequence of LP > Nodes on the left edges on the right > 00 NOT 01 > 01 True 02, 00 // cycle > 02 L > Which has NOTHING to do with the statement you are replying to, showing your utter stupidity.
[toc] | [prev] | [next] | [standalone]
| From | Mikko <mikko.levanto@iki.fi> |
|---|---|
| Date | 2024-05-29 11:25 +0300 |
| Subject | Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT |
| Message-ID | <v36opq$12i6f$1@dont-email.me> |
| In reply to | #334658 |
On 2024-05-28 14:59:30 +0000, olcott said: > On 5/28/2024 1:59 AM, Mikko wrote: >> On 2024-05-27 14:34:14 +0000, olcott said: >> >>> ?- LP = not(true(LP)). >>> LP = not(true(LP)). >>> >>> ?- unify_with_occurs_check(LP, not(true(LP))). >>> false. >>> >>> In other words Prolog has detected a cycle in the directed graph of the >>> evaluation sequence of the structure of the Liar Paradox. Experts seem >>> to think that Prolog is taking "not" and "true" as meaningless and is >>> only evaluating the structure of the expression. >> >> The words "not" and "true" of Prolog are meaningful in some contexts >> but not above. The word "true" is meaningful only when it has no arguments. >> > > That Prolog construes any expression having the same structure as the > Liar Paradox as having a cycle in the directed graph of its evaluation > sequence already completely proves my point. In other words Prolog > is saying that there is something wrong with the expression and it must > be rejected. > >> You could try >> ?- LP = not(true(LP), true(LP). >> >> or >> ?- LP = not(true(LP), not(true(LP)). >> >> The predicate unify_with_occurs_check checks whether the resulting >> sructure is acyclic because that is its purpose. Whether a simple > > Yes exactly. If I knew that Prolog did this then I would not have > created Minimal Type Theory that does this same thing. That I did > create MTT that does do this same thing makes my understanding much > deeper. Prolog does not reject LP = not(true(LP)). It can accept it as syntactically valid. Thaat unify_with_occurs_check(LP, not(true(LP)) fails does not mean anything except when it is used, and then it does not reject but simplu evaluates to false, just like 1 = 2 is false but not erroneous. >> unification like LP = not(true(LP)) does same is implementation >> dependent as Prolog rules permit but do not require that. In a >> typical implementation a simple unification does not check for >> cycles. >> > > ISO Prolog implementations have the built-in predicate > unify_with_occurs_check/2 for sound unification > https://en.wikipedia.org/wiki/Occurs_check#Sound_unification > > Alternatively such expressions crash or remain stuck in infinite loops. Not necessarily. What happes depends on the implementation and on what you do with such structures. You already saw that your ?- LP = not(true(LP)). does not crash and does not remain stuck in infinite loop. >> Anyway, none of this is relevant to the topic of this thread or >> topics of sci.logic. If you want to talk nore about Prolog do it in comp.lang.prolog. -- Mikko
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2024-05-29 08:31 -0500 |
| Subject | Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT |
| Message-ID | <v37anj$159q4$5@dont-email.me> |
| In reply to | #334677 |
On 5/29/2024 3:25 AM, Mikko wrote: > On 2024-05-28 14:59:30 +0000, olcott said: > >> On 5/28/2024 1:59 AM, Mikko wrote: >>> On 2024-05-27 14:34:14 +0000, olcott said: >>> >>>> ?- LP = not(true(LP)). >>>> LP = not(true(LP)). >>>> >>>> ?- unify_with_occurs_check(LP, not(true(LP))). >>>> false. >>>> >>>> In other words Prolog has detected a cycle in the directed graph of the >>>> evaluation sequence of the structure of the Liar Paradox. Experts seem >>>> to think that Prolog is taking "not" and "true" as meaningless and is >>>> only evaluating the structure of the expression. >>> >>> The words "not" and "true" of Prolog are meaningful in some contexts >>> but not above. The word "true" is meaningful only when it has no >>> arguments. >>> >> >> That Prolog construes any expression having the same structure as the >> Liar Paradox as having a cycle in the directed graph of its evaluation >> sequence already completely proves my point. In other words Prolog >> is saying that there is something wrong with the expression and it must >> be rejected. >> >>> You could try >>> ?- LP = not(true(LP), true(LP). >>> >>> or >>> ?- LP = not(true(LP), not(true(LP)). >>> >>> The predicate unify_with_occurs_check checks whether the resulting >>> sructure is acyclic because that is its purpose. Whether a simple >> >> Yes exactly. If I knew that Prolog did this then I would not have >> created Minimal Type Theory that does this same thing. That I did >> create MTT that does do this same thing makes my understanding much >> deeper. > > Prolog does not reject LP = not(true(LP)). It can accept it as > syntactically valid. Thaat unify_with_occurs_check(LP, not(true(LP)) > fails does not mean anything except when it is used, and then it > does not reject but simplu evaluates to false, just like 1 = 2 > is false but not erroneous. > It correctly determines that there is a cycle in the directed graph of the evaluation sequence of the expression, which is like an infinite loop in a program. You can understand this or fail to understand this, disagreement is incorrect. If you have any disagreement then please back up your claims with proof. >>> unification like LP = not(true(LP)) does same is implementation >>> dependent as Prolog rules permit but do not require that. In a >>> typical implementation a simple unification does not check for >>> cycles. >>> >> >> ISO Prolog implementations have the built-in predicate >> unify_with_occurs_check/2 for sound unification >> https://en.wikipedia.org/wiki/Occurs_check#Sound_unification >> >> Alternatively such expressions crash or remain stuck in infinite loops. > > Not necessarily. What happes depends on the implementation and on what > you do with such structures. You already saw that your > > ?- LP = not(true(LP)). > > does not crash and does not remain stuck in infinite loop. > >>> Anyway, none of this is relevant to the topic of this thread or >>> topics of sci.logic. > > If you want to talk nore about Prolog do it in comp.lang.prolog. > It is relevant to sci.logic in that it exposes fundamental flaws with classical logic. That contradictory result apparently throws us into the lion’s den of semantic incoherence. The incoherence is due to the fact that, according to the rules of classical logic, anything follows from a contradiction, even 1 + 1 = 3. https://iep.utm.edu/liar-paradox/# -- Copyright 2024 Olcott "Talent hits a target no one else can hit; Genius hits a target no one else can see." Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | Mikko <mikko.levanto@iki.fi> |
|---|---|
| Date | 2024-05-30 09:52 +0300 |
| Subject | Re: True on the basis of meaning --- Good job Richard ! ---Socratic method MTT |
| Message-ID | <v397n7$1j3rd$1@dont-email.me> |
| In reply to | #334681 |
On 2024-05-29 13:31:31 +0000, olcott said: > On 5/29/2024 3:25 AM, Mikko wrote: >> On 2024-05-28 14:59:30 +0000, olcott said: >> >>> On 5/28/2024 1:59 AM, Mikko wrote: >>>> On 2024-05-27 14:34:14 +0000, olcott said: >>>> >>>>> ?- LP = not(true(LP)). >>>>> LP = not(true(LP)). >>>>> >>>>> ?- unify_with_occurs_check(LP, not(true(LP))). >>>>> false. >>>>> >>>>> In other words Prolog has detected a cycle in the directed graph of the >>>>> evaluation sequence of the structure of the Liar Paradox. Experts seem >>>>> to think that Prolog is taking "not" and "true" as meaningless and is >>>>> only evaluating the structure of the expression. >>>> >>>> The words "not" and "true" of Prolog are meaningful in some contexts >>>> but not above. The word "true" is meaningful only when it has no arguments. >>>> >>> >>> That Prolog construes any expression having the same structure as the >>> Liar Paradox as having a cycle in the directed graph of its evaluation >>> sequence already completely proves my point. In other words Prolog >>> is saying that there is something wrong with the expression and it must >>> be rejected. >>> >>>> You could try >>>> ?- LP = not(true(LP), true(LP). >>>> >>>> or >>>> ?- LP = not(true(LP), not(true(LP)). >>>> >>>> The predicate unify_with_occurs_check checks whether the resulting >>>> sructure is acyclic because that is its purpose. Whether a simple >>> >>> Yes exactly. If I knew that Prolog did this then I would not have >>> created Minimal Type Theory that does this same thing. That I did >>> create MTT that does do this same thing makes my understanding much >>> deeper. >> >> Prolog does not reject LP = not(true(LP)). It can accept it as >> syntactically valid. Thaat unify_with_occurs_check(LP, not(true(LP)) >> fails does not mean anything except when it is used, and then it >> does not reject but simplu evaluates to false, just like 1 = 2 >> is false but not erroneous. >> > > It correctly determines that there is a cycle in the directed graph > of the evaluation sequence of the expression, which is like an > infinite loop in a program. > > You can understand this or fail to understand this, disagreement is > incorrect. If you have any disagreement then please back up your > claims with proof. > >>>> unification like LP = not(true(LP)) does same is implementation >>>> dependent as Prolog rules permit but do not require that. In a >>>> typical implementation a simple unification does not check for >>>> cycles. >>>> >>> >>> ISO Prolog implementations have the built-in predicate >>> unify_with_occurs_check/2 for sound unification >>> https://en.wikipedia.org/wiki/Occurs_check#Sound_unification >>> >>> Alternatively such expressions crash or remain stuck in infinite loops. >> >> Not necessarily. What happes depends on the implementation and on what >> you do with such structures. You already saw that your >> >> ?- LP = not(true(LP)). >> >> does not crash and does not remain stuck in infinite loop. >> >>>> Anyway, none of this is relevant to the topic of this thread or >>>> topics of sci.logic. >> >> If you want to talk nore about Prolog do it in comp.lang.prolog. >> > > It is relevant to sci.logic in that it exposes fundamental flaws > with classical logic. It does not expose any flaw in classical logic. Flaws in your understanding of calssical logics are already sufficiently known. -- Mikko
[toc] | [prev] | [next] | [standalone]
Page 7 of 11 — ← Prev page 1 … 5 6 [7] 8 9 … 11 Next page →
Back to top | Article view | sci.logic
csiph-web