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

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