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

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

Show all headers | View raw

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 | Next — 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