From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=DKIMWL_WL_HIGH,DKIM_SIGNED, DKIM_VALID,HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE, RCVD_IN_DNSWL_NONE,T_SCC_BODY_TEXT_LINE,UNPARSEABLE_RELAY autolearn=ham autolearn_force=no version=3.4.4 Received: from AUS01-ME3-obe.outbound.protection.outlook.com (mail-me3aus01hn2244.outbound.protection.outlook.com [52.100.209.244]) by inbox.vuxu.org (Postfix) with ESMTP id 9138729FCE for ; Thu, 8 Feb 2024 21:30:49 +0100 (CET) ARC-Seal: i=4; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=pass; b=PDtlQsLx48UOwWRAGGYf2fnVed3Qze6FY7YCCxiPgLNeadGmk8Bo3KoR3EdUnliQ3uAzW5dITUadMLExTaDe0uiGDmds6BS2uN+aenTpcyLQkH9CDXjpVreVQYU7ICJYcORHq0TFuq6r5qpKFaJ075IDsXwJ1bYUIkAfRuPJ6XeYW/m4VFkpgNAR/NHx2TYDuPihtjvatzgSBic+HJdEZFebOQCX8regRzZMFRfmWOoW+y7vYbmil+yjVpOAkKwoBtym2xrx1N7OqxhwsE1sLdQ1z0O/qFgiyiK1rw09ulbHFEVaCGPtiBpp4ZnTmlQjnYS6uV//iRTwCLutN8os1g== ARC-Message-Signature: i=4; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=XNjDckuv2V+2PaI7LYLJWXFh4f8lauis+KAiDB9XM2U=; b=mzLcv3ryPuieOSj3eFbUGvoM4YoA2i8GeL4JaTh21rXQwyMdTaK+yxzD9whlvnXPw2A1g3htUtWCuJCbDVi40uLTCrIoEwzR9iMU6O11rYCtZs91kCNa9MV5/cBqiOLyMgt+/KuPtorfZXPYytzCPOL2Fij9KUhYoWczCXhcbvLDPdtSINTKJi4hX9TbaH7vJEViUW4BYtVj2rBWEuvp954EAF+X+WAj4Hrz8Mm8qViD34fay5m2516WDCv+SPCmCai1gDT4f9o6iIMJnvUQdf0mB9EcVnTV+XXOu+xgl/NMmvUxqn9qvhMyuu9eowUIQe8Q8hjqZ07I7yRmBiLsEQ== ARC-Authentication-Results: i=4; mx.microsoft.com 1; spf=pass (sender ip is 130.239.40.25) smtp.rcpttodomain=mq.edu.au smtp.mailfrom=cs.umu.se; dmarc=pass (p=none sp=none pct=10) action=none header.from=cs.umu.se; dkim=fail (body hash did not verify) header.d=cs.umu.se; dkim=fail (body hash did not verify) header.d=cs.umu.se; arc=pass (0 oda=0 ltdi=0 93) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=groups.office.net; s=selector1; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=XNjDckuv2V+2PaI7LYLJWXFh4f8lauis+KAiDB9XM2U=; b=q4+vbJ3MR8BEp54LfTzz1ZgJmtZzj/xoY6sUXa6CfrITH0EZKK0YDv8O8TINuzYEOeDN6wPBqKhkYHR0Z8naG1mydwUyAXJnmh4LivVwN14uSX4mYlGrtQh7npid83TOxYxqYXUJ0PXuMkDLYS4hl/skUvOhu/ixHpj0thwSr6ZXQ+UoziBRG4v8SLSjncrswhqemVtfPbyJMj3cHKxOb73zxNzXpBY1bcUwYryDmhy1b9qFQeNbUUs830Pt0hN9KdA5HwmyWoLtMpVwRsssRfiAJ5mfQNviUB4kGq5JiorKwj3rDyzij5JxI9yZiZ63qF/gwbMUGEfnr5V60EdHfw== Received: from SmtpServer.Submit by SYBPR01MB5551 with Microsoft SMTP Server id 15.20.7270.24; Thu, 8 Feb 2024 20:30:45 +0000 ARC-Seal: i=3; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=pass; b=S2cM8KhjRd0+xFh6eUodoumlVW83gcjkfYDikVSOiTFWd333Rze/BkewodDQJ0UsUZghoPzhjxWGIT1QXoyPEHT3hM1+6GfSrDvhz0VJqVC6pJ9iCzLzY342FMweD3uY4Hygt0si4+j+HKnVQGp7QWH3Q+IqcKBgT6LsMGY3bYkVuVSaR8BSIGlQ8Qlu7DOOQ0JDTiFNsm6ttCzXGWesy5TLDU383Ejvz9BNFiOA/WxdH1An3sDN6wBp8Mm/2yKtFNAjf0iRPZ3vzdLlYJAkDuV6DT9l4cn/inYRRmLmFzkphsHmZ0jEDxsLpeO2ufjAuVylTRgqylNMkiU1607btw== ARC-Message-Signature: i=3; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=3GW/f2CKHK9SjzmRHOtBxydUTGjShKNeoVUA2bi8kAs=; b=jB2bElUZ7Nmsw8FYFeZdraAfrqg/1gUMnFFKyAFFZubZfM0p8P+WXFeGtMxaqzRbfWfFSmQuwprlMgkSd9K1eykI0H+btsMiDvZmTmsCYR0Yq8gWWOPFP1RmGdZl4HYcuF01pleLkx5LwXKuBuwXBrYqOA3NggtzyuzJxcOXUUlb9hxjQOX6WlnOTkpjliTbQgsRcesf9GDTldHnYK7uAyGgZszZBf6zE0dUXamRu58/jvRXqF4sWwogLxIMWrfiofHl6+sM9D4XR3CHdtVYWB1tN38jlpZNLOSIFhnuHUGDaHBQ5qi5bPpJfvKJGoBZSKVUAx4TPAkJOfXXjty2uQ== ARC-Authentication-Results: i=3; mx.microsoft.com 1; spf=pass (sender ip is 130.239.40.25) smtp.rcpttodomain=mq.edu.au smtp.mailfrom=cs.umu.se; dmarc=pass (p=none sp=none pct=10) action=none header.from=cs.umu.se; dkim=fail (body hash did not verify) header.d=cs.umu.se; dkim=fail (body hash did not verify) header.d=cs.umu.se; arc=pass (0 oda=0 ltdi=0 93) Received: from SY8PR01MB9121.ausprd01.prod.outlook.com (2603:10c6:10:22c::16) by SYBPR01MB5551.ausprd01.prod.outlook.com (2603:10c6:10:e4::8) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.7270.24; Thu, 8 Feb 2024 20:30:40 +0000 Received: from ME3PR01MB5480.ausprd01.prod.outlook.com (2603:10c6:220:7::8) by SY8PR01MB9121.ausprd01.prod.outlook.com (2603:10c6:10:22c::16) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.7270.24; Thu, 8 Feb 2024 20:30:37 +0000 Received: from ME3PR01MB5480.ausprd01.prod.outlook.com ([fe80::6b0f:c883:3328:f0b5]) by ME3PR01MB5480.ausprd01.prod.outlook.com ([fe80::6b0f:c883:3328:f0b5%6]) with mapi id 15.20.7270.024; Thu, 8 Feb 2024 20:30:36 +0000 ARC-Seal: i=2; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=pass; b=R3gJM7CPkCX/mlRj5ftqBpheMherDFVKmUuHv3QdvDL2t7uYGYTS+QAYR9BlnTrqhU/o+Vou5cpUEQw4ZYGg3ukiUszS2BmIUjyX8HLCjMIO1s1tbKJchUsxtZcssTjqcDaOIy0Jxmzohzh3kchKDmgMBfHDdgAL0DboSSShyA9lZTTeB12eyHrqTQv01uSn5P69LthGL74uhZysYn4bIYj+hOpnoPSDuBAO7kZnBtk6Jn/eVnALxHk9V1YASBSZVUJJO9deH+b2R1qj2Xbwup3+/CbWdYi/z7I+ecWUWqottJM4X9BlTFr6xKBnIEWfURiGZIhQShl1sQyD+rOZUQ== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=3GW/f2CKHK9SjzmRHOtBxydUTGjShKNeoVUA2bi8kAs=; b=j07IBifszdjsYbiwamxNCVHWo9jC4qI2K0EQKDVltWfOmH23hdCzZKStEpTNx4ny9PNp4ugoE7u+ZU5bf4nk4251p2gnt9nTRyUcMXWUypZwrcwaULunGvYci6KA0X+AntAdcu4Qf/ULBjhjM/0HhUVAspywdH3ZGReg6/Ub9wqXjFbI32jr+5HWzcCafy93dKHZWApPkKUykEqHvz4hx13wD8bDItUSytBCamNuiOlBfYI7vgUTe7m+Z9uUSWW7u77tCDQ5CrpF8or7rEWl8BV/PKuMMgxoTpnsVGA+Y9MArHfcz6fNzC+4wjK3TT2Ee1U0o+6Q7ud2MO42DBaXrQ== ARC-Authentication-Results: i=2; mx.microsoft.com 1; spf=pass (sender ip is 130.239.40.25) smtp.rcpttodomain=mq.edu.au smtp.mailfrom=cs.umu.se; dmarc=pass (p=none sp=none pct=10) action=none header.from=cs.umu.se; dkim=fail (body hash did not verify) header.d=cs.umu.se; dkim=fail (body hash did not verify) header.d=cs.umu.se; arc=pass (0 oda=0 ltdi=0 93) Received: from ME2PR01CA0229.ausprd01.prod.outlook.com (2603:10c6:220:19::25) by SY4PR01MB6106.ausprd01.prod.outlook.com (2603:10c6:10:f9::10) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.7249.39; Thu, 8 Feb 2024 10:39:18 +0000 Received: from ME3AUS01FT022.eop-AUS01.prod.protection.outlook.com (2603:10c6:220:19:cafe::bb) by ME2PR01CA0229.outlook.office365.com (2603:10c6:220:19::25) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.7249.38 via Frontend Transport; Thu, 8 Feb 2024 10:39:18 +0000 Authentication-Results: spf=pass (sender IP is 130.239.40.25) smtp.mailfrom=cs.umu.se; dkim=fail (body hash did not verify) header.d=cs.umu.se;dmarc=pass action=none header.from=cs.umu.se; Received-SPF: Pass (protection.outlook.com: domain of cs.umu.se designates 130.239.40.25 as permitted sender) receiver=protection.outlook.com; client-ip=130.239.40.25; helo=mail.cs.umu.se; pr=C Received: from au-smtp-inbound-delivery-1.mimecast.com (103.96.20.101) by ME3AUS01FT022.mail.protection.outlook.com (10.114.155.117) with Microsoft SMTP Server (version=TLS1_3, cipher=TLS_AES_256_GCM_SHA384) id 15.20.7270.23 via Frontend Transport; Thu, 8 Feb 2024 10:39:17 +0000 ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=dkim.mimecast.com; s=201903; t=1707388756; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version:content-type:content-type: in-reply-to:in-reply-to:references:references:dkim-signature; bh=3GW/f2CKHK9SjzmRHOtBxydUTGjShKNeoVUA2bi8kAs=; b=mJAjcUDpzA07Qa3UvG9Ensmw3HFd7LgqGQNeBHtsaTyIBLiHPggiF++JiJCQTcnbaqURq9 jWJPqnryY/ZGKOwc5X6weZrsHlFInsEAAeSTJjNm9nSlLESJTn5ucdAu6cFqIojke7k9e/ qQfx1RY4n5tvtgLuqmo68ueZ3j/sJ4ZgFt94fjPpg6NYfsTuKctqFeiXpN3pJUsoryDnmU sjUZxwYRpM7CMFGgOqBo9fO3SMTDRTyJa7svHnluvKvOkVe4r5TsrflnX/xYpD9kAFG26T 1dLF7r9vsFV5MuP/WEhNFMdgCwwAlX3G5kGCSFsJmljjt66O/xJsMn3iC9+vqw== ARC-Seal: i=1; s=201903; d=dkim.mimecast.com; t=1707388756; a=rsa-sha256; cv=none; b=ZS2VeuMS6FbuyrXp3bnTaclk4L774pzVgWecelOttqNIy9zTbZY7odTnLlBgiz1hzrjWzw 3s6E+8nof4J6B5rhEpCwqFhsAwFPZEy0ybB5wl3mHcWTyKYNbohCpxDyzifuUAPyzffUi4 O5rQLQiJz8e01Q9GkoRpBDk5/OwTHLWCGDC53ZR2eP6LWl6MX3UV37H2Q4OjwoiOCsxTLT EQl+uKtytrietlpMrqRflJSMB0vLM2B69jHz/H3g45wW30PyxTNC9skqsffyi9gZHaG+Fz ht62b+sKMBiX5z2awPcfmlIu+aAroYO4Vvjqc0/V6HtP8jB6DTUFtIQrBwb1nA== ARC-Authentication-Results: i=1; relay.mimecast.com; dkim=fail ("body hash did not verify") header.d=cs.umu.se header.s=dkim header.b=mv5u5PVd; dkim=fail ("body hash did not verify") header.d=cs.umu.se header.s=dkim header.b=EJpRsTEh; dmarc=pass (policy=none) header.from=cs.umu.se; spf=pass (relay.mimecast.com: domain of peklund@cs.umu.se designates 130.239.40.25 as permitted sender) smtp.mailfrom=peklund@cs.umu.se Received: from mail.cs.umu.se (mail.cs.umu.se [130.239.40.25]) by relay.mimecast.com with ESMTP with STARTTLS (version=TLSv1.3, cipher=TLS_AES_256_GCM_SHA384) id au-mta-97-2pYXePwrMKCnDhKnbZ0yuQ-1; Thu, 08 Feb 2024 21:39:12 +1100 X-MC-Unique: 2pYXePwrMKCnDhKnbZ0yuQ-1 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=cs.umu.se; s=dkim; t=1707388746; bh=B+NIJgQOzm0Cz4ifsMR/9b7gAiRRzTUikcalsp22zig=; h=Date:From:To:Cc:Subject:In-Reply-To:References:From; b=mv5u5PVdnD6BuStjkprfIkqcwqoY419f6PPEMFrk1aJQHZtQeYfzlSwWqG/FHYJk5 PbPZfdIr1m01OW1NMFib9MAqmsDeyHjiLkqLta15/oiY+WmsnwKc4oIQy4ZopJ40MN pe4Fufq+BtcNqlDdzcO0uCEJyw5iozCBfwipRpWVp4qP2uHV4OsrifUEe3agQtpOEV LQK0m66yy0170/g8pgiD/dxxSI03WX2wFbOsx5f+BfIZNjuuB4JU1LX4Eh+D+c1I+Q Z5DPKIQDv95R3jWtFM981OduMx3zC7UpiAbvLY9+ppcqXm80Y4SmXNXJszFugzb6Fa EbNlGOilTTEJw== Received: from localhost (localhost [127.0.0.1]) by amavisd-new (Postfix) with ESMTP id 4TVtky2Dn8z6B; Thu, 8 Feb 2024 11:39:06 +0100 (CET) X-Virus-Scanned: Debian amavis at cs.umu.se Received: from mail.cs.umu.se ([127.0.0.1]) by localhost (mail-vm2.cs.umu.se [127.0.0.1]) (amavis, port 10024) with LMTP id j3aD35XI11rz; Thu, 8 Feb 2024 11:39:05 +0100 (CET) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=cs.umu.se; s=dkim; t=1707388745; bh=B+NIJgQOzm0Cz4ifsMR/9b7gAiRRzTUikcalsp22zig=; h=Date:From:To:Cc:Subject:In-Reply-To:References:From; b=EJpRsTEhE3LMoqqUnQkbK+ojbRZAdvrffa1kjZxME8VzTbA+lKsDINUW+QDKvt8aR wgnPZD6PXjdJO6vVtfnzyXAmUeOWH4xAunB4JkHSui9ioOsCWlZ8HwZ9IxgX/P35ev UYfaJAH69mVIhx5AaW/wV690kdT9EJthxyAEJhB5wujzwO6ssC5ZALw/JYIk3qQ5OS EzBMIFdziM3v9mIpskmH81L93swy+tUGVG+wcGpzsCqGfpSqgCljNJlgqShVyKrKiR myXD7giKivsaDAQm3V7Qv/CDFAcUmJ+/Vi/aMIj33tbV7gmEjXMeivvMqckxCdk6R9 qBcu46PJoBWcA== Received: from webmail.cs.umu.se (webmail-vm.cs.umu.se [IPv6:2001:6b0:e:4040::68]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256) (No client certificate requested) (Authenticated sender: peklund) by mail.cs.umu.se (Postfix) with ESMTPSA id 4TVtkw57dDz4Q; Thu, 8 Feb 2024 11:39:04 +0100 (CET) Received: from KwiFi3eUDZkkMPNRg3Egj1RYw/Tmvzp3KqBSSy47r+8= (1uPvY2fPIk0Hitmo5yP/ZV6xKpwUiITR) by webmail.cs.umu.se with HTTP (HTTP/1.1 POST); Thu, 08 Feb 2024 11:39:04 +0100 MIME-Version: 1.0 Date: Thu, 08 Feb 2024 12:39:04 +0200 From: Patrik Eklund To: Vaughan Pratt CC: Categories mailing list Subject: Re: Monadicity questions In-Reply-To: References: <9e9cb7c9a56b7b0c01ea26ca622f8553@cs.umu.se> Message-ID: <9e1e9adda042d255754149546fb66527@cs.umu.se> X-Sender: peklund@cs.umu.se Authentication-Results-Original: relay.mimecast.com; dkim=fail ("body hash did not verify") header.d=cs.umu.se header.s=dkim header.b=mv5u5PVd; dkim=fail ("body hash did not verify") header.d=cs.umu.se header.s=dkim header.b=EJpRsTEh; dmarc=pass (policy=none) header.from=cs.umu.se; spf=pass (relay.mimecast.com: domain of peklund@cs.umu.se designates 130.239.40.25 as permitted sender) smtp.mailfrom=peklund@cs.umu.se X-Mimecast-Spam-Score: 0 X-Mimecast-Impersonation-Protect: Policy=MQ - Tag Header Only on Default Settings;Similar Internal Domain=false;Similar Monitored External Domain=false;Custom External Domain=false;Mimecast External Domain=false;Newly Observed Domain=false;Internal User Name=false;Custom Display Name List=false;Reply-to Address Mismatch=false;Targeted Threat Dictionary=false;Mimecast Threat Dictionary=false;Custom Threat Dictionary=false Content-Type: multipart/alternative; boundary="=_aa5f59a9f66015554b4e0d04814fb6bb" X-EOPAttributedMessage: 0 X-EOPTenantAttributedMessage: 82c514c1-a717-4087-be06-d40d2070ad52:0 X-MS-Exchange-SkipListedInternetSender: ip=[130.239.40.25];domain=mail.cs.umu.se X-MS-Exchange-ExternalOriginalInternetSender: ip=[130.239.40.25];domain=mail.cs.umu.se X-MS-PublicTrafficType: Email X-MS-TrafficTypeDiagnostic: ME3AUS01FT022:EE_|SY4PR01MB6106:EE_|SY8PR01MB9121:EE_|SYBPR01MB5551:EE_ X-MS-Office365-Filtering-Correlation-Id: cde1824e-822c-48cf-4dc0-08dc2892338b X-Moderation-Data: 2/8/2024 8:30:35 PM X-LD-Processed: 82c514c1-a717-4087-be06-d40d2070ad52,ExtAddr,ExtAddr X-MS-Exchange-AtpMessageProperties: SA X-MS-Exchange-SenderADCheck: 0 X-MS-Exchange-AntiSpam-Relay: 0 X-Microsoft-Antispam: BCL:0; X-Microsoft-Antispam-Message-Info: QWicvUg33HFf7kOjeW8OWhkK/DfLHQw0yspLso0YVCrWt/16GyqAFXUbD2Ia15udQS73ZKdiEZrkl2SkwwT9+mylNHw3O7FtxD8063qBOndaRnk++RXkX2QslEAtCIiVPx/L7s+g+XXrBKbBd26zjA/gQLWKAFx7StYmTABaTPWD2Ue1JNWHss0+wSlKELsGqm6fB26y34aINg0Xf7csEI2PgdA2R/tr/t+qN2r2JVcTTWgQSb6cYmI+AxL8USf7oulCU1JZP+0ls7sr29coelOo3i5cK/upGBFtOahg/cOACchVTHZQXbumU13KGQ09lnOIo9yFCFaTxwfrEMUegve+28X7Cbz2WKBcIR6jyaD5jmkQZoGkfTdothJ5NSzrTaot/HtYQxFn4x27YCZvBl0BKdCLBLM+dCbUn+PTcVXnbF7RKw3MudQj3cJXyj11z/FMmlfb3AiqEWwY5jYcojZqXTYuBHUuF01GpngqX1vgpDiDQ1+F+V+ag5TSCiGePehFnVnXQnJJU55S7z14LPl4MTbxNJ9GIDDMzdlMC/X2rvrq+IOJL8pv12BTDV+Vf1mrU5XrHF53LOfaigh3y9u06w5aNjQXPxJJ6ND+qzjP1q9iy6P8CqscfUbdh7cPxStPEsh5g33RFL+WVNR8LiJgrDeNVYmw8twYefIbKjR9MCON1z+0FqrkdGlPv0YhkNAEm4xjYnwQtDQLAnXLQJMr0IoS0rTygof9V2w1czk= X-Forefront-Antispam-Report: CIP:103.96.20.101;CTRY:SE;LANG:en;SCL:1;SRV:;IPV:NLI;SFV:NSPM;H:mail.cs.umu.se;PTR:mail.cs.umu.se;CAT:NONE;SFS:(13230031)(4636009)(346002)(396003)(376002)(39860400002)(136003)(451199024)(64100799003)(1800799012)(48200799006)(82310400011)(40470700004)(7276002)(7366002)(7336002)(7406005)(7416002)(82740400003)(30864003)(5660300002)(2906002)(156005)(24736004)(53546011)(33964004)(426003)(108616005)(89122003)(88732003)(76576003)(498600001)(86362001)(66574015)(336012)(26005)(2616005)(41300700001)(36756003)(83380400001)(8936002)(8676002)(3480700007)(68406010)(7116003)(70586007)(6862004)(4326008)(7596003)(786003)(316002)(41110700001)(41090700016)(41080700001);DIR:OUT;SFP:1501; X-Auto-Response-Suppress: DR, OOF, AutoReply X-MS-Exchange-CrossTenant-Network-Message-Id: cde1824e-822c-48cf-4dc0-08dc2892338b X-MS-Exchange-CrossTenant-Id: 82c514c1-a717-4087-be06-d40d2070ad52 X-MS-Exchange-CrossTenant-AuthSource: ME3AUS01FT022.eop-AUS01.prod.protection.outlook.com X-MS-Exchange-CrossTenant-AuthAs: Anonymous X-MS-Exchange-CrossTenant-FromEntityHeader: Internet X-MS-Exchange-CrossTenant-OriginalArrivalTime: 08 Feb 2024 20:30:36.8852 (UTC) X-MS-Exchange-CrossTenant-MailboxType: HOSTED X-MS-Exchange-CrossTenant-UserPrincipalName: Kml8yGFPuTRbqM1cvLXhc+LzaC5qiIOkDZP8FB9OAoko/N/cVCkbqvatzfyDNiSNSNASTfZqguF7mmVFstYd9XeZ6XarGhOS/nQUtkgABNWElRIySGg2FX/alP6K0LJgXEjD5gwidzV2CPjzjHUNoSzVJDY3HYQlbbDzUt3O9s3s9dhy9U3UyGTsQWDcnoOVTrF1flys4AKI3i09nXUwaA== X-MS-Exchange-Transport-CrossTenantHeadersStamped: SYBPR01MB5551 X-MS-Exchange-UnifiedGroup-DisplayName: Categories mailing list X-MS-Exchange-UnifiedGroup-Address: categories@mq.edu.au X-MS-Exchange-UnifiedGroup-MailboxGuid: 9c2f954e-92a7-451b-b723-a07075d7adb5 X-MS-Exchange-UnifiedGroup-CustomizedMessage: RedeemedBusinessGuests X-MS-Exchange-Parent-Message-Id: <9e1e9adda042d255754149546fb66527@cs.umu.se> Auto-Submitted: auto-generated X-MS-Exchange-Generated-Message-Source: Throttled Fork Delivery Agent X-MS-Exchange-AntiSpam-MessageData-ChunkCount: 1 X-MS-Exchange-AntiSpam-MessageData-0: =?utf-8?B?SzZORFp5dXdQYzh5S2VpZkQ3NXIwMXo3ZHFRWkZGN3RpOURXMTIvd0o5eHQx?= =?utf-8?B?dy9VeVFZb1NVWVc2OHMxRm5Bc3lOTmtoL0c3b1NOZXhIcW9JdGdScVNtakV4?= =?utf-8?B?cnZqVExtV05qMXA3U0ZrQ0VHRmk3ZXZkZGJsOXplOGU2VysrOEJoUjN1eGlX?= =?utf-8?B?a0YwZTMxUms2UWVpQ3JQdlBObHNjcVVKb3kwblpTUmdETFBpeWUwdURnUGhh?= =?utf-8?B?WUFnUVRoR3ZQUXBOWEVNUHJLUWtDamZpQzg1WFRNMm9ScjlvV05sZ3FvOHE1?= =?utf-8?B?QThGTG1SdFh2b0dZWXhBOHJlUjdBUVFFNm84K2dTNFV6SGRUMmV2T1h0OTJz?= =?utf-8?B?RElCY1pFZ0phaW9JMWNveS9ZSm1tR1V3M2llVm56ZmRDelpQNTR0MysvSnoy?= =?utf-8?B?V0RySG5ITUs0cmJXUGFLSFNtdDVBVFlHYTRRM3VjSHJZU1A4SEVsQm9FaU92?= =?utf-8?B?eDhHaW5Kc1M5NExKSjVCb044aWZtb0gwakhNMXFUcTVQelNaTnM5SXJ5UGUx?= =?utf-8?B?N2pFcXJkU3pnSkNoWHpFT0pDaHFaZEdlY1FxZTdCOW1WZVN2OGhQelhyOXVl?= =?utf-8?B?MTFSUmcya2hNR3g2RkdqWFdlNVI3d2pvRTYzeFJRVC9nUzB5ZXpWLzVjdUg0?= =?utf-8?B?UXFUcVhzdmszdDBNejliVS9qUkJ2QUtjOVBqeGtLQnJnaFhkV0tFVld4Rklp?= =?utf-8?B?YTZXbUE3QTJneGdGSVNIYUhDcnBIM3JqK1ZERWlrY1ZlVmIvYnJlU2JFeU13?= =?utf-8?B?RU5DQjZSdkc4VWxaNTcrL05yaVR1ZUxuNmNBdXJzdVRmM3pXOXZ0dk4veDV5?= =?utf-8?B?ei9nU3FZelBhbTRndVpVUXdQMVVRcjRuVVBlVmhmSW5pbXRuL1FzTmlYWUFZ?= =?utf-8?B?Mmxnbm1KaXEyOXloazRmQmFYeThKWlhWMmQ1bjF5M3RZNk1VZDEyeUVUemYv?= =?utf-8?B?LzdFTHJUTjlJUTRaVmZVRDg4Nm54V3cxVzhTZWdUQUh6R3Q3bEVySXpHQnk5?= =?utf-8?B?SWNiS05IVUVmc0lxRnlybWVDNklBakxGR1krSjNjZ2ZTRitwWjlPTUEyWVBx?= =?utf-8?B?dEM0eVd5aExGdE5rRlQ0emJpYnYzdFIvNmY3YzF4QmJOTEVGSmM2czFVZGtz?= =?utf-8?B?WVZOVzZzWlpHWnc5TjY1SmJicXhwcFc2RExyd1JWejErY1dibHhUa1ppQS9p?= =?utf-8?B?NERPQnlOWDhxcGpkaEJTOGxHcE40OW1ZbG1IcVJ2elovdFFyeHY3eXpXUEpJ?= =?utf-8?B?NHk2bnJ5MUJnWXhwaGVvMVc1eDJtdDhwVUxqenpQZmJVVjBCSEFVSVdUZ24w?= =?utf-8?B?WmNOR3FCUWFkRmFMbWhHaElndi9QODhNYnl3UlZoMVJJdkZQbnZmU3FXRDZp?= =?utf-8?B?ekhmdnVSOCtqRmVxcWlHRjNUVlcwZzhFaVBpNFNFUUlkbTJXZmUvNEk1c0dx?= =?utf-8?B?Sk8walpYeGtZc2h3ZlFva1g5NG44NkYyM0Y1MzhzZzdzTEkrdURwb2hOVmFT?= =?utf-8?B?cjlKazh6Q1BpRW9oeHozOUVTeXRmaGRmS3ZHRFRUbHdjdW8wYnNRc2lTZEI4?= =?utf-8?B?S2FZVEtDa0ZyQjc2ekVOQzlMUUpSWXNVTlVxRkJ4WUZTYlliVXNReFRhWFVR?= =?utf-8?B?Q3pwbmdjazRHNDRweENwcDI1MVZRelFMUDRHMnEvc0I0ZnpYclpNZU9WZnpr?= =?utf-8?B?Wng3MG5nQUlhMkxkam91WDd2U05sT2wwUFJudlEwNTVhWDg2c21lSWQwN1Vk?= =?utf-8?B?VVdsaFMyeUJKREQ4M2lac2I0RFZZNWZudVUrV1N1Z25GQWgvUUJ2SGxjWEx6?= =?utf-8?B?SzR0YU1Sbnl6NWt3NGxjQjgwYjcvOFAwTDkyQ0V4aVVYNGh3cUNzMTcwb3J4?= =?utf-8?B?SzRhYmkxTzRRMjlnRFRybDU0cG1DQVNLWlZmODROeWRXN2ttVWFReFdyZGp5?= =?utf-8?B?RDJiVFR1THJ4TlpBTUxyeHB2N3Y5ZzZQek04QThoSExOblIzMGVMaE9XRjBo?= =?utf-8?B?cEhkcks4c2RRPT0=?= X-OriginatorOrg: mq.edu.au --=_aa5f59a9f66015554b4e0d04814fb6bb Content-Type: text/plain; charset="utf-8"; format=flowed Content-Transfer-Encoding: quoted-printable Hi Vaughan, I hesitate to say anything specifically about Goldbach's conjecture, but le= t me comment at least on "proof ... exists". The very basic, simple and first idea of "lativity" is that it was never go= od that symbolic logic was ``freed from its undue obsession with the forms = of ordinary algebra'', like Principia writes in its PREFACE, referring to P= eano having said that, but Peano never did say that. Peano did say "We shal= l generally write signs on a single line" (Lat. Signa plerumque in eadem li= nea scribemus), but he didn't say "For a monadic term and formula construct= ion, just go with a magma; don't care about multi-sortedness and universal = algebra, they won't do any good". I don't know who to blame, Russell or Whi= tehead, for fake reference to Peano, but I tend to choose Russell. He had s= truggled with substitution, and PM continued to struggle with substitution.= Everybody else did, over decades to come, until GdM II is printed and beyo= nd. If we say "a conjecture is true", what do we mean? Do we mean that the form= ula (sentence formed categorically from underlying terms, again formed cate= gorically, and based on signatures, whether denoted a la Benabou or not) is= true, where that 'true' is the boolean constant in the underlying signatur= e? Or do we mean that it is "true" that we can find a proof for that conjec= ture, i.e. "proof ... exists" is "true". Lativity would say that the latter= "true" is not the "true" we have as sorted in the signature. I've often commented that "P is true" and "|-P is true" cannot use the same= "true". PM struggled with this, GdM struggled with this. P is a formula, |= -P is not. There may be a proof for P, but it makes no sense saying there m= ay or may not be a proof for |-P. John Stuart Mill was very smart. He said = =E2=80=9Cnothing but a Proposition can be an object of proof=E2=80=9D. G=C3= =B6del thinks differently, as Bw and Bew are of the same type, kind of. It's good if formalization proceeds latively, from signature to term to sen= tence to entailment to proof rules to proofs ...", and even better if alway= s "closing the door behind you" so that nobody comes up with viewing a proo= f sequence as a constant operator in the starting point signature. I feel u= ncomfortable to speak of a "lative axiomatization", unless by "axiomatizati= on" we mean "from signature to term to sentence to entailment to proof rule= s to proofs", because then, by definition of lativity, axiomatization is la= tive. So, within syntax, we should keep things apart, and also, as far as borderl= ines are concerned, between object and meta. We shouldn't shift things in m= eta sometimes to be used objectively or vice versa. Numbers and numerals ar= e on different sides of that borderline. GdM writes about Nummern and Ziffe= rn, but does not really make that borderline explicit. And indeed, I'm sad = to say, GdM never tried out rigour concerning types. Neither did Grundz=C3= =BCge. And G=C3=B6del 1931 is extremely illative in these respect along the= whole progression of "from signature to term to sentence to entailment to = proof rules to proofs". On GdM, already at its starting point, in GdM I =C2=A71, GdM "departs even = further from such rigour by making a dubious statement basically saying tha= t a boolean predicate symbol complies with its arity but need not be bound = to respect any specific typing of its domain, as long as satisfiability of = a formula is invariant under a one-to-one mapping of one typing to another"= . I put that in quotation marks because I quote directly from drafting I pr= esently have on what I have called a "dialogue" between GdM II =C2=A7=C2=A7= 4-5 and G=C3=B6del 1931. I'm trying to use categorical terms constructions = and "categorically lative axiomatization" to explain why and where things g= o wrong. So, to your question "Would you then call the conjecture undecidable?", I a= m unable to provide an answer until I understand latively what is meant by = "conjecture" as related to formula or entailment or something else, and wha= t is understood as "decidable" as related to a more lative definition of "p= roof sequence" including all its ingredients. I don't think PM's, GdM's and= G=C3=B6del's notions of "decidability" are mutually isomorphic. Putting symbols one by one in sequence is "no good", not good at all. Russe= ll made a fake reference to Peano, and even if Russell would have said bein= g freed from the burden of algebra is something good without referring to P= eano, I would say Russell's approach is "no good". Foundations must be revisited. Foundations need category theory more than c= ategory theory needs foundations. I would invite everybody to think about t= he way foundations might be revisited using categorical constructions, and = thereby making logical constructions much more "lative" than they are in tr= aditional foundations of logic (and computing for that matter), and in part= icular for the reason to finally get rid of self-referentiality and malicio= us use of antinomies. Doing so will make discussions on answers to your que= stion, Vaughan, really interesting. That's my credo. Has been for a long time. Best, Patrik On 2024-02-08 08:20, Vaughan Pratt wrote: On Sun, Feb 4, 2024 at 11:30=E2=80=AFPM Patrik Eklund > wrote: [...] Not clear to me what David precisely means by "no new", but in our ca= se we have been used to say "logic must be lative" in the sense that "first= terms, then sentences from terms" and no new terms from that, and "then en= tailment constructions from sentences" so that no new sentences are constru= cted from entailment. Here is where logic mixes "true" and "provable", and = this is the very spot which allows G=C3=B6del to "prove" incompleteness usi= ng the Liar and Richard's technique. [...] Patrik, how does "lative" bear on Goldbach's conjecture in the event that i= t is true, and furthermore provably so in some consistent non-lative recurs= ively enumerable axiomatization of arithmetic, but for which it can be show= n that no proof of the conjecture exists in any lative axiomatization? Would you then call the conjecture undecidable? Vaughan Pratt You're receiving this message because you're a member of the Categories mai= ling list group from Macquarie University. To take part in this conversatio= n, reply all to this message. View group files | Leave group | = Learn more about Microsoft 365 Groups --=_aa5f59a9f66015554b4e0d04814fb6bb Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=UTF-8

Hi Vaughan,

I hesitate to say anything specifically about Goldbach's conjecture, but= let me comment at least on "proof ... exists".

The very basic, simple and first idea of "lativity" is that it= was never good that symbolic logic was ``freed from its undue obsession wi= th the forms of ordinary algebra'', like Principia writes in its PREFACE, r= eferring to Peano having said that, but Peano never did say that. Peano did say "We shall generally write signs on = a single line" (Lat. Signa plerumque in eadem linea scribemus), but he= didn't say "For a monadic term and formula construction, just go with= a magma; don't care about multi-sortedness and universal algebra, they won't do any good". I don't know who to blame= , Russell or Whitehead, for fake reference to Peano, but I tend to choose R= ussell. He had struggled with substitution, and PM continued to struggle wi= th substitution. Everybody else did, over decades to come, until GdM II is printed and beyond.

If we say "a conjecture is true", what do we mean? Do we mean = that the formula (sentence formed categorically from underlying terms, agai= n formed categorically, and based on signatures, whether denoted a la Benab= ou or not) is true, where that 'true' is the boolean constant in the underlying signature? Or do we mean that it is &qu= ot;true" that we can find a proof for that conjecture, i.e. "proo= f ... exists" is "true". Lativity would say that the latter = "true" is not the "true" we have as sorted in the signa= ture. 

I've often commented that "P is true" and "|-P is true&qu= ot; cannot use the same "true". PM struggled with this, GdM strug= gled with this. P is a formula, |-P is not. There may be a proof for P, but= it makes no sense saying there may or may not be a proof for |-P. John Stuart Mill was very smart. He said =E2=80=9Cnothing but a Propo= sition can be an object of proof=E2=80=9D. G=C3=B6del thinks differently, a= s Bw and Bew are of the same type, kind of.

It's good if formalization proceeds latively, from signature to term to = sentence to entailment to proof rules to proofs ...", and even better = if always "closing the door behind you" so that nobody comes up w= ith viewing a proof sequence as a constant operator in the starting point signature. I feel uncomfortable to speak of a "= lative axiomatization", unless by "axiomatization" we mean &= quot;from signature to term to sentence to entailment to proof rules to pro= ofs", because then, by definition of lativity, axiomatization is lative.

So, within syntax, we should keep things apart, and also, as far as bord= erlines are concerned, between object and meta. We shouldn't shift things i= n meta sometimes to be used objectively or vice versa. Numbers and numerals= are on different sides of that borderline. GdM writes about Nummern and Ziffern, but does not really make= that borderline explicit. And indeed, I'm sad to say, GdM never tried out = rigour concerning types. Neither did Grundz=C3=BCge. And G=C3=B6del 1931 is= extremely illative in these respect along the whole progression of "from signature to term to sentence to entai= lment to proof rules to proofs".

On GdM, already at its starting point, in GdM I =C2=A71, GdM "depar= ts even further from such rigour by making a dubious statement basically sa= ying that a boolean predicate symbol complies with its arity but need not b= e bound to respect any specific typing of its domain, as long as satisfiability of a formula is invariant under a on= e-to-one mapping of one typing to another". I put that in quotation ma= rks because I quote directly from drafting I presently have on what I have = called a "dialogue" between GdM II =C2=A7=C2=A74-5 and G=C3=B6del 1931. I'm trying to use categorical terms constructions and= "categorically lative axiomatization" to explain why and where t= hings go wrong.

So, to your question "Would you then call the conjecture undecidabl= e?", I am unable to provide an answer until I understand latively what= is meant by "conjecture" as related to formula or entailment or = something else, and what is understood as "decidable" as related to a more lative definition of "proof sequence" inclu= ding all its ingredients. I don't think PM's, GdM's and G=C3=B6del's notion= s of "decidability" are mutually isomorphic.

Putting symbols one by one in sequence is "no good", not good = at all. Russell made a fake reference to Peano, and even if Russell would h= ave said being freed from the burden of algebra is something good without r= eferring to Peano, I would say Russell's approach is "no good".

Foundations must be revisited. Foundations need category theory more tha= n category theory needs foundations. I would invite everybody to think abou= t the way foundations might be revisited using categorical constructions, a= nd thereby making logical constructions much more "lative" than they are in traditional foundations of l= ogic (and computing for that matter), and in particular for the reason to f= inally get rid of self-referentiality and malicious use of antinomies. Doin= g so will make discussions on answers to your question, Vaughan, really interesting.

That's my credo. Has been for a long time.

Best,

Patrik


On 2024-02-08 08:20, Vaughan Pratt wrote:

On Sun, Feb 4, 2= 024 at 11:30=E2=80=AFPM Patrik Eklund <peklund@cs.umu.se> wrote:

[...] Not clear to me what David precisely means by "no new", but in our case we have been used to say "logic must be la= tive" in the sense that "first terms, then sentences from terms&q= uot; and no new terms from that, and "then entailment constructions fr= om sentences" so that no new sentences are constructed from entailment= . Here is where logic mixes "true" and "provable", and t= his is the very spot which allows G=C3=B6del to "prove" incomplet= eness using the Liar and Richard's technique. [...]

 
Patrik, how does= "lative" bear on Goldbach's conjecture in the event that it is t= rue, and furthermore provably so in some consistent non-lative recursively = enumerable axiomatization of arithmetic, but for which it can be shown that no proof of the conjecture exists in any lative= axiomatization?
 
Would you then c= all the conjecture undecidable?
 
Vaughan Pratt
 
 
 
 
 
 
 
You're receiving this message because you're a member of the Categories mai= ling list group from Macquarie University. To take part in this conversatio= n, reply all to this message.
 
View group files   |   Leav= e group   |&n= bsp;  Learn more about Microsoft 365 Groups
 
--=_aa5f59a9f66015554b4e0d04814fb6bb--