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

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