Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]


Groups > sci.physics > #887905

Re: An Ode to Dan Christensen: The Curry's Paradox in Fitch Style

From Mild Shock <janburse@fastmail.fm>
Newsgroups sci.physics
Subject Re: An Ode to Dan Christensen: The Curry's Paradox in Fitch Style
Date 2024-06-05 08:57 +0200
Message-ID <v3p27v$17co2$3@solani.org> (permalink)
References <v3p1ir$17ca8$1@solani.org>

Show all headers | View raw


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

Back to sci.physics | Previous | NextPrevious in thread | Next in thread | Find similar


Thread

An Ode to Dan Christensen: The Curry's Paradox in Fitch Style Mild Shock <janburse@fastmail.fm> - 2024-06-05 08:45 +0200
  Re: An Ode to Dan Christensen: The Curry's Paradox in Fitch Style Mild Shock <janburse@fastmail.fm> - 2024-06-05 08:57 +0200
    Re: An Ode to Dan Christensen: The Curry's Paradox in Fitch Style Mild Shock <janburse@fastmail.fm> - 2024-06-06 23:29 +0200

csiph-web