Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  newsreader  groups  login

Message-ID:  

Gee, Toto, I don't think we're in Kansas anymore.


tech / sci.math / Re: North America after the Civil War 2020

SubjectAuthor
o Re: North America after the Civil War 2020Mostowski Collapse

1
Re: North America after the Civil War 2020

<6d2cb799-855e-4e1a-a7ab-8a00b77bc28cn@googlegroups.com>

  copy mid

https://www.novabbs.com/tech/article-flat.php?id=126712&group=sci.math#126712

  copy link   Newsgroups: sci.math
X-Received: by 2002:ac8:5909:0:b0:3b1:c62b:c140 with SMTP id 9-20020ac85909000000b003b1c62bc140mr1316620qty.313.1675882814654;
Wed, 08 Feb 2023 11:00:14 -0800 (PST)
X-Received: by 2002:aca:42c5:0:b0:378:9fb5:3fbc with SMTP id
p188-20020aca42c5000000b003789fb53fbcmr232864oia.152.1675882814198; Wed, 08
Feb 2023 11:00:14 -0800 (PST)
Path: i2pn2.org!i2pn.org!usenet.blueworldhosting.com!feed1.usenet.blueworldhosting.com!peer01.iad!feed-me.highwinds-media.com!news.highwinds-media.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: sci.math
Date: Wed, 8 Feb 2023 11:00:13 -0800 (PST)
In-Reply-To: <84b6a534-96fa-4082-b8a0-186a4ae63d5an@googlegroups.com>
Injection-Info: google-groups.googlegroups.com; posting-host=77.57.53.44; posting-account=UjEXBwoAAAAOk5fiB8WdHvZddFg9nJ9r
NNTP-Posting-Host: 77.57.53.44
References: <b1b09a88-c226-4666-89e7-726e548ad5ben@googlegroups.com>
<80e7b981-e4a3-452f-a185-fff66577cde5n@googlegroups.com> <4e6e15fe-114c-48f8-a8de-b6de616f2081n@googlegroups.com>
<f31716e6-45c7-4a0b-a287-217385bec461n@googlegroups.com> <rq88um$1i3h$1@gioia.aioe.org>
<1314ae21-7d35-497d-bf85-fa2068d54099n@googlegroups.com> <rqdird$10v4$1@gioia.aioe.org>
<241343d4-2c0c-49bc-a97b-40675b1613a9n@googlegroups.com> <8e1c09f2-9f8c-4783-9c72-309de301412dn@googlegroups.com>
<rqorp4$ia7$1@gioia.aioe.org> <9b3c67c3-8e70-4a5b-8b8c-97cb49a829f0n@googlegroups.com>
<f19a1726-d15f-4e55-b15b-dccff8715da5n@googlegroups.com> <373286cd-a5cc-4aa3-8a63-68df18211cd6n@googlegroups.com>
<91129e3a-08d6-4010-9b88-e5bc2a883723n@googlegroups.com> <a1d2827e-990b-4261-859f-6f169f341a0en@googlegroups.com>
<3f267649-1de3-4135-a8ee-21c44c571330n@googlegroups.com> <2099295f-e1d4-41f2-9d7b-7f81b246ed27n@googlegroups.com>
<0cb27cdf-fdfd-4232-863e-70dbbcfc7782n@googlegroups.com> <s26hta$c5j$1@gioia.aioe.org>
<559c0388-e00a-459a-a084-8c1023713d05n@googlegroups.com> <b39be52e-cbbd-4f1b-b6e6-a39dbed70149n@googlegroups.com>
<88a8bda9-904f-4626-a681-000802e4a4e1n@googlegroups.com> <e03755bd-f076-4ad7-a1ef-c522d3ddceafn@googlegroups.com>
<26a5b38b-9b34-41cc-9594-1902b43423acn@googlegroups.com> <5a6ab4e0-a288-4c6d-9dd6-52cab167b3cen@googlegroups.com>
<84b6a534-96fa-4082-b8a0-186a4ae63d5an@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <6d2cb799-855e-4e1a-a7ab-8a00b77bc28cn@googlegroups.com>
Subject: Re: North America after the Civil War 2020
From: burse...@gmail.com (Mostowski Collapse)
Injection-Date: Wed, 08 Feb 2023 19:00:14 +0000
Content-Type: text/plain; charset="UTF-8"
X-Received-Bytes: 4424
 by: Mostowski Collapse - Wed, 8 Feb 2023 19:00 UTC

Hi,

Well if these formulas are all
intuitionistically valid:

A & B => [A => B]
A & ~B => ~[A => B]
~A => [A => B]

Then it begs the question, what did you verify?
Did you verify THE truth table, or something else?
How can you verify THE truth table,

if you only make positive demonstrations? You
only demonstrate that your logic shows something,
such a demonstration has a blind spot.

The truth table also expresses what is not,
and a truth table is used in evaluating formulas,
not only single standing.

Usually in logic one doesn't proof truth tables.
This would only show that your calculus is
sound. But is it also complete?

Bye

P.S.: The above formulas are all intuitionistically
valid. So how do you know that your prover is classical
logic, if at all, and not intuitionistic logic?

----------- Ax
a,a,b --> b
------------ R->
a,b --> a->b
------------- L/\
a/\b --> a->b

--------------- Ax
a,bot,b --> bot
------------------ L0->1
a,b,b->bot --> bot
--------------------- L0->1
a->b,a,b->bot --> bot
--------------------- R~
a,b->bot --> ~ (a->b)
--------------------- L~def
a,~b --> ~ (a->b)
------------------- L/\
a/\ ~b --> ~ (a->b)

----------- Lbot
bot,a --> b
-------------- L0->1
a,a->bot --> b
--------------- R->
a->bot --> a->b
--------------- L~def
~a --> a->b

https://www.vidal-rosset.net/g4-prover/

Dan Christensen schrieb am Mittwoch, 8. Februar 2023 um 15:55:07 UTC+1:
> See my reply just now to your identical posting at sci.logic
>
> Dan
>
> On Wednesday, February 8, 2023 at 3:31:00 AM UTC-5, Mostowski Collapse wrote:
> > I am currently trying to dig up a little Pelletier writing.
> > The idea "direct implication" could be well deserved.
> > For example Dan Christensen has this inference rule:
> >
> > Proof By Contradiction (Introducing ~):
> > https://dcproof.wordpress.com/2017/12/28/if-pigs-could-fly/
> >
> [snip]

1
server_pubkey.txt

rocksolid light 0.9.81
clearnet tor