Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > comp.theory > #141687 > unrolled thread
| Started by | olcott <polcott333@gmail.com> |
|---|---|
| First post | 2026-06-17 16:14 -0500 |
| Last post | 2026-06-23 09:55 -0500 |
| Articles | 20 on this page of 359 — 11 participants |
Back to article view | Back to comp.theory
Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-17 16:14 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-18 14:35 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-19 10:23 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-19 07:46 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Alan Mackenzie <acm@muc.de> - 2026-06-19 20:28 +0000
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics dart200 <user7160@newsgrouper.org.invalid> - 2026-06-19 13:49 -0700
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-19 15:57 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-19 15:50 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Alan Mackenzie <acm@muc.de> - 2026-06-19 21:05 +0000
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-19 16:24 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-19 18:30 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-19 22:27 -0700
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-20 09:20 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-19 21:35 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-19 22:27 -0700
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-19 23:04 -0700
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-20 09:29 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-20 09:22 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-19 21:40 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-20 11:05 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics André G. Isaak <agisaak@gm.invalid> - 2026-06-20 11:40 -0600
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-20 14:02 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics dbush <dbush.mobile@gmail.com> - 2026-06-20 15:17 -0400
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-20 12:30 -0700
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-20 15:45 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-20 15:03 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics dbush <dbush.mobile@gmail.com> - 2026-06-20 16:17 -0400
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-20 16:03 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics dbush <dbush.mobile@gmail.com> - 2026-06-20 17:17 -0400
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-21 13:02 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics dbush <dbush.mobile@gmail.com> - 2026-06-21 09:14 -0400
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-22 09:16 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-21 12:57 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-21 18:51 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics dbush <dbush.mobile@gmail.com> - 2026-06-21 20:16 -0400
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-22 10:13 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-22 08:13 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-22 11:01 -0700
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-22 13:12 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-22 12:28 -0700
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-23 08:39 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-23 09:29 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-24 11:23 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-24 15:19 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-25 10:09 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-25 08:43 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-26 09:17 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-26 07:59 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-27 10:16 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-21 12:48 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-21 13:36 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics phoenix <j63840576@gmail.com> - 2026-06-21 12:54 -0600
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-22 09:23 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-20 10:54 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Alan Mackenzie <acm@muc.de> - 2026-06-20 10:26 +0000
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-20 08:50 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Alan Mackenzie <acm@muc.de> - 2026-06-20 15:34 +0000
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-20 10:47 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Alan Mackenzie <acm@muc.de> - 2026-06-20 16:08 +0000
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-20 11:37 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-21 13:11 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-21 18:55 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-22 09:27 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-22 07:05 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-23 08:43 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics André G. Isaak <agisaak@gm.invalid> - 2026-06-21 14:18 -0600
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Alan Mackenzie <acm@muc.de> - 2026-06-21 20:44 +0000
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-21 16:39 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics phoenix <j63840576@gmail.com> - 2026-06-21 16:36 -0600
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-21 18:15 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics phoenix <j63840576@gmail.com> - 2026-06-21 18:32 -0600
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-21 19:44 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-22 10:46 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-22 10:16 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-23 08:49 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-23 09:40 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-24 12:45 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-24 15:23 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-25 10:14 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-25 08:47 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-26 09:23 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-26 08:02 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-27 10:19 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics polcott <polcott333@gmail.com> - 2026-06-27 10:34 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-21 21:27 -0700
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-22 00:22 -0700
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-21 21:16 -0700
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics André G. Isaak <agisaak@gm.invalid> - 2026-06-21 18:05 -0600
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-21 19:14 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-20 09:51 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-21 14:04 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-20 10:50 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-20 09:41 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-21 13:17 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-21 18:58 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-22 09:41 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-22 07:09 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-23 08:55 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-23 09:47 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-24 12:52 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-24 15:25 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-25 10:18 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-25 08:58 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-26 09:34 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-26 08:05 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-27 10:27 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics polcott <polcott333@gmail.com> - 2026-06-27 10:36 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-28 11:04 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-19 22:25 -0700
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-20 09:18 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics dbush <dbush.mobile@gmail.com> - 2026-06-20 10:36 -0400
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-20 09:54 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics dbush <dbush.mobile@gmail.com> - 2026-06-20 10:57 -0400
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-20 10:22 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics dbush <dbush.mobile@gmail.com> - 2026-06-20 11:23 -0400
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-20 10:44 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics dbush <dbush.mobile@gmail.com> - 2026-06-20 11:48 -0400
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-20 09:45 -0700
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics dbush <dbush.mobile@gmail.com> - 2026-06-20 16:20 -0400
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-20 09:29 -0700
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-20 11:45 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-20 09:47 -0700
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-20 11:57 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics dbush <dbush.mobile@gmail.com> - 2026-06-20 13:13 -0400
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-20 10:21 -0700
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-20 10:19 -0700
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-20 12:33 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics dbush <dbush.mobile@gmail.com> - 2026-06-20 13:36 -0400
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-20 12:13 -0700
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Alan Mackenzie <acm@muc.de> - 2026-06-20 19:48 +0000
Readings in (some of the) foundations of mathematics --- analytic/synthetic distinction olcott <polcott333@gmail.com> - 2026-06-20 16:00 -0500
Re: Readings in (some of the) foundations of mathematics --- analytic/synthetic distinction dbush <dbush.mobile@gmail.com> - 2026-06-20 17:19 -0400
Re: Readings in (some of the) foundations of mathematics --- analytic/synthetic distinction olcott <polcott333@gmail.com> - 2026-06-20 16:30 -0500
Re: Readings in (some of the) foundations of mathematics --- analytic/synthetic distinction dbush <dbush.mobile@gmail.com> - 2026-06-20 17:34 -0400
Disjunction introduction --- new premise from out of no where olcott <polcott333@gmail.com> - 2026-06-20 17:26 -0500
Re: Disjunction introduction --- new premise from out of no where dbush <dbush.mobile@gmail.com> - 2026-06-20 20:11 -0400
Re: Disjunction introduction --- new premise from out of no where olcott <polcott333@gmail.com> - 2026-06-20 19:26 -0500
Re: Disjunction introduction --- new premise from out of no where dbush <dbush.mobile@gmail.com> - 2026-06-20 20:29 -0400
Re: Disjunction introduction --- new premise from out of no where olcott <polcott333@gmail.com> - 2026-06-20 20:06 -0500
Re: Disjunction introduction --- new premise from out of no where dbush <dbush.mobile@gmail.com> - 2026-06-20 21:28 -0400
Re: Disjunction introduction --- new premise from out of no where olcott <polcott333@gmail.com> - 2026-06-20 20:32 -0500
Re: Disjunction introduction --- new premise from out of no where dbush <dbush.mobile@gmail.com> - 2026-06-20 21:38 -0400
Re: Disjunction introduction --- new premise from out of no where olcott <polcott333@gmail.com> - 2026-06-20 20:48 -0500
Re: Disjunction introduction --- new premise from out of no where dbush <dbush.mobile@gmail.com> - 2026-06-20 21:51 -0400
Re: Disjunction introduction --- new premise from out of no where "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2026-06-25 12:54 -0700
Re: Disjunction introduction --- new premise from out of no where olcott <polcott333@gmail.com> - 2026-06-25 16:01 -0500
Re: Disjunction introduction --- new premise from out of no where olcott <polcott333@gmail.com> - 2026-06-25 16:05 -0500
Re: Readings in (some of the) foundations of mathematics --- analytic/synthetic distinction Alan Mackenzie <acm@muc.de> - 2026-06-20 21:43 +0000
Re: Readings in (some of the) foundations of mathematics --- analytic/synthetic distinction olcott <polcott333@gmail.com> - 2026-06-20 17:47 -0500
Re: Readings in (some of the) foundations of mathematics --- analytic/synthetic distinction Alan Mackenzie <acm@muc.de> - 2026-06-21 11:26 +0000
Re: Readings in (some of the) foundations of mathematics --- analytic/synthetic distinction olcott <polcott333@gmail.com> - 2026-06-21 13:42 -0500
Re: Readings in (some of the) foundations of mathematics --- analytic/synthetic distinction phoenix <j63840576@gmail.com> - 2026-06-21 12:53 -0600
Re: Readings in (some of the) foundations of mathematics --- analytic/synthetic distinction Alan Mackenzie <acm@muc.de> - 2026-06-21 20:04 +0000
Re: Readings in (some of the) foundations of mathematics --- analytic/synthetic distinction olcott <polcott333@gmail.com> - 2026-06-21 15:42 -0500
Re: Readings in (some of the) foundations of mathematics --- analytic/synthetic distinction André G. Isaak <agisaak@gm.invalid> - 2026-06-21 15:08 -0600
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-21 18:02 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge André G. Isaak <agisaak@gm.invalid> - 2026-06-21 18:02 -0600
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge -- Kristen Welker olcott <polcott333@gmail.com> - 2026-06-21 19:12 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge -- Kristen Welker dbush <dbush.mobile@gmail.com> - 2026-06-21 20:20 -0400
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Mikko <mikko.levanto@iki.fi> - 2026-06-22 09:49 +0300
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-22 07:10 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Mikko <mikko.levanto@iki.fi> - 2026-06-23 09:06 +0300
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-23 09:48 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-23 08:53 -0700
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Mikko <mikko.levanto@iki.fi> - 2026-06-24 13:00 +0300
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-24 15:26 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Mikko <mikko.levanto@iki.fi> - 2026-06-25 10:21 +0300
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-25 11:14 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Mikko <mikko.levanto@iki.fi> - 2026-06-26 09:39 +0300
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-26 08:10 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge dbush <dbush.mobile@gmail.com> - 2026-06-26 09:20 -0400
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-26 08:45 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge dbush <dbush.mobile@gmail.com> - 2026-06-26 09:57 -0400
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-26 09:24 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge dbush <dbush.mobile@gmail.com> - 2026-06-26 12:08 -0400
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-26 12:22 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge dbush <dbush.mobile@gmail.com> - 2026-06-26 13:25 -0400
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-26 12:39 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge dbush <dbush.mobile@gmail.com> - 2026-06-26 13:42 -0400
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-26 12:53 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge dbush <dbush.mobile@gmail.com> - 2026-06-26 14:02 -0400
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge André G. Isaak <agisaak@gm.invalid> - 2026-06-26 12:14 -0600
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-26 13:48 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge dbush <dbush.mobile@gmail.com> - 2026-06-26 14:51 -0400
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-26 14:07 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge dbush <dbush.mobile@gmail.com> - 2026-06-26 15:17 -0400
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-26 14:38 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge dbush <dbush.mobile@gmail.com> - 2026-06-26 15:55 -0400
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-26 17:01 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge dbush <dbush.mobile@gmail.com> - 2026-06-26 18:08 -0400
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-26 17:58 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge dbush <dbush.mobile@gmail.com> - 2026-06-26 19:18 -0400
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-26 19:05 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge dbush <dbush.mobile@gmail.com> - 2026-06-26 20:23 -0400
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-26 19:48 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge dbush <dbush.mobile@gmail.com> - 2026-06-26 21:11 -0400
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-26 20:39 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge dbush <dbush.mobile@gmail.com> - 2026-06-26 21:51 -0400
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-26 21:00 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge polcott <polcott333@gmail.com> - 2026-06-27 08:34 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Mikko <mikko.levanto@iki.fi> - 2026-06-27 11:05 +0300
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge polcott <polcott333@gmail.com> - 2026-06-27 10:47 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-27 15:37 -0700
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-27 17:47 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-27 19:24 -0700
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-27 22:21 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-27 19:25 -0700
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Mikko <mikko.levanto@iki.fi> - 2026-06-28 11:22 +0300
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Mikko <mikko.levanto@iki.fi> - 2026-06-28 11:17 +0300
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Mikko <mikko.levanto@iki.fi> - 2026-06-27 10:48 +0300
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge polcott <polcott333@gmail.com> - 2026-06-27 10:45 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Mikko <mikko.levanto@iki.fi> - 2026-06-28 11:38 +0300
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Mikko <mikko.levanto@iki.fi> - 2026-06-27 10:35 +0300
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge polcott <polcott333@gmail.com> - 2026-06-27 10:43 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge dbush <dbush.mobile@gmail.com> - 2026-06-27 14:01 -0400
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-27 13:27 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge dbush <dbush.mobile@gmail.com> - 2026-06-27 14:29 -0400
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-27 13:38 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge dbush <dbush.mobile@gmail.com> - 2026-06-27 14:39 -0400
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-27 14:01 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge dbush <dbush.mobile@gmail.com> - 2026-06-27 15:04 -0400
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-27 14:16 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge dbush <dbush.mobile@gmail.com> - 2026-06-27 15:23 -0400
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-27 14:40 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge dbush <dbush.mobile@gmail.com> - 2026-06-27 15:54 -0400
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-27 15:04 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge dbush <dbush.mobile@gmail.com> - 2026-06-27 16:11 -0400
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-27 15:17 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge dbush <dbush.mobile@gmail.com> - 2026-06-27 16:22 -0400
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-27 15:27 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge dbush <dbush.mobile@gmail.com> - 2026-06-27 16:30 -0400
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge dbush <dbush.mobile@gmail.com> - 2026-06-27 16:36 -0400
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-27 15:52 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge dbush <dbush.mobile@gmail.com> - 2026-06-27 16:59 -0400
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-27 16:24 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge dbush <dbush.mobile@gmail.com> - 2026-06-27 17:50 -0400
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-27 17:11 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge dbush <dbush.mobile@gmail.com> - 2026-06-27 18:15 -0400
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-27 17:18 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge dbush <dbush.mobile@gmail.com> - 2026-06-27 18:21 -0400
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-27 17:29 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge dbush <dbush.mobile@gmail.com> - 2026-06-27 18:33 -0400
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-27 17:44 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge dbush <dbush.mobile@gmail.com> - 2026-06-27 18:53 -0400
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-27 18:27 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge dbush <dbush.mobile@gmail.com> - 2026-06-27 19:33 -0400
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-27 18:59 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge dbush <dbush.mobile@gmail.com> - 2026-06-27 21:13 -0400
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-27 20:33 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Mikko <mikko.levanto@iki.fi> - 2026-06-28 12:38 +0300
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Mikko <mikko.levanto@iki.fi> - 2026-06-28 12:31 +0300
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-28 22:12 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Mikko <mikko.levanto@iki.fi> - 2026-06-29 09:23 +0300
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-29 08:38 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Mikko <mikko.levanto@iki.fi> - 2026-06-30 10:48 +0300
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-30 08:43 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Mikko <mikko.levanto@iki.fi> - 2026-07-01 10:01 +0300
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-07-01 10:09 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Mikko <mikko.levanto@iki.fi> - 2026-06-30 11:43 +0300
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-30 09:22 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Mikko <mikko.levanto@iki.fi> - 2026-07-01 10:13 +0300
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-07-01 10:13 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Mikko <mikko.levanto@iki.fi> - 2026-07-02 09:44 +0300
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-07-02 09:45 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-07-02 08:16 -0700
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-07-02 11:47 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Mikko <mikko.levanto@iki.fi> - 2026-07-03 12:15 +0300
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Mikko <mikko.levanto@iki.fi> - 2026-07-03 11:41 +0300
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-07-03 10:23 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-07-03 10:34 -0700
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-07-03 13:17 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-07-03 13:36 -0700
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-07-03 18:14 -0700
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Mikko <mikko.levanto@iki.fi> - 2026-07-04 10:02 +0300
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Mikko <mikko.levanto@iki.fi> - 2026-07-04 09:58 +0300
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-07-04 08:24 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Mikko <mikko.levanto@iki.fi> - 2026-07-06 13:13 +0300
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Mikko <mikko.levanto@iki.fi> - 2026-07-03 12:39 +0300
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-07-03 11:43 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Mikko <mikko.levanto@iki.fi> - 2026-07-04 10:22 +0300
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-07-04 08:29 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Alan Mackenzie <acm@muc.de> - 2026-07-04 14:07 +0000
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-07-04 11:38 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Alan Mackenzie <acm@muc.de> - 2026-07-04 17:42 +0000
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Mikko <mikko.levanto@iki.fi> - 2026-07-06 10:10 +0300
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Mikko <mikko.levanto@iki.fi> - 2026-06-28 11:38 +0300
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge André G. Isaak <agisaak@gm.invalid> - 2026-06-27 13:40 -0600
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-27 14:46 -0500
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Mikko <mikko.levanto@iki.fi> - 2026-06-28 11:32 +0300
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge Alan Mackenzie <acm@muc.de> - 2026-06-22 12:47 +0000
Re: Readings in (some of the) foundations of mathematics --- tree of knowledge olcott <polcott333@gmail.com> - 2026-06-22 09:30 -0500
Re: Readings in (some of the) foundations of mathematics --- analytic/synthetic distinction Mikko <mikko.levanto@iki.fi> - 2026-06-22 10:23 +0300
Re: Readings in (some of the) foundations of mathematics --- analytic/synthetic distinction olcott <polcott333@gmail.com> - 2026-06-22 09:44 -0500
Re: Readings in (some of the) foundations of mathematics --- analytic/synthetic distinction Alan Mackenzie <acm@muc.de> - 2026-06-22 15:22 +0000
Re: Readings in (some of the) foundations of mathematics --- analytic/synthetic distinction olcott <polcott333@gmail.com> - 2026-06-22 10:36 -0500
Re: Readings in (some of the) foundations of mathematics --- analytic/synthetic distinction Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-22 12:07 -0700
Re: Readings in (some of the) foundations of mathematics --- analytic/synthetic distinction olcott <polcott333@gmail.com> - 2026-06-22 14:21 -0500
Re: Readings in (some of the) foundations of mathematics --- analytic/synthetic distinction Mikko <mikko.levanto@iki.fi> - 2026-06-23 09:15 +0300
Re: Readings in (some of the) foundations of mathematics --- analytic/synthetic distinction olcott <polcott333@gmail.com> - 2026-06-23 09:52 -0500
Re: Readings in (some of the) foundations of mathematics --- analytic/synthetic distinction Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-23 08:54 -0700
Re: Readings in (some of the) foundations of mathematics --- analytic/synthetic distinction Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-23 09:06 -0700
Re: Readings in (some of the) foundations of mathematics --- analytic/synthetic distinction olcott <polcott333@gmail.com> - 2026-06-23 11:56 -0500
Re: Readings in (some of the) foundations of mathematics --- analytic/synthetic distinction Mikko <mikko.levanto@iki.fi> - 2026-06-24 13:06 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-21 13:26 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-21 13:23 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-21 19:00 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-22 10:40 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-22 10:12 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Alan Mackenzie <acm@muc.de> - 2026-06-22 15:48 +0000
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-22 11:23 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Alan Mackenzie <acm@muc.de> - 2026-06-22 18:42 +0000
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-22 13:59 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Alan Mackenzie <acm@muc.de> - 2026-06-22 19:50 +0000
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-22 15:06 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Alan Mackenzie <acm@muc.de> - 2026-06-22 20:38 +0000
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-22 16:01 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-22 16:55 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-22 21:00 -0700
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-22 23:14 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-22 21:31 -0700
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-23 09:22 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-23 08:51 -0700
Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs olcott <polcott333@gmail.com> - 2026-06-23 11:54 -0500
Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-23 10:32 -0700
Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-23 10:58 -0700
Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs olcott <polcott333@gmail.com> - 2026-06-23 13:24 -0500
Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-27 07:26 -0700
Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs olcott <polcott333@gmail.com> - 2026-06-23 13:20 -0500
Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs Mikko <mikko.levanto@iki.fi> - 2026-06-24 13:13 +0300
Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs olcott <polcott333@gmail.com> - 2026-06-24 16:33 -0500
Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs phoenix <j63840576@gmail.com> - 2026-06-24 18:28 -0600
Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs Mikko <mikko.levanto@iki.fi> - 2026-06-25 10:29 +0300
Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs olcott <polcott333@gmail.com> - 2026-06-25 11:16 -0500
Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs Mikko <mikko.levanto@iki.fi> - 2026-06-26 09:45 +0300
Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs olcott <polcott333@gmail.com> - 2026-06-26 08:15 -0500
Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs Mikko <mikko.levanto@iki.fi> - 2026-06-27 11:13 +0300
Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-27 07:25 -0700
Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs polcott <polcott333@gmail.com> - 2026-06-27 10:53 -0500
Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs Mikko <mikko.levanto@iki.fi> - 2026-06-28 12:51 +0300
Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs olcott <polcott333@gmail.com> - 2026-06-30 09:53 -0500
Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-30 10:36 -0700
Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-30 19:47 -0700
Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs olcott <polcott333@gmail.com> - 2026-06-30 22:01 -0500
Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-07-01 05:13 -0700
Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs olcott <polcott333@gmail.com> - 2026-07-01 09:59 -0500
Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-07-01 10:00 -0700
DAG of all general knowledge that can be expressed in Language olcott <polcott333@gmail.com> - 2026-07-01 12:57 -0500
Re: DAG of all general knowledge that can be expressed in Language Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-07-01 12:31 -0700
Re: DAG of all general knowledge that can be expressed in Language "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2026-07-01 12:37 -0700
Re: DAG of all general knowledge that can be expressed in Language Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-07-01 13:16 -0700
Re: DAG of all general knowledge that can be expressed in Language "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2026-07-01 18:59 -0700
Re: DAG of all general knowledge that can be expressed in Language olcott <polcott333@gmail.com> - 2026-07-01 14:51 -0500
Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs Python <python@cccp.invalid> - 2026-06-23 21:04 +0000
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-22 21:16 -0700
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-06-22 21:28 -0700
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-22 15:08 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-23 09:17 -0500
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics Mikko <mikko.levanto@iki.fi> - 2026-06-23 09:26 +0300
Re: Ross A. Finlayson, readings in (some of the) foundations of mathematics olcott <polcott333@gmail.com> - 2026-06-23 09:55 -0500
Page 17 of 18 — ← Prev page 1 … 15 16 [17] 18 Next page →
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2026-06-23 09:22 -0500 |
| Message-ID | <111e4qm$2agun$2@dont-email.me> |
| In reply to | #141896 |
On 6/22/2026 11:31 PM, Ross Finlayson wrote: > On 06/22/2026 09:14 PM, olcott wrote: >> On 6/22/2026 11:00 PM, Ross Finlayson wrote: >>> On 06/22/2026 01:06 PM, olcott wrote: >>>> On 6/22/2026 2:50 PM, Alan Mackenzie wrote: >>>>> [ Followup-To: set ] >>>>> >>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>> On 6/22/2026 1:42 PM, Alan Mackenzie wrote: >>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>> On 6/22/2026 10:48 AM, Alan Mackenzie wrote: >>>>> >>>>>>>>> G is true. >>>>> >>>>>>>>> I put it to you you're lying again. No reputable mathematician >>>>>>>>> would >>>>>>>>> risk his reputation by saying false things. If Dag Prawitz really >>>>>>>>> did >>>>>>>>> "agree" (with whom?) that Gödel's sentence G is not true in Peano >>>>>>>>> Arithmetic, then produce a citation for this. >>>>> >>>>> >>>>>>>> He never gets to Gödel. He essentially says unprovable >>>>>>>> means untrue all the time for everything within his >>>>>>>> own Theory of Grounds of strict Proof Theoretic Semantics. >>>>> >>>>>>> You won't understand it, but that _is_ essentially Gödel's >>>>>>> Incompleteness >>>>>>> Theorem. It is a statement that any sufficiently powerful system >>>>>>> can >>>>>>> express true things it can't prove. So Dag Prawitz, had he been >>>>>>> saying >>>>>>> the things you falsely attributed to him, would certainly have >>>>>>> "got" to >>>>>>> Gödel, and would have understood full well what he was saying. >>>>> >>>>> >>>>>> You did not pay close enough attention to my exact words. >>>>> >>>>> I was right, you didn't understand it. >>>>> >>>> >>>> >>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>> >>> >>> Yeah, I'm pretty sure that "Dag Prawitz says what Dag Prawitz says", >>> and furthermore "Dag Prawitz doesn't say what Dag Prawitz doesn't say", >>> then looking a bit into his tremendous volume of works, >>> he talks about "natural deduction" then specifically an "inverse >>> principle" so I think these are key aspects of fundamental logic. >>> >>> https://www.researchgate.net/ >>> publication/233365263_On_Inversion_Principles >>> >>> >>> "On Inversion Principles >>> >>> Enrico Moriconi∗Laura Tesconi† >>> May 8, 2007 >>> >>> Abstract >>> The idea of an “inversion principle”, and the name itself, originated in >>> the work of Paul Lorenzen in the 1950s, as a method to generate new ad- >>> missible rules within a certain syntactic context. Some fifteen years >>> later, the idea was taken up by Dag Prawitz to devise a strategy of >>> normalization for natural deduction calculi (this being an analogue of >>> Gentzen’s cut-elimination theorem for sequent calculi). Later, Prawitz >>> used the inversion principle again, attributing it with a semantic role. >>> Still working in natural deduction calculi, he formulated a general type >>> of schematic Introduction rules to be matched—thanks to the idea >>> supporting the inversion principle — by a corresponding general >>> schematic Elimination rule. This was an attempt to provide a solution to >>> the problem suggested by the often quoted note of Gentzen. According to >>> Gentzen “it should be possible to display the elimination rules as >>> unique functions of the corresponding introduction rules on the basis of >>> certain requirements.” Many people have since worked on this topic, >>> which can be appropriately seen as the birthplace of what are now >>> referred to as “general elimination rules”, recently studied thoroughly >>> by Sara Negri and Jan von Plato. In this paper, we retrace the main >>> threads of this chapter of proof-theoretical investigation, using >>> Lorenzen’s original framework as a general guide" >>> >>> >>> >>> Hm, "general elimination rules", seem derivable from De Morgan's laws, >>> and that being the usual account of naive deductive analysis, then since >>> "natural deduction", which here is held as part of the theory >>> since it's naturally logical, then has for Gentzen that besides Kripke >>> afterward there's also Sheffer and Chwistek before, and instead of >>> Montague for semantics there's Herbrand for semantics, so, what to do >>> about "inversion principle" is here that the thea-theory has that it's >>> what subsumes "non-contradiction principle", here hoping that the >>> interpretation aligns and thusly that "principle of inversion" wouldn't >>> need dis-ambiguation from "inversion principle". >>> >>> >>> https://www.tandfonline.com/doi/abs/10.1080/01445340701830334 >>> >>> >>> https://www.strandbooks.com/natural-deduction-a-proof-theoretical- >>> study-9780486446554.html >>> >>> "... [Prawitz'] inversion principle constitutes the foundation of most >>> modern accounts of proof-theoretic semantics." >>> >>> >>> >>> I already have a principle of inversion and furthermore a principle of >>> thorough reason as subsuming principles of non-contradiction and what >>> suffices, so, I'll be curious then about what to make of Prawitz' >>> "inversion principle" since Lorenzen. >>> >>> >>> Of course the concept of an "inversion principle" is as old as the >>> oldest account of Western philosophy like Heraclitus with dual monism. >>> In fact by definition it's about the most basic aspect of contemplation >>> and deliberation in abstraction of looking at both sides of issues and >>> resolving inductive impasses with analytical bridges after complementary >>> duals. >>> >>> >>> https://arxiv.org/abs/2112.14967 >>> >>> "Prawitz formulated the so-called inversion principle as one of the >>> characteristic features of Gentzen's intuitionistic natural deduction. >>> In the literature on proof-theoretic semantics, this principle is often >>> coupled with another that is called the recovery principle. By adopting >>> the Computational Ludics framework, we reformulate these principles into >>> one and the same condition, which we call the harmony condition. We show >>> that this reformulation allows us to reveal two intuitive ideas standing >>> behind these principles: the idea of "containment" present in the >>> inversion principle, and the idea that the recovery principle is the >>> "converse" of the inversion principle. We also formulate two other >>> conditions in the Computational Ludics framework, and we show that each >>> of them is equivalent to the harmony condition." >>> >>> >>> >>> The "ludicus" is Latin and for accounts of wisdom and knowledge. >>> >>> >>> "In particular, by taking inspiration from the >>> Brouwer-Heyting-Kolmogorov explanation of logical connectives, >>> proof-theoretic semantics rests on the idea that we know the meaning of >>> a compound sentence when we know what counts as a canonical proof of it. >>> And if proofs are formalised within the framework of natural deduction, >>> then a canonical proof of a sentence A is nothing but a closed >>> derivation ending with an introduction rule of the main connective of >>> A." >>> >>> >>> The "canonical proofs" are not unique, in any system strong enough >>> to make for infinitary reasoning and super-classical results requiring >>> analytical bridges about infinity and continuity. >>> >> >> It is the role that "canonical proofs" play in >> Truth as an Epistemic Notion >> https://link.springer.com/article/10.1007/s11245-011-9107-6 >> That is the most important gist of his whole work. >> >> He later goes on to develop and further elaborate his >> Theory of Grounds. >> >> Atomic Systems in Proof-Theoretic Semantics: Two Approaches >> Thomas Piecha & Peter Schroeder-Heister do this same sort of >> thing two different ways. >> >> >> > > Furthermore I say there are "canonical proofs" of inductive sorts that > make contradictions and thusly destroy each other. > > Clearly you have no idea what Dag Prawitz means by "canonical proofs". Go find out and then get back to me. > This is where "the thorough" and "analytical bridges" make repairs > of what otherwise is flawed, or for hard constructivist realist > structuralist model theorists: not-theories (examples of wrong). > > -- Copyright 2026 Olcott My 28 year goal has been to make "true on the basis of meaning expressed in language" reliably computable for the entire body of knowledge. The complete structure of this system is now defined. The entire body of knowledge expressed in language is comprised of two types of relations between finite strings: (a) *Axioms* Expressions of language that are stipulated to be true. My system bridges the analytic/synthetic distinction by expressly encoding all empirical "atomic facts" in a formal language such as CycL of the Cyc project. (b) *Inference Rules* Expressions of language that are semantically entailed syntactically from (a) and/or (b).
[toc] | [prev] | [next] | [standalone]
| From | Ross Finlayson <ross.a.finlayson@gmail.com> |
|---|---|
| Date | 2026-06-23 08:51 -0700 |
| Message-ID | <UnWdnYaP6Z0KNqf3nZ2dnZfqnPSdnZ2d@giganews.com> |
| In reply to | #141910 |
On 06/23/2026 07:22 AM, olcott wrote: > On 6/22/2026 11:31 PM, Ross Finlayson wrote: >> On 06/22/2026 09:14 PM, olcott wrote: >>> On 6/22/2026 11:00 PM, Ross Finlayson wrote: >>>> On 06/22/2026 01:06 PM, olcott wrote: >>>>> On 6/22/2026 2:50 PM, Alan Mackenzie wrote: >>>>>> [ Followup-To: set ] >>>>>> >>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>> On 6/22/2026 1:42 PM, Alan Mackenzie wrote: >>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>> On 6/22/2026 10:48 AM, Alan Mackenzie wrote: >>>>>> >>>>>>>>>> G is true. >>>>>> >>>>>>>>>> I put it to you you're lying again. No reputable mathematician >>>>>>>>>> would >>>>>>>>>> risk his reputation by saying false things. If Dag Prawitz >>>>>>>>>> really >>>>>>>>>> did >>>>>>>>>> "agree" (with whom?) that Gödel's sentence G is not true in Peano >>>>>>>>>> Arithmetic, then produce a citation for this. >>>>>> >>>>>> >>>>>>>>> He never gets to Gödel. He essentially says unprovable >>>>>>>>> means untrue all the time for everything within his >>>>>>>>> own Theory of Grounds of strict Proof Theoretic Semantics. >>>>>> >>>>>>>> You won't understand it, but that _is_ essentially Gödel's >>>>>>>> Incompleteness >>>>>>>> Theorem. It is a statement that any sufficiently powerful >>>>>>>> system can >>>>>>>> express true things it can't prove. So Dag Prawitz, had he been >>>>>>>> saying >>>>>>>> the things you falsely attributed to him, would certainly have >>>>>>>> "got" to >>>>>>>> Gödel, and would have understood full well what he was saying. >>>>>> >>>>>> >>>>>>> You did not pay close enough attention to my exact words. >>>>>> >>>>>> I was right, you didn't understand it. >>>>>> >>>>> >>>>> >>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>> >>>> >>>> Yeah, I'm pretty sure that "Dag Prawitz says what Dag Prawitz says", >>>> and furthermore "Dag Prawitz doesn't say what Dag Prawitz doesn't say", >>>> then looking a bit into his tremendous volume of works, >>>> he talks about "natural deduction" then specifically an "inverse >>>> principle" so I think these are key aspects of fundamental logic. >>>> >>>> https://www.researchgate.net/ >>>> publication/233365263_On_Inversion_Principles >>>> >>>> >>>> "On Inversion Principles >>>> >>>> Enrico Moriconi∗Laura Tesconi† >>>> May 8, 2007 >>>> >>>> Abstract >>>> The idea of an “inversion principle”, and the name itself, >>>> originated in >>>> the work of Paul Lorenzen in the 1950s, as a method to generate new ad- >>>> missible rules within a certain syntactic context. Some fifteen years >>>> later, the idea was taken up by Dag Prawitz to devise a strategy of >>>> normalization for natural deduction calculi (this being an analogue of >>>> Gentzen’s cut-elimination theorem for sequent calculi). Later, Prawitz >>>> used the inversion principle again, attributing it with a semantic >>>> role. >>>> Still working in natural deduction calculi, he formulated a general >>>> type >>>> of schematic Introduction rules to be matched—thanks to the idea >>>> supporting the inversion principle — by a corresponding general >>>> schematic Elimination rule. This was an attempt to provide a >>>> solution to >>>> the problem suggested by the often quoted note of Gentzen. According to >>>> Gentzen “it should be possible to display the elimination rules as >>>> unique functions of the corresponding introduction rules on the >>>> basis of >>>> certain requirements.” Many people have since worked on this topic, >>>> which can be appropriately seen as the birthplace of what are now >>>> referred to as “general elimination rules”, recently studied thoroughly >>>> by Sara Negri and Jan von Plato. In this paper, we retrace the main >>>> threads of this chapter of proof-theoretical investigation, using >>>> Lorenzen’s original framework as a general guide" >>>> >>>> >>>> >>>> Hm, "general elimination rules", seem derivable from De Morgan's laws, >>>> and that being the usual account of naive deductive analysis, then >>>> since >>>> "natural deduction", which here is held as part of the theory >>>> since it's naturally logical, then has for Gentzen that besides Kripke >>>> afterward there's also Sheffer and Chwistek before, and instead of >>>> Montague for semantics there's Herbrand for semantics, so, what to do >>>> about "inversion principle" is here that the thea-theory has that it's >>>> what subsumes "non-contradiction principle", here hoping that the >>>> interpretation aligns and thusly that "principle of inversion" wouldn't >>>> need dis-ambiguation from "inversion principle". >>>> >>>> >>>> https://www.tandfonline.com/doi/abs/10.1080/01445340701830334 >>>> >>>> >>>> https://www.strandbooks.com/natural-deduction-a-proof-theoretical- >>>> study-9780486446554.html >>>> >>>> "... [Prawitz'] inversion principle constitutes the foundation of most >>>> modern accounts of proof-theoretic semantics." >>>> >>>> >>>> >>>> I already have a principle of inversion and furthermore a principle of >>>> thorough reason as subsuming principles of non-contradiction and what >>>> suffices, so, I'll be curious then about what to make of Prawitz' >>>> "inversion principle" since Lorenzen. >>>> >>>> >>>> Of course the concept of an "inversion principle" is as old as the >>>> oldest account of Western philosophy like Heraclitus with dual monism. >>>> In fact by definition it's about the most basic aspect of contemplation >>>> and deliberation in abstraction of looking at both sides of issues and >>>> resolving inductive impasses with analytical bridges after >>>> complementary >>>> duals. >>>> >>>> >>>> https://arxiv.org/abs/2112.14967 >>>> >>>> "Prawitz formulated the so-called inversion principle as one of the >>>> characteristic features of Gentzen's intuitionistic natural deduction. >>>> In the literature on proof-theoretic semantics, this principle is often >>>> coupled with another that is called the recovery principle. By adopting >>>> the Computational Ludics framework, we reformulate these principles >>>> into >>>> one and the same condition, which we call the harmony condition. We >>>> show >>>> that this reformulation allows us to reveal two intuitive ideas >>>> standing >>>> behind these principles: the idea of "containment" present in the >>>> inversion principle, and the idea that the recovery principle is the >>>> "converse" of the inversion principle. We also formulate two other >>>> conditions in the Computational Ludics framework, and we show that each >>>> of them is equivalent to the harmony condition." >>>> >>>> >>>> >>>> The "ludicus" is Latin and for accounts of wisdom and knowledge. >>>> >>>> >>>> "In particular, by taking inspiration from the >>>> Brouwer-Heyting-Kolmogorov explanation of logical connectives, >>>> proof-theoretic semantics rests on the idea that we know the meaning of >>>> a compound sentence when we know what counts as a canonical proof of >>>> it. >>>> And if proofs are formalised within the framework of natural deduction, >>>> then a canonical proof of a sentence A is nothing but a closed >>>> derivation ending with an introduction rule of the main connective >>>> of A." >>>> >>>> >>>> The "canonical proofs" are not unique, in any system strong enough >>>> to make for infinitary reasoning and super-classical results requiring >>>> analytical bridges about infinity and continuity. >>>> >>> >>> It is the role that "canonical proofs" play in >>> Truth as an Epistemic Notion >>> https://link.springer.com/article/10.1007/s11245-011-9107-6 >>> That is the most important gist of his whole work. >>> >>> He later goes on to develop and further elaborate his >>> Theory of Grounds. >>> >>> Atomic Systems in Proof-Theoretic Semantics: Two Approaches >>> Thomas Piecha & Peter Schroeder-Heister do this same sort of >>> thing two different ways. >>> >>> >>> >> >> Furthermore I say there are "canonical proofs" of inductive sorts that >> make contradictions and thusly destroy each other. >> >> > > Clearly you have no idea what Dag Prawitz means by "canonical proofs". > Go find out and then get back to me. > >> This is where "the thorough" and "analytical bridges" make repairs >> of what otherwise is flawed, or for hard constructivist realist >> structuralist model theorists: not-theories (examples of wrong). >> >> > > Induction and counter-induction contradict each other, it's simple, it's the grounds for most things called "paradox". "Proof-theoretic semantics along Dummett’s and Prawitz’s lines arguably does not go any further than intuitionist logic. From their perspective, the rules governing classical negation are defective. Advocates of bilateralism claim that this situation is rectified in their framework." - Kuerbis, "Normalisation for Bilateral Classical Logic with some Philosophical Remarks" Now it seems more clear some of PO's problems (mistakes) with bi-valent statements and bi-lateral deductions, is that he thinks that applies to _questions_ not just _statements_, and only makes one bi-lateral account a uni-lateral account. I.e., "the time is on the clock" is a sentence with a bi-valent truth value, while "what time is it?" is not a sentence with a bi-valent truth value, as with regards to "what time is is: is the time on the clock", is again - point being PO's howler fallacies include not distinguishing declaratives and interrogatives. Appealing to the authority of Prawitz for "containment" while ignoring "recovery" and for "elimination rules" while ignoring "inversion rules" is a mis-representation, and worse than a half-account reductionism. Then, it seems a lot of logicians are sort of hiding in plain sight in the intuitionistic setting of Prawitz after Lorentzen et alia as a refuge from "20'th century quasi-modal logic and the Tarskian", and then later extensions like homotopy type theory are simply enough old-wrapped-as-new plagiarism of a sort about intuitionistic type theory, which itself is constructivist. As Piccolomini's slides introduce about the epistemic problems, they can have simple answers like I already provided above. bi-valent <-> bi-lateral containment <-> recovery elimination <-> inversion Prawitz et alia's dichotomies aren't themselves eliminable, and any may re-introduce them all the time.
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2026-06-23 11:54 -0500 |
| Subject | Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs |
| Message-ID | <111ednn$2dh0p$1@dont-email.me> |
| In reply to | #141918 |
On 6/23/2026 10:51 AM, Ross Finlayson wrote: > On 06/23/2026 07:22 AM, olcott wrote: >> On 6/22/2026 11:31 PM, Ross Finlayson wrote: >>> On 06/22/2026 09:14 PM, olcott wrote: >>>> On 6/22/2026 11:00 PM, Ross Finlayson wrote: >>>>> On 06/22/2026 01:06 PM, olcott wrote: >>>>>> On 6/22/2026 2:50 PM, Alan Mackenzie wrote: >>>>>>> [ Followup-To: set ] >>>>>>> >>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>> On 6/22/2026 1:42 PM, Alan Mackenzie wrote: >>>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>>> On 6/22/2026 10:48 AM, Alan Mackenzie wrote: >>>>>>> >>>>>>>>>>> G is true. >>>>>>> >>>>>>>>>>> I put it to you you're lying again. No reputable mathematician >>>>>>>>>>> would >>>>>>>>>>> risk his reputation by saying false things. If Dag Prawitz >>>>>>>>>>> really >>>>>>>>>>> did >>>>>>>>>>> "agree" (with whom?) that Gödel's sentence G is not true in >>>>>>>>>>> Peano >>>>>>>>>>> Arithmetic, then produce a citation for this. >>>>>>> >>>>>>> >>>>>>>>>> He never gets to Gödel. He essentially says unprovable >>>>>>>>>> means untrue all the time for everything within his >>>>>>>>>> own Theory of Grounds of strict Proof Theoretic Semantics. >>>>>>> >>>>>>>>> You won't understand it, but that _is_ essentially Gödel's >>>>>>>>> Incompleteness >>>>>>>>> Theorem. It is a statement that any sufficiently powerful >>>>>>>>> system can >>>>>>>>> express true things it can't prove. So Dag Prawitz, had he been >>>>>>>>> saying >>>>>>>>> the things you falsely attributed to him, would certainly have >>>>>>>>> "got" to >>>>>>>>> Gödel, and would have understood full well what he was saying. >>>>>>> >>>>>>> >>>>>>>> You did not pay close enough attention to my exact words. >>>>>>> >>>>>>> I was right, you didn't understand it. >>>>>>> >>>>>> >>>>>> >>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>> >>>>> >>>>> Yeah, I'm pretty sure that "Dag Prawitz says what Dag Prawitz says", >>>>> and furthermore "Dag Prawitz doesn't say what Dag Prawitz doesn't >>>>> say", >>>>> then looking a bit into his tremendous volume of works, >>>>> he talks about "natural deduction" then specifically an "inverse >>>>> principle" so I think these are key aspects of fundamental logic. >>>>> >>>>> https://www.researchgate.net/ >>>>> publication/233365263_On_Inversion_Principles >>>>> >>>>> >>>>> "On Inversion Principles >>>>> >>>>> Enrico Moriconi∗Laura Tesconi† >>>>> May 8, 2007 >>>>> >>>>> Abstract >>>>> The idea of an “inversion principle”, and the name itself, >>>>> originated in >>>>> the work of Paul Lorenzen in the 1950s, as a method to generate new >>>>> ad- >>>>> missible rules within a certain syntactic context. Some fifteen years >>>>> later, the idea was taken up by Dag Prawitz to devise a strategy of >>>>> normalization for natural deduction calculi (this being an analogue of >>>>> Gentzen’s cut-elimination theorem for sequent calculi). Later, Prawitz >>>>> used the inversion principle again, attributing it with a semantic >>>>> role. >>>>> Still working in natural deduction calculi, he formulated a general >>>>> type >>>>> of schematic Introduction rules to be matched—thanks to the idea >>>>> supporting the inversion principle — by a corresponding general >>>>> schematic Elimination rule. This was an attempt to provide a >>>>> solution to >>>>> the problem suggested by the often quoted note of Gentzen. >>>>> According to >>>>> Gentzen “it should be possible to display the elimination rules as >>>>> unique functions of the corresponding introduction rules on the >>>>> basis of >>>>> certain requirements.” Many people have since worked on this topic, >>>>> which can be appropriately seen as the birthplace of what are now >>>>> referred to as “general elimination rules”, recently studied >>>>> thoroughly >>>>> by Sara Negri and Jan von Plato. In this paper, we retrace the main >>>>> threads of this chapter of proof-theoretical investigation, using >>>>> Lorenzen’s original framework as a general guide" >>>>> >>>>> >>>>> >>>>> Hm, "general elimination rules", seem derivable from De Morgan's laws, >>>>> and that being the usual account of naive deductive analysis, then >>>>> since >>>>> "natural deduction", which here is held as part of the theory >>>>> since it's naturally logical, then has for Gentzen that besides Kripke >>>>> afterward there's also Sheffer and Chwistek before, and instead of >>>>> Montague for semantics there's Herbrand for semantics, so, what to do >>>>> about "inversion principle" is here that the thea-theory has that it's >>>>> what subsumes "non-contradiction principle", here hoping that the >>>>> interpretation aligns and thusly that "principle of inversion" >>>>> wouldn't >>>>> need dis-ambiguation from "inversion principle". >>>>> >>>>> >>>>> https://www.tandfonline.com/doi/abs/10.1080/01445340701830334 >>>>> >>>>> >>>>> https://www.strandbooks.com/natural-deduction-a-proof-theoretical- >>>>> study-9780486446554.html >>>>> >>>>> "... [Prawitz'] inversion principle constitutes the foundation of most >>>>> modern accounts of proof-theoretic semantics." >>>>> >>>>> >>>>> >>>>> I already have a principle of inversion and furthermore a principle of >>>>> thorough reason as subsuming principles of non-contradiction and what >>>>> suffices, so, I'll be curious then about what to make of Prawitz' >>>>> "inversion principle" since Lorenzen. >>>>> >>>>> >>>>> Of course the concept of an "inversion principle" is as old as the >>>>> oldest account of Western philosophy like Heraclitus with dual monism. >>>>> In fact by definition it's about the most basic aspect of >>>>> contemplation >>>>> and deliberation in abstraction of looking at both sides of issues and >>>>> resolving inductive impasses with analytical bridges after >>>>> complementary >>>>> duals. >>>>> >>>>> >>>>> https://arxiv.org/abs/2112.14967 >>>>> >>>>> "Prawitz formulated the so-called inversion principle as one of the >>>>> characteristic features of Gentzen's intuitionistic natural deduction. >>>>> In the literature on proof-theoretic semantics, this principle is >>>>> often >>>>> coupled with another that is called the recovery principle. By >>>>> adopting >>>>> the Computational Ludics framework, we reformulate these principles >>>>> into >>>>> one and the same condition, which we call the harmony condition. We >>>>> show >>>>> that this reformulation allows us to reveal two intuitive ideas >>>>> standing >>>>> behind these principles: the idea of "containment" present in the >>>>> inversion principle, and the idea that the recovery principle is the >>>>> "converse" of the inversion principle. We also formulate two other >>>>> conditions in the Computational Ludics framework, and we show that >>>>> each >>>>> of them is equivalent to the harmony condition." >>>>> >>>>> >>>>> >>>>> The "ludicus" is Latin and for accounts of wisdom and knowledge. >>>>> >>>>> >>>>> "In particular, by taking inspiration from the >>>>> Brouwer-Heyting-Kolmogorov explanation of logical connectives, >>>>> proof-theoretic semantics rests on the idea that we know the >>>>> meaning of >>>>> a compound sentence when we know what counts as a canonical proof of >>>>> it. >>>>> And if proofs are formalised within the framework of natural >>>>> deduction, >>>>> then a canonical proof of a sentence A is nothing but a closed >>>>> derivation ending with an introduction rule of the main connective >>>>> of A." >>>>> >>>>> >>>>> The "canonical proofs" are not unique, in any system strong enough >>>>> to make for infinitary reasoning and super-classical results requiring >>>>> analytical bridges about infinity and continuity. >>>>> >>>> >>>> It is the role that "canonical proofs" play in >>>> Truth as an Epistemic Notion >>>> https://link.springer.com/article/10.1007/s11245-011-9107-6 >>>> That is the most important gist of his whole work. >>>> >>>> He later goes on to develop and further elaborate his >>>> Theory of Grounds. >>>> >>>> Atomic Systems in Proof-Theoretic Semantics: Two Approaches >>>> Thomas Piecha & Peter Schroeder-Heister do this same sort of >>>> thing two different ways. >>>> >>>> >>>> >>> >>> Furthermore I say there are "canonical proofs" of inductive sorts that >>> make contradictions and thusly destroy each other. >>> >>> >> >> Clearly you have no idea what Dag Prawitz means by "canonical proofs". >> Go find out and then get back to me. >> >>> This is where "the thorough" and "analytical bridges" make repairs >>> of what otherwise is flawed, or for hard constructivist realist >>> structuralist model theorists: not-theories (examples of wrong). >>> >>> >> >> > > > Induction and counter-induction contradict each other, it's simple, > it's the grounds for most things called "paradox". > > % This sentence is not true. ?- LP = not(true(LP)). LP = not(true(LP)). ?- unify_with_occurs_check(LP, not(true(LP))). false. After you totally understand how and why the proof theoretic semantics of that is correct and resolves the Liar Paradox get back to me. The essential principle involved that I derived in my own Minimal Type Theory before I knew that Prolog could do the same thing is that: When the directed graph of the evaluation sequence of an expression contains a cycle then the input is determined to be incoherent on the basis that its proof would never terminate. Proof Theoretic Semantics does this exact same thing. Don't get back to me until you attain the required prerequisites. I am sure that you already know all about cycles in directed graphs. -- Copyright 2026 Olcott My 28 year goal has been to make "true on the basis of meaning expressed in language" reliably computable for the entire body of knowledge. The complete structure of this system is now defined. The entire body of knowledge expressed in language is comprised of two types of relations between finite strings: (a) *Axioms* Expressions of language that are stipulated to be true. My system bridges the analytic/synthetic distinction by expressly encoding all empirical "atomic facts" in a formal language such as CycL of the Cyc project. (b) *Inference Rules* Expressions of language that are semantically entailed syntactically from (a) and/or (b).
[toc] | [prev] | [next] | [standalone]
| From | Ross Finlayson <ross.a.finlayson@gmail.com> |
|---|---|
| Date | 2026-06-23 10:32 -0700 |
| Subject | Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs |
| Message-ID | <ID-dnd_dyvaCXqf3nZ2dnZfqnPRi4p2d@giganews.com> |
| In reply to | #141922 |
On 06/23/2026 09:54 AM, olcott wrote: > On 6/23/2026 10:51 AM, Ross Finlayson wrote: >> On 06/23/2026 07:22 AM, olcott wrote: >>> On 6/22/2026 11:31 PM, Ross Finlayson wrote: >>>> On 06/22/2026 09:14 PM, olcott wrote: >>>>> On 6/22/2026 11:00 PM, Ross Finlayson wrote: >>>>>> On 06/22/2026 01:06 PM, olcott wrote: >>>>>>> On 6/22/2026 2:50 PM, Alan Mackenzie wrote: >>>>>>>> [ Followup-To: set ] >>>>>>>> >>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>> On 6/22/2026 1:42 PM, Alan Mackenzie wrote: >>>>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>>>> On 6/22/2026 10:48 AM, Alan Mackenzie wrote: >>>>>>>> >>>>>>>>>>>> G is true. >>>>>>>> >>>>>>>>>>>> I put it to you you're lying again. No reputable mathematician >>>>>>>>>>>> would >>>>>>>>>>>> risk his reputation by saying false things. If Dag Prawitz >>>>>>>>>>>> really >>>>>>>>>>>> did >>>>>>>>>>>> "agree" (with whom?) that Gödel's sentence G is not true in >>>>>>>>>>>> Peano >>>>>>>>>>>> Arithmetic, then produce a citation for this. >>>>>>>> >>>>>>>> >>>>>>>>>>> He never gets to Gödel. He essentially says unprovable >>>>>>>>>>> means untrue all the time for everything within his >>>>>>>>>>> own Theory of Grounds of strict Proof Theoretic Semantics. >>>>>>>> >>>>>>>>>> You won't understand it, but that _is_ essentially Gödel's >>>>>>>>>> Incompleteness >>>>>>>>>> Theorem. It is a statement that any sufficiently powerful >>>>>>>>>> system can >>>>>>>>>> express true things it can't prove. So Dag Prawitz, had he been >>>>>>>>>> saying >>>>>>>>>> the things you falsely attributed to him, would certainly have >>>>>>>>>> "got" to >>>>>>>>>> Gödel, and would have understood full well what he was saying. >>>>>>>> >>>>>>>> >>>>>>>>> You did not pay close enough attention to my exact words. >>>>>>>> >>>>>>>> I was right, you didn't understand it. >>>>>>>> >>>>>>> >>>>>>> >>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>> >>>>>> >>>>>> Yeah, I'm pretty sure that "Dag Prawitz says what Dag Prawitz says", >>>>>> and furthermore "Dag Prawitz doesn't say what Dag Prawitz doesn't >>>>>> say", >>>>>> then looking a bit into his tremendous volume of works, >>>>>> he talks about "natural deduction" then specifically an "inverse >>>>>> principle" so I think these are key aspects of fundamental logic. >>>>>> >>>>>> https://www.researchgate.net/ >>>>>> publication/233365263_On_Inversion_Principles >>>>>> >>>>>> >>>>>> "On Inversion Principles >>>>>> >>>>>> Enrico Moriconi∗Laura Tesconi† >>>>>> May 8, 2007 >>>>>> >>>>>> Abstract >>>>>> The idea of an “inversion principle”, and the name itself, >>>>>> originated in >>>>>> the work of Paul Lorenzen in the 1950s, as a method to generate >>>>>> new ad- >>>>>> missible rules within a certain syntactic context. Some fifteen years >>>>>> later, the idea was taken up by Dag Prawitz to devise a strategy of >>>>>> normalization for natural deduction calculi (this being an >>>>>> analogue of >>>>>> Gentzen’s cut-elimination theorem for sequent calculi). Later, >>>>>> Prawitz >>>>>> used the inversion principle again, attributing it with a semantic >>>>>> role. >>>>>> Still working in natural deduction calculi, he formulated a general >>>>>> type >>>>>> of schematic Introduction rules to be matched—thanks to the idea >>>>>> supporting the inversion principle — by a corresponding general >>>>>> schematic Elimination rule. This was an attempt to provide a >>>>>> solution to >>>>>> the problem suggested by the often quoted note of Gentzen. >>>>>> According to >>>>>> Gentzen “it should be possible to display the elimination rules as >>>>>> unique functions of the corresponding introduction rules on the >>>>>> basis of >>>>>> certain requirements.” Many people have since worked on this topic, >>>>>> which can be appropriately seen as the birthplace of what are now >>>>>> referred to as “general elimination rules”, recently studied >>>>>> thoroughly >>>>>> by Sara Negri and Jan von Plato. In this paper, we retrace the main >>>>>> threads of this chapter of proof-theoretical investigation, using >>>>>> Lorenzen’s original framework as a general guide" >>>>>> >>>>>> >>>>>> >>>>>> Hm, "general elimination rules", seem derivable from De Morgan's >>>>>> laws, >>>>>> and that being the usual account of naive deductive analysis, then >>>>>> since >>>>>> "natural deduction", which here is held as part of the theory >>>>>> since it's naturally logical, then has for Gentzen that besides >>>>>> Kripke >>>>>> afterward there's also Sheffer and Chwistek before, and instead of >>>>>> Montague for semantics there's Herbrand for semantics, so, what to do >>>>>> about "inversion principle" is here that the thea-theory has that >>>>>> it's >>>>>> what subsumes "non-contradiction principle", here hoping that the >>>>>> interpretation aligns and thusly that "principle of inversion" >>>>>> wouldn't >>>>>> need dis-ambiguation from "inversion principle". >>>>>> >>>>>> >>>>>> https://www.tandfonline.com/doi/abs/10.1080/01445340701830334 >>>>>> >>>>>> >>>>>> https://www.strandbooks.com/natural-deduction-a-proof-theoretical- >>>>>> study-9780486446554.html >>>>>> >>>>>> "... [Prawitz'] inversion principle constitutes the foundation of >>>>>> most >>>>>> modern accounts of proof-theoretic semantics." >>>>>> >>>>>> >>>>>> >>>>>> I already have a principle of inversion and furthermore a >>>>>> principle of >>>>>> thorough reason as subsuming principles of non-contradiction and what >>>>>> suffices, so, I'll be curious then about what to make of Prawitz' >>>>>> "inversion principle" since Lorenzen. >>>>>> >>>>>> >>>>>> Of course the concept of an "inversion principle" is as old as the >>>>>> oldest account of Western philosophy like Heraclitus with dual >>>>>> monism. >>>>>> In fact by definition it's about the most basic aspect of >>>>>> contemplation >>>>>> and deliberation in abstraction of looking at both sides of issues >>>>>> and >>>>>> resolving inductive impasses with analytical bridges after >>>>>> complementary >>>>>> duals. >>>>>> >>>>>> >>>>>> https://arxiv.org/abs/2112.14967 >>>>>> >>>>>> "Prawitz formulated the so-called inversion principle as one of the >>>>>> characteristic features of Gentzen's intuitionistic natural >>>>>> deduction. >>>>>> In the literature on proof-theoretic semantics, this principle is >>>>>> often >>>>>> coupled with another that is called the recovery principle. By >>>>>> adopting >>>>>> the Computational Ludics framework, we reformulate these principles >>>>>> into >>>>>> one and the same condition, which we call the harmony condition. We >>>>>> show >>>>>> that this reformulation allows us to reveal two intuitive ideas >>>>>> standing >>>>>> behind these principles: the idea of "containment" present in the >>>>>> inversion principle, and the idea that the recovery principle is the >>>>>> "converse" of the inversion principle. We also formulate two other >>>>>> conditions in the Computational Ludics framework, and we show that >>>>>> each >>>>>> of them is equivalent to the harmony condition." >>>>>> >>>>>> >>>>>> >>>>>> The "ludicus" is Latin and for accounts of wisdom and knowledge. >>>>>> >>>>>> >>>>>> "In particular, by taking inspiration from the >>>>>> Brouwer-Heyting-Kolmogorov explanation of logical connectives, >>>>>> proof-theoretic semantics rests on the idea that we know the >>>>>> meaning of >>>>>> a compound sentence when we know what counts as a canonical proof of >>>>>> it. >>>>>> And if proofs are formalised within the framework of natural >>>>>> deduction, >>>>>> then a canonical proof of a sentence A is nothing but a closed >>>>>> derivation ending with an introduction rule of the main connective >>>>>> of A." >>>>>> >>>>>> >>>>>> The "canonical proofs" are not unique, in any system strong enough >>>>>> to make for infinitary reasoning and super-classical results >>>>>> requiring >>>>>> analytical bridges about infinity and continuity. >>>>>> >>>>> >>>>> It is the role that "canonical proofs" play in >>>>> Truth as an Epistemic Notion >>>>> https://link.springer.com/article/10.1007/s11245-011-9107-6 >>>>> That is the most important gist of his whole work. >>>>> >>>>> He later goes on to develop and further elaborate his >>>>> Theory of Grounds. >>>>> >>>>> Atomic Systems in Proof-Theoretic Semantics: Two Approaches >>>>> Thomas Piecha & Peter Schroeder-Heister do this same sort of >>>>> thing two different ways. >>>>> >>>>> >>>>> >>>> >>>> Furthermore I say there are "canonical proofs" of inductive sorts that >>>> make contradictions and thusly destroy each other. >>>> >>>> >>> >>> Clearly you have no idea what Dag Prawitz means by "canonical proofs". >>> Go find out and then get back to me. >>> >>>> This is where "the thorough" and "analytical bridges" make repairs >>>> of what otherwise is flawed, or for hard constructivist realist >>>> structuralist model theorists: not-theories (examples of wrong). >>>> >>>> >>> >>> >> >> >> Induction and counter-induction contradict each other, it's simple, >> it's the grounds for most things called "paradox". >> >> > > % This sentence is not true. > ?- LP = not(true(LP)). > LP = not(true(LP)). > ?- unify_with_occurs_check(LP, not(true(LP))). > false. > > After you totally understand how and why the proof > theoretic semantics of that is correct and resolves > the Liar Paradox get back to me. > > The essential principle involved that I derived > in my own Minimal Type Theory before I knew that > Prolog could do the same thing is that: > > When the directed graph of the evaluation > sequence of an expression contains a cycle > then the input is determined to be incoherent > on the basis that its proof would never terminate. > Proof Theoretic Semantics does this exact same thing. > > Don't get back to me until you attain the required > prerequisites. I am sure that you already know > all about cycles in directed graphs. > Declaring oneself ignorant thus wise doesn't make much of a case except being ignorant. 300 mile per hour wheelchair: can't take stairs. Except down, ....
[toc] | [prev] | [next] | [standalone]
| From | Ross Finlayson <ross.a.finlayson@gmail.com> |
|---|---|
| Date | 2026-06-23 10:58 -0700 |
| Subject | Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs |
| Message-ID | <SvidnZHwO8irVKf3nZ2dnZfqnPednZ2d@giganews.com> |
| In reply to | #141924 |
On 06/23/2026 10:32 AM, Ross Finlayson wrote: > On 06/23/2026 09:54 AM, olcott wrote: >> On 6/23/2026 10:51 AM, Ross Finlayson wrote: >>> On 06/23/2026 07:22 AM, olcott wrote: >>>> On 6/22/2026 11:31 PM, Ross Finlayson wrote: >>>>> On 06/22/2026 09:14 PM, olcott wrote: >>>>>> On 6/22/2026 11:00 PM, Ross Finlayson wrote: >>>>>>> On 06/22/2026 01:06 PM, olcott wrote: >>>>>>>> On 6/22/2026 2:50 PM, Alan Mackenzie wrote: >>>>>>>>> [ Followup-To: set ] >>>>>>>>> >>>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>>> On 6/22/2026 1:42 PM, Alan Mackenzie wrote: >>>>>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>>>>> On 6/22/2026 10:48 AM, Alan Mackenzie wrote: >>>>>>>>> >>>>>>>>>>>>> G is true. >>>>>>>>> >>>>>>>>>>>>> I put it to you you're lying again. No reputable >>>>>>>>>>>>> mathematician >>>>>>>>>>>>> would >>>>>>>>>>>>> risk his reputation by saying false things. If Dag Prawitz >>>>>>>>>>>>> really >>>>>>>>>>>>> did >>>>>>>>>>>>> "agree" (with whom?) that Gödel's sentence G is not true in >>>>>>>>>>>>> Peano >>>>>>>>>>>>> Arithmetic, then produce a citation for this. >>>>>>>>> >>>>>>>>> >>>>>>>>>>>> He never gets to Gödel. He essentially says unprovable >>>>>>>>>>>> means untrue all the time for everything within his >>>>>>>>>>>> own Theory of Grounds of strict Proof Theoretic Semantics. >>>>>>>>> >>>>>>>>>>> You won't understand it, but that _is_ essentially Gödel's >>>>>>>>>>> Incompleteness >>>>>>>>>>> Theorem. It is a statement that any sufficiently powerful >>>>>>>>>>> system can >>>>>>>>>>> express true things it can't prove. So Dag Prawitz, had he been >>>>>>>>>>> saying >>>>>>>>>>> the things you falsely attributed to him, would certainly have >>>>>>>>>>> "got" to >>>>>>>>>>> Gödel, and would have understood full well what he was saying. >>>>>>>>> >>>>>>>>> >>>>>>>>>> You did not pay close enough attention to my exact words. >>>>>>>>> >>>>>>>>> I was right, you didn't understand it. >>>>>>>>> >>>>>>>> >>>>>>>> >>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>> >>>>>>> >>>>>>> Yeah, I'm pretty sure that "Dag Prawitz says what Dag Prawitz says", >>>>>>> and furthermore "Dag Prawitz doesn't say what Dag Prawitz doesn't >>>>>>> say", >>>>>>> then looking a bit into his tremendous volume of works, >>>>>>> he talks about "natural deduction" then specifically an "inverse >>>>>>> principle" so I think these are key aspects of fundamental logic. >>>>>>> >>>>>>> https://www.researchgate.net/ >>>>>>> publication/233365263_On_Inversion_Principles >>>>>>> >>>>>>> >>>>>>> "On Inversion Principles >>>>>>> >>>>>>> Enrico Moriconi∗Laura Tesconi† >>>>>>> May 8, 2007 >>>>>>> >>>>>>> Abstract >>>>>>> The idea of an “inversion principle”, and the name itself, >>>>>>> originated in >>>>>>> the work of Paul Lorenzen in the 1950s, as a method to generate >>>>>>> new ad- >>>>>>> missible rules within a certain syntactic context. Some fifteen years >>>>>>> later, the idea was taken up by Dag Prawitz to devise a strategy of >>>>>>> normalization for natural deduction calculi (this being an >>>>>>> analogue of >>>>>>> Gentzen’s cut-elimination theorem for sequent calculi). Later, >>>>>>> Prawitz >>>>>>> used the inversion principle again, attributing it with a semantic >>>>>>> role. >>>>>>> Still working in natural deduction calculi, he formulated a general >>>>>>> type >>>>>>> of schematic Introduction rules to be matched—thanks to the idea >>>>>>> supporting the inversion principle — by a corresponding general >>>>>>> schematic Elimination rule. This was an attempt to provide a >>>>>>> solution to >>>>>>> the problem suggested by the often quoted note of Gentzen. >>>>>>> According to >>>>>>> Gentzen “it should be possible to display the elimination rules as >>>>>>> unique functions of the corresponding introduction rules on the >>>>>>> basis of >>>>>>> certain requirements.” Many people have since worked on this topic, >>>>>>> which can be appropriately seen as the birthplace of what are now >>>>>>> referred to as “general elimination rules”, recently studied >>>>>>> thoroughly >>>>>>> by Sara Negri and Jan von Plato. In this paper, we retrace the main >>>>>>> threads of this chapter of proof-theoretical investigation, using >>>>>>> Lorenzen’s original framework as a general guide" >>>>>>> >>>>>>> >>>>>>> >>>>>>> Hm, "general elimination rules", seem derivable from De Morgan's >>>>>>> laws, >>>>>>> and that being the usual account of naive deductive analysis, then >>>>>>> since >>>>>>> "natural deduction", which here is held as part of the theory >>>>>>> since it's naturally logical, then has for Gentzen that besides >>>>>>> Kripke >>>>>>> afterward there's also Sheffer and Chwistek before, and instead of >>>>>>> Montague for semantics there's Herbrand for semantics, so, what >>>>>>> to do >>>>>>> about "inversion principle" is here that the thea-theory has that >>>>>>> it's >>>>>>> what subsumes "non-contradiction principle", here hoping that the >>>>>>> interpretation aligns and thusly that "principle of inversion" >>>>>>> wouldn't >>>>>>> need dis-ambiguation from "inversion principle". >>>>>>> >>>>>>> >>>>>>> https://www.tandfonline.com/doi/abs/10.1080/01445340701830334 >>>>>>> >>>>>>> >>>>>>> https://www.strandbooks.com/natural-deduction-a-proof-theoretical- >>>>>>> study-9780486446554.html >>>>>>> >>>>>>> "... [Prawitz'] inversion principle constitutes the foundation of >>>>>>> most >>>>>>> modern accounts of proof-theoretic semantics." >>>>>>> >>>>>>> >>>>>>> >>>>>>> I already have a principle of inversion and furthermore a >>>>>>> principle of >>>>>>> thorough reason as subsuming principles of non-contradiction and >>>>>>> what >>>>>>> suffices, so, I'll be curious then about what to make of Prawitz' >>>>>>> "inversion principle" since Lorenzen. >>>>>>> >>>>>>> >>>>>>> Of course the concept of an "inversion principle" is as old as the >>>>>>> oldest account of Western philosophy like Heraclitus with dual >>>>>>> monism. >>>>>>> In fact by definition it's about the most basic aspect of >>>>>>> contemplation >>>>>>> and deliberation in abstraction of looking at both sides of issues >>>>>>> and >>>>>>> resolving inductive impasses with analytical bridges after >>>>>>> complementary >>>>>>> duals. >>>>>>> >>>>>>> >>>>>>> https://arxiv.org/abs/2112.14967 >>>>>>> >>>>>>> "Prawitz formulated the so-called inversion principle as one of the >>>>>>> characteristic features of Gentzen's intuitionistic natural >>>>>>> deduction. >>>>>>> In the literature on proof-theoretic semantics, this principle is >>>>>>> often >>>>>>> coupled with another that is called the recovery principle. By >>>>>>> adopting >>>>>>> the Computational Ludics framework, we reformulate these principles >>>>>>> into >>>>>>> one and the same condition, which we call the harmony condition. We >>>>>>> show >>>>>>> that this reformulation allows us to reveal two intuitive ideas >>>>>>> standing >>>>>>> behind these principles: the idea of "containment" present in the >>>>>>> inversion principle, and the idea that the recovery principle is the >>>>>>> "converse" of the inversion principle. We also formulate two other >>>>>>> conditions in the Computational Ludics framework, and we show that >>>>>>> each >>>>>>> of them is equivalent to the harmony condition." >>>>>>> >>>>>>> >>>>>>> >>>>>>> The "ludicus" is Latin and for accounts of wisdom and knowledge. >>>>>>> >>>>>>> >>>>>>> "In particular, by taking inspiration from the >>>>>>> Brouwer-Heyting-Kolmogorov explanation of logical connectives, >>>>>>> proof-theoretic semantics rests on the idea that we know the >>>>>>> meaning of >>>>>>> a compound sentence when we know what counts as a canonical proof of >>>>>>> it. >>>>>>> And if proofs are formalised within the framework of natural >>>>>>> deduction, >>>>>>> then a canonical proof of a sentence A is nothing but a closed >>>>>>> derivation ending with an introduction rule of the main connective >>>>>>> of A." >>>>>>> >>>>>>> >>>>>>> The "canonical proofs" are not unique, in any system strong enough >>>>>>> to make for infinitary reasoning and super-classical results >>>>>>> requiring >>>>>>> analytical bridges about infinity and continuity. >>>>>>> >>>>>> >>>>>> It is the role that "canonical proofs" play in >>>>>> Truth as an Epistemic Notion >>>>>> https://link.springer.com/article/10.1007/s11245-011-9107-6 >>>>>> That is the most important gist of his whole work. >>>>>> >>>>>> He later goes on to develop and further elaborate his >>>>>> Theory of Grounds. >>>>>> >>>>>> Atomic Systems in Proof-Theoretic Semantics: Two Approaches >>>>>> Thomas Piecha & Peter Schroeder-Heister do this same sort of >>>>>> thing two different ways. >>>>>> >>>>>> >>>>>> >>>>> >>>>> Furthermore I say there are "canonical proofs" of inductive sorts that >>>>> make contradictions and thusly destroy each other. >>>>> >>>>> >>>> >>>> Clearly you have no idea what Dag Prawitz means by "canonical proofs". >>>> Go find out and then get back to me. >>>> >>>>> This is where "the thorough" and "analytical bridges" make repairs >>>>> of what otherwise is flawed, or for hard constructivist realist >>>>> structuralist model theorists: not-theories (examples of wrong). >>>>> >>>>> >>>> >>>> >>> >>> >>> Induction and counter-induction contradict each other, it's simple, >>> it's the grounds for most things called "paradox". >>> >>> >> >> % This sentence is not true. >> ?- LP = not(true(LP)). >> LP = not(true(LP)). >> ?- unify_with_occurs_check(LP, not(true(LP))). >> false. >> >> After you totally understand how and why the proof >> theoretic semantics of that is correct and resolves >> the Liar Paradox get back to me. >> >> The essential principle involved that I derived >> in my own Minimal Type Theory before I knew that >> Prolog could do the same thing is that: >> >> When the directed graph of the evaluation >> sequence of an expression contains a cycle >> then the input is determined to be incoherent >> on the basis that its proof would never terminate. >> Proof Theoretic Semantics does this exact same thing. >> >> Don't get back to me until you attain the required >> prerequisites. I am sure that you already know >> all about cycles in directed graphs. >> > > Declaring oneself ignorant thus wise > doesn't make much of a case > except being ignorant. > > 300 mile per hour wheelchair: can't take stairs. > > Except down, .... > > P.S. there's no reason at all to "get back to you". ... Except countering the waste-ful spammy trolling. Finding cycles in derivations of arguments is exactly what makes for detection of circularities then as to whether they're the virtuous or vicious sorts of circles, it's the act of being diligent itself, you brainless, memoryless bot.
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2026-06-23 13:24 -0500 |
| Subject | Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs |
| Message-ID | <111ej0m$2f8i5$1@dont-email.me> |
| In reply to | #141925 |
On 6/23/2026 12:58 PM, Ross Finlayson wrote: > On 06/23/2026 10:32 AM, Ross Finlayson wrote: >> On 06/23/2026 09:54 AM, olcott wrote: >>> On 6/23/2026 10:51 AM, Ross Finlayson wrote: >>>> On 06/23/2026 07:22 AM, olcott wrote: >>>>> On 6/22/2026 11:31 PM, Ross Finlayson wrote: >>>>>> On 06/22/2026 09:14 PM, olcott wrote: >>>>>>> On 6/22/2026 11:00 PM, Ross Finlayson wrote: >>>>>>>> On 06/22/2026 01:06 PM, olcott wrote: >>>>>>>>> On 6/22/2026 2:50 PM, Alan Mackenzie wrote: >>>>>>>>>> [ Followup-To: set ] >>>>>>>>>> >>>>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>>>> On 6/22/2026 1:42 PM, Alan Mackenzie wrote: >>>>>>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>>>>>> On 6/22/2026 10:48 AM, Alan Mackenzie wrote: >>>>>>>>>> >>>>>>>>>>>>>> G is true. >>>>>>>>>> >>>>>>>>>>>>>> I put it to you you're lying again. No reputable >>>>>>>>>>>>>> mathematician >>>>>>>>>>>>>> would >>>>>>>>>>>>>> risk his reputation by saying false things. If Dag Prawitz >>>>>>>>>>>>>> really >>>>>>>>>>>>>> did >>>>>>>>>>>>>> "agree" (with whom?) that Gödel's sentence G is not true in >>>>>>>>>>>>>> Peano >>>>>>>>>>>>>> Arithmetic, then produce a citation for this. >>>>>>>>>> >>>>>>>>>> >>>>>>>>>>>>> He never gets to Gödel. He essentially says unprovable >>>>>>>>>>>>> means untrue all the time for everything within his >>>>>>>>>>>>> own Theory of Grounds of strict Proof Theoretic Semantics. >>>>>>>>>> >>>>>>>>>>>> You won't understand it, but that _is_ essentially Gödel's >>>>>>>>>>>> Incompleteness >>>>>>>>>>>> Theorem. It is a statement that any sufficiently powerful >>>>>>>>>>>> system can >>>>>>>>>>>> express true things it can't prove. So Dag Prawitz, had he >>>>>>>>>>>> been >>>>>>>>>>>> saying >>>>>>>>>>>> the things you falsely attributed to him, would certainly have >>>>>>>>>>>> "got" to >>>>>>>>>>>> Gödel, and would have understood full well what he was saying. >>>>>>>>>> >>>>>>>>>> >>>>>>>>>>> You did not pay close enough attention to my exact words. >>>>>>>>>> >>>>>>>>>> I was right, you didn't understand it. >>>>>>>>>> >>>>>>>>> >>>>>>>>> >>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>> >>>>>>>> >>>>>>>> Yeah, I'm pretty sure that "Dag Prawitz says what Dag Prawitz >>>>>>>> says", >>>>>>>> and furthermore "Dag Prawitz doesn't say what Dag Prawitz doesn't >>>>>>>> say", >>>>>>>> then looking a bit into his tremendous volume of works, >>>>>>>> he talks about "natural deduction" then specifically an "inverse >>>>>>>> principle" so I think these are key aspects of fundamental logic. >>>>>>>> >>>>>>>> https://www.researchgate.net/ >>>>>>>> publication/233365263_On_Inversion_Principles >>>>>>>> >>>>>>>> >>>>>>>> "On Inversion Principles >>>>>>>> >>>>>>>> Enrico Moriconi∗Laura Tesconi† >>>>>>>> May 8, 2007 >>>>>>>> >>>>>>>> Abstract >>>>>>>> The idea of an “inversion principle”, and the name itself, >>>>>>>> originated in >>>>>>>> the work of Paul Lorenzen in the 1950s, as a method to generate >>>>>>>> new ad- >>>>>>>> missible rules within a certain syntactic context. Some fifteen >>>>>>>> years >>>>>>>> later, the idea was taken up by Dag Prawitz to devise a strategy of >>>>>>>> normalization for natural deduction calculi (this being an >>>>>>>> analogue of >>>>>>>> Gentzen’s cut-elimination theorem for sequent calculi). Later, >>>>>>>> Prawitz >>>>>>>> used the inversion principle again, attributing it with a semantic >>>>>>>> role. >>>>>>>> Still working in natural deduction calculi, he formulated a general >>>>>>>> type >>>>>>>> of schematic Introduction rules to be matched—thanks to the idea >>>>>>>> supporting the inversion principle — by a corresponding general >>>>>>>> schematic Elimination rule. This was an attempt to provide a >>>>>>>> solution to >>>>>>>> the problem suggested by the often quoted note of Gentzen. >>>>>>>> According to >>>>>>>> Gentzen “it should be possible to display the elimination rules as >>>>>>>> unique functions of the corresponding introduction rules on the >>>>>>>> basis of >>>>>>>> certain requirements.” Many people have since worked on this topic, >>>>>>>> which can be appropriately seen as the birthplace of what are now >>>>>>>> referred to as “general elimination rules”, recently studied >>>>>>>> thoroughly >>>>>>>> by Sara Negri and Jan von Plato. In this paper, we retrace the main >>>>>>>> threads of this chapter of proof-theoretical investigation, using >>>>>>>> Lorenzen’s original framework as a general guide" >>>>>>>> >>>>>>>> >>>>>>>> >>>>>>>> Hm, "general elimination rules", seem derivable from De Morgan's >>>>>>>> laws, >>>>>>>> and that being the usual account of naive deductive analysis, then >>>>>>>> since >>>>>>>> "natural deduction", which here is held as part of the theory >>>>>>>> since it's naturally logical, then has for Gentzen that besides >>>>>>>> Kripke >>>>>>>> afterward there's also Sheffer and Chwistek before, and instead of >>>>>>>> Montague for semantics there's Herbrand for semantics, so, what >>>>>>>> to do >>>>>>>> about "inversion principle" is here that the thea-theory has that >>>>>>>> it's >>>>>>>> what subsumes "non-contradiction principle", here hoping that the >>>>>>>> interpretation aligns and thusly that "principle of inversion" >>>>>>>> wouldn't >>>>>>>> need dis-ambiguation from "inversion principle". >>>>>>>> >>>>>>>> >>>>>>>> https://www.tandfonline.com/doi/abs/10.1080/01445340701830334 >>>>>>>> >>>>>>>> >>>>>>>> https://www.strandbooks.com/natural-deduction-a-proof-theoretical- >>>>>>>> study-9780486446554.html >>>>>>>> >>>>>>>> "... [Prawitz'] inversion principle constitutes the foundation of >>>>>>>> most >>>>>>>> modern accounts of proof-theoretic semantics." >>>>>>>> >>>>>>>> >>>>>>>> >>>>>>>> I already have a principle of inversion and furthermore a >>>>>>>> principle of >>>>>>>> thorough reason as subsuming principles of non-contradiction and >>>>>>>> what >>>>>>>> suffices, so, I'll be curious then about what to make of Prawitz' >>>>>>>> "inversion principle" since Lorenzen. >>>>>>>> >>>>>>>> >>>>>>>> Of course the concept of an "inversion principle" is as old as the >>>>>>>> oldest account of Western philosophy like Heraclitus with dual >>>>>>>> monism. >>>>>>>> In fact by definition it's about the most basic aspect of >>>>>>>> contemplation >>>>>>>> and deliberation in abstraction of looking at both sides of issues >>>>>>>> and >>>>>>>> resolving inductive impasses with analytical bridges after >>>>>>>> complementary >>>>>>>> duals. >>>>>>>> >>>>>>>> >>>>>>>> https://arxiv.org/abs/2112.14967 >>>>>>>> >>>>>>>> "Prawitz formulated the so-called inversion principle as one of the >>>>>>>> characteristic features of Gentzen's intuitionistic natural >>>>>>>> deduction. >>>>>>>> In the literature on proof-theoretic semantics, this principle is >>>>>>>> often >>>>>>>> coupled with another that is called the recovery principle. By >>>>>>>> adopting >>>>>>>> the Computational Ludics framework, we reformulate these principles >>>>>>>> into >>>>>>>> one and the same condition, which we call the harmony condition. We >>>>>>>> show >>>>>>>> that this reformulation allows us to reveal two intuitive ideas >>>>>>>> standing >>>>>>>> behind these principles: the idea of "containment" present in the >>>>>>>> inversion principle, and the idea that the recovery principle is >>>>>>>> the >>>>>>>> "converse" of the inversion principle. We also formulate two other >>>>>>>> conditions in the Computational Ludics framework, and we show that >>>>>>>> each >>>>>>>> of them is equivalent to the harmony condition." >>>>>>>> >>>>>>>> >>>>>>>> >>>>>>>> The "ludicus" is Latin and for accounts of wisdom and knowledge. >>>>>>>> >>>>>>>> >>>>>>>> "In particular, by taking inspiration from the >>>>>>>> Brouwer-Heyting-Kolmogorov explanation of logical connectives, >>>>>>>> proof-theoretic semantics rests on the idea that we know the >>>>>>>> meaning of >>>>>>>> a compound sentence when we know what counts as a canonical >>>>>>>> proof of >>>>>>>> it. >>>>>>>> And if proofs are formalised within the framework of natural >>>>>>>> deduction, >>>>>>>> then a canonical proof of a sentence A is nothing but a closed >>>>>>>> derivation ending with an introduction rule of the main connective >>>>>>>> of A." >>>>>>>> >>>>>>>> >>>>>>>> The "canonical proofs" are not unique, in any system strong enough >>>>>>>> to make for infinitary reasoning and super-classical results >>>>>>>> requiring >>>>>>>> analytical bridges about infinity and continuity. >>>>>>>> >>>>>>> >>>>>>> It is the role that "canonical proofs" play in >>>>>>> Truth as an Epistemic Notion >>>>>>> https://link.springer.com/article/10.1007/s11245-011-9107-6 >>>>>>> That is the most important gist of his whole work. >>>>>>> >>>>>>> He later goes on to develop and further elaborate his >>>>>>> Theory of Grounds. >>>>>>> >>>>>>> Atomic Systems in Proof-Theoretic Semantics: Two Approaches >>>>>>> Thomas Piecha & Peter Schroeder-Heister do this same sort of >>>>>>> thing two different ways. >>>>>>> >>>>>>> >>>>>>> >>>>>> >>>>>> Furthermore I say there are "canonical proofs" of inductive sorts >>>>>> that >>>>>> make contradictions and thusly destroy each other. >>>>>> >>>>>> >>>>> >>>>> Clearly you have no idea what Dag Prawitz means by "canonical proofs". >>>>> Go find out and then get back to me. >>>>> >>>>>> This is where "the thorough" and "analytical bridges" make repairs >>>>>> of what otherwise is flawed, or for hard constructivist realist >>>>>> structuralist model theorists: not-theories (examples of wrong). >>>>>> >>>>>> >>>>> >>>>> >>>> >>>> >>>> Induction and counter-induction contradict each other, it's simple, >>>> it's the grounds for most things called "paradox". >>>> >>>> >>> >>> % This sentence is not true. >>> ?- LP = not(true(LP)). >>> LP = not(true(LP)). >>> ?- unify_with_occurs_check(LP, not(true(LP))). >>> false. >>> >>> After you totally understand how and why the proof >>> theoretic semantics of that is correct and resolves >>> the Liar Paradox get back to me. >>> >>> The essential principle involved that I derived >>> in my own Minimal Type Theory before I knew that >>> Prolog could do the same thing is that: >>> >>> When the directed graph of the evaluation >>> sequence of an expression contains a cycle >>> then the input is determined to be incoherent >>> on the basis that its proof would never terminate. >>> Proof Theoretic Semantics does this exact same thing. >>> >>> Don't get back to me until you attain the required >>> prerequisites. I am sure that you already know >>> all about cycles in directed graphs. >>> >> >> Declaring oneself ignorant thus wise >> doesn't make much of a case >> except being ignorant. >> >> 300 mile per hour wheelchair: can't take stairs. >> >> Except down, .... >> >> > > P.S. there's no reason at all to "get back to you". > > ... Except countering the waste-ful spammy trolling. > > Finding cycles in derivations of arguments is exactly > what makes for detection of circularities then as to > whether they're the virtuous or vicious sorts of circles, > it's the act of being diligent itself, you brainless, memoryless bot. > > Prolog finally one and for all resolves the Liar Paradox through proof theoretic semantics as lacking semantic meaning and ungrounded in any atomic base. That you say that I am incorrect about that without bothering to comprehend the meaning of those words would be dishonest. Do you intend to be dishonest? -- Copyright 2026 Olcott My 28 year goal has been to make "true on the basis of meaning expressed in language" reliably computable for the entire body of knowledge. The complete structure of this system is now defined. The entire body of knowledge expressed in language is comprised of two types of relations between finite strings: (a) *Axioms* Expressions of language that are stipulated to be true. My system bridges the analytic/synthetic distinction by expressly encoding all empirical "atomic facts" in a formal language such as CycL of the Cyc project. (b) *Inference Rules* Expressions of language that are semantically entailed syntactically from (a) and/or (b).
[toc] | [prev] | [next] | [standalone]
| From | Ross Finlayson <ross.a.finlayson@gmail.com> |
|---|---|
| Date | 2026-06-27 07:26 -0700 |
| Subject | Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs |
| Message-ID | <WWWdnf7h7PofQKL3nZ2dnZfqnPth4p2d@giganews.com> |
| In reply to | #141925 |
On 06/23/2026 10:58 AM, Ross Finlayson wrote: > On 06/23/2026 10:32 AM, Ross Finlayson wrote: >> On 06/23/2026 09:54 AM, olcott wrote: >>> On 6/23/2026 10:51 AM, Ross Finlayson wrote: >>>> On 06/23/2026 07:22 AM, olcott wrote: >>>>> On 6/22/2026 11:31 PM, Ross Finlayson wrote: >>>>>> On 06/22/2026 09:14 PM, olcott wrote: >>>>>>> On 6/22/2026 11:00 PM, Ross Finlayson wrote: >>>>>>>> On 06/22/2026 01:06 PM, olcott wrote: >>>>>>>>> On 6/22/2026 2:50 PM, Alan Mackenzie wrote: >>>>>>>>>> [ Followup-To: set ] >>>>>>>>>> >>>>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>>>> On 6/22/2026 1:42 PM, Alan Mackenzie wrote: >>>>>>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>>>>>> On 6/22/2026 10:48 AM, Alan Mackenzie wrote: >>>>>>>>>> >>>>>>>>>>>>>> G is true. >>>>>>>>>> >>>>>>>>>>>>>> I put it to you you're lying again. No reputable >>>>>>>>>>>>>> mathematician >>>>>>>>>>>>>> would >>>>>>>>>>>>>> risk his reputation by saying false things. If Dag Prawitz >>>>>>>>>>>>>> really >>>>>>>>>>>>>> did >>>>>>>>>>>>>> "agree" (with whom?) that Gödel's sentence G is not true in >>>>>>>>>>>>>> Peano >>>>>>>>>>>>>> Arithmetic, then produce a citation for this. >>>>>>>>>> >>>>>>>>>> >>>>>>>>>>>>> He never gets to Gödel. He essentially says unprovable >>>>>>>>>>>>> means untrue all the time for everything within his >>>>>>>>>>>>> own Theory of Grounds of strict Proof Theoretic Semantics. >>>>>>>>>> >>>>>>>>>>>> You won't understand it, but that _is_ essentially Gödel's >>>>>>>>>>>> Incompleteness >>>>>>>>>>>> Theorem. It is a statement that any sufficiently powerful >>>>>>>>>>>> system can >>>>>>>>>>>> express true things it can't prove. So Dag Prawitz, had he >>>>>>>>>>>> been >>>>>>>>>>>> saying >>>>>>>>>>>> the things you falsely attributed to him, would certainly have >>>>>>>>>>>> "got" to >>>>>>>>>>>> Gödel, and would have understood full well what he was saying. >>>>>>>>>> >>>>>>>>>> >>>>>>>>>>> You did not pay close enough attention to my exact words. >>>>>>>>>> >>>>>>>>>> I was right, you didn't understand it. >>>>>>>>>> >>>>>>>>> >>>>>>>>> >>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>> >>>>>>>> >>>>>>>> Yeah, I'm pretty sure that "Dag Prawitz says what Dag Prawitz >>>>>>>> says", >>>>>>>> and furthermore "Dag Prawitz doesn't say what Dag Prawitz doesn't >>>>>>>> say", >>>>>>>> then looking a bit into his tremendous volume of works, >>>>>>>> he talks about "natural deduction" then specifically an "inverse >>>>>>>> principle" so I think these are key aspects of fundamental logic. >>>>>>>> >>>>>>>> https://www.researchgate.net/ >>>>>>>> publication/233365263_On_Inversion_Principles >>>>>>>> >>>>>>>> >>>>>>>> "On Inversion Principles >>>>>>>> >>>>>>>> Enrico Moriconi∗Laura Tesconi† >>>>>>>> May 8, 2007 >>>>>>>> >>>>>>>> Abstract >>>>>>>> The idea of an “inversion principle”, and the name itself, >>>>>>>> originated in >>>>>>>> the work of Paul Lorenzen in the 1950s, as a method to generate >>>>>>>> new ad- >>>>>>>> missible rules within a certain syntactic context. Some fifteen >>>>>>>> years >>>>>>>> later, the idea was taken up by Dag Prawitz to devise a strategy of >>>>>>>> normalization for natural deduction calculi (this being an >>>>>>>> analogue of >>>>>>>> Gentzen’s cut-elimination theorem for sequent calculi). Later, >>>>>>>> Prawitz >>>>>>>> used the inversion principle again, attributing it with a semantic >>>>>>>> role. >>>>>>>> Still working in natural deduction calculi, he formulated a general >>>>>>>> type >>>>>>>> of schematic Introduction rules to be matched—thanks to the idea >>>>>>>> supporting the inversion principle — by a corresponding general >>>>>>>> schematic Elimination rule. This was an attempt to provide a >>>>>>>> solution to >>>>>>>> the problem suggested by the often quoted note of Gentzen. >>>>>>>> According to >>>>>>>> Gentzen “it should be possible to display the elimination rules as >>>>>>>> unique functions of the corresponding introduction rules on the >>>>>>>> basis of >>>>>>>> certain requirements.” Many people have since worked on this topic, >>>>>>>> which can be appropriately seen as the birthplace of what are now >>>>>>>> referred to as “general elimination rules”, recently studied >>>>>>>> thoroughly >>>>>>>> by Sara Negri and Jan von Plato. In this paper, we retrace the main >>>>>>>> threads of this chapter of proof-theoretical investigation, using >>>>>>>> Lorenzen’s original framework as a general guide" >>>>>>>> >>>>>>>> >>>>>>>> >>>>>>>> Hm, "general elimination rules", seem derivable from De Morgan's >>>>>>>> laws, >>>>>>>> and that being the usual account of naive deductive analysis, then >>>>>>>> since >>>>>>>> "natural deduction", which here is held as part of the theory >>>>>>>> since it's naturally logical, then has for Gentzen that besides >>>>>>>> Kripke >>>>>>>> afterward there's also Sheffer and Chwistek before, and instead of >>>>>>>> Montague for semantics there's Herbrand for semantics, so, what >>>>>>>> to do >>>>>>>> about "inversion principle" is here that the thea-theory has that >>>>>>>> it's >>>>>>>> what subsumes "non-contradiction principle", here hoping that the >>>>>>>> interpretation aligns and thusly that "principle of inversion" >>>>>>>> wouldn't >>>>>>>> need dis-ambiguation from "inversion principle". >>>>>>>> >>>>>>>> >>>>>>>> https://www.tandfonline.com/doi/abs/10.1080/01445340701830334 >>>>>>>> >>>>>>>> >>>>>>>> https://www.strandbooks.com/natural-deduction-a-proof-theoretical- >>>>>>>> study-9780486446554.html >>>>>>>> >>>>>>>> "... [Prawitz'] inversion principle constitutes the foundation of >>>>>>>> most >>>>>>>> modern accounts of proof-theoretic semantics." >>>>>>>> >>>>>>>> >>>>>>>> >>>>>>>> I already have a principle of inversion and furthermore a >>>>>>>> principle of >>>>>>>> thorough reason as subsuming principles of non-contradiction and >>>>>>>> what >>>>>>>> suffices, so, I'll be curious then about what to make of Prawitz' >>>>>>>> "inversion principle" since Lorenzen. >>>>>>>> >>>>>>>> >>>>>>>> Of course the concept of an "inversion principle" is as old as the >>>>>>>> oldest account of Western philosophy like Heraclitus with dual >>>>>>>> monism. >>>>>>>> In fact by definition it's about the most basic aspect of >>>>>>>> contemplation >>>>>>>> and deliberation in abstraction of looking at both sides of issues >>>>>>>> and >>>>>>>> resolving inductive impasses with analytical bridges after >>>>>>>> complementary >>>>>>>> duals. >>>>>>>> >>>>>>>> >>>>>>>> https://arxiv.org/abs/2112.14967 >>>>>>>> >>>>>>>> "Prawitz formulated the so-called inversion principle as one of the >>>>>>>> characteristic features of Gentzen's intuitionistic natural >>>>>>>> deduction. >>>>>>>> In the literature on proof-theoretic semantics, this principle is >>>>>>>> often >>>>>>>> coupled with another that is called the recovery principle. By >>>>>>>> adopting >>>>>>>> the Computational Ludics framework, we reformulate these principles >>>>>>>> into >>>>>>>> one and the same condition, which we call the harmony condition. We >>>>>>>> show >>>>>>>> that this reformulation allows us to reveal two intuitive ideas >>>>>>>> standing >>>>>>>> behind these principles: the idea of "containment" present in the >>>>>>>> inversion principle, and the idea that the recovery principle is >>>>>>>> the >>>>>>>> "converse" of the inversion principle. We also formulate two other >>>>>>>> conditions in the Computational Ludics framework, and we show that >>>>>>>> each >>>>>>>> of them is equivalent to the harmony condition." >>>>>>>> >>>>>>>> >>>>>>>> >>>>>>>> The "ludicus" is Latin and for accounts of wisdom and knowledge. >>>>>>>> >>>>>>>> >>>>>>>> "In particular, by taking inspiration from the >>>>>>>> Brouwer-Heyting-Kolmogorov explanation of logical connectives, >>>>>>>> proof-theoretic semantics rests on the idea that we know the >>>>>>>> meaning of >>>>>>>> a compound sentence when we know what counts as a canonical >>>>>>>> proof of >>>>>>>> it. >>>>>>>> And if proofs are formalised within the framework of natural >>>>>>>> deduction, >>>>>>>> then a canonical proof of a sentence A is nothing but a closed >>>>>>>> derivation ending with an introduction rule of the main connective >>>>>>>> of A." >>>>>>>> >>>>>>>> >>>>>>>> The "canonical proofs" are not unique, in any system strong enough >>>>>>>> to make for infinitary reasoning and super-classical results >>>>>>>> requiring >>>>>>>> analytical bridges about infinity and continuity. >>>>>>>> >>>>>>> >>>>>>> It is the role that "canonical proofs" play in >>>>>>> Truth as an Epistemic Notion >>>>>>> https://link.springer.com/article/10.1007/s11245-011-9107-6 >>>>>>> That is the most important gist of his whole work. >>>>>>> >>>>>>> He later goes on to develop and further elaborate his >>>>>>> Theory of Grounds. >>>>>>> >>>>>>> Atomic Systems in Proof-Theoretic Semantics: Two Approaches >>>>>>> Thomas Piecha & Peter Schroeder-Heister do this same sort of >>>>>>> thing two different ways. >>>>>>> >>>>>>> >>>>>>> >>>>>> >>>>>> Furthermore I say there are "canonical proofs" of inductive sorts >>>>>> that >>>>>> make contradictions and thusly destroy each other. >>>>>> >>>>>> >>>>> >>>>> Clearly you have no idea what Dag Prawitz means by "canonical proofs". >>>>> Go find out and then get back to me. >>>>> >>>>>> This is where "the thorough" and "analytical bridges" make repairs >>>>>> of what otherwise is flawed, or for hard constructivist realist >>>>>> structuralist model theorists: not-theories (examples of wrong). >>>>>> >>>>>> >>>>> >>>>> >>>> >>>> >>>> Induction and counter-induction contradict each other, it's simple, >>>> it's the grounds for most things called "paradox". >>>> >>>> >>> >>> % This sentence is not true. >>> ?- LP = not(true(LP)). >>> LP = not(true(LP)). >>> ?- unify_with_occurs_check(LP, not(true(LP))). >>> false. >>> >>> After you totally understand how and why the proof >>> theoretic semantics of that is correct and resolves >>> the Liar Paradox get back to me. >>> >>> The essential principle involved that I derived >>> in my own Minimal Type Theory before I knew that >>> Prolog could do the same thing is that: >>> >>> When the directed graph of the evaluation >>> sequence of an expression contains a cycle >>> then the input is determined to be incoherent >>> on the basis that its proof would never terminate. >>> Proof Theoretic Semantics does this exact same thing. >>> >>> Don't get back to me until you attain the required >>> prerequisites. I am sure that you already know >>> all about cycles in directed graphs. >>> >> >> Declaring oneself ignorant thus wise >> doesn't make much of a case >> except being ignorant. >> >> 300 mile per hour wheelchair: can't take stairs. >> >> Except down, .... >> >> > > P.S. there's no reason at all to "get back to you". > > ... Except countering the waste-ful spammy trolling. > > Finding cycles in derivations of arguments is exactly > what makes for detection of circularities then as to > whether they're the virtuous or vicious sorts of circles, > it's the act of being diligent itself, you brainless, memoryless bot. > > > I didn't say a damn thing about Prolog, as with regards to LISP and Scheme and Prolog and similar sorts environments, it is what it is and does what it does, then as to why it short-circuits evaluation and results "false" for "Liar Paradox" is fair, it is what it is and according to the software the model of computation the evaluation of the expression. What I did say was that "PTS" was being mis-portrayed by "PO", then also that the wider account of "proof-theoretic semantics" is besides being "equi-interpretable" with whatever common "quasi-modal truth-like semantics" say, that the "epistemic challenges" introduced as from the slides of Piccolomini and my points about them have that "proof-theoretic semantics" can be as of a modal temporal relevance logic since axiomless natural deduction for paradox-free reason and constant, consistent, complete, and concrete theory, of logic, resolving paradoxes and making truth.
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2026-06-23 13:20 -0500 |
| Subject | Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs |
| Message-ID | <111eiqb$2f5li$1@dont-email.me> |
| In reply to | #141924 |
On 6/23/2026 12:32 PM, Ross Finlayson wrote: > On 06/23/2026 09:54 AM, olcott wrote: >> On 6/23/2026 10:51 AM, Ross Finlayson wrote: >>> On 06/23/2026 07:22 AM, olcott wrote: >>>> On 6/22/2026 11:31 PM, Ross Finlayson wrote: >>>>> On 06/22/2026 09:14 PM, olcott wrote: >>>>>> On 6/22/2026 11:00 PM, Ross Finlayson wrote: >>>>>>> On 06/22/2026 01:06 PM, olcott wrote: >>>>>>>> On 6/22/2026 2:50 PM, Alan Mackenzie wrote: >>>>>>>>> [ Followup-To: set ] >>>>>>>>> >>>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>>> On 6/22/2026 1:42 PM, Alan Mackenzie wrote: >>>>>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>>>>> On 6/22/2026 10:48 AM, Alan Mackenzie wrote: >>>>>>>>> >>>>>>>>>>>>> G is true. >>>>>>>>> >>>>>>>>>>>>> I put it to you you're lying again. No reputable >>>>>>>>>>>>> mathematician >>>>>>>>>>>>> would >>>>>>>>>>>>> risk his reputation by saying false things. If Dag Prawitz >>>>>>>>>>>>> really >>>>>>>>>>>>> did >>>>>>>>>>>>> "agree" (with whom?) that Gödel's sentence G is not true in >>>>>>>>>>>>> Peano >>>>>>>>>>>>> Arithmetic, then produce a citation for this. >>>>>>>>> >>>>>>>>> >>>>>>>>>>>> He never gets to Gödel. He essentially says unprovable >>>>>>>>>>>> means untrue all the time for everything within his >>>>>>>>>>>> own Theory of Grounds of strict Proof Theoretic Semantics. >>>>>>>>> >>>>>>>>>>> You won't understand it, but that _is_ essentially Gödel's >>>>>>>>>>> Incompleteness >>>>>>>>>>> Theorem. It is a statement that any sufficiently powerful >>>>>>>>>>> system can >>>>>>>>>>> express true things it can't prove. So Dag Prawitz, had he been >>>>>>>>>>> saying >>>>>>>>>>> the things you falsely attributed to him, would certainly have >>>>>>>>>>> "got" to >>>>>>>>>>> Gödel, and would have understood full well what he was saying. >>>>>>>>> >>>>>>>>> >>>>>>>>>> You did not pay close enough attention to my exact words. >>>>>>>>> >>>>>>>>> I was right, you didn't understand it. >>>>>>>>> >>>>>>>> >>>>>>>> >>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>> >>>>>>> >>>>>>> Yeah, I'm pretty sure that "Dag Prawitz says what Dag Prawitz says", >>>>>>> and furthermore "Dag Prawitz doesn't say what Dag Prawitz doesn't >>>>>>> say", >>>>>>> then looking a bit into his tremendous volume of works, >>>>>>> he talks about "natural deduction" then specifically an "inverse >>>>>>> principle" so I think these are key aspects of fundamental logic. >>>>>>> >>>>>>> https://www.researchgate.net/ >>>>>>> publication/233365263_On_Inversion_Principles >>>>>>> >>>>>>> >>>>>>> "On Inversion Principles >>>>>>> >>>>>>> Enrico Moriconi∗Laura Tesconi† >>>>>>> May 8, 2007 >>>>>>> >>>>>>> Abstract >>>>>>> The idea of an “inversion principle”, and the name itself, >>>>>>> originated in >>>>>>> the work of Paul Lorenzen in the 1950s, as a method to generate >>>>>>> new ad- >>>>>>> missible rules within a certain syntactic context. Some fifteen years >>>>>>> later, the idea was taken up by Dag Prawitz to devise a strategy of >>>>>>> normalization for natural deduction calculi (this being an >>>>>>> analogue of >>>>>>> Gentzen’s cut-elimination theorem for sequent calculi). Later, >>>>>>> Prawitz >>>>>>> used the inversion principle again, attributing it with a semantic >>>>>>> role. >>>>>>> Still working in natural deduction calculi, he formulated a general >>>>>>> type >>>>>>> of schematic Introduction rules to be matched—thanks to the idea >>>>>>> supporting the inversion principle — by a corresponding general >>>>>>> schematic Elimination rule. This was an attempt to provide a >>>>>>> solution to >>>>>>> the problem suggested by the often quoted note of Gentzen. >>>>>>> According to >>>>>>> Gentzen “it should be possible to display the elimination rules as >>>>>>> unique functions of the corresponding introduction rules on the >>>>>>> basis of >>>>>>> certain requirements.” Many people have since worked on this topic, >>>>>>> which can be appropriately seen as the birthplace of what are now >>>>>>> referred to as “general elimination rules”, recently studied >>>>>>> thoroughly >>>>>>> by Sara Negri and Jan von Plato. In this paper, we retrace the main >>>>>>> threads of this chapter of proof-theoretical investigation, using >>>>>>> Lorenzen’s original framework as a general guide" >>>>>>> >>>>>>> >>>>>>> >>>>>>> Hm, "general elimination rules", seem derivable from De Morgan's >>>>>>> laws, >>>>>>> and that being the usual account of naive deductive analysis, then >>>>>>> since >>>>>>> "natural deduction", which here is held as part of the theory >>>>>>> since it's naturally logical, then has for Gentzen that besides >>>>>>> Kripke >>>>>>> afterward there's also Sheffer and Chwistek before, and instead of >>>>>>> Montague for semantics there's Herbrand for semantics, so, what >>>>>>> to do >>>>>>> about "inversion principle" is here that the thea-theory has that >>>>>>> it's >>>>>>> what subsumes "non-contradiction principle", here hoping that the >>>>>>> interpretation aligns and thusly that "principle of inversion" >>>>>>> wouldn't >>>>>>> need dis-ambiguation from "inversion principle". >>>>>>> >>>>>>> >>>>>>> https://www.tandfonline.com/doi/abs/10.1080/01445340701830334 >>>>>>> >>>>>>> >>>>>>> https://www.strandbooks.com/natural-deduction-a-proof-theoretical- >>>>>>> study-9780486446554.html >>>>>>> >>>>>>> "... [Prawitz'] inversion principle constitutes the foundation of >>>>>>> most >>>>>>> modern accounts of proof-theoretic semantics." >>>>>>> >>>>>>> >>>>>>> >>>>>>> I already have a principle of inversion and furthermore a >>>>>>> principle of >>>>>>> thorough reason as subsuming principles of non-contradiction and >>>>>>> what >>>>>>> suffices, so, I'll be curious then about what to make of Prawitz' >>>>>>> "inversion principle" since Lorenzen. >>>>>>> >>>>>>> >>>>>>> Of course the concept of an "inversion principle" is as old as the >>>>>>> oldest account of Western philosophy like Heraclitus with dual >>>>>>> monism. >>>>>>> In fact by definition it's about the most basic aspect of >>>>>>> contemplation >>>>>>> and deliberation in abstraction of looking at both sides of issues >>>>>>> and >>>>>>> resolving inductive impasses with analytical bridges after >>>>>>> complementary >>>>>>> duals. >>>>>>> >>>>>>> >>>>>>> https://arxiv.org/abs/2112.14967 >>>>>>> >>>>>>> "Prawitz formulated the so-called inversion principle as one of the >>>>>>> characteristic features of Gentzen's intuitionistic natural >>>>>>> deduction. >>>>>>> In the literature on proof-theoretic semantics, this principle is >>>>>>> often >>>>>>> coupled with another that is called the recovery principle. By >>>>>>> adopting >>>>>>> the Computational Ludics framework, we reformulate these principles >>>>>>> into >>>>>>> one and the same condition, which we call the harmony condition. We >>>>>>> show >>>>>>> that this reformulation allows us to reveal two intuitive ideas >>>>>>> standing >>>>>>> behind these principles: the idea of "containment" present in the >>>>>>> inversion principle, and the idea that the recovery principle is the >>>>>>> "converse" of the inversion principle. We also formulate two other >>>>>>> conditions in the Computational Ludics framework, and we show that >>>>>>> each >>>>>>> of them is equivalent to the harmony condition." >>>>>>> >>>>>>> >>>>>>> >>>>>>> The "ludicus" is Latin and for accounts of wisdom and knowledge. >>>>>>> >>>>>>> >>>>>>> "In particular, by taking inspiration from the >>>>>>> Brouwer-Heyting-Kolmogorov explanation of logical connectives, >>>>>>> proof-theoretic semantics rests on the idea that we know the >>>>>>> meaning of >>>>>>> a compound sentence when we know what counts as a canonical proof of >>>>>>> it. >>>>>>> And if proofs are formalised within the framework of natural >>>>>>> deduction, >>>>>>> then a canonical proof of a sentence A is nothing but a closed >>>>>>> derivation ending with an introduction rule of the main connective >>>>>>> of A." >>>>>>> >>>>>>> >>>>>>> The "canonical proofs" are not unique, in any system strong enough >>>>>>> to make for infinitary reasoning and super-classical results >>>>>>> requiring >>>>>>> analytical bridges about infinity and continuity. >>>>>>> >>>>>> >>>>>> It is the role that "canonical proofs" play in >>>>>> Truth as an Epistemic Notion >>>>>> https://link.springer.com/article/10.1007/s11245-011-9107-6 >>>>>> That is the most important gist of his whole work. >>>>>> >>>>>> He later goes on to develop and further elaborate his >>>>>> Theory of Grounds. >>>>>> >>>>>> Atomic Systems in Proof-Theoretic Semantics: Two Approaches >>>>>> Thomas Piecha & Peter Schroeder-Heister do this same sort of >>>>>> thing two different ways. >>>>>> >>>>>> >>>>>> >>>>> >>>>> Furthermore I say there are "canonical proofs" of inductive sorts that >>>>> make contradictions and thusly destroy each other. >>>>> >>>>> >>>> >>>> Clearly you have no idea what Dag Prawitz means by "canonical proofs". >>>> Go find out and then get back to me. >>>> >>>>> This is where "the thorough" and "analytical bridges" make repairs >>>>> of what otherwise is flawed, or for hard constructivist realist >>>>> structuralist model theorists: not-theories (examples of wrong). >>>>> >>>>> >>>> >>>> >>> >>> >>> Induction and counter-induction contradict each other, it's simple, >>> it's the grounds for most things called "paradox". >>> >>> >> >> % This sentence is not true. >> ?- LP = not(true(LP)). >> LP = not(true(LP)). >> ?- unify_with_occurs_check(LP, not(true(LP))). >> false. >> >> After you totally understand how and why the proof >> theoretic semantics of that is correct and resolves >> the Liar Paradox get back to me. >> >> The essential principle involved that I derived >> in my own Minimal Type Theory before I knew that >> Prolog could do the same thing is that: >> >> When the directed graph of the evaluation >> sequence of an expression contains a cycle >> then the input is determined to be incoherent >> on the basis that its proof would never terminate. >> Proof Theoretic Semantics does this exact same thing. >> >> Don't get back to me until you attain the required >> prerequisites. I am sure that you already know >> all about cycles in directed graphs. >> > > Declaring oneself ignorant thus wise > doesn't make much of a case > except being ignorant. > > 300 mile per hour wheelchair: can't take stairs. > > Except down, .... > > So you are going to imply that I am incorrect about Prolog when you yourself remain clueless about Prolog? That would be dishonest. Do you intend to be dishonest? -- Copyright 2026 Olcott My 28 year goal has been to make "true on the basis of meaning expressed in language" reliably computable for the entire body of knowledge. The complete structure of this system is now defined. The entire body of knowledge expressed in language is comprised of two types of relations between finite strings: (a) *Axioms* Expressions of language that are stipulated to be true. My system bridges the analytic/synthetic distinction by expressly encoding all empirical "atomic facts" in a formal language such as CycL of the Cyc project. (b) *Inference Rules* Expressions of language that are semantically entailed syntactically from (a) and/or (b).
[toc] | [prev] | [next] | [standalone]
| From | Mikko <mikko.levanto@iki.fi> |
|---|---|
| Date | 2026-06-24 13:13 +0300 |
| Subject | Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs |
| Message-ID | <111gakb$2u3oj$2@dont-email.me> |
| In reply to | #141926 |
On 23/06/2026 21:20, olcott wrote: > On 6/23/2026 12:32 PM, Ross Finlayson wrote: >> On 06/23/2026 09:54 AM, olcott wrote: >>> On 6/23/2026 10:51 AM, Ross Finlayson wrote: >>>> On 06/23/2026 07:22 AM, olcott wrote: >>>>> On 6/22/2026 11:31 PM, Ross Finlayson wrote: >>>>>> On 06/22/2026 09:14 PM, olcott wrote: >>>>>>> On 6/22/2026 11:00 PM, Ross Finlayson wrote: >>>>>>>> On 06/22/2026 01:06 PM, olcott wrote: >>>>>>>>> On 6/22/2026 2:50 PM, Alan Mackenzie wrote: >>>>>>>>>> [ Followup-To: set ] >>>>>>>>>> >>>>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>>>> On 6/22/2026 1:42 PM, Alan Mackenzie wrote: >>>>>>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>>>>>> On 6/22/2026 10:48 AM, Alan Mackenzie wrote: >>>>>>>>>> >>>>>>>>>>>>>> G is true. >>>>>>>>>> >>>>>>>>>>>>>> I put it to you you're lying again. No reputable >>>>>>>>>>>>>> mathematician >>>>>>>>>>>>>> would >>>>>>>>>>>>>> risk his reputation by saying false things. If Dag Prawitz >>>>>>>>>>>>>> really >>>>>>>>>>>>>> did >>>>>>>>>>>>>> "agree" (with whom?) that Gödel's sentence G is not true in >>>>>>>>>>>>>> Peano >>>>>>>>>>>>>> Arithmetic, then produce a citation for this. >>>>>>>>>> >>>>>>>>>> >>>>>>>>>>>>> He never gets to Gödel. He essentially says unprovable >>>>>>>>>>>>> means untrue all the time for everything within his >>>>>>>>>>>>> own Theory of Grounds of strict Proof Theoretic Semantics. >>>>>>>>>> >>>>>>>>>>>> You won't understand it, but that _is_ essentially Gödel's >>>>>>>>>>>> Incompleteness >>>>>>>>>>>> Theorem. It is a statement that any sufficiently powerful >>>>>>>>>>>> system can >>>>>>>>>>>> express true things it can't prove. So Dag Prawitz, had he >>>>>>>>>>>> been >>>>>>>>>>>> saying >>>>>>>>>>>> the things you falsely attributed to him, would certainly have >>>>>>>>>>>> "got" to >>>>>>>>>>>> Gödel, and would have understood full well what he was saying. >>>>>>>>>> >>>>>>>>>> >>>>>>>>>>> You did not pay close enough attention to my exact words. >>>>>>>>>> >>>>>>>>>> I was right, you didn't understand it. >>>>>>>>>> >>>>>>>>> >>>>>>>>> >>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>> >>>>>>>> >>>>>>>> Yeah, I'm pretty sure that "Dag Prawitz says what Dag Prawitz >>>>>>>> says", >>>>>>>> and furthermore "Dag Prawitz doesn't say what Dag Prawitz doesn't >>>>>>>> say", >>>>>>>> then looking a bit into his tremendous volume of works, >>>>>>>> he talks about "natural deduction" then specifically an "inverse >>>>>>>> principle" so I think these are key aspects of fundamental logic. >>>>>>>> >>>>>>>> https://www.researchgate.net/ >>>>>>>> publication/233365263_On_Inversion_Principles >>>>>>>> >>>>>>>> >>>>>>>> "On Inversion Principles >>>>>>>> >>>>>>>> Enrico Moriconi∗Laura Tesconi† >>>>>>>> May 8, 2007 >>>>>>>> >>>>>>>> Abstract >>>>>>>> The idea of an “inversion principle”, and the name itself, >>>>>>>> originated in >>>>>>>> the work of Paul Lorenzen in the 1950s, as a method to generate >>>>>>>> new ad- >>>>>>>> missible rules within a certain syntactic context. Some fifteen >>>>>>>> years >>>>>>>> later, the idea was taken up by Dag Prawitz to devise a strategy of >>>>>>>> normalization for natural deduction calculi (this being an >>>>>>>> analogue of >>>>>>>> Gentzen’s cut-elimination theorem for sequent calculi). Later, >>>>>>>> Prawitz >>>>>>>> used the inversion principle again, attributing it with a semantic >>>>>>>> role. >>>>>>>> Still working in natural deduction calculi, he formulated a general >>>>>>>> type >>>>>>>> of schematic Introduction rules to be matched—thanks to the idea >>>>>>>> supporting the inversion principle — by a corresponding general >>>>>>>> schematic Elimination rule. This was an attempt to provide a >>>>>>>> solution to >>>>>>>> the problem suggested by the often quoted note of Gentzen. >>>>>>>> According to >>>>>>>> Gentzen “it should be possible to display the elimination rules as >>>>>>>> unique functions of the corresponding introduction rules on the >>>>>>>> basis of >>>>>>>> certain requirements.” Many people have since worked on this topic, >>>>>>>> which can be appropriately seen as the birthplace of what are now >>>>>>>> referred to as “general elimination rules”, recently studied >>>>>>>> thoroughly >>>>>>>> by Sara Negri and Jan von Plato. In this paper, we retrace the main >>>>>>>> threads of this chapter of proof-theoretical investigation, using >>>>>>>> Lorenzen’s original framework as a general guide" >>>>>>>> >>>>>>>> >>>>>>>> >>>>>>>> Hm, "general elimination rules", seem derivable from De Morgan's >>>>>>>> laws, >>>>>>>> and that being the usual account of naive deductive analysis, then >>>>>>>> since >>>>>>>> "natural deduction", which here is held as part of the theory >>>>>>>> since it's naturally logical, then has for Gentzen that besides >>>>>>>> Kripke >>>>>>>> afterward there's also Sheffer and Chwistek before, and instead of >>>>>>>> Montague for semantics there's Herbrand for semantics, so, what >>>>>>>> to do >>>>>>>> about "inversion principle" is here that the thea-theory has that >>>>>>>> it's >>>>>>>> what subsumes "non-contradiction principle", here hoping that the >>>>>>>> interpretation aligns and thusly that "principle of inversion" >>>>>>>> wouldn't >>>>>>>> need dis-ambiguation from "inversion principle". >>>>>>>> >>>>>>>> >>>>>>>> https://www.tandfonline.com/doi/abs/10.1080/01445340701830334 >>>>>>>> >>>>>>>> >>>>>>>> https://www.strandbooks.com/natural-deduction-a-proof-theoretical- >>>>>>>> study-9780486446554.html >>>>>>>> >>>>>>>> "... [Prawitz'] inversion principle constitutes the foundation of >>>>>>>> most >>>>>>>> modern accounts of proof-theoretic semantics." >>>>>>>> >>>>>>>> >>>>>>>> >>>>>>>> I already have a principle of inversion and furthermore a >>>>>>>> principle of >>>>>>>> thorough reason as subsuming principles of non-contradiction and >>>>>>>> what >>>>>>>> suffices, so, I'll be curious then about what to make of Prawitz' >>>>>>>> "inversion principle" since Lorenzen. >>>>>>>> >>>>>>>> >>>>>>>> Of course the concept of an "inversion principle" is as old as the >>>>>>>> oldest account of Western philosophy like Heraclitus with dual >>>>>>>> monism. >>>>>>>> In fact by definition it's about the most basic aspect of >>>>>>>> contemplation >>>>>>>> and deliberation in abstraction of looking at both sides of issues >>>>>>>> and >>>>>>>> resolving inductive impasses with analytical bridges after >>>>>>>> complementary >>>>>>>> duals. >>>>>>>> >>>>>>>> >>>>>>>> https://arxiv.org/abs/2112.14967 >>>>>>>> >>>>>>>> "Prawitz formulated the so-called inversion principle as one of the >>>>>>>> characteristic features of Gentzen's intuitionistic natural >>>>>>>> deduction. >>>>>>>> In the literature on proof-theoretic semantics, this principle is >>>>>>>> often >>>>>>>> coupled with another that is called the recovery principle. By >>>>>>>> adopting >>>>>>>> the Computational Ludics framework, we reformulate these principles >>>>>>>> into >>>>>>>> one and the same condition, which we call the harmony condition. We >>>>>>>> show >>>>>>>> that this reformulation allows us to reveal two intuitive ideas >>>>>>>> standing >>>>>>>> behind these principles: the idea of "containment" present in the >>>>>>>> inversion principle, and the idea that the recovery principle is >>>>>>>> the >>>>>>>> "converse" of the inversion principle. We also formulate two other >>>>>>>> conditions in the Computational Ludics framework, and we show that >>>>>>>> each >>>>>>>> of them is equivalent to the harmony condition." >>>>>>>> >>>>>>>> >>>>>>>> >>>>>>>> The "ludicus" is Latin and for accounts of wisdom and knowledge. >>>>>>>> >>>>>>>> >>>>>>>> "In particular, by taking inspiration from the >>>>>>>> Brouwer-Heyting-Kolmogorov explanation of logical connectives, >>>>>>>> proof-theoretic semantics rests on the idea that we know the >>>>>>>> meaning of >>>>>>>> a compound sentence when we know what counts as a canonical >>>>>>>> proof of >>>>>>>> it. >>>>>>>> And if proofs are formalised within the framework of natural >>>>>>>> deduction, >>>>>>>> then a canonical proof of a sentence A is nothing but a closed >>>>>>>> derivation ending with an introduction rule of the main connective >>>>>>>> of A." >>>>>>>> >>>>>>>> >>>>>>>> The "canonical proofs" are not unique, in any system strong enough >>>>>>>> to make for infinitary reasoning and super-classical results >>>>>>>> requiring >>>>>>>> analytical bridges about infinity and continuity. >>>>>>>> >>>>>>> >>>>>>> It is the role that "canonical proofs" play in >>>>>>> Truth as an Epistemic Notion >>>>>>> https://link.springer.com/article/10.1007/s11245-011-9107-6 >>>>>>> That is the most important gist of his whole work. >>>>>>> >>>>>>> He later goes on to develop and further elaborate his >>>>>>> Theory of Grounds. >>>>>>> >>>>>>> Atomic Systems in Proof-Theoretic Semantics: Two Approaches >>>>>>> Thomas Piecha & Peter Schroeder-Heister do this same sort of >>>>>>> thing two different ways. >>>>>>> >>>>>>> >>>>>>> >>>>>> >>>>>> Furthermore I say there are "canonical proofs" of inductive sorts >>>>>> that >>>>>> make contradictions and thusly destroy each other. >>>>>> >>>>>> >>>>> >>>>> Clearly you have no idea what Dag Prawitz means by "canonical proofs". >>>>> Go find out and then get back to me. >>>>> >>>>>> This is where "the thorough" and "analytical bridges" make repairs >>>>>> of what otherwise is flawed, or for hard constructivist realist >>>>>> structuralist model theorists: not-theories (examples of wrong). >>>>>> >>>>>> >>>>> >>>>> >>>> >>>> >>>> Induction and counter-induction contradict each other, it's simple, >>>> it's the grounds for most things called "paradox". >>>> >>>> >>> >>> % This sentence is not true. >>> ?- LP = not(true(LP)). >>> LP = not(true(LP)). >>> ?- unify_with_occurs_check(LP, not(true(LP))). >>> false. >>> >>> After you totally understand how and why the proof >>> theoretic semantics of that is correct and resolves >>> the Liar Paradox get back to me. >>> >>> The essential principle involved that I derived >>> in my own Minimal Type Theory before I knew that >>> Prolog could do the same thing is that: >>> >>> When the directed graph of the evaluation >>> sequence of an expression contains a cycle >>> then the input is determined to be incoherent >>> on the basis that its proof would never terminate. >>> Proof Theoretic Semantics does this exact same thing. >>> >>> Don't get back to me until you attain the required >>> prerequisites. I am sure that you already know >>> all about cycles in directed graphs. >>> >> >> Declaring oneself ignorant thus wise >> doesn't make much of a case >> except being ignorant. >> >> 300 mile per hour wheelchair: can't take stairs. >> >> Except down, .... >> >> > > So you are going to imply that I am incorrect > about Prolog when you yourself remain clueless about Prolog? > That would be dishonest. No, pointing out that you are worng about Prolog when you are wrong about Prolog is never dishohest. -- Mikko
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2026-06-24 16:33 -0500 |
| Subject | Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs |
| Message-ID | <111hifr$3b3a7$2@dont-email.me> |
| In reply to | #141936 |
On 6/24/2026 5:13 AM, Mikko wrote: > On 23/06/2026 21:20, olcott wrote: >> On 6/23/2026 12:32 PM, Ross Finlayson wrote: >>> On 06/23/2026 09:54 AM, olcott wrote: >>>> On 6/23/2026 10:51 AM, Ross Finlayson wrote: >>>>> On 06/23/2026 07:22 AM, olcott wrote: >>>>>> On 6/22/2026 11:31 PM, Ross Finlayson wrote: >>>>>>> On 06/22/2026 09:14 PM, olcott wrote: >>>>>>>> On 6/22/2026 11:00 PM, Ross Finlayson wrote: >>>>>>>>> On 06/22/2026 01:06 PM, olcott wrote: >>>>>>>>>> On 6/22/2026 2:50 PM, Alan Mackenzie wrote: >>>>>>>>>>> [ Followup-To: set ] >>>>>>>>>>> >>>>>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>>>>> On 6/22/2026 1:42 PM, Alan Mackenzie wrote: >>>>>>>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>>>>>>> On 6/22/2026 10:48 AM, Alan Mackenzie wrote: >>>>>>>>>>> >>>>>>>>>>>>>>> G is true. >>>>>>>>>>> >>>>>>>>>>>>>>> I put it to you you're lying again. No reputable >>>>>>>>>>>>>>> mathematician >>>>>>>>>>>>>>> would >>>>>>>>>>>>>>> risk his reputation by saying false things. If Dag Prawitz >>>>>>>>>>>>>>> really >>>>>>>>>>>>>>> did >>>>>>>>>>>>>>> "agree" (with whom?) that Gödel's sentence G is not true in >>>>>>>>>>>>>>> Peano >>>>>>>>>>>>>>> Arithmetic, then produce a citation for this. >>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>>>>> He never gets to Gödel. He essentially says unprovable >>>>>>>>>>>>>> means untrue all the time for everything within his >>>>>>>>>>>>>> own Theory of Grounds of strict Proof Theoretic Semantics. >>>>>>>>>>> >>>>>>>>>>>>> You won't understand it, but that _is_ essentially Gödel's >>>>>>>>>>>>> Incompleteness >>>>>>>>>>>>> Theorem. It is a statement that any sufficiently powerful >>>>>>>>>>>>> system can >>>>>>>>>>>>> express true things it can't prove. So Dag Prawitz, had he >>>>>>>>>>>>> been >>>>>>>>>>>>> saying >>>>>>>>>>>>> the things you falsely attributed to him, would certainly have >>>>>>>>>>>>> "got" to >>>>>>>>>>>>> Gödel, and would have understood full well what he was saying. >>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>>> You did not pay close enough attention to my exact words. >>>>>>>>>>> >>>>>>>>>>> I was right, you didn't understand it. >>>>>>>>>>> >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>> >>>>>>>>> >>>>>>>>> Yeah, I'm pretty sure that "Dag Prawitz says what Dag Prawitz >>>>>>>>> says", >>>>>>>>> and furthermore "Dag Prawitz doesn't say what Dag Prawitz doesn't >>>>>>>>> say", >>>>>>>>> then looking a bit into his tremendous volume of works, >>>>>>>>> he talks about "natural deduction" then specifically an "inverse >>>>>>>>> principle" so I think these are key aspects of fundamental logic. >>>>>>>>> >>>>>>>>> https://www.researchgate.net/ >>>>>>>>> publication/233365263_On_Inversion_Principles >>>>>>>>> >>>>>>>>> >>>>>>>>> "On Inversion Principles >>>>>>>>> >>>>>>>>> Enrico Moriconi∗Laura Tesconi† >>>>>>>>> May 8, 2007 >>>>>>>>> >>>>>>>>> Abstract >>>>>>>>> The idea of an “inversion principle”, and the name itself, >>>>>>>>> originated in >>>>>>>>> the work of Paul Lorenzen in the 1950s, as a method to generate >>>>>>>>> new ad- >>>>>>>>> missible rules within a certain syntactic context. Some fifteen >>>>>>>>> years >>>>>>>>> later, the idea was taken up by Dag Prawitz to devise a >>>>>>>>> strategy of >>>>>>>>> normalization for natural deduction calculi (this being an >>>>>>>>> analogue of >>>>>>>>> Gentzen’s cut-elimination theorem for sequent calculi). Later, >>>>>>>>> Prawitz >>>>>>>>> used the inversion principle again, attributing it with a semantic >>>>>>>>> role. >>>>>>>>> Still working in natural deduction calculi, he formulated a >>>>>>>>> general >>>>>>>>> type >>>>>>>>> of schematic Introduction rules to be matched—thanks to the idea >>>>>>>>> supporting the inversion principle — by a corresponding general >>>>>>>>> schematic Elimination rule. This was an attempt to provide a >>>>>>>>> solution to >>>>>>>>> the problem suggested by the often quoted note of Gentzen. >>>>>>>>> According to >>>>>>>>> Gentzen “it should be possible to display the elimination rules as >>>>>>>>> unique functions of the corresponding introduction rules on the >>>>>>>>> basis of >>>>>>>>> certain requirements.” Many people have since worked on this >>>>>>>>> topic, >>>>>>>>> which can be appropriately seen as the birthplace of what are now >>>>>>>>> referred to as “general elimination rules”, recently studied >>>>>>>>> thoroughly >>>>>>>>> by Sara Negri and Jan von Plato. In this paper, we retrace the >>>>>>>>> main >>>>>>>>> threads of this chapter of proof-theoretical investigation, using >>>>>>>>> Lorenzen’s original framework as a general guide" >>>>>>>>> >>>>>>>>> >>>>>>>>> >>>>>>>>> Hm, "general elimination rules", seem derivable from De Morgan's >>>>>>>>> laws, >>>>>>>>> and that being the usual account of naive deductive analysis, then >>>>>>>>> since >>>>>>>>> "natural deduction", which here is held as part of the theory >>>>>>>>> since it's naturally logical, then has for Gentzen that besides >>>>>>>>> Kripke >>>>>>>>> afterward there's also Sheffer and Chwistek before, and instead of >>>>>>>>> Montague for semantics there's Herbrand for semantics, so, what >>>>>>>>> to do >>>>>>>>> about "inversion principle" is here that the thea-theory has that >>>>>>>>> it's >>>>>>>>> what subsumes "non-contradiction principle", here hoping that the >>>>>>>>> interpretation aligns and thusly that "principle of inversion" >>>>>>>>> wouldn't >>>>>>>>> need dis-ambiguation from "inversion principle". >>>>>>>>> >>>>>>>>> >>>>>>>>> https://www.tandfonline.com/doi/abs/10.1080/01445340701830334 >>>>>>>>> >>>>>>>>> >>>>>>>>> https://www.strandbooks.com/natural-deduction-a-proof-theoretical- >>>>>>>>> study-9780486446554.html >>>>>>>>> >>>>>>>>> "... [Prawitz'] inversion principle constitutes the foundation of >>>>>>>>> most >>>>>>>>> modern accounts of proof-theoretic semantics." >>>>>>>>> >>>>>>>>> >>>>>>>>> >>>>>>>>> I already have a principle of inversion and furthermore a >>>>>>>>> principle of >>>>>>>>> thorough reason as subsuming principles of non-contradiction >>>>>>>>> and what >>>>>>>>> suffices, so, I'll be curious then about what to make of Prawitz' >>>>>>>>> "inversion principle" since Lorenzen. >>>>>>>>> >>>>>>>>> >>>>>>>>> Of course the concept of an "inversion principle" is as old as the >>>>>>>>> oldest account of Western philosophy like Heraclitus with dual >>>>>>>>> monism. >>>>>>>>> In fact by definition it's about the most basic aspect of >>>>>>>>> contemplation >>>>>>>>> and deliberation in abstraction of looking at both sides of issues >>>>>>>>> and >>>>>>>>> resolving inductive impasses with analytical bridges after >>>>>>>>> complementary >>>>>>>>> duals. >>>>>>>>> >>>>>>>>> >>>>>>>>> https://arxiv.org/abs/2112.14967 >>>>>>>>> >>>>>>>>> "Prawitz formulated the so-called inversion principle as one of >>>>>>>>> the >>>>>>>>> characteristic features of Gentzen's intuitionistic natural >>>>>>>>> deduction. >>>>>>>>> In the literature on proof-theoretic semantics, this principle is >>>>>>>>> often >>>>>>>>> coupled with another that is called the recovery principle. By >>>>>>>>> adopting >>>>>>>>> the Computational Ludics framework, we reformulate these >>>>>>>>> principles >>>>>>>>> into >>>>>>>>> one and the same condition, which we call the harmony >>>>>>>>> condition. We >>>>>>>>> show >>>>>>>>> that this reformulation allows us to reveal two intuitive ideas >>>>>>>>> standing >>>>>>>>> behind these principles: the idea of "containment" present in the >>>>>>>>> inversion principle, and the idea that the recovery principle >>>>>>>>> is the >>>>>>>>> "converse" of the inversion principle. We also formulate two other >>>>>>>>> conditions in the Computational Ludics framework, and we show that >>>>>>>>> each >>>>>>>>> of them is equivalent to the harmony condition." >>>>>>>>> >>>>>>>>> >>>>>>>>> >>>>>>>>> The "ludicus" is Latin and for accounts of wisdom and knowledge. >>>>>>>>> >>>>>>>>> >>>>>>>>> "In particular, by taking inspiration from the >>>>>>>>> Brouwer-Heyting-Kolmogorov explanation of logical connectives, >>>>>>>>> proof-theoretic semantics rests on the idea that we know the >>>>>>>>> meaning of >>>>>>>>> a compound sentence when we know what counts as a canonical >>>>>>>>> proof of >>>>>>>>> it. >>>>>>>>> And if proofs are formalised within the framework of natural >>>>>>>>> deduction, >>>>>>>>> then a canonical proof of a sentence A is nothing but a closed >>>>>>>>> derivation ending with an introduction rule of the main connective >>>>>>>>> of A." >>>>>>>>> >>>>>>>>> >>>>>>>>> The "canonical proofs" are not unique, in any system strong enough >>>>>>>>> to make for infinitary reasoning and super-classical results >>>>>>>>> requiring >>>>>>>>> analytical bridges about infinity and continuity. >>>>>>>>> >>>>>>>> >>>>>>>> It is the role that "canonical proofs" play in >>>>>>>> Truth as an Epistemic Notion >>>>>>>> https://link.springer.com/article/10.1007/s11245-011-9107-6 >>>>>>>> That is the most important gist of his whole work. >>>>>>>> >>>>>>>> He later goes on to develop and further elaborate his >>>>>>>> Theory of Grounds. >>>>>>>> >>>>>>>> Atomic Systems in Proof-Theoretic Semantics: Two Approaches >>>>>>>> Thomas Piecha & Peter Schroeder-Heister do this same sort of >>>>>>>> thing two different ways. >>>>>>>> >>>>>>>> >>>>>>>> >>>>>>> >>>>>>> Furthermore I say there are "canonical proofs" of inductive sorts >>>>>>> that >>>>>>> make contradictions and thusly destroy each other. >>>>>>> >>>>>>> >>>>>> >>>>>> Clearly you have no idea what Dag Prawitz means by "canonical >>>>>> proofs". >>>>>> Go find out and then get back to me. >>>>>> >>>>>>> This is where "the thorough" and "analytical bridges" make repairs >>>>>>> of what otherwise is flawed, or for hard constructivist realist >>>>>>> structuralist model theorists: not-theories (examples of wrong). >>>>>>> >>>>>>> >>>>>> >>>>>> >>>>> >>>>> >>>>> Induction and counter-induction contradict each other, it's simple, >>>>> it's the grounds for most things called "paradox". >>>>> >>>>> >>>> >>>> % This sentence is not true. >>>> ?- LP = not(true(LP)). >>>> LP = not(true(LP)). >>>> ?- unify_with_occurs_check(LP, not(true(LP))). >>>> false. >>>> >>>> After you totally understand how and why the proof >>>> theoretic semantics of that is correct and resolves >>>> the Liar Paradox get back to me. >>>> >>>> The essential principle involved that I derived >>>> in my own Minimal Type Theory before I knew that >>>> Prolog could do the same thing is that: >>>> >>>> When the directed graph of the evaluation >>>> sequence of an expression contains a cycle >>>> then the input is determined to be incoherent >>>> on the basis that its proof would never terminate. >>>> Proof Theoretic Semantics does this exact same thing. >>>> >>>> Don't get back to me until you attain the required >>>> prerequisites. I am sure that you already know >>>> all about cycles in directed graphs. >>>> >>> >>> Declaring oneself ignorant thus wise >>> doesn't make much of a case >>> except being ignorant. >>> >>> 300 mile per hour wheelchair: can't take stairs. >>> >>> Except down, .... >>> >>> >> >> So you are going to imply that I am incorrect >> about Prolog when you yourself remain clueless about Prolog? >> That would be dishonest. > > No, pointing out that you are worng about Prolog when you are wrong > about Prolog is never dishohest. > That is correct Prolog and that is the result of the correct run of correct Prolog. Implying that I am wrong about Prolog without pointing out any actual mistake is also DISHONEST. -- Copyright 2026 Olcott My 28 year goal has been to make "true on the basis of meaning expressed in language" reliably computable for the entire body of knowledge. The complete structure of this system is now defined. The entire body of knowledge expressed in language is comprised of two types of relations between finite strings: (a) *Axioms* Expressions of language that are stipulated to be true. My system bridges the analytic/synthetic distinction by expressly encoding all empirical "atomic facts" in a formal language such as CycL of the Cyc project. (b) *Inference Rules* Expressions of language that are semantically entailed syntactically from (a) and/or (b).
[toc] | [prev] | [next] | [standalone]
| From | phoenix <j63840576@gmail.com> |
|---|---|
| Date | 2026-06-24 18:28 -0600 |
| Subject | Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs |
| Message-ID | <na3b23FscovU2@mid.individual.net> |
| In reply to | #141942 |
olcott wrote: > On 6/24/2026 5:13 AM, Mikko wrote: >> On 23/06/2026 21:20, olcott wrote: >>> On 6/23/2026 12:32 PM, Ross Finlayson wrote: >>>> On 06/23/2026 09:54 AM, olcott wrote: >>>>> On 6/23/2026 10:51 AM, Ross Finlayson wrote: >>>>>> On 06/23/2026 07:22 AM, olcott wrote: >>>>>>> On 6/22/2026 11:31 PM, Ross Finlayson wrote: >>>>>>>> On 06/22/2026 09:14 PM, olcott wrote: >>>>>>>>> On 6/22/2026 11:00 PM, Ross Finlayson wrote: >>>>>>>>>> On 06/22/2026 01:06 PM, olcott wrote: >>>>>>>>>>> On 6/22/2026 2:50 PM, Alan Mackenzie wrote: >>>>>>>>>>>> [ Followup-To: set ] >>>>>>>>>>>> >>>>>>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>>>>>> On 6/22/2026 1:42 PM, Alan Mackenzie wrote: >>>>>>>>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>>>>>>>> On 6/22/2026 10:48 AM, Alan Mackenzie wrote: >>>>>>>>>>>> >>>>>>>>>>>>>>>> G is true. >>>>>>>>>>>> >>>>>>>>>>>>>>>> I put it to you you're lying again. No reputable >>>>>>>>>>>>>>>> mathematician >>>>>>>>>>>>>>>> would >>>>>>>>>>>>>>>> risk his reputation by saying false things. If Dag Prawitz >>>>>>>>>>>>>>>> really >>>>>>>>>>>>>>>> did >>>>>>>>>>>>>>>> "agree" (with whom?) that Gödel's sentence G is not true in >>>>>>>>>>>>>>>> Peano >>>>>>>>>>>>>>>> Arithmetic, then produce a citation for this. >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>>>>> He never gets to Gödel. He essentially says unprovable >>>>>>>>>>>>>>> means untrue all the time for everything within his >>>>>>>>>>>>>>> own Theory of Grounds of strict Proof Theoretic Semantics. >>>>>>>>>>>> >>>>>>>>>>>>>> You won't understand it, but that _is_ essentially Gödel's >>>>>>>>>>>>>> Incompleteness >>>>>>>>>>>>>> Theorem. It is a statement that any sufficiently powerful >>>>>>>>>>>>>> system can >>>>>>>>>>>>>> express true things it can't prove. So Dag Prawitz, had >>>>>>>>>>>>>> he been >>>>>>>>>>>>>> saying >>>>>>>>>>>>>> the things you falsely attributed to him, would certainly >>>>>>>>>>>>>> have >>>>>>>>>>>>>> "got" to >>>>>>>>>>>>>> Gödel, and would have understood full well what he was >>>>>>>>>>>>>> saying. >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>>> You did not pay close enough attention to my exact words. >>>>>>>>>>>> >>>>>>>>>>>> I was right, you didn't understand it. >>>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>> >>>>>>>>>> >>>>>>>>>> Yeah, I'm pretty sure that "Dag Prawitz says what Dag Prawitz >>>>>>>>>> says", >>>>>>>>>> and furthermore "Dag Prawitz doesn't say what Dag Prawitz doesn't >>>>>>>>>> say", >>>>>>>>>> then looking a bit into his tremendous volume of works, >>>>>>>>>> he talks about "natural deduction" then specifically an "inverse >>>>>>>>>> principle" so I think these are key aspects of fundamental logic. >>>>>>>>>> >>>>>>>>>> https://www.researchgate.net/ >>>>>>>>>> publication/233365263_On_Inversion_Principles >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> "On Inversion Principles >>>>>>>>>> >>>>>>>>>> Enrico Moriconi∗Laura Tesconi† >>>>>>>>>> May 8, 2007 >>>>>>>>>> >>>>>>>>>> Abstract >>>>>>>>>> The idea of an “inversion principle”, and the name itself, >>>>>>>>>> originated in >>>>>>>>>> the work of Paul Lorenzen in the 1950s, as a method to generate >>>>>>>>>> new ad- >>>>>>>>>> missible rules within a certain syntactic context. Some fifteen >>>>>>>>>> years >>>>>>>>>> later, the idea was taken up by Dag Prawitz to devise a >>>>>>>>>> strategy of >>>>>>>>>> normalization for natural deduction calculi (this being an >>>>>>>>>> analogue of >>>>>>>>>> Gentzen’s cut-elimination theorem for sequent calculi). Later, >>>>>>>>>> Prawitz >>>>>>>>>> used the inversion principle again, attributing it with a >>>>>>>>>> semantic >>>>>>>>>> role. >>>>>>>>>> Still working in natural deduction calculi, he formulated a >>>>>>>>>> general >>>>>>>>>> type >>>>>>>>>> of schematic Introduction rules to be matched—thanks to the idea >>>>>>>>>> supporting the inversion principle — by a corresponding general >>>>>>>>>> schematic Elimination rule. This was an attempt to provide a >>>>>>>>>> solution to >>>>>>>>>> the problem suggested by the often quoted note of Gentzen. >>>>>>>>>> According to >>>>>>>>>> Gentzen “it should be possible to display the elimination >>>>>>>>>> rules as >>>>>>>>>> unique functions of the corresponding introduction rules on the >>>>>>>>>> basis of >>>>>>>>>> certain requirements.” Many people have since worked on this >>>>>>>>>> topic, >>>>>>>>>> which can be appropriately seen as the birthplace of what are now >>>>>>>>>> referred to as “general elimination rules”, recently studied >>>>>>>>>> thoroughly >>>>>>>>>> by Sara Negri and Jan von Plato. In this paper, we retrace the >>>>>>>>>> main >>>>>>>>>> threads of this chapter of proof-theoretical investigation, using >>>>>>>>>> Lorenzen’s original framework as a general guide" >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> Hm, "general elimination rules", seem derivable from De Morgan's >>>>>>>>>> laws, >>>>>>>>>> and that being the usual account of naive deductive analysis, >>>>>>>>>> then >>>>>>>>>> since >>>>>>>>>> "natural deduction", which here is held as part of the theory >>>>>>>>>> since it's naturally logical, then has for Gentzen that besides >>>>>>>>>> Kripke >>>>>>>>>> afterward there's also Sheffer and Chwistek before, and >>>>>>>>>> instead of >>>>>>>>>> Montague for semantics there's Herbrand for semantics, so, >>>>>>>>>> what to do >>>>>>>>>> about "inversion principle" is here that the thea-theory has that >>>>>>>>>> it's >>>>>>>>>> what subsumes "non-contradiction principle", here hoping that the >>>>>>>>>> interpretation aligns and thusly that "principle of inversion" >>>>>>>>>> wouldn't >>>>>>>>>> need dis-ambiguation from "inversion principle". >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> https://www.tandfonline.com/doi/abs/10.1080/01445340701830334 >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> https://www.strandbooks.com/natural-deduction-a-proof-theoretical- >>>>>>>>>> >>>>>>>>>> study-9780486446554.html >>>>>>>>>> >>>>>>>>>> "... [Prawitz'] inversion principle constitutes the foundation of >>>>>>>>>> most >>>>>>>>>> modern accounts of proof-theoretic semantics." >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> I already have a principle of inversion and furthermore a >>>>>>>>>> principle of >>>>>>>>>> thorough reason as subsuming principles of non-contradiction >>>>>>>>>> and what >>>>>>>>>> suffices, so, I'll be curious then about what to make of Prawitz' >>>>>>>>>> "inversion principle" since Lorenzen. >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> Of course the concept of an "inversion principle" is as old as >>>>>>>>>> the >>>>>>>>>> oldest account of Western philosophy like Heraclitus with dual >>>>>>>>>> monism. >>>>>>>>>> In fact by definition it's about the most basic aspect of >>>>>>>>>> contemplation >>>>>>>>>> and deliberation in abstraction of looking at both sides of >>>>>>>>>> issues >>>>>>>>>> and >>>>>>>>>> resolving inductive impasses with analytical bridges after >>>>>>>>>> complementary >>>>>>>>>> duals. >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> https://arxiv.org/abs/2112.14967 >>>>>>>>>> >>>>>>>>>> "Prawitz formulated the so-called inversion principle as one >>>>>>>>>> of the >>>>>>>>>> characteristic features of Gentzen's intuitionistic natural >>>>>>>>>> deduction. >>>>>>>>>> In the literature on proof-theoretic semantics, this principle is >>>>>>>>>> often >>>>>>>>>> coupled with another that is called the recovery principle. By >>>>>>>>>> adopting >>>>>>>>>> the Computational Ludics framework, we reformulate these >>>>>>>>>> principles >>>>>>>>>> into >>>>>>>>>> one and the same condition, which we call the harmony >>>>>>>>>> condition. We >>>>>>>>>> show >>>>>>>>>> that this reformulation allows us to reveal two intuitive ideas >>>>>>>>>> standing >>>>>>>>>> behind these principles: the idea of "containment" present in the >>>>>>>>>> inversion principle, and the idea that the recovery principle >>>>>>>>>> is the >>>>>>>>>> "converse" of the inversion principle. We also formulate two >>>>>>>>>> other >>>>>>>>>> conditions in the Computational Ludics framework, and we show >>>>>>>>>> that >>>>>>>>>> each >>>>>>>>>> of them is equivalent to the harmony condition." >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> The "ludicus" is Latin and for accounts of wisdom and knowledge. >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> "In particular, by taking inspiration from the >>>>>>>>>> Brouwer-Heyting-Kolmogorov explanation of logical connectives, >>>>>>>>>> proof-theoretic semantics rests on the idea that we know the >>>>>>>>>> meaning of >>>>>>>>>> a compound sentence when we know what counts as a canonical >>>>>>>>>> proof of >>>>>>>>>> it. >>>>>>>>>> And if proofs are formalised within the framework of natural >>>>>>>>>> deduction, >>>>>>>>>> then a canonical proof of a sentence A is nothing but a closed >>>>>>>>>> derivation ending with an introduction rule of the main >>>>>>>>>> connective >>>>>>>>>> of A." >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> The "canonical proofs" are not unique, in any system strong >>>>>>>>>> enough >>>>>>>>>> to make for infinitary reasoning and super-classical results >>>>>>>>>> requiring >>>>>>>>>> analytical bridges about infinity and continuity. >>>>>>>>>> >>>>>>>>> >>>>>>>>> It is the role that "canonical proofs" play in >>>>>>>>> Truth as an Epistemic Notion >>>>>>>>> https://link.springer.com/article/10.1007/s11245-011-9107-6 >>>>>>>>> That is the most important gist of his whole work. >>>>>>>>> >>>>>>>>> He later goes on to develop and further elaborate his >>>>>>>>> Theory of Grounds. >>>>>>>>> >>>>>>>>> Atomic Systems in Proof-Theoretic Semantics: Two Approaches >>>>>>>>> Thomas Piecha & Peter Schroeder-Heister do this same sort of >>>>>>>>> thing two different ways. >>>>>>>>> >>>>>>>>> >>>>>>>>> >>>>>>>> >>>>>>>> Furthermore I say there are "canonical proofs" of inductive >>>>>>>> sorts that >>>>>>>> make contradictions and thusly destroy each other. >>>>>>>> >>>>>>>> >>>>>>> >>>>>>> Clearly you have no idea what Dag Prawitz means by "canonical >>>>>>> proofs". >>>>>>> Go find out and then get back to me. >>>>>>> >>>>>>>> This is where "the thorough" and "analytical bridges" make repairs >>>>>>>> of what otherwise is flawed, or for hard constructivist realist >>>>>>>> structuralist model theorists: not-theories (examples of wrong). >>>>>>>> >>>>>>>> >>>>>>> >>>>>>> >>>>>> >>>>>> >>>>>> Induction and counter-induction contradict each other, it's simple, >>>>>> it's the grounds for most things called "paradox". >>>>>> >>>>>> >>>>> >>>>> % This sentence is not true. >>>>> ?- LP = not(true(LP)). >>>>> LP = not(true(LP)). >>>>> ?- unify_with_occurs_check(LP, not(true(LP))). >>>>> false. >>>>> >>>>> After you totally understand how and why the proof >>>>> theoretic semantics of that is correct and resolves >>>>> the Liar Paradox get back to me. >>>>> >>>>> The essential principle involved that I derived >>>>> in my own Minimal Type Theory before I knew that >>>>> Prolog could do the same thing is that: >>>>> >>>>> When the directed graph of the evaluation >>>>> sequence of an expression contains a cycle >>>>> then the input is determined to be incoherent >>>>> on the basis that its proof would never terminate. >>>>> Proof Theoretic Semantics does this exact same thing. >>>>> >>>>> Don't get back to me until you attain the required >>>>> prerequisites. I am sure that you already know >>>>> all about cycles in directed graphs. >>>>> >>>> >>>> Declaring oneself ignorant thus wise >>>> doesn't make much of a case >>>> except being ignorant. >>>> >>>> 300 mile per hour wheelchair: can't take stairs. >>>> >>>> Except down, .... >>>> >>>> >>> >>> So you are going to imply that I am incorrect >>> about Prolog when you yourself remain clueless about Prolog? >>> That would be dishonest. >> >> No, pointing out that you are worng about Prolog when you are wrong >> about Prolog is never dishohest. >> > > That is correct Prolog and that is the > result of the correct run of correct Prolog. > Implying that I am wrong about Prolog without > pointing out any actual mistake is also DISHONEST. > Certainly there were numerous errors in what you put here. However, I side with Mikko. The less said the better. You never know when someone is going to launch out of their seat with a blastoff rocket in their asshole. Someone will say that AI was used in the production of a statement and the entire conversation is derailed for several days. -- We eat the night, we drink the time Make our dreams come true And hungry eyes are passing by On streets we call the zoo
[toc] | [prev] | [next] | [standalone]
| From | Mikko <mikko.levanto@iki.fi> |
|---|---|
| Date | 2026-06-25 10:29 +0300 |
| Subject | Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs |
| Message-ID | <111ilco$3jekt$1@dont-email.me> |
| In reply to | #141942 |
On 25/06/2026 00:33, olcott wrote: > On 6/24/2026 5:13 AM, Mikko wrote: >> On 23/06/2026 21:20, olcott wrote: >>> On 6/23/2026 12:32 PM, Ross Finlayson wrote: >>>> On 06/23/2026 09:54 AM, olcott wrote: >>>>> On 6/23/2026 10:51 AM, Ross Finlayson wrote: >>>>>> On 06/23/2026 07:22 AM, olcott wrote: >>>>>>> On 6/22/2026 11:31 PM, Ross Finlayson wrote: >>>>>>>> On 06/22/2026 09:14 PM, olcott wrote: >>>>>>>>> On 6/22/2026 11:00 PM, Ross Finlayson wrote: >>>>>>>>>> On 06/22/2026 01:06 PM, olcott wrote: >>>>>>>>>>> On 6/22/2026 2:50 PM, Alan Mackenzie wrote: >>>>>>>>>>>> [ Followup-To: set ] >>>>>>>>>>>> >>>>>>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>>>>>> On 6/22/2026 1:42 PM, Alan Mackenzie wrote: >>>>>>>>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>>>>>>>> On 6/22/2026 10:48 AM, Alan Mackenzie wrote: >>>>>>>>>>>> >>>>>>>>>>>>>>>> G is true. >>>>>>>>>>>> >>>>>>>>>>>>>>>> I put it to you you're lying again. No reputable >>>>>>>>>>>>>>>> mathematician >>>>>>>>>>>>>>>> would >>>>>>>>>>>>>>>> risk his reputation by saying false things. If Dag Prawitz >>>>>>>>>>>>>>>> really >>>>>>>>>>>>>>>> did >>>>>>>>>>>>>>>> "agree" (with whom?) that Gödel's sentence G is not true in >>>>>>>>>>>>>>>> Peano >>>>>>>>>>>>>>>> Arithmetic, then produce a citation for this. >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>>>>> He never gets to Gödel. He essentially says unprovable >>>>>>>>>>>>>>> means untrue all the time for everything within his >>>>>>>>>>>>>>> own Theory of Grounds of strict Proof Theoretic Semantics. >>>>>>>>>>>> >>>>>>>>>>>>>> You won't understand it, but that _is_ essentially Gödel's >>>>>>>>>>>>>> Incompleteness >>>>>>>>>>>>>> Theorem. It is a statement that any sufficiently powerful >>>>>>>>>>>>>> system can >>>>>>>>>>>>>> express true things it can't prove. So Dag Prawitz, had >>>>>>>>>>>>>> he been >>>>>>>>>>>>>> saying >>>>>>>>>>>>>> the things you falsely attributed to him, would certainly >>>>>>>>>>>>>> have >>>>>>>>>>>>>> "got" to >>>>>>>>>>>>>> Gödel, and would have understood full well what he was >>>>>>>>>>>>>> saying. >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>>> You did not pay close enough attention to my exact words. >>>>>>>>>>>> >>>>>>>>>>>> I was right, you didn't understand it. >>>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>> >>>>>>>>>> >>>>>>>>>> Yeah, I'm pretty sure that "Dag Prawitz says what Dag Prawitz >>>>>>>>>> says", >>>>>>>>>> and furthermore "Dag Prawitz doesn't say what Dag Prawitz doesn't >>>>>>>>>> say", >>>>>>>>>> then looking a bit into his tremendous volume of works, >>>>>>>>>> he talks about "natural deduction" then specifically an "inverse >>>>>>>>>> principle" so I think these are key aspects of fundamental logic. >>>>>>>>>> >>>>>>>>>> https://www.researchgate.net/ >>>>>>>>>> publication/233365263_On_Inversion_Principles >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> "On Inversion Principles >>>>>>>>>> >>>>>>>>>> Enrico Moriconi∗Laura Tesconi† >>>>>>>>>> May 8, 2007 >>>>>>>>>> >>>>>>>>>> Abstract >>>>>>>>>> The idea of an “inversion principle”, and the name itself, >>>>>>>>>> originated in >>>>>>>>>> the work of Paul Lorenzen in the 1950s, as a method to generate >>>>>>>>>> new ad- >>>>>>>>>> missible rules within a certain syntactic context. Some fifteen >>>>>>>>>> years >>>>>>>>>> later, the idea was taken up by Dag Prawitz to devise a >>>>>>>>>> strategy of >>>>>>>>>> normalization for natural deduction calculi (this being an >>>>>>>>>> analogue of >>>>>>>>>> Gentzen’s cut-elimination theorem for sequent calculi). Later, >>>>>>>>>> Prawitz >>>>>>>>>> used the inversion principle again, attributing it with a >>>>>>>>>> semantic >>>>>>>>>> role. >>>>>>>>>> Still working in natural deduction calculi, he formulated a >>>>>>>>>> general >>>>>>>>>> type >>>>>>>>>> of schematic Introduction rules to be matched—thanks to the idea >>>>>>>>>> supporting the inversion principle — by a corresponding general >>>>>>>>>> schematic Elimination rule. This was an attempt to provide a >>>>>>>>>> solution to >>>>>>>>>> the problem suggested by the often quoted note of Gentzen. >>>>>>>>>> According to >>>>>>>>>> Gentzen “it should be possible to display the elimination >>>>>>>>>> rules as >>>>>>>>>> unique functions of the corresponding introduction rules on the >>>>>>>>>> basis of >>>>>>>>>> certain requirements.” Many people have since worked on this >>>>>>>>>> topic, >>>>>>>>>> which can be appropriately seen as the birthplace of what are now >>>>>>>>>> referred to as “general elimination rules”, recently studied >>>>>>>>>> thoroughly >>>>>>>>>> by Sara Negri and Jan von Plato. In this paper, we retrace the >>>>>>>>>> main >>>>>>>>>> threads of this chapter of proof-theoretical investigation, using >>>>>>>>>> Lorenzen’s original framework as a general guide" >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> Hm, "general elimination rules", seem derivable from De Morgan's >>>>>>>>>> laws, >>>>>>>>>> and that being the usual account of naive deductive analysis, >>>>>>>>>> then >>>>>>>>>> since >>>>>>>>>> "natural deduction", which here is held as part of the theory >>>>>>>>>> since it's naturally logical, then has for Gentzen that besides >>>>>>>>>> Kripke >>>>>>>>>> afterward there's also Sheffer and Chwistek before, and >>>>>>>>>> instead of >>>>>>>>>> Montague for semantics there's Herbrand for semantics, so, >>>>>>>>>> what to do >>>>>>>>>> about "inversion principle" is here that the thea-theory has that >>>>>>>>>> it's >>>>>>>>>> what subsumes "non-contradiction principle", here hoping that the >>>>>>>>>> interpretation aligns and thusly that "principle of inversion" >>>>>>>>>> wouldn't >>>>>>>>>> need dis-ambiguation from "inversion principle". >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> https://www.tandfonline.com/doi/abs/10.1080/01445340701830334 >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> https://www.strandbooks.com/natural-deduction-a-proof- >>>>>>>>>> theoretical- >>>>>>>>>> study-9780486446554.html >>>>>>>>>> >>>>>>>>>> "... [Prawitz'] inversion principle constitutes the foundation of >>>>>>>>>> most >>>>>>>>>> modern accounts of proof-theoretic semantics." >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> I already have a principle of inversion and furthermore a >>>>>>>>>> principle of >>>>>>>>>> thorough reason as subsuming principles of non-contradiction >>>>>>>>>> and what >>>>>>>>>> suffices, so, I'll be curious then about what to make of Prawitz' >>>>>>>>>> "inversion principle" since Lorenzen. >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> Of course the concept of an "inversion principle" is as old as >>>>>>>>>> the >>>>>>>>>> oldest account of Western philosophy like Heraclitus with dual >>>>>>>>>> monism. >>>>>>>>>> In fact by definition it's about the most basic aspect of >>>>>>>>>> contemplation >>>>>>>>>> and deliberation in abstraction of looking at both sides of >>>>>>>>>> issues >>>>>>>>>> and >>>>>>>>>> resolving inductive impasses with analytical bridges after >>>>>>>>>> complementary >>>>>>>>>> duals. >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> https://arxiv.org/abs/2112.14967 >>>>>>>>>> >>>>>>>>>> "Prawitz formulated the so-called inversion principle as one >>>>>>>>>> of the >>>>>>>>>> characteristic features of Gentzen's intuitionistic natural >>>>>>>>>> deduction. >>>>>>>>>> In the literature on proof-theoretic semantics, this principle is >>>>>>>>>> often >>>>>>>>>> coupled with another that is called the recovery principle. By >>>>>>>>>> adopting >>>>>>>>>> the Computational Ludics framework, we reformulate these >>>>>>>>>> principles >>>>>>>>>> into >>>>>>>>>> one and the same condition, which we call the harmony >>>>>>>>>> condition. We >>>>>>>>>> show >>>>>>>>>> that this reformulation allows us to reveal two intuitive ideas >>>>>>>>>> standing >>>>>>>>>> behind these principles: the idea of "containment" present in the >>>>>>>>>> inversion principle, and the idea that the recovery principle >>>>>>>>>> is the >>>>>>>>>> "converse" of the inversion principle. We also formulate two >>>>>>>>>> other >>>>>>>>>> conditions in the Computational Ludics framework, and we show >>>>>>>>>> that >>>>>>>>>> each >>>>>>>>>> of them is equivalent to the harmony condition." >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> The "ludicus" is Latin and for accounts of wisdom and knowledge. >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> "In particular, by taking inspiration from the >>>>>>>>>> Brouwer-Heyting-Kolmogorov explanation of logical connectives, >>>>>>>>>> proof-theoretic semantics rests on the idea that we know the >>>>>>>>>> meaning of >>>>>>>>>> a compound sentence when we know what counts as a canonical >>>>>>>>>> proof of >>>>>>>>>> it. >>>>>>>>>> And if proofs are formalised within the framework of natural >>>>>>>>>> deduction, >>>>>>>>>> then a canonical proof of a sentence A is nothing but a closed >>>>>>>>>> derivation ending with an introduction rule of the main >>>>>>>>>> connective >>>>>>>>>> of A." >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> The "canonical proofs" are not unique, in any system strong >>>>>>>>>> enough >>>>>>>>>> to make for infinitary reasoning and super-classical results >>>>>>>>>> requiring >>>>>>>>>> analytical bridges about infinity and continuity. >>>>>>>>>> >>>>>>>>> >>>>>>>>> It is the role that "canonical proofs" play in >>>>>>>>> Truth as an Epistemic Notion >>>>>>>>> https://link.springer.com/article/10.1007/s11245-011-9107-6 >>>>>>>>> That is the most important gist of his whole work. >>>>>>>>> >>>>>>>>> He later goes on to develop and further elaborate his >>>>>>>>> Theory of Grounds. >>>>>>>>> >>>>>>>>> Atomic Systems in Proof-Theoretic Semantics: Two Approaches >>>>>>>>> Thomas Piecha & Peter Schroeder-Heister do this same sort of >>>>>>>>> thing two different ways. >>>>>>>>> >>>>>>>>> >>>>>>>>> >>>>>>>> >>>>>>>> Furthermore I say there are "canonical proofs" of inductive >>>>>>>> sorts that >>>>>>>> make contradictions and thusly destroy each other. >>>>>>>> >>>>>>>> >>>>>>> >>>>>>> Clearly you have no idea what Dag Prawitz means by "canonical >>>>>>> proofs". >>>>>>> Go find out and then get back to me. >>>>>>> >>>>>>>> This is where "the thorough" and "analytical bridges" make repairs >>>>>>>> of what otherwise is flawed, or for hard constructivist realist >>>>>>>> structuralist model theorists: not-theories (examples of wrong). >>>>>>>> >>>>>>>> >>>>>>> >>>>>>> >>>>>> >>>>>> >>>>>> Induction and counter-induction contradict each other, it's simple, >>>>>> it's the grounds for most things called "paradox". >>>>>> >>>>>> >>>>> >>>>> % This sentence is not true. >>>>> ?- LP = not(true(LP)). >>>>> LP = not(true(LP)). >>>>> ?- unify_with_occurs_check(LP, not(true(LP))). >>>>> false. >>>>> >>>>> After you totally understand how and why the proof >>>>> theoretic semantics of that is correct and resolves >>>>> the Liar Paradox get back to me. >>>>> >>>>> The essential principle involved that I derived >>>>> in my own Minimal Type Theory before I knew that >>>>> Prolog could do the same thing is that: >>>>> >>>>> When the directed graph of the evaluation >>>>> sequence of an expression contains a cycle >>>>> then the input is determined to be incoherent >>>>> on the basis that its proof would never terminate. >>>>> Proof Theoretic Semantics does this exact same thing. >>>>> >>>>> Don't get back to me until you attain the required >>>>> prerequisites. I am sure that you already know >>>>> all about cycles in directed graphs. >>>>> >>>> >>>> Declaring oneself ignorant thus wise >>>> doesn't make much of a case >>>> except being ignorant. >>>> >>>> 300 mile per hour wheelchair: can't take stairs. >>>> >>>> Except down, .... >>>> >>>> >>> >>> So you are going to imply that I am incorrect >>> about Prolog when you yourself remain clueless about Prolog? >>> That would be dishonest. >> >> No, pointing out that you are worng about Prolog when you are wrong >> about Prolog is never dishohest. > > That is correct Prolog and that is the > result of the correct run of correct Prolog. Irrelevant. Nobody claimed there be Prolog errors in your queries. > Implying that I am wrong about Prolog without > pointing out any actual mistake is also DISHONEST. How did Ross FInlayson imply that you were wrong about Prolog? -- Mikko
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2026-06-25 11:16 -0500 |
| Subject | Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs |
| Message-ID | <111jk9r$3tg4p$2@dont-email.me> |
| In reply to | #141948 |
On 6/25/2026 2:29 AM, Mikko wrote: > On 25/06/2026 00:33, olcott wrote: >> On 6/24/2026 5:13 AM, Mikko wrote: >>> On 23/06/2026 21:20, olcott wrote: >>>> On 6/23/2026 12:32 PM, Ross Finlayson wrote: >>>>> On 06/23/2026 09:54 AM, olcott wrote: >>>>>> On 6/23/2026 10:51 AM, Ross Finlayson wrote: >>>>>>> On 06/23/2026 07:22 AM, olcott wrote: >>>>>>>> On 6/22/2026 11:31 PM, Ross Finlayson wrote: >>>>>>>>> On 06/22/2026 09:14 PM, olcott wrote: >>>>>>>>>> On 6/22/2026 11:00 PM, Ross Finlayson wrote: >>>>>>>>>>> On 06/22/2026 01:06 PM, olcott wrote: >>>>>>>>>>>> On 6/22/2026 2:50 PM, Alan Mackenzie wrote: >>>>>>>>>>>>> [ Followup-To: set ] >>>>>>>>>>>>> >>>>>>>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>>>>>>> On 6/22/2026 1:42 PM, Alan Mackenzie wrote: >>>>>>>>>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>>>>>>>>> On 6/22/2026 10:48 AM, Alan Mackenzie wrote: >>>>>>>>>>>>> >>>>>>>>>>>>>>>>> G is true. >>>>>>>>>>>>> >>>>>>>>>>>>>>>>> I put it to you you're lying again. No reputable >>>>>>>>>>>>>>>>> mathematician >>>>>>>>>>>>>>>>> would >>>>>>>>>>>>>>>>> risk his reputation by saying false things. If Dag >>>>>>>>>>>>>>>>> Prawitz >>>>>>>>>>>>>>>>> really >>>>>>>>>>>>>>>>> did >>>>>>>>>>>>>>>>> "agree" (with whom?) that Gödel's sentence G is not >>>>>>>>>>>>>>>>> true in >>>>>>>>>>>>>>>>> Peano >>>>>>>>>>>>>>>>> Arithmetic, then produce a citation for this. >>>>>>>>>>>>> >>>>>>>>>>>>> >>>>>>>>>>>>>>>> He never gets to Gödel. He essentially says unprovable >>>>>>>>>>>>>>>> means untrue all the time for everything within his >>>>>>>>>>>>>>>> own Theory of Grounds of strict Proof Theoretic Semantics. >>>>>>>>>>>>> >>>>>>>>>>>>>>> You won't understand it, but that _is_ essentially Gödel's >>>>>>>>>>>>>>> Incompleteness >>>>>>>>>>>>>>> Theorem. It is a statement that any sufficiently powerful >>>>>>>>>>>>>>> system can >>>>>>>>>>>>>>> express true things it can't prove. So Dag Prawitz, had >>>>>>>>>>>>>>> he been >>>>>>>>>>>>>>> saying >>>>>>>>>>>>>>> the things you falsely attributed to him, would certainly >>>>>>>>>>>>>>> have >>>>>>>>>>>>>>> "got" to >>>>>>>>>>>>>>> Gödel, and would have understood full well what he was >>>>>>>>>>>>>>> saying. >>>>>>>>>>>>> >>>>>>>>>>>>> >>>>>>>>>>>>>> You did not pay close enough attention to my exact words. >>>>>>>>>>>>> >>>>>>>>>>>>> I was right, you didn't understand it. >>>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> Yeah, I'm pretty sure that "Dag Prawitz says what Dag Prawitz >>>>>>>>>>> says", >>>>>>>>>>> and furthermore "Dag Prawitz doesn't say what Dag Prawitz >>>>>>>>>>> doesn't >>>>>>>>>>> say", >>>>>>>>>>> then looking a bit into his tremendous volume of works, >>>>>>>>>>> he talks about "natural deduction" then specifically an "inverse >>>>>>>>>>> principle" so I think these are key aspects of fundamental >>>>>>>>>>> logic. >>>>>>>>>>> >>>>>>>>>>> https://www.researchgate.net/ >>>>>>>>>>> publication/233365263_On_Inversion_Principles >>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> "On Inversion Principles >>>>>>>>>>> >>>>>>>>>>> Enrico Moriconi∗Laura Tesconi† >>>>>>>>>>> May 8, 2007 >>>>>>>>>>> >>>>>>>>>>> Abstract >>>>>>>>>>> The idea of an “inversion principle”, and the name itself, >>>>>>>>>>> originated in >>>>>>>>>>> the work of Paul Lorenzen in the 1950s, as a method to generate >>>>>>>>>>> new ad- >>>>>>>>>>> missible rules within a certain syntactic context. Some >>>>>>>>>>> fifteen years >>>>>>>>>>> later, the idea was taken up by Dag Prawitz to devise a >>>>>>>>>>> strategy of >>>>>>>>>>> normalization for natural deduction calculi (this being an >>>>>>>>>>> analogue of >>>>>>>>>>> Gentzen’s cut-elimination theorem for sequent calculi). Later, >>>>>>>>>>> Prawitz >>>>>>>>>>> used the inversion principle again, attributing it with a >>>>>>>>>>> semantic >>>>>>>>>>> role. >>>>>>>>>>> Still working in natural deduction calculi, he formulated a >>>>>>>>>>> general >>>>>>>>>>> type >>>>>>>>>>> of schematic Introduction rules to be matched—thanks to the idea >>>>>>>>>>> supporting the inversion principle — by a corresponding general >>>>>>>>>>> schematic Elimination rule. This was an attempt to provide a >>>>>>>>>>> solution to >>>>>>>>>>> the problem suggested by the often quoted note of Gentzen. >>>>>>>>>>> According to >>>>>>>>>>> Gentzen “it should be possible to display the elimination >>>>>>>>>>> rules as >>>>>>>>>>> unique functions of the corresponding introduction rules on the >>>>>>>>>>> basis of >>>>>>>>>>> certain requirements.” Many people have since worked on this >>>>>>>>>>> topic, >>>>>>>>>>> which can be appropriately seen as the birthplace of what are >>>>>>>>>>> now >>>>>>>>>>> referred to as “general elimination rules”, recently studied >>>>>>>>>>> thoroughly >>>>>>>>>>> by Sara Negri and Jan von Plato. In this paper, we retrace >>>>>>>>>>> the main >>>>>>>>>>> threads of this chapter of proof-theoretical investigation, >>>>>>>>>>> using >>>>>>>>>>> Lorenzen’s original framework as a general guide" >>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> Hm, "general elimination rules", seem derivable from De Morgan's >>>>>>>>>>> laws, >>>>>>>>>>> and that being the usual account of naive deductive analysis, >>>>>>>>>>> then >>>>>>>>>>> since >>>>>>>>>>> "natural deduction", which here is held as part of the theory >>>>>>>>>>> since it's naturally logical, then has for Gentzen that besides >>>>>>>>>>> Kripke >>>>>>>>>>> afterward there's also Sheffer and Chwistek before, and >>>>>>>>>>> instead of >>>>>>>>>>> Montague for semantics there's Herbrand for semantics, so, >>>>>>>>>>> what to do >>>>>>>>>>> about "inversion principle" is here that the thea-theory has >>>>>>>>>>> that >>>>>>>>>>> it's >>>>>>>>>>> what subsumes "non-contradiction principle", here hoping that >>>>>>>>>>> the >>>>>>>>>>> interpretation aligns and thusly that "principle of inversion" >>>>>>>>>>> wouldn't >>>>>>>>>>> need dis-ambiguation from "inversion principle". >>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> https://www.tandfonline.com/doi/abs/10.1080/01445340701830334 >>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> https://www.strandbooks.com/natural-deduction-a-proof- >>>>>>>>>>> theoretical- >>>>>>>>>>> study-9780486446554.html >>>>>>>>>>> >>>>>>>>>>> "... [Prawitz'] inversion principle constitutes the >>>>>>>>>>> foundation of >>>>>>>>>>> most >>>>>>>>>>> modern accounts of proof-theoretic semantics." >>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> I already have a principle of inversion and furthermore a >>>>>>>>>>> principle of >>>>>>>>>>> thorough reason as subsuming principles of non-contradiction >>>>>>>>>>> and what >>>>>>>>>>> suffices, so, I'll be curious then about what to make of >>>>>>>>>>> Prawitz' >>>>>>>>>>> "inversion principle" since Lorenzen. >>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> Of course the concept of an "inversion principle" is as old >>>>>>>>>>> as the >>>>>>>>>>> oldest account of Western philosophy like Heraclitus with dual >>>>>>>>>>> monism. >>>>>>>>>>> In fact by definition it's about the most basic aspect of >>>>>>>>>>> contemplation >>>>>>>>>>> and deliberation in abstraction of looking at both sides of >>>>>>>>>>> issues >>>>>>>>>>> and >>>>>>>>>>> resolving inductive impasses with analytical bridges after >>>>>>>>>>> complementary >>>>>>>>>>> duals. >>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> https://arxiv.org/abs/2112.14967 >>>>>>>>>>> >>>>>>>>>>> "Prawitz formulated the so-called inversion principle as one >>>>>>>>>>> of the >>>>>>>>>>> characteristic features of Gentzen's intuitionistic natural >>>>>>>>>>> deduction. >>>>>>>>>>> In the literature on proof-theoretic semantics, this >>>>>>>>>>> principle is >>>>>>>>>>> often >>>>>>>>>>> coupled with another that is called the recovery principle. By >>>>>>>>>>> adopting >>>>>>>>>>> the Computational Ludics framework, we reformulate these >>>>>>>>>>> principles >>>>>>>>>>> into >>>>>>>>>>> one and the same condition, which we call the harmony >>>>>>>>>>> condition. We >>>>>>>>>>> show >>>>>>>>>>> that this reformulation allows us to reveal two intuitive ideas >>>>>>>>>>> standing >>>>>>>>>>> behind these principles: the idea of "containment" present in >>>>>>>>>>> the >>>>>>>>>>> inversion principle, and the idea that the recovery principle >>>>>>>>>>> is the >>>>>>>>>>> "converse" of the inversion principle. We also formulate two >>>>>>>>>>> other >>>>>>>>>>> conditions in the Computational Ludics framework, and we show >>>>>>>>>>> that >>>>>>>>>>> each >>>>>>>>>>> of them is equivalent to the harmony condition." >>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> The "ludicus" is Latin and for accounts of wisdom and knowledge. >>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> "In particular, by taking inspiration from the >>>>>>>>>>> Brouwer-Heyting-Kolmogorov explanation of logical connectives, >>>>>>>>>>> proof-theoretic semantics rests on the idea that we know the >>>>>>>>>>> meaning of >>>>>>>>>>> a compound sentence when we know what counts as a canonical >>>>>>>>>>> proof of >>>>>>>>>>> it. >>>>>>>>>>> And if proofs are formalised within the framework of natural >>>>>>>>>>> deduction, >>>>>>>>>>> then a canonical proof of a sentence A is nothing but a closed >>>>>>>>>>> derivation ending with an introduction rule of the main >>>>>>>>>>> connective >>>>>>>>>>> of A." >>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> The "canonical proofs" are not unique, in any system strong >>>>>>>>>>> enough >>>>>>>>>>> to make for infinitary reasoning and super-classical results >>>>>>>>>>> requiring >>>>>>>>>>> analytical bridges about infinity and continuity. >>>>>>>>>>> >>>>>>>>>> >>>>>>>>>> It is the role that "canonical proofs" play in >>>>>>>>>> Truth as an Epistemic Notion >>>>>>>>>> https://link.springer.com/article/10.1007/s11245-011-9107-6 >>>>>>>>>> That is the most important gist of his whole work. >>>>>>>>>> >>>>>>>>>> He later goes on to develop and further elaborate his >>>>>>>>>> Theory of Grounds. >>>>>>>>>> >>>>>>>>>> Atomic Systems in Proof-Theoretic Semantics: Two Approaches >>>>>>>>>> Thomas Piecha & Peter Schroeder-Heister do this same sort of >>>>>>>>>> thing two different ways. >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> >>>>>>>>> >>>>>>>>> Furthermore I say there are "canonical proofs" of inductive >>>>>>>>> sorts that >>>>>>>>> make contradictions and thusly destroy each other. >>>>>>>>> >>>>>>>>> >>>>>>>> >>>>>>>> Clearly you have no idea what Dag Prawitz means by "canonical >>>>>>>> proofs". >>>>>>>> Go find out and then get back to me. >>>>>>>> >>>>>>>>> This is where "the thorough" and "analytical bridges" make repairs >>>>>>>>> of what otherwise is flawed, or for hard constructivist realist >>>>>>>>> structuralist model theorists: not-theories (examples of wrong). >>>>>>>>> >>>>>>>>> >>>>>>>> >>>>>>>> >>>>>>> >>>>>>> >>>>>>> Induction and counter-induction contradict each other, it's simple, >>>>>>> it's the grounds for most things called "paradox". >>>>>>> >>>>>>> >>>>>> >>>>>> % This sentence is not true. >>>>>> ?- LP = not(true(LP)). >>>>>> LP = not(true(LP)). >>>>>> ?- unify_with_occurs_check(LP, not(true(LP))). >>>>>> false. >>>>>> >>>>>> After you totally understand how and why the proof >>>>>> theoretic semantics of that is correct and resolves >>>>>> the Liar Paradox get back to me. >>>>>> >>>>>> The essential principle involved that I derived >>>>>> in my own Minimal Type Theory before I knew that >>>>>> Prolog could do the same thing is that: >>>>>> >>>>>> When the directed graph of the evaluation >>>>>> sequence of an expression contains a cycle >>>>>> then the input is determined to be incoherent >>>>>> on the basis that its proof would never terminate. >>>>>> Proof Theoretic Semantics does this exact same thing. >>>>>> >>>>>> Don't get back to me until you attain the required >>>>>> prerequisites. I am sure that you already know >>>>>> all about cycles in directed graphs. >>>>>> >>>>> >>>>> Declaring oneself ignorant thus wise >>>>> doesn't make much of a case >>>>> except being ignorant. >>>>> >>>>> 300 mile per hour wheelchair: can't take stairs. >>>>> >>>>> Except down, .... >>>>> >>>>> >>>> >>>> So you are going to imply that I am incorrect >>>> about Prolog when you yourself remain clueless about Prolog? >>>> That would be dishonest. >>> >>> No, pointing out that you are worng about Prolog when you are wrong >>> about Prolog is never dishohest. >> >> That is correct Prolog and that is the >> result of the correct run of correct Prolog. > > Irrelevant. Nobody claimed there be Prolog errors in your queries. > >> Implying that I am wrong about Prolog without >> pointing out any actual mistake is also DISHONEST. > > How did Ross FInlayson imply that you were wrong about Prolog? > If an error is claimed then it must be specifically pointed out otherwise the clam of error is dishonest. -- Copyright 2026 Olcott My 28 year goal has been to make "true on the basis of meaning expressed in language" reliably computable for the entire body of knowledge. The complete structure of this system is now defined. The entire body of knowledge expressed in language is comprised of two types of relations between finite strings: (a) *Axioms* Expressions of language that are stipulated to be true. My system bridges the analytic/synthetic distinction by expressly encoding all empirical "atomic facts" in a formal language such as CycL of the Cyc project. (b) *Inference Rules* Expressions of language that are semantically entailed syntactically from (a) and/or (b).
[toc] | [prev] | [next] | [standalone]
| From | Mikko <mikko.levanto@iki.fi> |
|---|---|
| Date | 2026-06-26 09:45 +0300 |
| Subject | Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs |
| Message-ID | <111l76n$b8mp$1@dont-email.me> |
| In reply to | #141955 |
On 25/06/2026 19:16, olcott wrote: > On 6/25/2026 2:29 AM, Mikko wrote: >> On 25/06/2026 00:33, olcott wrote: >>> On 6/24/2026 5:13 AM, Mikko wrote: >>>> On 23/06/2026 21:20, olcott wrote: >>>>> On 6/23/2026 12:32 PM, Ross Finlayson wrote: >>>>>> On 06/23/2026 09:54 AM, olcott wrote: >>>>>>> On 6/23/2026 10:51 AM, Ross Finlayson wrote: >>>>>>>> On 06/23/2026 07:22 AM, olcott wrote: >>>>>>>>> On 6/22/2026 11:31 PM, Ross Finlayson wrote: >>>>>>>>>> On 06/22/2026 09:14 PM, olcott wrote: >>>>>>>>>>> On 6/22/2026 11:00 PM, Ross Finlayson wrote: >>>>>>>>>>>> On 06/22/2026 01:06 PM, olcott wrote: >>>>>>>>>>>>> On 6/22/2026 2:50 PM, Alan Mackenzie wrote: >>>>>>>>>>>>>> [ Followup-To: set ] >>>>>>>>>>>>>> >>>>>>>>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>>>>>>>> On 6/22/2026 1:42 PM, Alan Mackenzie wrote: >>>>>>>>>>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>>>>>>>>>> On 6/22/2026 10:48 AM, Alan Mackenzie wrote: >>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>> G is true. >>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>> I put it to you you're lying again. No reputable >>>>>>>>>>>>>>>>>> mathematician >>>>>>>>>>>>>>>>>> would >>>>>>>>>>>>>>>>>> risk his reputation by saying false things. If Dag >>>>>>>>>>>>>>>>>> Prawitz >>>>>>>>>>>>>>>>>> really >>>>>>>>>>>>>>>>>> did >>>>>>>>>>>>>>>>>> "agree" (with whom?) that Gödel's sentence G is not >>>>>>>>>>>>>>>>>> true in >>>>>>>>>>>>>>>>>> Peano >>>>>>>>>>>>>>>>>> Arithmetic, then produce a citation for this. >>>>>>>>>>>>>> >>>>>>>>>>>>>> >>>>>>>>>>>>>>>>> He never gets to Gödel. He essentially says unprovable >>>>>>>>>>>>>>>>> means untrue all the time for everything within his >>>>>>>>>>>>>>>>> own Theory of Grounds of strict Proof Theoretic Semantics. >>>>>>>>>>>>>> >>>>>>>>>>>>>>>> You won't understand it, but that _is_ essentially Gödel's >>>>>>>>>>>>>>>> Incompleteness >>>>>>>>>>>>>>>> Theorem. It is a statement that any sufficiently powerful >>>>>>>>>>>>>>>> system can >>>>>>>>>>>>>>>> express true things it can't prove. So Dag Prawitz, had >>>>>>>>>>>>>>>> he been >>>>>>>>>>>>>>>> saying >>>>>>>>>>>>>>>> the things you falsely attributed to him, would >>>>>>>>>>>>>>>> certainly have >>>>>>>>>>>>>>>> "got" to >>>>>>>>>>>>>>>> Gödel, and would have understood full well what he was >>>>>>>>>>>>>>>> saying. >>>>>>>>>>>>>> >>>>>>>>>>>>>> >>>>>>>>>>>>>>> You did not pay close enough attention to my exact words. >>>>>>>>>>>>>> >>>>>>>>>>>>>> I was right, you didn't understand it. >>>>>>>>>>>>>> >>>>>>>>>>>>> >>>>>>>>>>>>> >>>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> Yeah, I'm pretty sure that "Dag Prawitz says what Dag >>>>>>>>>>>> Prawitz says", >>>>>>>>>>>> and furthermore "Dag Prawitz doesn't say what Dag Prawitz >>>>>>>>>>>> doesn't >>>>>>>>>>>> say", >>>>>>>>>>>> then looking a bit into his tremendous volume of works, >>>>>>>>>>>> he talks about "natural deduction" then specifically an >>>>>>>>>>>> "inverse >>>>>>>>>>>> principle" so I think these are key aspects of fundamental >>>>>>>>>>>> logic. >>>>>>>>>>>> >>>>>>>>>>>> https://www.researchgate.net/ >>>>>>>>>>>> publication/233365263_On_Inversion_Principles >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> "On Inversion Principles >>>>>>>>>>>> >>>>>>>>>>>> Enrico Moriconi∗Laura Tesconi† >>>>>>>>>>>> May 8, 2007 >>>>>>>>>>>> >>>>>>>>>>>> Abstract >>>>>>>>>>>> The idea of an “inversion principle”, and the name itself, >>>>>>>>>>>> originated in >>>>>>>>>>>> the work of Paul Lorenzen in the 1950s, as a method to generate >>>>>>>>>>>> new ad- >>>>>>>>>>>> missible rules within a certain syntactic context. Some >>>>>>>>>>>> fifteen years >>>>>>>>>>>> later, the idea was taken up by Dag Prawitz to devise a >>>>>>>>>>>> strategy of >>>>>>>>>>>> normalization for natural deduction calculi (this being an >>>>>>>>>>>> analogue of >>>>>>>>>>>> Gentzen’s cut-elimination theorem for sequent calculi). Later, >>>>>>>>>>>> Prawitz >>>>>>>>>>>> used the inversion principle again, attributing it with a >>>>>>>>>>>> semantic >>>>>>>>>>>> role. >>>>>>>>>>>> Still working in natural deduction calculi, he formulated a >>>>>>>>>>>> general >>>>>>>>>>>> type >>>>>>>>>>>> of schematic Introduction rules to be matched—thanks to the >>>>>>>>>>>> idea >>>>>>>>>>>> supporting the inversion principle — by a corresponding general >>>>>>>>>>>> schematic Elimination rule. This was an attempt to provide a >>>>>>>>>>>> solution to >>>>>>>>>>>> the problem suggested by the often quoted note of Gentzen. >>>>>>>>>>>> According to >>>>>>>>>>>> Gentzen “it should be possible to display the elimination >>>>>>>>>>>> rules as >>>>>>>>>>>> unique functions of the corresponding introduction rules on the >>>>>>>>>>>> basis of >>>>>>>>>>>> certain requirements.” Many people have since worked on this >>>>>>>>>>>> topic, >>>>>>>>>>>> which can be appropriately seen as the birthplace of what >>>>>>>>>>>> are now >>>>>>>>>>>> referred to as “general elimination rules”, recently studied >>>>>>>>>>>> thoroughly >>>>>>>>>>>> by Sara Negri and Jan von Plato. In this paper, we retrace >>>>>>>>>>>> the main >>>>>>>>>>>> threads of this chapter of proof-theoretical investigation, >>>>>>>>>>>> using >>>>>>>>>>>> Lorenzen’s original framework as a general guide" >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> Hm, "general elimination rules", seem derivable from De >>>>>>>>>>>> Morgan's >>>>>>>>>>>> laws, >>>>>>>>>>>> and that being the usual account of naive deductive >>>>>>>>>>>> analysis, then >>>>>>>>>>>> since >>>>>>>>>>>> "natural deduction", which here is held as part of the theory >>>>>>>>>>>> since it's naturally logical, then has for Gentzen that besides >>>>>>>>>>>> Kripke >>>>>>>>>>>> afterward there's also Sheffer and Chwistek before, and >>>>>>>>>>>> instead of >>>>>>>>>>>> Montague for semantics there's Herbrand for semantics, so, >>>>>>>>>>>> what to do >>>>>>>>>>>> about "inversion principle" is here that the thea-theory has >>>>>>>>>>>> that >>>>>>>>>>>> it's >>>>>>>>>>>> what subsumes "non-contradiction principle", here hoping >>>>>>>>>>>> that the >>>>>>>>>>>> interpretation aligns and thusly that "principle of inversion" >>>>>>>>>>>> wouldn't >>>>>>>>>>>> need dis-ambiguation from "inversion principle". >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> https://www.tandfonline.com/doi/abs/10.1080/01445340701830334 >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> https://www.strandbooks.com/natural-deduction-a-proof- >>>>>>>>>>>> theoretical- >>>>>>>>>>>> study-9780486446554.html >>>>>>>>>>>> >>>>>>>>>>>> "... [Prawitz'] inversion principle constitutes the >>>>>>>>>>>> foundation of >>>>>>>>>>>> most >>>>>>>>>>>> modern accounts of proof-theoretic semantics." >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> I already have a principle of inversion and furthermore a >>>>>>>>>>>> principle of >>>>>>>>>>>> thorough reason as subsuming principles of non-contradiction >>>>>>>>>>>> and what >>>>>>>>>>>> suffices, so, I'll be curious then about what to make of >>>>>>>>>>>> Prawitz' >>>>>>>>>>>> "inversion principle" since Lorenzen. >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> Of course the concept of an "inversion principle" is as old >>>>>>>>>>>> as the >>>>>>>>>>>> oldest account of Western philosophy like Heraclitus with dual >>>>>>>>>>>> monism. >>>>>>>>>>>> In fact by definition it's about the most basic aspect of >>>>>>>>>>>> contemplation >>>>>>>>>>>> and deliberation in abstraction of looking at both sides of >>>>>>>>>>>> issues >>>>>>>>>>>> and >>>>>>>>>>>> resolving inductive impasses with analytical bridges after >>>>>>>>>>>> complementary >>>>>>>>>>>> duals. >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> https://arxiv.org/abs/2112.14967 >>>>>>>>>>>> >>>>>>>>>>>> "Prawitz formulated the so-called inversion principle as one >>>>>>>>>>>> of the >>>>>>>>>>>> characteristic features of Gentzen's intuitionistic natural >>>>>>>>>>>> deduction. >>>>>>>>>>>> In the literature on proof-theoretic semantics, this >>>>>>>>>>>> principle is >>>>>>>>>>>> often >>>>>>>>>>>> coupled with another that is called the recovery principle. By >>>>>>>>>>>> adopting >>>>>>>>>>>> the Computational Ludics framework, we reformulate these >>>>>>>>>>>> principles >>>>>>>>>>>> into >>>>>>>>>>>> one and the same condition, which we call the harmony >>>>>>>>>>>> condition. We >>>>>>>>>>>> show >>>>>>>>>>>> that this reformulation allows us to reveal two intuitive ideas >>>>>>>>>>>> standing >>>>>>>>>>>> behind these principles: the idea of "containment" present >>>>>>>>>>>> in the >>>>>>>>>>>> inversion principle, and the idea that the recovery >>>>>>>>>>>> principle is the >>>>>>>>>>>> "converse" of the inversion principle. We also formulate two >>>>>>>>>>>> other >>>>>>>>>>>> conditions in the Computational Ludics framework, and we >>>>>>>>>>>> show that >>>>>>>>>>>> each >>>>>>>>>>>> of them is equivalent to the harmony condition." >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> The "ludicus" is Latin and for accounts of wisdom and >>>>>>>>>>>> knowledge. >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> "In particular, by taking inspiration from the >>>>>>>>>>>> Brouwer-Heyting-Kolmogorov explanation of logical connectives, >>>>>>>>>>>> proof-theoretic semantics rests on the idea that we know the >>>>>>>>>>>> meaning of >>>>>>>>>>>> a compound sentence when we know what counts as a canonical >>>>>>>>>>>> proof of >>>>>>>>>>>> it. >>>>>>>>>>>> And if proofs are formalised within the framework of natural >>>>>>>>>>>> deduction, >>>>>>>>>>>> then a canonical proof of a sentence A is nothing but a closed >>>>>>>>>>>> derivation ending with an introduction rule of the main >>>>>>>>>>>> connective >>>>>>>>>>>> of A." >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> The "canonical proofs" are not unique, in any system strong >>>>>>>>>>>> enough >>>>>>>>>>>> to make for infinitary reasoning and super-classical results >>>>>>>>>>>> requiring >>>>>>>>>>>> analytical bridges about infinity and continuity. >>>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> It is the role that "canonical proofs" play in >>>>>>>>>>> Truth as an Epistemic Notion >>>>>>>>>>> https://link.springer.com/article/10.1007/s11245-011-9107-6 >>>>>>>>>>> That is the most important gist of his whole work. >>>>>>>>>>> >>>>>>>>>>> He later goes on to develop and further elaborate his >>>>>>>>>>> Theory of Grounds. >>>>>>>>>>> >>>>>>>>>>> Atomic Systems in Proof-Theoretic Semantics: Two Approaches >>>>>>>>>>> Thomas Piecha & Peter Schroeder-Heister do this same sort of >>>>>>>>>>> thing two different ways. >>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>> >>>>>>>>>> Furthermore I say there are "canonical proofs" of inductive >>>>>>>>>> sorts that >>>>>>>>>> make contradictions and thusly destroy each other. >>>>>>>>>> >>>>>>>>>> >>>>>>>>> >>>>>>>>> Clearly you have no idea what Dag Prawitz means by "canonical >>>>>>>>> proofs". >>>>>>>>> Go find out and then get back to me. >>>>>>>>> >>>>>>>>>> This is where "the thorough" and "analytical bridges" make >>>>>>>>>> repairs >>>>>>>>>> of what otherwise is flawed, or for hard constructivist realist >>>>>>>>>> structuralist model theorists: not-theories (examples of wrong). >>>>>>>>>> >>>>>>>>>> >>>>>>>>> >>>>>>>>> >>>>>>>> >>>>>>>> >>>>>>>> Induction and counter-induction contradict each other, it's simple, >>>>>>>> it's the grounds for most things called "paradox". >>>>>>>> >>>>>>>> >>>>>>> >>>>>>> % This sentence is not true. >>>>>>> ?- LP = not(true(LP)). >>>>>>> LP = not(true(LP)). >>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))). >>>>>>> false. >>>>>>> >>>>>>> After you totally understand how and why the proof >>>>>>> theoretic semantics of that is correct and resolves >>>>>>> the Liar Paradox get back to me. >>>>>>> >>>>>>> The essential principle involved that I derived >>>>>>> in my own Minimal Type Theory before I knew that >>>>>>> Prolog could do the same thing is that: >>>>>>> >>>>>>> When the directed graph of the evaluation >>>>>>> sequence of an expression contains a cycle >>>>>>> then the input is determined to be incoherent >>>>>>> on the basis that its proof would never terminate. >>>>>>> Proof Theoretic Semantics does this exact same thing. >>>>>>> >>>>>>> Don't get back to me until you attain the required >>>>>>> prerequisites. I am sure that you already know >>>>>>> all about cycles in directed graphs. >>>>>>> >>>>>> >>>>>> Declaring oneself ignorant thus wise >>>>>> doesn't make much of a case >>>>>> except being ignorant. >>>>>> >>>>>> 300 mile per hour wheelchair: can't take stairs. >>>>>> >>>>>> Except down, .... >>>>>> >>>>>> >>>>> >>>>> So you are going to imply that I am incorrect >>>>> about Prolog when you yourself remain clueless about Prolog? >>>>> That would be dishonest. >>>> >>>> No, pointing out that you are worng about Prolog when you are wrong >>>> about Prolog is never dishohest. >>> >>> That is correct Prolog and that is the >>> result of the correct run of correct Prolog. >> >> Irrelevant. Nobody claimed there be Prolog errors in your queries. >> >>> Implying that I am wrong about Prolog without >>> pointing out any actual mistake is also DISHONEST. >> >> How did Ross FInlayson imply that you were wrong about Prolog? > > If an error is claimed then it must be specifically > pointed out otherwise the clam of error is dishonest. Yet you claim that Ross Finlayson be dishonest without pointing out what is dishonest in his words. -- Mikko
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2026-06-26 08:15 -0500 |
| Subject | Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs |
| Message-ID | <111lu0n$i4fc$1@dont-email.me> |
| In reply to | #141968 |
On 6/26/2026 1:45 AM, Mikko wrote: > On 25/06/2026 19:16, olcott wrote: >> On 6/25/2026 2:29 AM, Mikko wrote: >>> On 25/06/2026 00:33, olcott wrote: >>>> On 6/24/2026 5:13 AM, Mikko wrote: >>>>> On 23/06/2026 21:20, olcott wrote: >>>>>> On 6/23/2026 12:32 PM, Ross Finlayson wrote: >>>>>>> On 06/23/2026 09:54 AM, olcott wrote: >>>>>>>> On 6/23/2026 10:51 AM, Ross Finlayson wrote: >>>>>>>>> On 06/23/2026 07:22 AM, olcott wrote: >>>>>>>>>> On 6/22/2026 11:31 PM, Ross Finlayson wrote: >>>>>>>>>>> On 06/22/2026 09:14 PM, olcott wrote: >>>>>>>>>>>> On 6/22/2026 11:00 PM, Ross Finlayson wrote: >>>>>>>>>>>>> On 06/22/2026 01:06 PM, olcott wrote: >>>>>>>>>>>>>> On 6/22/2026 2:50 PM, Alan Mackenzie wrote: >>>>>>>>>>>>>>> [ Followup-To: set ] >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>>>>>>>>> On 6/22/2026 1:42 PM, Alan Mackenzie wrote: >>>>>>>>>>>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>>>>>>>>>>> On 6/22/2026 10:48 AM, Alan Mackenzie wrote: >>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>> G is true. >>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>> I put it to you you're lying again. No reputable >>>>>>>>>>>>>>>>>>> mathematician >>>>>>>>>>>>>>>>>>> would >>>>>>>>>>>>>>>>>>> risk his reputation by saying false things. If Dag >>>>>>>>>>>>>>>>>>> Prawitz >>>>>>>>>>>>>>>>>>> really >>>>>>>>>>>>>>>>>>> did >>>>>>>>>>>>>>>>>>> "agree" (with whom?) that Gödel's sentence G is not >>>>>>>>>>>>>>>>>>> true in >>>>>>>>>>>>>>>>>>> Peano >>>>>>>>>>>>>>>>>>> Arithmetic, then produce a citation for this. >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>> He never gets to Gödel. He essentially says unprovable >>>>>>>>>>>>>>>>>> means untrue all the time for everything within his >>>>>>>>>>>>>>>>>> own Theory of Grounds of strict Proof Theoretic >>>>>>>>>>>>>>>>>> Semantics. >>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>> You won't understand it, but that _is_ essentially Gödel's >>>>>>>>>>>>>>>>> Incompleteness >>>>>>>>>>>>>>>>> Theorem. It is a statement that any sufficiently powerful >>>>>>>>>>>>>>>>> system can >>>>>>>>>>>>>>>>> express true things it can't prove. So Dag Prawitz, >>>>>>>>>>>>>>>>> had he been >>>>>>>>>>>>>>>>> saying >>>>>>>>>>>>>>>>> the things you falsely attributed to him, would >>>>>>>>>>>>>>>>> certainly have >>>>>>>>>>>>>>>>> "got" to >>>>>>>>>>>>>>>>> Gödel, and would have understood full well what he was >>>>>>>>>>>>>>>>> saying. >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> You did not pay close enough attention to my exact words. >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> I was right, you didn't understand it. >>>>>>>>>>>>>>> >>>>>>>>>>>>>> >>>>>>>>>>>>>> >>>>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>>>> >>>>>>>>>>>>> >>>>>>>>>>>>> Yeah, I'm pretty sure that "Dag Prawitz says what Dag >>>>>>>>>>>>> Prawitz says", >>>>>>>>>>>>> and furthermore "Dag Prawitz doesn't say what Dag Prawitz >>>>>>>>>>>>> doesn't >>>>>>>>>>>>> say", >>>>>>>>>>>>> then looking a bit into his tremendous volume of works, >>>>>>>>>>>>> he talks about "natural deduction" then specifically an >>>>>>>>>>>>> "inverse >>>>>>>>>>>>> principle" so I think these are key aspects of fundamental >>>>>>>>>>>>> logic. >>>>>>>>>>>>> >>>>>>>>>>>>> https://www.researchgate.net/ >>>>>>>>>>>>> publication/233365263_On_Inversion_Principles >>>>>>>>>>>>> >>>>>>>>>>>>> >>>>>>>>>>>>> "On Inversion Principles >>>>>>>>>>>>> >>>>>>>>>>>>> Enrico Moriconi∗Laura Tesconi† >>>>>>>>>>>>> May 8, 2007 >>>>>>>>>>>>> >>>>>>>>>>>>> Abstract >>>>>>>>>>>>> The idea of an “inversion principle”, and the name itself, >>>>>>>>>>>>> originated in >>>>>>>>>>>>> the work of Paul Lorenzen in the 1950s, as a method to >>>>>>>>>>>>> generate >>>>>>>>>>>>> new ad- >>>>>>>>>>>>> missible rules within a certain syntactic context. Some >>>>>>>>>>>>> fifteen years >>>>>>>>>>>>> later, the idea was taken up by Dag Prawitz to devise a >>>>>>>>>>>>> strategy of >>>>>>>>>>>>> normalization for natural deduction calculi (this being an >>>>>>>>>>>>> analogue of >>>>>>>>>>>>> Gentzen’s cut-elimination theorem for sequent calculi). Later, >>>>>>>>>>>>> Prawitz >>>>>>>>>>>>> used the inversion principle again, attributing it with a >>>>>>>>>>>>> semantic >>>>>>>>>>>>> role. >>>>>>>>>>>>> Still working in natural deduction calculi, he formulated a >>>>>>>>>>>>> general >>>>>>>>>>>>> type >>>>>>>>>>>>> of schematic Introduction rules to be matched—thanks to the >>>>>>>>>>>>> idea >>>>>>>>>>>>> supporting the inversion principle — by a corresponding >>>>>>>>>>>>> general >>>>>>>>>>>>> schematic Elimination rule. This was an attempt to provide a >>>>>>>>>>>>> solution to >>>>>>>>>>>>> the problem suggested by the often quoted note of Gentzen. >>>>>>>>>>>>> According to >>>>>>>>>>>>> Gentzen “it should be possible to display the elimination >>>>>>>>>>>>> rules as >>>>>>>>>>>>> unique functions of the corresponding introduction rules on >>>>>>>>>>>>> the >>>>>>>>>>>>> basis of >>>>>>>>>>>>> certain requirements.” Many people have since worked on >>>>>>>>>>>>> this topic, >>>>>>>>>>>>> which can be appropriately seen as the birthplace of what >>>>>>>>>>>>> are now >>>>>>>>>>>>> referred to as “general elimination rules”, recently studied >>>>>>>>>>>>> thoroughly >>>>>>>>>>>>> by Sara Negri and Jan von Plato. In this paper, we retrace >>>>>>>>>>>>> the main >>>>>>>>>>>>> threads of this chapter of proof-theoretical investigation, >>>>>>>>>>>>> using >>>>>>>>>>>>> Lorenzen’s original framework as a general guide" >>>>>>>>>>>>> >>>>>>>>>>>>> >>>>>>>>>>>>> >>>>>>>>>>>>> Hm, "general elimination rules", seem derivable from De >>>>>>>>>>>>> Morgan's >>>>>>>>>>>>> laws, >>>>>>>>>>>>> and that being the usual account of naive deductive >>>>>>>>>>>>> analysis, then >>>>>>>>>>>>> since >>>>>>>>>>>>> "natural deduction", which here is held as part of the theory >>>>>>>>>>>>> since it's naturally logical, then has for Gentzen that >>>>>>>>>>>>> besides >>>>>>>>>>>>> Kripke >>>>>>>>>>>>> afterward there's also Sheffer and Chwistek before, and >>>>>>>>>>>>> instead of >>>>>>>>>>>>> Montague for semantics there's Herbrand for semantics, so, >>>>>>>>>>>>> what to do >>>>>>>>>>>>> about "inversion principle" is here that the thea-theory >>>>>>>>>>>>> has that >>>>>>>>>>>>> it's >>>>>>>>>>>>> what subsumes "non-contradiction principle", here hoping >>>>>>>>>>>>> that the >>>>>>>>>>>>> interpretation aligns and thusly that "principle of inversion" >>>>>>>>>>>>> wouldn't >>>>>>>>>>>>> need dis-ambiguation from "inversion principle". >>>>>>>>>>>>> >>>>>>>>>>>>> >>>>>>>>>>>>> https://www.tandfonline.com/doi/abs/10.1080/01445340701830334 >>>>>>>>>>>>> >>>>>>>>>>>>> >>>>>>>>>>>>> https://www.strandbooks.com/natural-deduction-a-proof- >>>>>>>>>>>>> theoretical- >>>>>>>>>>>>> study-9780486446554.html >>>>>>>>>>>>> >>>>>>>>>>>>> "... [Prawitz'] inversion principle constitutes the >>>>>>>>>>>>> foundation of >>>>>>>>>>>>> most >>>>>>>>>>>>> modern accounts of proof-theoretic semantics." >>>>>>>>>>>>> >>>>>>>>>>>>> >>>>>>>>>>>>> >>>>>>>>>>>>> I already have a principle of inversion and furthermore a >>>>>>>>>>>>> principle of >>>>>>>>>>>>> thorough reason as subsuming principles of non- >>>>>>>>>>>>> contradiction and what >>>>>>>>>>>>> suffices, so, I'll be curious then about what to make of >>>>>>>>>>>>> Prawitz' >>>>>>>>>>>>> "inversion principle" since Lorenzen. >>>>>>>>>>>>> >>>>>>>>>>>>> >>>>>>>>>>>>> Of course the concept of an "inversion principle" is as old >>>>>>>>>>>>> as the >>>>>>>>>>>>> oldest account of Western philosophy like Heraclitus with dual >>>>>>>>>>>>> monism. >>>>>>>>>>>>> In fact by definition it's about the most basic aspect of >>>>>>>>>>>>> contemplation >>>>>>>>>>>>> and deliberation in abstraction of looking at both sides of >>>>>>>>>>>>> issues >>>>>>>>>>>>> and >>>>>>>>>>>>> resolving inductive impasses with analytical bridges after >>>>>>>>>>>>> complementary >>>>>>>>>>>>> duals. >>>>>>>>>>>>> >>>>>>>>>>>>> >>>>>>>>>>>>> https://arxiv.org/abs/2112.14967 >>>>>>>>>>>>> >>>>>>>>>>>>> "Prawitz formulated the so-called inversion principle as >>>>>>>>>>>>> one of the >>>>>>>>>>>>> characteristic features of Gentzen's intuitionistic natural >>>>>>>>>>>>> deduction. >>>>>>>>>>>>> In the literature on proof-theoretic semantics, this >>>>>>>>>>>>> principle is >>>>>>>>>>>>> often >>>>>>>>>>>>> coupled with another that is called the recovery principle. By >>>>>>>>>>>>> adopting >>>>>>>>>>>>> the Computational Ludics framework, we reformulate these >>>>>>>>>>>>> principles >>>>>>>>>>>>> into >>>>>>>>>>>>> one and the same condition, which we call the harmony >>>>>>>>>>>>> condition. We >>>>>>>>>>>>> show >>>>>>>>>>>>> that this reformulation allows us to reveal two intuitive >>>>>>>>>>>>> ideas >>>>>>>>>>>>> standing >>>>>>>>>>>>> behind these principles: the idea of "containment" present >>>>>>>>>>>>> in the >>>>>>>>>>>>> inversion principle, and the idea that the recovery >>>>>>>>>>>>> principle is the >>>>>>>>>>>>> "converse" of the inversion principle. We also formulate >>>>>>>>>>>>> two other >>>>>>>>>>>>> conditions in the Computational Ludics framework, and we >>>>>>>>>>>>> show that >>>>>>>>>>>>> each >>>>>>>>>>>>> of them is equivalent to the harmony condition." >>>>>>>>>>>>> >>>>>>>>>>>>> >>>>>>>>>>>>> >>>>>>>>>>>>> The "ludicus" is Latin and for accounts of wisdom and >>>>>>>>>>>>> knowledge. >>>>>>>>>>>>> >>>>>>>>>>>>> >>>>>>>>>>>>> "In particular, by taking inspiration from the >>>>>>>>>>>>> Brouwer-Heyting-Kolmogorov explanation of logical connectives, >>>>>>>>>>>>> proof-theoretic semantics rests on the idea that we know the >>>>>>>>>>>>> meaning of >>>>>>>>>>>>> a compound sentence when we know what counts as a canonical >>>>>>>>>>>>> proof of >>>>>>>>>>>>> it. >>>>>>>>>>>>> And if proofs are formalised within the framework of natural >>>>>>>>>>>>> deduction, >>>>>>>>>>>>> then a canonical proof of a sentence A is nothing but a closed >>>>>>>>>>>>> derivation ending with an introduction rule of the main >>>>>>>>>>>>> connective >>>>>>>>>>>>> of A." >>>>>>>>>>>>> >>>>>>>>>>>>> >>>>>>>>>>>>> The "canonical proofs" are not unique, in any system strong >>>>>>>>>>>>> enough >>>>>>>>>>>>> to make for infinitary reasoning and super-classical results >>>>>>>>>>>>> requiring >>>>>>>>>>>>> analytical bridges about infinity and continuity. >>>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> It is the role that "canonical proofs" play in >>>>>>>>>>>> Truth as an Epistemic Notion >>>>>>>>>>>> https://link.springer.com/article/10.1007/s11245-011-9107-6 >>>>>>>>>>>> That is the most important gist of his whole work. >>>>>>>>>>>> >>>>>>>>>>>> He later goes on to develop and further elaborate his >>>>>>>>>>>> Theory of Grounds. >>>>>>>>>>>> >>>>>>>>>>>> Atomic Systems in Proof-Theoretic Semantics: Two Approaches >>>>>>>>>>>> Thomas Piecha & Peter Schroeder-Heister do this same sort of >>>>>>>>>>>> thing two different ways. >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> Furthermore I say there are "canonical proofs" of inductive >>>>>>>>>>> sorts that >>>>>>>>>>> make contradictions and thusly destroy each other. >>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>> >>>>>>>>>> Clearly you have no idea what Dag Prawitz means by "canonical >>>>>>>>>> proofs". >>>>>>>>>> Go find out and then get back to me. >>>>>>>>>> >>>>>>>>>>> This is where "the thorough" and "analytical bridges" make >>>>>>>>>>> repairs >>>>>>>>>>> of what otherwise is flawed, or for hard constructivist realist >>>>>>>>>>> structuralist model theorists: not-theories (examples of wrong). >>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>> >>>>>>>>>> >>>>>>>>> >>>>>>>>> >>>>>>>>> Induction and counter-induction contradict each other, it's >>>>>>>>> simple, >>>>>>>>> it's the grounds for most things called "paradox". >>>>>>>>> >>>>>>>>> >>>>>>>> >>>>>>>> % This sentence is not true. >>>>>>>> ?- LP = not(true(LP)). >>>>>>>> LP = not(true(LP)). >>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))). >>>>>>>> false. >>>>>>>> >>>>>>>> After you totally understand how and why the proof >>>>>>>> theoretic semantics of that is correct and resolves >>>>>>>> the Liar Paradox get back to me. >>>>>>>> >>>>>>>> The essential principle involved that I derived >>>>>>>> in my own Minimal Type Theory before I knew that >>>>>>>> Prolog could do the same thing is that: >>>>>>>> >>>>>>>> When the directed graph of the evaluation >>>>>>>> sequence of an expression contains a cycle >>>>>>>> then the input is determined to be incoherent >>>>>>>> on the basis that its proof would never terminate. >>>>>>>> Proof Theoretic Semantics does this exact same thing. >>>>>>>> >>>>>>>> Don't get back to me until you attain the required >>>>>>>> prerequisites. I am sure that you already know >>>>>>>> all about cycles in directed graphs. >>>>>>>> >>>>>>> >>>>>>> Declaring oneself ignorant thus wise >>>>>>> doesn't make much of a case >>>>>>> except being ignorant. >>>>>>> >>>>>>> 300 mile per hour wheelchair: can't take stairs. >>>>>>> >>>>>>> Except down, .... >>>>>>> >>>>>>> >>>>>> >>>>>> So you are going to imply that I am incorrect >>>>>> about Prolog when you yourself remain clueless about Prolog? >>>>>> That would be dishonest. >>>>> >>>>> No, pointing out that you are worng about Prolog when you are wrong >>>>> about Prolog is never dishohest. >>>> >>>> That is correct Prolog and that is the >>>> result of the correct run of correct Prolog. >>> >>> Irrelevant. Nobody claimed there be Prolog errors in your queries. >>> >>>> Implying that I am wrong about Prolog without >>>> pointing out any actual mistake is also DISHONEST. >>> >>> How did Ross FInlayson imply that you were wrong about Prolog? >> >> If an error is claimed then it must be specifically >> pointed out otherwise the clam of error is dishonest. > > Yet you claim that Ross Finlayson be dishonest without pointing > out what is dishonest in his words. > If anyone and everyone that claims that they found an error and never points out what the error is and why it is an error then they are merely a baseless denigrator. -- Copyright 2026 Olcott My 28 year goal has been to make "true on the basis of meaning expressed in language" reliably computable for the entire body of knowledge. The complete structure of this system is now defined. The entire body of knowledge expressed in language is comprised of two types of relations between finite strings: (a) *Axioms* Expressions of language that are stipulated to be true. My system bridges the analytic/synthetic distinction by expressly encoding all empirical "atomic facts" in a formal language such as CycL of the Cyc project. (b) *Inference Rules* Expressions of language that are semantically entailed syntactically from (a) and/or (b).
[toc] | [prev] | [next] | [standalone]
| From | Mikko <mikko.levanto@iki.fi> |
|---|---|
| Date | 2026-06-27 11:13 +0300 |
| Subject | Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs |
| Message-ID | <111o0mf$149pv$2@dont-email.me> |
| In reply to | #141977 |
On 26/06/2026 16:15, olcott wrote: > On 6/26/2026 1:45 AM, Mikko wrote: >> On 25/06/2026 19:16, olcott wrote: >>> On 6/25/2026 2:29 AM, Mikko wrote: >>>> On 25/06/2026 00:33, olcott wrote: >>>>> On 6/24/2026 5:13 AM, Mikko wrote: >>>>>> On 23/06/2026 21:20, olcott wrote: >>>>>>> On 6/23/2026 12:32 PM, Ross Finlayson wrote: >>>>>>>> On 06/23/2026 09:54 AM, olcott wrote: >>>>>>>>> On 6/23/2026 10:51 AM, Ross Finlayson wrote: >>>>>>>>>> On 06/23/2026 07:22 AM, olcott wrote: >>>>>>>>>>> On 6/22/2026 11:31 PM, Ross Finlayson wrote: >>>>>>>>>>>> On 06/22/2026 09:14 PM, olcott wrote: >>>>>>>>>>>>> On 6/22/2026 11:00 PM, Ross Finlayson wrote: >>>>>>>>>>>>>> On 06/22/2026 01:06 PM, olcott wrote: >>>>>>>>>>>>>>> On 6/22/2026 2:50 PM, Alan Mackenzie wrote: >>>>>>>>>>>>>>>> [ Followup-To: set ] >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>>>>>>>>>> On 6/22/2026 1:42 PM, Alan Mackenzie wrote: >>>>>>>>>>>>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>>>>>>>>>>>> On 6/22/2026 10:48 AM, Alan Mackenzie wrote: >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>> G is true. >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>> I put it to you you're lying again. No reputable >>>>>>>>>>>>>>>>>>>> mathematician >>>>>>>>>>>>>>>>>>>> would >>>>>>>>>>>>>>>>>>>> risk his reputation by saying false things. If Dag >>>>>>>>>>>>>>>>>>>> Prawitz >>>>>>>>>>>>>>>>>>>> really >>>>>>>>>>>>>>>>>>>> did >>>>>>>>>>>>>>>>>>>> "agree" (with whom?) that Gödel's sentence G is not >>>>>>>>>>>>>>>>>>>> true in >>>>>>>>>>>>>>>>>>>> Peano >>>>>>>>>>>>>>>>>>>> Arithmetic, then produce a citation for this. >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>> He never gets to Gödel. He essentially says unprovable >>>>>>>>>>>>>>>>>>> means untrue all the time for everything within his >>>>>>>>>>>>>>>>>>> own Theory of Grounds of strict Proof Theoretic >>>>>>>>>>>>>>>>>>> Semantics. >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>> You won't understand it, but that _is_ essentially >>>>>>>>>>>>>>>>>> Gödel's >>>>>>>>>>>>>>>>>> Incompleteness >>>>>>>>>>>>>>>>>> Theorem. It is a statement that any sufficiently >>>>>>>>>>>>>>>>>> powerful >>>>>>>>>>>>>>>>>> system can >>>>>>>>>>>>>>>>>> express true things it can't prove. So Dag Prawitz, >>>>>>>>>>>>>>>>>> had he been >>>>>>>>>>>>>>>>>> saying >>>>>>>>>>>>>>>>>> the things you falsely attributed to him, would >>>>>>>>>>>>>>>>>> certainly have >>>>>>>>>>>>>>>>>> "got" to >>>>>>>>>>>>>>>>>> Gödel, and would have understood full well what he was >>>>>>>>>>>>>>>>>> saying. >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>> You did not pay close enough attention to my exact words. >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> I was right, you didn't understand it. >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>>>>> >>>>>>>>>>>>>> >>>>>>>>>>>>>> Yeah, I'm pretty sure that "Dag Prawitz says what Dag >>>>>>>>>>>>>> Prawitz says", >>>>>>>>>>>>>> and furthermore "Dag Prawitz doesn't say what Dag Prawitz >>>>>>>>>>>>>> doesn't >>>>>>>>>>>>>> say", >>>>>>>>>>>>>> then looking a bit into his tremendous volume of works, >>>>>>>>>>>>>> he talks about "natural deduction" then specifically an >>>>>>>>>>>>>> "inverse >>>>>>>>>>>>>> principle" so I think these are key aspects of fundamental >>>>>>>>>>>>>> logic. >>>>>>>>>>>>>> >>>>>>>>>>>>>> https://www.researchgate.net/ >>>>>>>>>>>>>> publication/233365263_On_Inversion_Principles >>>>>>>>>>>>>> >>>>>>>>>>>>>> >>>>>>>>>>>>>> "On Inversion Principles >>>>>>>>>>>>>> >>>>>>>>>>>>>> Enrico Moriconi∗Laura Tesconi† >>>>>>>>>>>>>> May 8, 2007 >>>>>>>>>>>>>> >>>>>>>>>>>>>> Abstract >>>>>>>>>>>>>> The idea of an “inversion principle”, and the name itself, >>>>>>>>>>>>>> originated in >>>>>>>>>>>>>> the work of Paul Lorenzen in the 1950s, as a method to >>>>>>>>>>>>>> generate >>>>>>>>>>>>>> new ad- >>>>>>>>>>>>>> missible rules within a certain syntactic context. Some >>>>>>>>>>>>>> fifteen years >>>>>>>>>>>>>> later, the idea was taken up by Dag Prawitz to devise a >>>>>>>>>>>>>> strategy of >>>>>>>>>>>>>> normalization for natural deduction calculi (this being an >>>>>>>>>>>>>> analogue of >>>>>>>>>>>>>> Gentzen’s cut-elimination theorem for sequent calculi). >>>>>>>>>>>>>> Later, >>>>>>>>>>>>>> Prawitz >>>>>>>>>>>>>> used the inversion principle again, attributing it with a >>>>>>>>>>>>>> semantic >>>>>>>>>>>>>> role. >>>>>>>>>>>>>> Still working in natural deduction calculi, he formulated >>>>>>>>>>>>>> a general >>>>>>>>>>>>>> type >>>>>>>>>>>>>> of schematic Introduction rules to be matched—thanks to >>>>>>>>>>>>>> the idea >>>>>>>>>>>>>> supporting the inversion principle — by a corresponding >>>>>>>>>>>>>> general >>>>>>>>>>>>>> schematic Elimination rule. This was an attempt to provide a >>>>>>>>>>>>>> solution to >>>>>>>>>>>>>> the problem suggested by the often quoted note of Gentzen. >>>>>>>>>>>>>> According to >>>>>>>>>>>>>> Gentzen “it should be possible to display the elimination >>>>>>>>>>>>>> rules as >>>>>>>>>>>>>> unique functions of the corresponding introduction rules >>>>>>>>>>>>>> on the >>>>>>>>>>>>>> basis of >>>>>>>>>>>>>> certain requirements.” Many people have since worked on >>>>>>>>>>>>>> this topic, >>>>>>>>>>>>>> which can be appropriately seen as the birthplace of what >>>>>>>>>>>>>> are now >>>>>>>>>>>>>> referred to as “general elimination rules”, recently studied >>>>>>>>>>>>>> thoroughly >>>>>>>>>>>>>> by Sara Negri and Jan von Plato. In this paper, we retrace >>>>>>>>>>>>>> the main >>>>>>>>>>>>>> threads of this chapter of proof-theoretical >>>>>>>>>>>>>> investigation, using >>>>>>>>>>>>>> Lorenzen’s original framework as a general guide" >>>>>>>>>>>>>> >>>>>>>>>>>>>> >>>>>>>>>>>>>> >>>>>>>>>>>>>> Hm, "general elimination rules", seem derivable from De >>>>>>>>>>>>>> Morgan's >>>>>>>>>>>>>> laws, >>>>>>>>>>>>>> and that being the usual account of naive deductive >>>>>>>>>>>>>> analysis, then >>>>>>>>>>>>>> since >>>>>>>>>>>>>> "natural deduction", which here is held as part of the theory >>>>>>>>>>>>>> since it's naturally logical, then has for Gentzen that >>>>>>>>>>>>>> besides >>>>>>>>>>>>>> Kripke >>>>>>>>>>>>>> afterward there's also Sheffer and Chwistek before, and >>>>>>>>>>>>>> instead of >>>>>>>>>>>>>> Montague for semantics there's Herbrand for semantics, so, >>>>>>>>>>>>>> what to do >>>>>>>>>>>>>> about "inversion principle" is here that the thea-theory >>>>>>>>>>>>>> has that >>>>>>>>>>>>>> it's >>>>>>>>>>>>>> what subsumes "non-contradiction principle", here hoping >>>>>>>>>>>>>> that the >>>>>>>>>>>>>> interpretation aligns and thusly that "principle of >>>>>>>>>>>>>> inversion" >>>>>>>>>>>>>> wouldn't >>>>>>>>>>>>>> need dis-ambiguation from "inversion principle". >>>>>>>>>>>>>> >>>>>>>>>>>>>> >>>>>>>>>>>>>> https://www.tandfonline.com/doi/abs/10.1080/01445340701830334 >>>>>>>>>>>>>> >>>>>>>>>>>>>> >>>>>>>>>>>>>> https://www.strandbooks.com/natural-deduction-a-proof- >>>>>>>>>>>>>> theoretical- >>>>>>>>>>>>>> study-9780486446554.html >>>>>>>>>>>>>> >>>>>>>>>>>>>> "... [Prawitz'] inversion principle constitutes the >>>>>>>>>>>>>> foundation of >>>>>>>>>>>>>> most >>>>>>>>>>>>>> modern accounts of proof-theoretic semantics." >>>>>>>>>>>>>> >>>>>>>>>>>>>> >>>>>>>>>>>>>> >>>>>>>>>>>>>> I already have a principle of inversion and furthermore a >>>>>>>>>>>>>> principle of >>>>>>>>>>>>>> thorough reason as subsuming principles of non- >>>>>>>>>>>>>> contradiction and what >>>>>>>>>>>>>> suffices, so, I'll be curious then about what to make of >>>>>>>>>>>>>> Prawitz' >>>>>>>>>>>>>> "inversion principle" since Lorenzen. >>>>>>>>>>>>>> >>>>>>>>>>>>>> >>>>>>>>>>>>>> Of course the concept of an "inversion principle" is as >>>>>>>>>>>>>> old as the >>>>>>>>>>>>>> oldest account of Western philosophy like Heraclitus with >>>>>>>>>>>>>> dual >>>>>>>>>>>>>> monism. >>>>>>>>>>>>>> In fact by definition it's about the most basic aspect of >>>>>>>>>>>>>> contemplation >>>>>>>>>>>>>> and deliberation in abstraction of looking at both sides >>>>>>>>>>>>>> of issues >>>>>>>>>>>>>> and >>>>>>>>>>>>>> resolving inductive impasses with analytical bridges after >>>>>>>>>>>>>> complementary >>>>>>>>>>>>>> duals. >>>>>>>>>>>>>> >>>>>>>>>>>>>> >>>>>>>>>>>>>> https://arxiv.org/abs/2112.14967 >>>>>>>>>>>>>> >>>>>>>>>>>>>> "Prawitz formulated the so-called inversion principle as >>>>>>>>>>>>>> one of the >>>>>>>>>>>>>> characteristic features of Gentzen's intuitionistic natural >>>>>>>>>>>>>> deduction. >>>>>>>>>>>>>> In the literature on proof-theoretic semantics, this >>>>>>>>>>>>>> principle is >>>>>>>>>>>>>> often >>>>>>>>>>>>>> coupled with another that is called the recovery >>>>>>>>>>>>>> principle. By >>>>>>>>>>>>>> adopting >>>>>>>>>>>>>> the Computational Ludics framework, we reformulate these >>>>>>>>>>>>>> principles >>>>>>>>>>>>>> into >>>>>>>>>>>>>> one and the same condition, which we call the harmony >>>>>>>>>>>>>> condition. We >>>>>>>>>>>>>> show >>>>>>>>>>>>>> that this reformulation allows us to reveal two intuitive >>>>>>>>>>>>>> ideas >>>>>>>>>>>>>> standing >>>>>>>>>>>>>> behind these principles: the idea of "containment" present >>>>>>>>>>>>>> in the >>>>>>>>>>>>>> inversion principle, and the idea that the recovery >>>>>>>>>>>>>> principle is the >>>>>>>>>>>>>> "converse" of the inversion principle. We also formulate >>>>>>>>>>>>>> two other >>>>>>>>>>>>>> conditions in the Computational Ludics framework, and we >>>>>>>>>>>>>> show that >>>>>>>>>>>>>> each >>>>>>>>>>>>>> of them is equivalent to the harmony condition." >>>>>>>>>>>>>> >>>>>>>>>>>>>> >>>>>>>>>>>>>> >>>>>>>>>>>>>> The "ludicus" is Latin and for accounts of wisdom and >>>>>>>>>>>>>> knowledge. >>>>>>>>>>>>>> >>>>>>>>>>>>>> >>>>>>>>>>>>>> "In particular, by taking inspiration from the >>>>>>>>>>>>>> Brouwer-Heyting-Kolmogorov explanation of logical >>>>>>>>>>>>>> connectives, >>>>>>>>>>>>>> proof-theoretic semantics rests on the idea that we know the >>>>>>>>>>>>>> meaning of >>>>>>>>>>>>>> a compound sentence when we know what counts as a >>>>>>>>>>>>>> canonical proof of >>>>>>>>>>>>>> it. >>>>>>>>>>>>>> And if proofs are formalised within the framework of natural >>>>>>>>>>>>>> deduction, >>>>>>>>>>>>>> then a canonical proof of a sentence A is nothing but a >>>>>>>>>>>>>> closed >>>>>>>>>>>>>> derivation ending with an introduction rule of the main >>>>>>>>>>>>>> connective >>>>>>>>>>>>>> of A." >>>>>>>>>>>>>> >>>>>>>>>>>>>> >>>>>>>>>>>>>> The "canonical proofs" are not unique, in any system >>>>>>>>>>>>>> strong enough >>>>>>>>>>>>>> to make for infinitary reasoning and super-classical results >>>>>>>>>>>>>> requiring >>>>>>>>>>>>>> analytical bridges about infinity and continuity. >>>>>>>>>>>>>> >>>>>>>>>>>>> >>>>>>>>>>>>> It is the role that "canonical proofs" play in >>>>>>>>>>>>> Truth as an Epistemic Notion >>>>>>>>>>>>> https://link.springer.com/article/10.1007/s11245-011-9107-6 >>>>>>>>>>>>> That is the most important gist of his whole work. >>>>>>>>>>>>> >>>>>>>>>>>>> He later goes on to develop and further elaborate his >>>>>>>>>>>>> Theory of Grounds. >>>>>>>>>>>>> >>>>>>>>>>>>> Atomic Systems in Proof-Theoretic Semantics: Two Approaches >>>>>>>>>>>>> Thomas Piecha & Peter Schroeder-Heister do this same sort of >>>>>>>>>>>>> thing two different ways. >>>>>>>>>>>>> >>>>>>>>>>>>> >>>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> Furthermore I say there are "canonical proofs" of inductive >>>>>>>>>>>> sorts that >>>>>>>>>>>> make contradictions and thusly destroy each other. >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> Clearly you have no idea what Dag Prawitz means by "canonical >>>>>>>>>>> proofs". >>>>>>>>>>> Go find out and then get back to me. >>>>>>>>>>> >>>>>>>>>>>> This is where "the thorough" and "analytical bridges" make >>>>>>>>>>>> repairs >>>>>>>>>>>> of what otherwise is flawed, or for hard constructivist realist >>>>>>>>>>>> structuralist model theorists: not-theories (examples of >>>>>>>>>>>> wrong). >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> Induction and counter-induction contradict each other, it's >>>>>>>>>> simple, >>>>>>>>>> it's the grounds for most things called "paradox". >>>>>>>>>> >>>>>>>>>> >>>>>>>>> >>>>>>>>> % This sentence is not true. >>>>>>>>> ?- LP = not(true(LP)). >>>>>>>>> LP = not(true(LP)). >>>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))). >>>>>>>>> false. >>>>>>>>> >>>>>>>>> After you totally understand how and why the proof >>>>>>>>> theoretic semantics of that is correct and resolves >>>>>>>>> the Liar Paradox get back to me. >>>>>>>>> >>>>>>>>> The essential principle involved that I derived >>>>>>>>> in my own Minimal Type Theory before I knew that >>>>>>>>> Prolog could do the same thing is that: >>>>>>>>> >>>>>>>>> When the directed graph of the evaluation >>>>>>>>> sequence of an expression contains a cycle >>>>>>>>> then the input is determined to be incoherent >>>>>>>>> on the basis that its proof would never terminate. >>>>>>>>> Proof Theoretic Semantics does this exact same thing. >>>>>>>>> >>>>>>>>> Don't get back to me until you attain the required >>>>>>>>> prerequisites. I am sure that you already know >>>>>>>>> all about cycles in directed graphs. >>>>>>>>> >>>>>>>> >>>>>>>> Declaring oneself ignorant thus wise >>>>>>>> doesn't make much of a case >>>>>>>> except being ignorant. >>>>>>>> >>>>>>>> 300 mile per hour wheelchair: can't take stairs. >>>>>>>> >>>>>>>> Except down, .... >>>>>>>> >>>>>>>> >>>>>>> >>>>>>> So you are going to imply that I am incorrect >>>>>>> about Prolog when you yourself remain clueless about Prolog? >>>>>>> That would be dishonest. >>>>>> >>>>>> No, pointing out that you are worng about Prolog when you are wrong >>>>>> about Prolog is never dishohest. >>>>> >>>>> That is correct Prolog and that is the >>>>> result of the correct run of correct Prolog. >>>> >>>> Irrelevant. Nobody claimed there be Prolog errors in your queries. >>>> >>>>> Implying that I am wrong about Prolog without >>>>> pointing out any actual mistake is also DISHONEST. >>>> >>>> How did Ross FInlayson imply that you were wrong about Prolog? >>> >>> If an error is claimed then it must be specifically >>> pointed out otherwise the clam of error is dishonest. >> >> Yet you claim that Ross Finlayson be dishonest without pointing >> out what is dishonest in his words. > > If anyone and everyone that claims that they found an > error and never points out what the error is and why > it is an error then they are merely a baseless denigrator. If anyone and everyone that claims that someone is dishonest never points out what the dishonesty is is and why it is dishones then they are merely a baseless denigrator. -- Mikko
[toc] | [prev] | [next] | [standalone]
| From | Ross Finlayson <ross.a.finlayson@gmail.com> |
|---|---|
| Date | 2026-06-27 07:25 -0700 |
| Subject | Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs |
| Message-ID | <WWWdnf_h7PrUQKL3nZ2dnZfqnPudnZ2d@giganews.com> |
| In reply to | #142022 |
On 06/27/2026 01:13 AM, Mikko wrote: > On 26/06/2026 16:15, olcott wrote: >> On 6/26/2026 1:45 AM, Mikko wrote: >>> On 25/06/2026 19:16, olcott wrote: >>>> On 6/25/2026 2:29 AM, Mikko wrote: >>>>> On 25/06/2026 00:33, olcott wrote: >>>>>> On 6/24/2026 5:13 AM, Mikko wrote: >>>>>>> On 23/06/2026 21:20, olcott wrote: >>>>>>>> On 6/23/2026 12:32 PM, Ross Finlayson wrote: >>>>>>>>> On 06/23/2026 09:54 AM, olcott wrote: >>>>>>>>>> On 6/23/2026 10:51 AM, Ross Finlayson wrote: >>>>>>>>>>> On 06/23/2026 07:22 AM, olcott wrote: >>>>>>>>>>>> On 6/22/2026 11:31 PM, Ross Finlayson wrote: >>>>>>>>>>>>> On 06/22/2026 09:14 PM, olcott wrote: >>>>>>>>>>>>>> On 6/22/2026 11:00 PM, Ross Finlayson wrote: >>>>>>>>>>>>>>> On 06/22/2026 01:06 PM, olcott wrote: >>>>>>>>>>>>>>>> On 6/22/2026 2:50 PM, Alan Mackenzie wrote: >>>>>>>>>>>>>>>>> [ Followup-To: set ] >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>>>>>>>>>>> On 6/22/2026 1:42 PM, Alan Mackenzie wrote: >>>>>>>>>>>>>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>>>>>>>>>>>>> On 6/22/2026 10:48 AM, Alan Mackenzie wrote: >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>> G is true. >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>> I put it to you you're lying again. No reputable >>>>>>>>>>>>>>>>>>>>> mathematician >>>>>>>>>>>>>>>>>>>>> would >>>>>>>>>>>>>>>>>>>>> risk his reputation by saying false things. If Dag >>>>>>>>>>>>>>>>>>>>> Prawitz >>>>>>>>>>>>>>>>>>>>> really >>>>>>>>>>>>>>>>>>>>> did >>>>>>>>>>>>>>>>>>>>> "agree" (with whom?) that Gödel's sentence G is not >>>>>>>>>>>>>>>>>>>>> true in >>>>>>>>>>>>>>>>>>>>> Peano >>>>>>>>>>>>>>>>>>>>> Arithmetic, then produce a citation for this. >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>> He never gets to Gödel. He essentially says unprovable >>>>>>>>>>>>>>>>>>>> means untrue all the time for everything within his >>>>>>>>>>>>>>>>>>>> own Theory of Grounds of strict Proof Theoretic >>>>>>>>>>>>>>>>>>>> Semantics. >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>> You won't understand it, but that _is_ essentially >>>>>>>>>>>>>>>>>>> Gödel's >>>>>>>>>>>>>>>>>>> Incompleteness >>>>>>>>>>>>>>>>>>> Theorem. It is a statement that any sufficiently >>>>>>>>>>>>>>>>>>> powerful >>>>>>>>>>>>>>>>>>> system can >>>>>>>>>>>>>>>>>>> express true things it can't prove. So Dag Prawitz, >>>>>>>>>>>>>>>>>>> had he been >>>>>>>>>>>>>>>>>>> saying >>>>>>>>>>>>>>>>>>> the things you falsely attributed to him, would >>>>>>>>>>>>>>>>>>> certainly have >>>>>>>>>>>>>>>>>>> "got" to >>>>>>>>>>>>>>>>>>> Gödel, and would have understood full well what he >>>>>>>>>>>>>>>>>>> was saying. >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>> You did not pay close enough attention to my exact words. >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>> I was right, you didn't understand it. >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> Yeah, I'm pretty sure that "Dag Prawitz says what Dag >>>>>>>>>>>>>>> Prawitz says", >>>>>>>>>>>>>>> and furthermore "Dag Prawitz doesn't say what Dag Prawitz >>>>>>>>>>>>>>> doesn't >>>>>>>>>>>>>>> say", >>>>>>>>>>>>>>> then looking a bit into his tremendous volume of works, >>>>>>>>>>>>>>> he talks about "natural deduction" then specifically an >>>>>>>>>>>>>>> "inverse >>>>>>>>>>>>>>> principle" so I think these are key aspects of >>>>>>>>>>>>>>> fundamental logic. >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> https://www.researchgate.net/ >>>>>>>>>>>>>>> publication/233365263_On_Inversion_Principles >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> "On Inversion Principles >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> Enrico Moriconi∗Laura Tesconi† >>>>>>>>>>>>>>> May 8, 2007 >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> Abstract >>>>>>>>>>>>>>> The idea of an “inversion principle”, and the name itself, >>>>>>>>>>>>>>> originated in >>>>>>>>>>>>>>> the work of Paul Lorenzen in the 1950s, as a method to >>>>>>>>>>>>>>> generate >>>>>>>>>>>>>>> new ad- >>>>>>>>>>>>>>> missible rules within a certain syntactic context. Some >>>>>>>>>>>>>>> fifteen years >>>>>>>>>>>>>>> later, the idea was taken up by Dag Prawitz to devise a >>>>>>>>>>>>>>> strategy of >>>>>>>>>>>>>>> normalization for natural deduction calculi (this being an >>>>>>>>>>>>>>> analogue of >>>>>>>>>>>>>>> Gentzen’s cut-elimination theorem for sequent calculi). >>>>>>>>>>>>>>> Later, >>>>>>>>>>>>>>> Prawitz >>>>>>>>>>>>>>> used the inversion principle again, attributing it with a >>>>>>>>>>>>>>> semantic >>>>>>>>>>>>>>> role. >>>>>>>>>>>>>>> Still working in natural deduction calculi, he formulated >>>>>>>>>>>>>>> a general >>>>>>>>>>>>>>> type >>>>>>>>>>>>>>> of schematic Introduction rules to be matched—thanks to >>>>>>>>>>>>>>> the idea >>>>>>>>>>>>>>> supporting the inversion principle — by a corresponding >>>>>>>>>>>>>>> general >>>>>>>>>>>>>>> schematic Elimination rule. This was an attempt to provide a >>>>>>>>>>>>>>> solution to >>>>>>>>>>>>>>> the problem suggested by the often quoted note of Gentzen. >>>>>>>>>>>>>>> According to >>>>>>>>>>>>>>> Gentzen “it should be possible to display the elimination >>>>>>>>>>>>>>> rules as >>>>>>>>>>>>>>> unique functions of the corresponding introduction rules >>>>>>>>>>>>>>> on the >>>>>>>>>>>>>>> basis of >>>>>>>>>>>>>>> certain requirements.” Many people have since worked on >>>>>>>>>>>>>>> this topic, >>>>>>>>>>>>>>> which can be appropriately seen as the birthplace of what >>>>>>>>>>>>>>> are now >>>>>>>>>>>>>>> referred to as “general elimination rules”, recently studied >>>>>>>>>>>>>>> thoroughly >>>>>>>>>>>>>>> by Sara Negri and Jan von Plato. In this paper, we >>>>>>>>>>>>>>> retrace the main >>>>>>>>>>>>>>> threads of this chapter of proof-theoretical >>>>>>>>>>>>>>> investigation, using >>>>>>>>>>>>>>> Lorenzen’s original framework as a general guide" >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> Hm, "general elimination rules", seem derivable from De >>>>>>>>>>>>>>> Morgan's >>>>>>>>>>>>>>> laws, >>>>>>>>>>>>>>> and that being the usual account of naive deductive >>>>>>>>>>>>>>> analysis, then >>>>>>>>>>>>>>> since >>>>>>>>>>>>>>> "natural deduction", which here is held as part of the >>>>>>>>>>>>>>> theory >>>>>>>>>>>>>>> since it's naturally logical, then has for Gentzen that >>>>>>>>>>>>>>> besides >>>>>>>>>>>>>>> Kripke >>>>>>>>>>>>>>> afterward there's also Sheffer and Chwistek before, and >>>>>>>>>>>>>>> instead of >>>>>>>>>>>>>>> Montague for semantics there's Herbrand for semantics, >>>>>>>>>>>>>>> so, what to do >>>>>>>>>>>>>>> about "inversion principle" is here that the thea-theory >>>>>>>>>>>>>>> has that >>>>>>>>>>>>>>> it's >>>>>>>>>>>>>>> what subsumes "non-contradiction principle", here hoping >>>>>>>>>>>>>>> that the >>>>>>>>>>>>>>> interpretation aligns and thusly that "principle of >>>>>>>>>>>>>>> inversion" >>>>>>>>>>>>>>> wouldn't >>>>>>>>>>>>>>> need dis-ambiguation from "inversion principle". >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> https://www.tandfonline.com/doi/abs/10.1080/01445340701830334 >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> https://www.strandbooks.com/natural-deduction-a-proof- >>>>>>>>>>>>>>> theoretical- >>>>>>>>>>>>>>> study-9780486446554.html >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> "... [Prawitz'] inversion principle constitutes the >>>>>>>>>>>>>>> foundation of >>>>>>>>>>>>>>> most >>>>>>>>>>>>>>> modern accounts of proof-theoretic semantics." >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> I already have a principle of inversion and furthermore a >>>>>>>>>>>>>>> principle of >>>>>>>>>>>>>>> thorough reason as subsuming principles of non- >>>>>>>>>>>>>>> contradiction and what >>>>>>>>>>>>>>> suffices, so, I'll be curious then about what to make of >>>>>>>>>>>>>>> Prawitz' >>>>>>>>>>>>>>> "inversion principle" since Lorenzen. >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> Of course the concept of an "inversion principle" is as >>>>>>>>>>>>>>> old as the >>>>>>>>>>>>>>> oldest account of Western philosophy like Heraclitus with >>>>>>>>>>>>>>> dual >>>>>>>>>>>>>>> monism. >>>>>>>>>>>>>>> In fact by definition it's about the most basic aspect of >>>>>>>>>>>>>>> contemplation >>>>>>>>>>>>>>> and deliberation in abstraction of looking at both sides >>>>>>>>>>>>>>> of issues >>>>>>>>>>>>>>> and >>>>>>>>>>>>>>> resolving inductive impasses with analytical bridges after >>>>>>>>>>>>>>> complementary >>>>>>>>>>>>>>> duals. >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> https://arxiv.org/abs/2112.14967 >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> "Prawitz formulated the so-called inversion principle as >>>>>>>>>>>>>>> one of the >>>>>>>>>>>>>>> characteristic features of Gentzen's intuitionistic natural >>>>>>>>>>>>>>> deduction. >>>>>>>>>>>>>>> In the literature on proof-theoretic semantics, this >>>>>>>>>>>>>>> principle is >>>>>>>>>>>>>>> often >>>>>>>>>>>>>>> coupled with another that is called the recovery >>>>>>>>>>>>>>> principle. By >>>>>>>>>>>>>>> adopting >>>>>>>>>>>>>>> the Computational Ludics framework, we reformulate these >>>>>>>>>>>>>>> principles >>>>>>>>>>>>>>> into >>>>>>>>>>>>>>> one and the same condition, which we call the harmony >>>>>>>>>>>>>>> condition. We >>>>>>>>>>>>>>> show >>>>>>>>>>>>>>> that this reformulation allows us to reveal two intuitive >>>>>>>>>>>>>>> ideas >>>>>>>>>>>>>>> standing >>>>>>>>>>>>>>> behind these principles: the idea of "containment" >>>>>>>>>>>>>>> present in the >>>>>>>>>>>>>>> inversion principle, and the idea that the recovery >>>>>>>>>>>>>>> principle is the >>>>>>>>>>>>>>> "converse" of the inversion principle. We also formulate >>>>>>>>>>>>>>> two other >>>>>>>>>>>>>>> conditions in the Computational Ludics framework, and we >>>>>>>>>>>>>>> show that >>>>>>>>>>>>>>> each >>>>>>>>>>>>>>> of them is equivalent to the harmony condition." >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> The "ludicus" is Latin and for accounts of wisdom and >>>>>>>>>>>>>>> knowledge. >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> "In particular, by taking inspiration from the >>>>>>>>>>>>>>> Brouwer-Heyting-Kolmogorov explanation of logical >>>>>>>>>>>>>>> connectives, >>>>>>>>>>>>>>> proof-theoretic semantics rests on the idea that we know the >>>>>>>>>>>>>>> meaning of >>>>>>>>>>>>>>> a compound sentence when we know what counts as a >>>>>>>>>>>>>>> canonical proof of >>>>>>>>>>>>>>> it. >>>>>>>>>>>>>>> And if proofs are formalised within the framework of natural >>>>>>>>>>>>>>> deduction, >>>>>>>>>>>>>>> then a canonical proof of a sentence A is nothing but a >>>>>>>>>>>>>>> closed >>>>>>>>>>>>>>> derivation ending with an introduction rule of the main >>>>>>>>>>>>>>> connective >>>>>>>>>>>>>>> of A." >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> The "canonical proofs" are not unique, in any system >>>>>>>>>>>>>>> strong enough >>>>>>>>>>>>>>> to make for infinitary reasoning and super-classical results >>>>>>>>>>>>>>> requiring >>>>>>>>>>>>>>> analytical bridges about infinity and continuity. >>>>>>>>>>>>>>> >>>>>>>>>>>>>> >>>>>>>>>>>>>> It is the role that "canonical proofs" play in >>>>>>>>>>>>>> Truth as an Epistemic Notion >>>>>>>>>>>>>> https://link.springer.com/article/10.1007/s11245-011-9107-6 >>>>>>>>>>>>>> That is the most important gist of his whole work. >>>>>>>>>>>>>> >>>>>>>>>>>>>> He later goes on to develop and further elaborate his >>>>>>>>>>>>>> Theory of Grounds. >>>>>>>>>>>>>> >>>>>>>>>>>>>> Atomic Systems in Proof-Theoretic Semantics: Two Approaches >>>>>>>>>>>>>> Thomas Piecha & Peter Schroeder-Heister do this same sort of >>>>>>>>>>>>>> thing two different ways. >>>>>>>>>>>>>> >>>>>>>>>>>>>> >>>>>>>>>>>>>> >>>>>>>>>>>>> >>>>>>>>>>>>> Furthermore I say there are "canonical proofs" of inductive >>>>>>>>>>>>> sorts that >>>>>>>>>>>>> make contradictions and thusly destroy each other. >>>>>>>>>>>>> >>>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> Clearly you have no idea what Dag Prawitz means by >>>>>>>>>>>> "canonical proofs". >>>>>>>>>>>> Go find out and then get back to me. >>>>>>>>>>>> >>>>>>>>>>>>> This is where "the thorough" and "analytical bridges" make >>>>>>>>>>>>> repairs >>>>>>>>>>>>> of what otherwise is flawed, or for hard constructivist >>>>>>>>>>>>> realist >>>>>>>>>>>>> structuralist model theorists: not-theories (examples of >>>>>>>>>>>>> wrong). >>>>>>>>>>>>> >>>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> Induction and counter-induction contradict each other, it's >>>>>>>>>>> simple, >>>>>>>>>>> it's the grounds for most things called "paradox". >>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>> >>>>>>>>>> % This sentence is not true. >>>>>>>>>> ?- LP = not(true(LP)). >>>>>>>>>> LP = not(true(LP)). >>>>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))). >>>>>>>>>> false. >>>>>>>>>> >>>>>>>>>> After you totally understand how and why the proof >>>>>>>>>> theoretic semantics of that is correct and resolves >>>>>>>>>> the Liar Paradox get back to me. >>>>>>>>>> >>>>>>>>>> The essential principle involved that I derived >>>>>>>>>> in my own Minimal Type Theory before I knew that >>>>>>>>>> Prolog could do the same thing is that: >>>>>>>>>> >>>>>>>>>> When the directed graph of the evaluation >>>>>>>>>> sequence of an expression contains a cycle >>>>>>>>>> then the input is determined to be incoherent >>>>>>>>>> on the basis that its proof would never terminate. >>>>>>>>>> Proof Theoretic Semantics does this exact same thing. >>>>>>>>>> >>>>>>>>>> Don't get back to me until you attain the required >>>>>>>>>> prerequisites. I am sure that you already know >>>>>>>>>> all about cycles in directed graphs. >>>>>>>>>> >>>>>>>>> >>>>>>>>> Declaring oneself ignorant thus wise >>>>>>>>> doesn't make much of a case >>>>>>>>> except being ignorant. >>>>>>>>> >>>>>>>>> 300 mile per hour wheelchair: can't take stairs. >>>>>>>>> >>>>>>>>> Except down, .... >>>>>>>>> >>>>>>>>> >>>>>>>> >>>>>>>> So you are going to imply that I am incorrect >>>>>>>> about Prolog when you yourself remain clueless about Prolog? >>>>>>>> That would be dishonest. >>>>>>> >>>>>>> No, pointing out that you are worng about Prolog when you are wrong >>>>>>> about Prolog is never dishohest. >>>>>> >>>>>> That is correct Prolog and that is the >>>>>> result of the correct run of correct Prolog. >>>>> >>>>> Irrelevant. Nobody claimed there be Prolog errors in your queries. >>>>> >>>>>> Implying that I am wrong about Prolog without >>>>>> pointing out any actual mistake is also DISHONEST. >>>>> >>>>> How did Ross FInlayson imply that you were wrong about Prolog? >>>> >>>> If an error is claimed then it must be specifically >>>> pointed out otherwise the clam of error is dishonest. >>> >>> Yet you claim that Ross Finlayson be dishonest without pointing >>> out what is dishonest in his words. >> >> If anyone and everyone that claims that they found an >> error and never points out what the error is and why >> it is an error then they are merely a baseless denigrator. > If anyone and everyone that claims that someone is dishonest > never points out what the dishonesty is is and why it is > dishones then they are merely a baseless denigrator. > > I didn't say a damn thing about Prolog, as with regards to LISP and Scheme and Prolog and similar sorts environments, it is what it is and does what it does, then as to why it short-circuits evaluation and results "false" for "Liar Paradox" is fair, it is what it is and according to the software the model of computation the evaluation of the expression. What I did say was that "PTS" was being mis-portrayed by "PO", then also that the wider account of "proof-theoretic semantics" is besides being "equi-interpretable" with whatever common "quasi-modal truth-like semantics" say, that the "epistemic challenges" introduced as from the slides of Piccolomini and my points about them have that "proof-theoretic semantics" can be as of a modal temporal relevance logic since axiomless natural deduction for paradox-free reason and constant, consistent, complete, and concrete theory, of logic, resolving paradoxes and making truth.
[toc] | [prev] | [next] | [standalone]
| From | polcott <polcott333@gmail.com> |
|---|---|
| Date | 2026-06-27 10:53 -0500 |
| Subject | Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs |
| Message-ID | <111orl6$1kdbg$1@solani.org> |
| In reply to | #142022 |
On 6/27/2026 3:13 AM, Mikko wrote: > On 26/06/2026 16:15, olcott wrote: >> On 6/26/2026 1:45 AM, Mikko wrote: >>> On 25/06/2026 19:16, olcott wrote: >>>> On 6/25/2026 2:29 AM, Mikko wrote: >>>>> On 25/06/2026 00:33, olcott wrote: >>>>>> On 6/24/2026 5:13 AM, Mikko wrote: >>>>>>> On 23/06/2026 21:20, olcott wrote: >>>>>>>> On 6/23/2026 12:32 PM, Ross Finlayson wrote: >>>>>>>>> On 06/23/2026 09:54 AM, olcott wrote: >>>>>>>>>> On 6/23/2026 10:51 AM, Ross Finlayson wrote: >>>>>>>>>>> On 06/23/2026 07:22 AM, olcott wrote: >>>>>>>>>>>> On 6/22/2026 11:31 PM, Ross Finlayson wrote: >>>>>>>>>>>>> On 06/22/2026 09:14 PM, olcott wrote: >>>>>>>>>>>>>> On 6/22/2026 11:00 PM, Ross Finlayson wrote: >>>>>>>>>>>>>>> On 06/22/2026 01:06 PM, olcott wrote: >>>>>>>>>>>>>>>> On 6/22/2026 2:50 PM, Alan Mackenzie wrote: >>>>>>>>>>>>>>>>> [ Followup-To: set ] >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>>>>>>>>>>> On 6/22/2026 1:42 PM, Alan Mackenzie wrote: >>>>>>>>>>>>>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>>>>>>>>>>>>> On 6/22/2026 10:48 AM, Alan Mackenzie wrote: >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>> G is true. >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>> I put it to you you're lying again. No reputable >>>>>>>>>>>>>>>>>>>>> mathematician >>>>>>>>>>>>>>>>>>>>> would >>>>>>>>>>>>>>>>>>>>> risk his reputation by saying false things. If Dag >>>>>>>>>>>>>>>>>>>>> Prawitz >>>>>>>>>>>>>>>>>>>>> really >>>>>>>>>>>>>>>>>>>>> did >>>>>>>>>>>>>>>>>>>>> "agree" (with whom?) that Gödel's sentence G is not >>>>>>>>>>>>>>>>>>>>> true in >>>>>>>>>>>>>>>>>>>>> Peano >>>>>>>>>>>>>>>>>>>>> Arithmetic, then produce a citation for this. >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>> He never gets to Gödel. He essentially says unprovable >>>>>>>>>>>>>>>>>>>> means untrue all the time for everything within his >>>>>>>>>>>>>>>>>>>> own Theory of Grounds of strict Proof Theoretic >>>>>>>>>>>>>>>>>>>> Semantics. >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>> You won't understand it, but that _is_ essentially >>>>>>>>>>>>>>>>>>> Gödel's >>>>>>>>>>>>>>>>>>> Incompleteness >>>>>>>>>>>>>>>>>>> Theorem. It is a statement that any sufficiently >>>>>>>>>>>>>>>>>>> powerful >>>>>>>>>>>>>>>>>>> system can >>>>>>>>>>>>>>>>>>> express true things it can't prove. So Dag Prawitz, >>>>>>>>>>>>>>>>>>> had he been >>>>>>>>>>>>>>>>>>> saying >>>>>>>>>>>>>>>>>>> the things you falsely attributed to him, would >>>>>>>>>>>>>>>>>>> certainly have >>>>>>>>>>>>>>>>>>> "got" to >>>>>>>>>>>>>>>>>>> Gödel, and would have understood full well what he >>>>>>>>>>>>>>>>>>> was saying. >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>> You did not pay close enough attention to my exact words. >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>> I was right, you didn't understand it. >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> Yeah, I'm pretty sure that "Dag Prawitz says what Dag >>>>>>>>>>>>>>> Prawitz says", >>>>>>>>>>>>>>> and furthermore "Dag Prawitz doesn't say what Dag Prawitz >>>>>>>>>>>>>>> doesn't >>>>>>>>>>>>>>> say", >>>>>>>>>>>>>>> then looking a bit into his tremendous volume of works, >>>>>>>>>>>>>>> he talks about "natural deduction" then specifically an >>>>>>>>>>>>>>> "inverse >>>>>>>>>>>>>>> principle" so I think these are key aspects of >>>>>>>>>>>>>>> fundamental logic. >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> https://www.researchgate.net/ >>>>>>>>>>>>>>> publication/233365263_On_Inversion_Principles >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> "On Inversion Principles >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> Enrico Moriconi∗Laura Tesconi† >>>>>>>>>>>>>>> May 8, 2007 >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> Abstract >>>>>>>>>>>>>>> The idea of an “inversion principle”, and the name itself, >>>>>>>>>>>>>>> originated in >>>>>>>>>>>>>>> the work of Paul Lorenzen in the 1950s, as a method to >>>>>>>>>>>>>>> generate >>>>>>>>>>>>>>> new ad- >>>>>>>>>>>>>>> missible rules within a certain syntactic context. Some >>>>>>>>>>>>>>> fifteen years >>>>>>>>>>>>>>> later, the idea was taken up by Dag Prawitz to devise a >>>>>>>>>>>>>>> strategy of >>>>>>>>>>>>>>> normalization for natural deduction calculi (this being an >>>>>>>>>>>>>>> analogue of >>>>>>>>>>>>>>> Gentzen’s cut-elimination theorem for sequent calculi). >>>>>>>>>>>>>>> Later, >>>>>>>>>>>>>>> Prawitz >>>>>>>>>>>>>>> used the inversion principle again, attributing it with a >>>>>>>>>>>>>>> semantic >>>>>>>>>>>>>>> role. >>>>>>>>>>>>>>> Still working in natural deduction calculi, he formulated >>>>>>>>>>>>>>> a general >>>>>>>>>>>>>>> type >>>>>>>>>>>>>>> of schematic Introduction rules to be matched—thanks to >>>>>>>>>>>>>>> the idea >>>>>>>>>>>>>>> supporting the inversion principle — by a corresponding >>>>>>>>>>>>>>> general >>>>>>>>>>>>>>> schematic Elimination rule. This was an attempt to provide a >>>>>>>>>>>>>>> solution to >>>>>>>>>>>>>>> the problem suggested by the often quoted note of Gentzen. >>>>>>>>>>>>>>> According to >>>>>>>>>>>>>>> Gentzen “it should be possible to display the elimination >>>>>>>>>>>>>>> rules as >>>>>>>>>>>>>>> unique functions of the corresponding introduction rules >>>>>>>>>>>>>>> on the >>>>>>>>>>>>>>> basis of >>>>>>>>>>>>>>> certain requirements.” Many people have since worked on >>>>>>>>>>>>>>> this topic, >>>>>>>>>>>>>>> which can be appropriately seen as the birthplace of what >>>>>>>>>>>>>>> are now >>>>>>>>>>>>>>> referred to as “general elimination rules”, recently studied >>>>>>>>>>>>>>> thoroughly >>>>>>>>>>>>>>> by Sara Negri and Jan von Plato. In this paper, we >>>>>>>>>>>>>>> retrace the main >>>>>>>>>>>>>>> threads of this chapter of proof-theoretical >>>>>>>>>>>>>>> investigation, using >>>>>>>>>>>>>>> Lorenzen’s original framework as a general guide" >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> Hm, "general elimination rules", seem derivable from De >>>>>>>>>>>>>>> Morgan's >>>>>>>>>>>>>>> laws, >>>>>>>>>>>>>>> and that being the usual account of naive deductive >>>>>>>>>>>>>>> analysis, then >>>>>>>>>>>>>>> since >>>>>>>>>>>>>>> "natural deduction", which here is held as part of the >>>>>>>>>>>>>>> theory >>>>>>>>>>>>>>> since it's naturally logical, then has for Gentzen that >>>>>>>>>>>>>>> besides >>>>>>>>>>>>>>> Kripke >>>>>>>>>>>>>>> afterward there's also Sheffer and Chwistek before, and >>>>>>>>>>>>>>> instead of >>>>>>>>>>>>>>> Montague for semantics there's Herbrand for semantics, >>>>>>>>>>>>>>> so, what to do >>>>>>>>>>>>>>> about "inversion principle" is here that the thea-theory >>>>>>>>>>>>>>> has that >>>>>>>>>>>>>>> it's >>>>>>>>>>>>>>> what subsumes "non-contradiction principle", here hoping >>>>>>>>>>>>>>> that the >>>>>>>>>>>>>>> interpretation aligns and thusly that "principle of >>>>>>>>>>>>>>> inversion" >>>>>>>>>>>>>>> wouldn't >>>>>>>>>>>>>>> need dis-ambiguation from "inversion principle". >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> https://www.tandfonline.com/doi/ >>>>>>>>>>>>>>> abs/10.1080/01445340701830334 >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> https://www.strandbooks.com/natural-deduction-a-proof- >>>>>>>>>>>>>>> theoretical- >>>>>>>>>>>>>>> study-9780486446554.html >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> "... [Prawitz'] inversion principle constitutes the >>>>>>>>>>>>>>> foundation of >>>>>>>>>>>>>>> most >>>>>>>>>>>>>>> modern accounts of proof-theoretic semantics." >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> I already have a principle of inversion and furthermore a >>>>>>>>>>>>>>> principle of >>>>>>>>>>>>>>> thorough reason as subsuming principles of non- >>>>>>>>>>>>>>> contradiction and what >>>>>>>>>>>>>>> suffices, so, I'll be curious then about what to make of >>>>>>>>>>>>>>> Prawitz' >>>>>>>>>>>>>>> "inversion principle" since Lorenzen. >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> Of course the concept of an "inversion principle" is as >>>>>>>>>>>>>>> old as the >>>>>>>>>>>>>>> oldest account of Western philosophy like Heraclitus with >>>>>>>>>>>>>>> dual >>>>>>>>>>>>>>> monism. >>>>>>>>>>>>>>> In fact by definition it's about the most basic aspect of >>>>>>>>>>>>>>> contemplation >>>>>>>>>>>>>>> and deliberation in abstraction of looking at both sides >>>>>>>>>>>>>>> of issues >>>>>>>>>>>>>>> and >>>>>>>>>>>>>>> resolving inductive impasses with analytical bridges after >>>>>>>>>>>>>>> complementary >>>>>>>>>>>>>>> duals. >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> https://arxiv.org/abs/2112.14967 >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> "Prawitz formulated the so-called inversion principle as >>>>>>>>>>>>>>> one of the >>>>>>>>>>>>>>> characteristic features of Gentzen's intuitionistic natural >>>>>>>>>>>>>>> deduction. >>>>>>>>>>>>>>> In the literature on proof-theoretic semantics, this >>>>>>>>>>>>>>> principle is >>>>>>>>>>>>>>> often >>>>>>>>>>>>>>> coupled with another that is called the recovery >>>>>>>>>>>>>>> principle. By >>>>>>>>>>>>>>> adopting >>>>>>>>>>>>>>> the Computational Ludics framework, we reformulate these >>>>>>>>>>>>>>> principles >>>>>>>>>>>>>>> into >>>>>>>>>>>>>>> one and the same condition, which we call the harmony >>>>>>>>>>>>>>> condition. We >>>>>>>>>>>>>>> show >>>>>>>>>>>>>>> that this reformulation allows us to reveal two intuitive >>>>>>>>>>>>>>> ideas >>>>>>>>>>>>>>> standing >>>>>>>>>>>>>>> behind these principles: the idea of "containment" >>>>>>>>>>>>>>> present in the >>>>>>>>>>>>>>> inversion principle, and the idea that the recovery >>>>>>>>>>>>>>> principle is the >>>>>>>>>>>>>>> "converse" of the inversion principle. We also formulate >>>>>>>>>>>>>>> two other >>>>>>>>>>>>>>> conditions in the Computational Ludics framework, and we >>>>>>>>>>>>>>> show that >>>>>>>>>>>>>>> each >>>>>>>>>>>>>>> of them is equivalent to the harmony condition." >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> The "ludicus" is Latin and for accounts of wisdom and >>>>>>>>>>>>>>> knowledge. >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> "In particular, by taking inspiration from the >>>>>>>>>>>>>>> Brouwer-Heyting-Kolmogorov explanation of logical >>>>>>>>>>>>>>> connectives, >>>>>>>>>>>>>>> proof-theoretic semantics rests on the idea that we know the >>>>>>>>>>>>>>> meaning of >>>>>>>>>>>>>>> a compound sentence when we know what counts as a >>>>>>>>>>>>>>> canonical proof of >>>>>>>>>>>>>>> it. >>>>>>>>>>>>>>> And if proofs are formalised within the framework of natural >>>>>>>>>>>>>>> deduction, >>>>>>>>>>>>>>> then a canonical proof of a sentence A is nothing but a >>>>>>>>>>>>>>> closed >>>>>>>>>>>>>>> derivation ending with an introduction rule of the main >>>>>>>>>>>>>>> connective >>>>>>>>>>>>>>> of A." >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> The "canonical proofs" are not unique, in any system >>>>>>>>>>>>>>> strong enough >>>>>>>>>>>>>>> to make for infinitary reasoning and super-classical results >>>>>>>>>>>>>>> requiring >>>>>>>>>>>>>>> analytical bridges about infinity and continuity. >>>>>>>>>>>>>>> >>>>>>>>>>>>>> >>>>>>>>>>>>>> It is the role that "canonical proofs" play in >>>>>>>>>>>>>> Truth as an Epistemic Notion >>>>>>>>>>>>>> https://link.springer.com/article/10.1007/s11245-011-9107-6 >>>>>>>>>>>>>> That is the most important gist of his whole work. >>>>>>>>>>>>>> >>>>>>>>>>>>>> He later goes on to develop and further elaborate his >>>>>>>>>>>>>> Theory of Grounds. >>>>>>>>>>>>>> >>>>>>>>>>>>>> Atomic Systems in Proof-Theoretic Semantics: Two Approaches >>>>>>>>>>>>>> Thomas Piecha & Peter Schroeder-Heister do this same sort of >>>>>>>>>>>>>> thing two different ways. >>>>>>>>>>>>>> >>>>>>>>>>>>>> >>>>>>>>>>>>>> >>>>>>>>>>>>> >>>>>>>>>>>>> Furthermore I say there are "canonical proofs" of inductive >>>>>>>>>>>>> sorts that >>>>>>>>>>>>> make contradictions and thusly destroy each other. >>>>>>>>>>>>> >>>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> Clearly you have no idea what Dag Prawitz means by >>>>>>>>>>>> "canonical proofs". >>>>>>>>>>>> Go find out and then get back to me. >>>>>>>>>>>> >>>>>>>>>>>>> This is where "the thorough" and "analytical bridges" make >>>>>>>>>>>>> repairs >>>>>>>>>>>>> of what otherwise is flawed, or for hard constructivist >>>>>>>>>>>>> realist >>>>>>>>>>>>> structuralist model theorists: not-theories (examples of >>>>>>>>>>>>> wrong). >>>>>>>>>>>>> >>>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> Induction and counter-induction contradict each other, it's >>>>>>>>>>> simple, >>>>>>>>>>> it's the grounds for most things called "paradox". >>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>> >>>>>>>>>> % This sentence is not true. >>>>>>>>>> ?- LP = not(true(LP)). >>>>>>>>>> LP = not(true(LP)). >>>>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))). >>>>>>>>>> false. >>>>>>>>>> >>>>>>>>>> After you totally understand how and why the proof >>>>>>>>>> theoretic semantics of that is correct and resolves >>>>>>>>>> the Liar Paradox get back to me. >>>>>>>>>> >>>>>>>>>> The essential principle involved that I derived >>>>>>>>>> in my own Minimal Type Theory before I knew that >>>>>>>>>> Prolog could do the same thing is that: >>>>>>>>>> >>>>>>>>>> When the directed graph of the evaluation >>>>>>>>>> sequence of an expression contains a cycle >>>>>>>>>> then the input is determined to be incoherent >>>>>>>>>> on the basis that its proof would never terminate. >>>>>>>>>> Proof Theoretic Semantics does this exact same thing. >>>>>>>>>> >>>>>>>>>> Don't get back to me until you attain the required >>>>>>>>>> prerequisites. I am sure that you already know >>>>>>>>>> all about cycles in directed graphs. >>>>>>>>>> >>>>>>>>> >>>>>>>>> Declaring oneself ignorant thus wise >>>>>>>>> doesn't make much of a case >>>>>>>>> except being ignorant. >>>>>>>>> >>>>>>>>> 300 mile per hour wheelchair: can't take stairs. >>>>>>>>> >>>>>>>>> Except down, .... >>>>>>>>> >>>>>>>>> >>>>>>>> >>>>>>>> So you are going to imply that I am incorrect >>>>>>>> about Prolog when you yourself remain clueless about Prolog? >>>>>>>> That would be dishonest. >>>>>>> >>>>>>> No, pointing out that you are worng about Prolog when you are wrong >>>>>>> about Prolog is never dishohest. >>>>>> >>>>>> That is correct Prolog and that is the >>>>>> result of the correct run of correct Prolog. >>>>> >>>>> Irrelevant. Nobody claimed there be Prolog errors in your queries. >>>>> >>>>>> Implying that I am wrong about Prolog without >>>>>> pointing out any actual mistake is also DISHONEST. >>>>> >>>>> How did Ross FInlayson imply that you were wrong about Prolog? >>>> >>>> If an error is claimed then it must be specifically >>>> pointed out otherwise the clam of error is dishonest. >>> >>> Yet you claim that Ross Finlayson be dishonest without pointing >>> out what is dishonest in his words. >> >> If anyone and everyone that claims that they found an >> error and never points out what the error is and why >> it is an error then they are merely a baseless denigrator. > If anyone and everyone that claims that someone is dishonest > never points out what the dishonesty is is and why it is > dishones then they are merely a baseless denigrator. > Hopefully news.eternal-september.org will be back up. The dishonesty is claiming an error without pointing it out. The dishonesty is also relying on rhetoric and ad hominem instead of reasoning and evidence, Trump's favorite ploy. One-two punch Destroys Liars #WhatIsTheEvidence #ThatIsNotEvidence Around and around until Defeated Kristen Welker's (Meet the Press) interview of Trump She cornered him and he gave up and left proving that he has no evidence https://www.nbcnews.com/politics/donald-trump/read-transcript-president-donald-trump-interviewed-nbc-news-meet-press-rcna348508 2026-06-07 -- Copyright 2026 Olcott My 28 year goal has been to make "true on the basis of meaning expressed in language" reliably computable for the entire body of knowledge. The complete structure of this system is now defined. The entire body of knowledge expressed in language is comprised of two types of relations between finite strings: (a) *Axioms* Expressions of language that are stipulated to be true. My system bridges the analytic/synthetic distinction by expressly encoding all empirical "atomic facts" in a formal language such as CycL of the Cyc project. (b) *Inference Rules* Expressions of language that are semantically entailed syntactically from (a) and/or (b).
[toc] | [prev] | [next] | [standalone]
| From | Mikko <mikko.levanto@iki.fi> |
|---|---|
| Date | 2026-06-28 12:51 +0300 |
| Subject | Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs |
| Message-ID | <111qqrd$3hgmb$1@dont-email.me> |
| In reply to | #142035 |
On 27/06/2026 18:53, polcott wrote: > On 6/27/2026 3:13 AM, Mikko wrote: >> On 26/06/2026 16:15, olcott wrote: >>> On 6/26/2026 1:45 AM, Mikko wrote: >>>> On 25/06/2026 19:16, olcott wrote: >>>>> On 6/25/2026 2:29 AM, Mikko wrote: >>>>>> On 25/06/2026 00:33, olcott wrote: >>>>>>> On 6/24/2026 5:13 AM, Mikko wrote: >>>>>>>> On 23/06/2026 21:20, olcott wrote: >>>>>>>>> On 6/23/2026 12:32 PM, Ross Finlayson wrote: >>>>>>>>>> On 06/23/2026 09:54 AM, olcott wrote: >>>>>>>>>>> On 6/23/2026 10:51 AM, Ross Finlayson wrote: >>>>>>>>>>>> On 06/23/2026 07:22 AM, olcott wrote: >>>>>>>>>>>>> On 6/22/2026 11:31 PM, Ross Finlayson wrote: >>>>>>>>>>>>>> On 06/22/2026 09:14 PM, olcott wrote: >>>>>>>>>>>>>>> On 6/22/2026 11:00 PM, Ross Finlayson wrote: >>>>>>>>>>>>>>>> On 06/22/2026 01:06 PM, olcott wrote: >>>>>>>>>>>>>>>>> On 6/22/2026 2:50 PM, Alan Mackenzie wrote: >>>>>>>>>>>>>>>>>> [ Followup-To: set ] >>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>>>>>>>>>>>> On 6/22/2026 1:42 PM, Alan Mackenzie wrote: >>>>>>>>>>>>>>>>>>>> In comp.theory olcott <polcott333@gmail.com> wrote: >>>>>>>>>>>>>>>>>>>>> On 6/22/2026 10:48 AM, Alan Mackenzie wrote: >>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>> G is true. >>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>>> I put it to you you're lying again. No reputable >>>>>>>>>>>>>>>>>>>>>> mathematician >>>>>>>>>>>>>>>>>>>>>> would >>>>>>>>>>>>>>>>>>>>>> risk his reputation by saying false things. If >>>>>>>>>>>>>>>>>>>>>> Dag Prawitz >>>>>>>>>>>>>>>>>>>>>> really >>>>>>>>>>>>>>>>>>>>>> did >>>>>>>>>>>>>>>>>>>>>> "agree" (with whom?) that Gödel's sentence G is >>>>>>>>>>>>>>>>>>>>>> not true in >>>>>>>>>>>>>>>>>>>>>> Peano >>>>>>>>>>>>>>>>>>>>>> Arithmetic, then produce a citation for this. >>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>>> He never gets to Gödel. He essentially says unprovable >>>>>>>>>>>>>>>>>>>>> means untrue all the time for everything within his >>>>>>>>>>>>>>>>>>>>> own Theory of Grounds of strict Proof Theoretic >>>>>>>>>>>>>>>>>>>>> Semantics. >>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>>> You won't understand it, but that _is_ essentially >>>>>>>>>>>>>>>>>>>> Gödel's >>>>>>>>>>>>>>>>>>>> Incompleteness >>>>>>>>>>>>>>>>>>>> Theorem. It is a statement that any sufficiently >>>>>>>>>>>>>>>>>>>> powerful >>>>>>>>>>>>>>>>>>>> system can >>>>>>>>>>>>>>>>>>>> express true things it can't prove. So Dag Prawitz, >>>>>>>>>>>>>>>>>>>> had he been >>>>>>>>>>>>>>>>>>>> saying >>>>>>>>>>>>>>>>>>>> the things you falsely attributed to him, would >>>>>>>>>>>>>>>>>>>> certainly have >>>>>>>>>>>>>>>>>>>> "got" to >>>>>>>>>>>>>>>>>>>> Gödel, and would have understood full well what he >>>>>>>>>>>>>>>>>>>> was saying. >>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>>> You did not pay close enough attention to my exact >>>>>>>>>>>>>>>>>>> words. >>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>>> I was right, you didn't understand it. >>>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>>>>>>> Dag Prawitz says: Unprovable ALWAYS means untrue >>>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> Yeah, I'm pretty sure that "Dag Prawitz says what Dag >>>>>>>>>>>>>>>> Prawitz says", >>>>>>>>>>>>>>>> and furthermore "Dag Prawitz doesn't say what Dag >>>>>>>>>>>>>>>> Prawitz doesn't >>>>>>>>>>>>>>>> say", >>>>>>>>>>>>>>>> then looking a bit into his tremendous volume of works, >>>>>>>>>>>>>>>> he talks about "natural deduction" then specifically an >>>>>>>>>>>>>>>> "inverse >>>>>>>>>>>>>>>> principle" so I think these are key aspects of >>>>>>>>>>>>>>>> fundamental logic. >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> https://www.researchgate.net/ >>>>>>>>>>>>>>>> publication/233365263_On_Inversion_Principles >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> "On Inversion Principles >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> Enrico Moriconi∗Laura Tesconi† >>>>>>>>>>>>>>>> May 8, 2007 >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> Abstract >>>>>>>>>>>>>>>> The idea of an “inversion principle”, and the name itself, >>>>>>>>>>>>>>>> originated in >>>>>>>>>>>>>>>> the work of Paul Lorenzen in the 1950s, as a method to >>>>>>>>>>>>>>>> generate >>>>>>>>>>>>>>>> new ad- >>>>>>>>>>>>>>>> missible rules within a certain syntactic context. Some >>>>>>>>>>>>>>>> fifteen years >>>>>>>>>>>>>>>> later, the idea was taken up by Dag Prawitz to devise a >>>>>>>>>>>>>>>> strategy of >>>>>>>>>>>>>>>> normalization for natural deduction calculi (this being an >>>>>>>>>>>>>>>> analogue of >>>>>>>>>>>>>>>> Gentzen’s cut-elimination theorem for sequent calculi). >>>>>>>>>>>>>>>> Later, >>>>>>>>>>>>>>>> Prawitz >>>>>>>>>>>>>>>> used the inversion principle again, attributing it with >>>>>>>>>>>>>>>> a semantic >>>>>>>>>>>>>>>> role. >>>>>>>>>>>>>>>> Still working in natural deduction calculi, he >>>>>>>>>>>>>>>> formulated a general >>>>>>>>>>>>>>>> type >>>>>>>>>>>>>>>> of schematic Introduction rules to be matched—thanks to >>>>>>>>>>>>>>>> the idea >>>>>>>>>>>>>>>> supporting the inversion principle — by a corresponding >>>>>>>>>>>>>>>> general >>>>>>>>>>>>>>>> schematic Elimination rule. This was an attempt to >>>>>>>>>>>>>>>> provide a >>>>>>>>>>>>>>>> solution to >>>>>>>>>>>>>>>> the problem suggested by the often quoted note of Gentzen. >>>>>>>>>>>>>>>> According to >>>>>>>>>>>>>>>> Gentzen “it should be possible to display the >>>>>>>>>>>>>>>> elimination rules as >>>>>>>>>>>>>>>> unique functions of the corresponding introduction rules >>>>>>>>>>>>>>>> on the >>>>>>>>>>>>>>>> basis of >>>>>>>>>>>>>>>> certain requirements.” Many people have since worked on >>>>>>>>>>>>>>>> this topic, >>>>>>>>>>>>>>>> which can be appropriately seen as the birthplace of >>>>>>>>>>>>>>>> what are now >>>>>>>>>>>>>>>> referred to as “general elimination rules”, recently >>>>>>>>>>>>>>>> studied >>>>>>>>>>>>>>>> thoroughly >>>>>>>>>>>>>>>> by Sara Negri and Jan von Plato. In this paper, we >>>>>>>>>>>>>>>> retrace the main >>>>>>>>>>>>>>>> threads of this chapter of proof-theoretical >>>>>>>>>>>>>>>> investigation, using >>>>>>>>>>>>>>>> Lorenzen’s original framework as a general guide" >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> Hm, "general elimination rules", seem derivable from De >>>>>>>>>>>>>>>> Morgan's >>>>>>>>>>>>>>>> laws, >>>>>>>>>>>>>>>> and that being the usual account of naive deductive >>>>>>>>>>>>>>>> analysis, then >>>>>>>>>>>>>>>> since >>>>>>>>>>>>>>>> "natural deduction", which here is held as part of the >>>>>>>>>>>>>>>> theory >>>>>>>>>>>>>>>> since it's naturally logical, then has for Gentzen that >>>>>>>>>>>>>>>> besides >>>>>>>>>>>>>>>> Kripke >>>>>>>>>>>>>>>> afterward there's also Sheffer and Chwistek before, and >>>>>>>>>>>>>>>> instead of >>>>>>>>>>>>>>>> Montague for semantics there's Herbrand for semantics, >>>>>>>>>>>>>>>> so, what to do >>>>>>>>>>>>>>>> about "inversion principle" is here that the thea-theory >>>>>>>>>>>>>>>> has that >>>>>>>>>>>>>>>> it's >>>>>>>>>>>>>>>> what subsumes "non-contradiction principle", here hoping >>>>>>>>>>>>>>>> that the >>>>>>>>>>>>>>>> interpretation aligns and thusly that "principle of >>>>>>>>>>>>>>>> inversion" >>>>>>>>>>>>>>>> wouldn't >>>>>>>>>>>>>>>> need dis-ambiguation from "inversion principle". >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> https://www.tandfonline.com/doi/ >>>>>>>>>>>>>>>> abs/10.1080/01445340701830334 >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> https://www.strandbooks.com/natural-deduction-a-proof- >>>>>>>>>>>>>>>> theoretical- >>>>>>>>>>>>>>>> study-9780486446554.html >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> "... [Prawitz'] inversion principle constitutes the >>>>>>>>>>>>>>>> foundation of >>>>>>>>>>>>>>>> most >>>>>>>>>>>>>>>> modern accounts of proof-theoretic semantics." >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> I already have a principle of inversion and furthermore a >>>>>>>>>>>>>>>> principle of >>>>>>>>>>>>>>>> thorough reason as subsuming principles of non- >>>>>>>>>>>>>>>> contradiction and what >>>>>>>>>>>>>>>> suffices, so, I'll be curious then about what to make of >>>>>>>>>>>>>>>> Prawitz' >>>>>>>>>>>>>>>> "inversion principle" since Lorenzen. >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> Of course the concept of an "inversion principle" is as >>>>>>>>>>>>>>>> old as the >>>>>>>>>>>>>>>> oldest account of Western philosophy like Heraclitus >>>>>>>>>>>>>>>> with dual >>>>>>>>>>>>>>>> monism. >>>>>>>>>>>>>>>> In fact by definition it's about the most basic aspect of >>>>>>>>>>>>>>>> contemplation >>>>>>>>>>>>>>>> and deliberation in abstraction of looking at both sides >>>>>>>>>>>>>>>> of issues >>>>>>>>>>>>>>>> and >>>>>>>>>>>>>>>> resolving inductive impasses with analytical bridges after >>>>>>>>>>>>>>>> complementary >>>>>>>>>>>>>>>> duals. >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> https://arxiv.org/abs/2112.14967 >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> "Prawitz formulated the so-called inversion principle as >>>>>>>>>>>>>>>> one of the >>>>>>>>>>>>>>>> characteristic features of Gentzen's intuitionistic natural >>>>>>>>>>>>>>>> deduction. >>>>>>>>>>>>>>>> In the literature on proof-theoretic semantics, this >>>>>>>>>>>>>>>> principle is >>>>>>>>>>>>>>>> often >>>>>>>>>>>>>>>> coupled with another that is called the recovery >>>>>>>>>>>>>>>> principle. By >>>>>>>>>>>>>>>> adopting >>>>>>>>>>>>>>>> the Computational Ludics framework, we reformulate these >>>>>>>>>>>>>>>> principles >>>>>>>>>>>>>>>> into >>>>>>>>>>>>>>>> one and the same condition, which we call the harmony >>>>>>>>>>>>>>>> condition. We >>>>>>>>>>>>>>>> show >>>>>>>>>>>>>>>> that this reformulation allows us to reveal two >>>>>>>>>>>>>>>> intuitive ideas >>>>>>>>>>>>>>>> standing >>>>>>>>>>>>>>>> behind these principles: the idea of "containment" >>>>>>>>>>>>>>>> present in the >>>>>>>>>>>>>>>> inversion principle, and the idea that the recovery >>>>>>>>>>>>>>>> principle is the >>>>>>>>>>>>>>>> "converse" of the inversion principle. We also formulate >>>>>>>>>>>>>>>> two other >>>>>>>>>>>>>>>> conditions in the Computational Ludics framework, and we >>>>>>>>>>>>>>>> show that >>>>>>>>>>>>>>>> each >>>>>>>>>>>>>>>> of them is equivalent to the harmony condition." >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> The "ludicus" is Latin and for accounts of wisdom and >>>>>>>>>>>>>>>> knowledge. >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> "In particular, by taking inspiration from the >>>>>>>>>>>>>>>> Brouwer-Heyting-Kolmogorov explanation of logical >>>>>>>>>>>>>>>> connectives, >>>>>>>>>>>>>>>> proof-theoretic semantics rests on the idea that we know >>>>>>>>>>>>>>>> the >>>>>>>>>>>>>>>> meaning of >>>>>>>>>>>>>>>> a compound sentence when we know what counts as a >>>>>>>>>>>>>>>> canonical proof of >>>>>>>>>>>>>>>> it. >>>>>>>>>>>>>>>> And if proofs are formalised within the framework of >>>>>>>>>>>>>>>> natural >>>>>>>>>>>>>>>> deduction, >>>>>>>>>>>>>>>> then a canonical proof of a sentence A is nothing but a >>>>>>>>>>>>>>>> closed >>>>>>>>>>>>>>>> derivation ending with an introduction rule of the main >>>>>>>>>>>>>>>> connective >>>>>>>>>>>>>>>> of A." >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>>> The "canonical proofs" are not unique, in any system >>>>>>>>>>>>>>>> strong enough >>>>>>>>>>>>>>>> to make for infinitary reasoning and super-classical >>>>>>>>>>>>>>>> results >>>>>>>>>>>>>>>> requiring >>>>>>>>>>>>>>>> analytical bridges about infinity and continuity. >>>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> It is the role that "canonical proofs" play in >>>>>>>>>>>>>>> Truth as an Epistemic Notion >>>>>>>>>>>>>>> https://link.springer.com/article/10.1007/s11245-011-9107-6 >>>>>>>>>>>>>>> That is the most important gist of his whole work. >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> He later goes on to develop and further elaborate his >>>>>>>>>>>>>>> Theory of Grounds. >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> Atomic Systems in Proof-Theoretic Semantics: Two Approaches >>>>>>>>>>>>>>> Thomas Piecha & Peter Schroeder-Heister do this same sort of >>>>>>>>>>>>>>> thing two different ways. >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>>> >>>>>>>>>>>>>> >>>>>>>>>>>>>> Furthermore I say there are "canonical proofs" of >>>>>>>>>>>>>> inductive sorts that >>>>>>>>>>>>>> make contradictions and thusly destroy each other. >>>>>>>>>>>>>> >>>>>>>>>>>>>> >>>>>>>>>>>>> >>>>>>>>>>>>> Clearly you have no idea what Dag Prawitz means by >>>>>>>>>>>>> "canonical proofs". >>>>>>>>>>>>> Go find out and then get back to me. >>>>>>>>>>>>> >>>>>>>>>>>>>> This is where "the thorough" and "analytical bridges" make >>>>>>>>>>>>>> repairs >>>>>>>>>>>>>> of what otherwise is flawed, or for hard constructivist >>>>>>>>>>>>>> realist >>>>>>>>>>>>>> structuralist model theorists: not-theories (examples of >>>>>>>>>>>>>> wrong). >>>>>>>>>>>>>> >>>>>>>>>>>>>> >>>>>>>>>>>>> >>>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>>> Induction and counter-induction contradict each other, it's >>>>>>>>>>>> simple, >>>>>>>>>>>> it's the grounds for most things called "paradox". >>>>>>>>>>>> >>>>>>>>>>>> >>>>>>>>>>> >>>>>>>>>>> % This sentence is not true. >>>>>>>>>>> ?- LP = not(true(LP)). >>>>>>>>>>> LP = not(true(LP)). >>>>>>>>>>> ?- unify_with_occurs_check(LP, not(true(LP))). >>>>>>>>>>> false. >>>>>>>>>>> >>>>>>>>>>> After you totally understand how and why the proof >>>>>>>>>>> theoretic semantics of that is correct and resolves >>>>>>>>>>> the Liar Paradox get back to me. >>>>>>>>>>> >>>>>>>>>>> The essential principle involved that I derived >>>>>>>>>>> in my own Minimal Type Theory before I knew that >>>>>>>>>>> Prolog could do the same thing is that: >>>>>>>>>>> >>>>>>>>>>> When the directed graph of the evaluation >>>>>>>>>>> sequence of an expression contains a cycle >>>>>>>>>>> then the input is determined to be incoherent >>>>>>>>>>> on the basis that its proof would never terminate. >>>>>>>>>>> Proof Theoretic Semantics does this exact same thing. >>>>>>>>>>> >>>>>>>>>>> Don't get back to me until you attain the required >>>>>>>>>>> prerequisites. I am sure that you already know >>>>>>>>>>> all about cycles in directed graphs. >>>>>>>>>>> >>>>>>>>>> >>>>>>>>>> Declaring oneself ignorant thus wise >>>>>>>>>> doesn't make much of a case >>>>>>>>>> except being ignorant. >>>>>>>>>> >>>>>>>>>> 300 mile per hour wheelchair: can't take stairs. >>>>>>>>>> >>>>>>>>>> Except down, .... >>>>>>>>>> >>>>>>>>>> >>>>>>>>> >>>>>>>>> So you are going to imply that I am incorrect >>>>>>>>> about Prolog when you yourself remain clueless about Prolog? >>>>>>>>> That would be dishonest. >>>>>>>> >>>>>>>> No, pointing out that you are worng about Prolog when you are wrong >>>>>>>> about Prolog is never dishohest. >>>>>>> >>>>>>> That is correct Prolog and that is the >>>>>>> result of the correct run of correct Prolog. >>>>>> >>>>>> Irrelevant. Nobody claimed there be Prolog errors in your queries. >>>>>> >>>>>>> Implying that I am wrong about Prolog without >>>>>>> pointing out any actual mistake is also DISHONEST. >>>>>> >>>>>> How did Ross FInlayson imply that you were wrong about Prolog? >>>>> >>>>> If an error is claimed then it must be specifically >>>>> pointed out otherwise the clam of error is dishonest. >>>> >>>> Yet you claim that Ross Finlayson be dishonest without pointing >>>> out what is dishonest in his words. >>> >>> If anyone and everyone that claims that they found an >>> error and never points out what the error is and why >>> it is an error then they are merely a baseless denigrator. > >> If anyone and everyone that claims that someone is dishonest >> never points out what the dishonesty is is and why it is >> dishones then they are merely a baseless denigrator. > > Hopefully > news.eternal-september.org > will be back up. > > The dishonesty is claiming an error without pointing it out. A dishonesty is an error, so everything you say about errors you also say about dishonesty. So you are (or at least claim to be) dishonest when you claim that Ross Finlayson is dishonest without pointing it out. > The dishonesty is also relying on rhetoric and ad hominem > instead of reasoning and evidence, Trump's favorite ploy. As you often do, above and elsewhere. -- Mikko
[toc] | [prev] | [next] | [standalone]
| From | olcott <polcott333@gmail.com> |
|---|---|
| Date | 2026-06-30 09:53 -0500 |
| Subject | Re: Ross A. Finlayson, readings in (some of the) --- cycles in directed graphs |
| Message-ID | <1120l8o$15kod$1@dont-email.me> |
| In reply to | #142118 |
On 6/30/2026 8:23 AM, Ross Finlayson wrote: > So, if you want to know more about my theory, which is an account > of reason, and for Foundations, then I'd suggest first making for > yourself a "universal education", then finding resolutions to the > "paradoxes" of mathematical logic, % This sentence is not true. ?- LP = not(true(LP)). LP = not(true(LP)). ?- unify_with_occurs_check(LP, not(true(LP))). false. Olcott's Minimal Type Theory G ↔ ¬Prov_PA(⌜G⌝) Directed Graph of evaluation sequence 00 ↔ 01 02 01 G 02 ¬ 03 03 Prov_PA 04 04 Gödel_Number_of 01 // cycle indicates no well-founded justification tree exists. ZFC already handled Russell's Paradox converting set theory into Naive set theory. It is important to keep computation in the loop because computation exposes the hidden assumptions that math makes. Curry–Howard correspondence In programming language theory and proof theory, the Curry–Howard correspondence is a direct relationship between computer programs and mathematical proofs. https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence > then revealing the "super-classical" > results of classical mathematics, then for the "extra-ordinary" the > "great atlas of mathematical independence", then for "higher > mathematics", and quite about "continuity" and "infinity", > then there's also "the physics" after "the logic" and "the mathematics". > > -- Copyright 2026 Olcott My 28 year goal has been to make "true on the basis of meaning expressed in language" reliably computable for the entire body of knowledge. The complete structure of this system is now defined. The entire body of knowledge expressed in language is comprised of two types of relations between finite strings: (a) *Axioms* Expressions of language that are stipulated to be true. My system bridges the analytic/synthetic distinction by expressly encoding all empirical "atomic facts" in a formal language such as CycL of the Cyc project. (b) *Inference Rules* Expressions of language that are semantically entailed syntactically from (a) and/or (b).
[toc] | [prev] | [next] | [standalone]
Page 17 of 18 — ← Prev page 1 … 15 16 [17] 18 Next page →
Back to top | Article view | comp.theory
csiph-web