Path: ...!news.mixmin.net!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail
From: Mild Shock <janburse@fastmail.fm>
Newsgroups: sci.math
Subject: Re: An Ode to Dan Christensen: The Curry's Paradox in Fitch Style
Date: Wed, 5 Jun 2024 08:56:29 +0200
Message-ID: <v3p26t$17co2$2@solani.org>
References: <v3p1kf$17ca8$2@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Wed, 5 Jun 2024 06:56:29 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="1291010"; mail-complaints-to="abuse@news.solani.org"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
 Firefox/91.0 SeaMonkey/2.53.18.2
Cancel-Lock: sha1:8Bn8ouEiBZkYE7eXY71EQoHzav4=
In-Reply-To: <v3p1kf$17ca8$2@solani.org>
X-User-ID: eJwFwYEBwDAEBMCVivxjHCT2H6F3MArHD8GDxVYvg43gwzFTV9MsWZsQ5rzEmt6X6rG+EFTPvLl5bb6a/gFHwRYE
Bytes: 2608
Lines: 43

Dan Christensen was my long term sparring
partner on sci.logic, but he somehow disappeared.
He had a proof tool, that implemented some sort

of free logic, and was heavily defending his tool,
and calling other tools that implemented the more
traditional non-free first order logic nonsense.

The last he posted on sci.logic was a solution
to the Russell paradox, where he got into multivalued
logic. But in a very stubborn way, and he didn't

accept again, that each resolution of the Russell
paradox, provokes a new kind of Russell paradox.
This was actually quite interesting

Mild Shock schrieb:
> We present a little tour de force in implementing
> a Prolog technology theorem prover for intuitionistic
> propositional and first order logic. The main idea
> was already demonstrated by John Slaney in
> his MINLOG System.
> 
> Instead of transforming a proof from NJ to LJ as in
> cut elimination, we transform a proof back from LJ
> to NJ. What helps us doing this transformation is
> extracting and rendering proof terms from
> the Curry-Howard isomorphism.
> 
> Drawing upon Jens Ottens ileanSeP and leanSeq we
> deviced propositional and first order proof search
> for LJ. We can render Fitch Style proofs of Curry's
> Paradox and the propositionally resembling Barber
> Paradox, whereby our logic assumes at least one
> Barber. Both are intuitionistically valid.
> 
> See also:
> 
> The Curry's Paradox in Fitch Style
> https://twitter.com/dogelogch/status/1798242629152637208
> 
> The Curry's Paradox in Fitch Style
> https://www.facebook.com/groups/dogelog