I did not say that becoming pretty is easy. 
There are errors on your website:
Error: File not created or not accessible.
user at 2
Error: Right parenthesis (“)”) missing.
user at 3
Error: Right parenthesis (“)”) missing.
user at 4
It works now.
@j4n_bur53 , unfortunately, there is a bug in your program:
show((![X]:f(X) => ![Y]:g(Y)) => (?[X]: ![Y]: (f(X) => g(Y)))).
\begin{prooftree}\AxiomC{}
\RightLabel{Ax}\UnaryInfC{
ERROR: Domain error: `variable_name' expected, found `'[''
ERROR: In:
ERROR: [20] write_term(f(a),[variable_names(...)])
ERROR: [19] render_list([f(...)],['X'=_842,...|...])
Probably easy to fix for you, but too difficult for me. 
joseph@mx:~$ swipl --version
SWI-Prolog version 9.0.4 for x86_64-linux
With risk of adding errors…
portray_clause/1 for the proof of this theorem via leanseq.pl :
?- decide((![X]: f(X) => ![Y]: g(Y)) => (?[X]: ![Y]: (f(X) => g(Y)))).
% 866 inferences, 0.000 CPU in 0.000 seconds (99% CPU, 4402867 Lips)
P_Proof: r_to([]>[((![A]:f(A)=>![B]:g(B))=> ?[A]:![B]:(f(A)=>g(B)))],
l_to([(![A]:f(A)=>![B]:g(B))]>[?[A]:![B]:(f(A)=>g(B))],
r_forall([]>[![A]:f(A), ?[A]:![B]:(f(A)=>g(B))],
r_exists([]>[f(f_sk(1, [])), ?[A]:![B]:(f(A)=>g(B))],
r_forall([]>[![C]:(f(f_sk(1, []))=>g(C)), f(f_sk(1, [])), ?[A]:![B]:(f(A)=>g(B))],
r_to([]>[(f(f_sk(1, []))=>g(f_sk(2, [f_sk(1, [])]))), f(f_sk(1, [])), ?[A]:![B]:(f(A)=>g(B))],
ax([f(f_sk(1, []))]>[g(f_sk(2, [f_sk(1, [])])), f(f_sk(1, [])), ?[A]:![B]:(f(A)=>g(B))],
ax))))),
r_exists([![B]:g(B)]>[?[A]:![B]:(f(A)=>g(B))],
r_forall([![B]:g(B)]>[![D]:(f(E)=>g(D)), ?[A]:![B]:(f(A)=>g(B))],
r_to([![B]:g(B)]>[(f(E)=>g(f_sk(3, [E]))), ?[A]:![B]:(f(A)=>g(B))],
l_forall([f(E), ![B]:g(B)]>[g(f_sk(3, [E])), ?[A]:![B]:(f(A)=>g(B))],
ax([g(f_sk(3, [E])), f(E), ![B]:g(B)]>[g(f_sk(3, [E])), ?[A]:![B]:(f(A)=>g(B))],
ax))))))).
@j4n_bur53 , thanks. To compare with the output of Naoyuki’s prover:
cl(first)> X@f(X) -> Y@g(Y) --> X#Y@(f(X) -> g(Y)).
_10282@f(_10282)->_10292@g(_10292)-->_10282#_10292@(f(_10282)->g(_10292)).
Trying to prove with threshold = 0 1 2
Succeed in proving _19520@f(_19520)->_19394@g(_19394) --> _19520#_19394@(f(_19520)->g(_19394)) (36 msec.)
pretty:1 =
------------------------------------ Ax --------------------------------------------- Ax
f(Z) --> f(Z),g(X1),X#Y@(f(X)->g(Y)) f(Y1),g(Z1),Y@g(Y) --> g(Z1),X#Y@(f(X)->g(Y))
-------------------------------------- R-> --------------------------------------------- L@
--> f(Z),f(Z)->g(X1),X#Y@(f(X)->g(Y)) f(Y1),Y@g(Y) --> g(Z1),X#Y@(f(X)->g(Y))
----------------------------------------- R@ ---------------------------------------- R->
--> f(Z),Y@(f(Z)->g(Y)),X#Y@(f(X)->g(Y)) Y@g(Y) --> f(Y1)->g(Z1),X#Y@(f(X)->g(Y))
----------------------------------------- R# ------------------------------------------- R@
--> f(Z),X#Y@(f(X)->g(Y)) Y@g(Y) --> Y@(f(Y1)->g(Y)),X#Y@(f(X)->g(Y))
---------------------------- R@ ------------------------------------------- R#
--> X@f(X),X#Y@(f(X)->g(Y)) Y@g(Y) --> X#Y@(f(X)->g(Y))
--------------------------------------------------------------------------- L->
X@f(X)->Y@g(Y) --> X#Y@(f(X)->g(Y))
yes
cl(first)>
Your correction works with my file and my system. Thanks. 
More seriously, I note that the proof with erasure shows on the right of the turnstile the proof of the theorem in Fitch style , i.e.
- | | Da :AS
- | | EyDy :EI1
- | Da → EyDy :->I1-2
- | Ax(Dx → EyDy) :AI3
The heart button looks a little bit stoopid…it is also very limiting that it is the only option available…just saying…these guys at discourse must be politically correct gurus…it is all the more contradictory that one should place hearts on posts of strangers…but of course we are nothing but one big family (and not dysfunctional I hope…) 
This document is very useful: http://www.actual.world/resources/tex/doc/Proofs.pdf
My favorite LaTeX macros for proofs in Fitch style Klüwer’s in the version given by Alexander W. Kocurek, June 8, 2019:
% $Id: fitch.sty,v 1.6 2003/06/28 16:53:00 johanw Exp $
% Macros for Fitch-style formal proofs
% Johan W. Klüwer, June 10, 2001
% EDITS (Alexander W. Kocurek, June 8, 2019)
% %\RequirePackage{mdwtab,latexsym,amsmath,amsfonts,ifthen}
% - too many fonts were loading
% - removed mdwtab, which redefines tabular, causing several conflicts such as overriding color in tabular cells and redefining \hline so that \hline without arguments no longer works
% ADDED (March 28, 2022)
% - added more flexibility for horizontal spacing
% - - \fitchsep controls separation between vertical lines
% - - \fitchnumsep controls separation between numbers and vertical lines
\RequirePackage{mathtools,amsmath,ifthen,array}
% Line height in proofs
\newlength{\fitchlineht}
\setlength{\fitchlineht}{1.5\baselineskip}
% Horizontal indent between proof levels
\newlength{\fitchindent}
\setlength{\fitchindent}{0.7em}
% Indent to comment
\newlength{\fitchcomind}
\setlength{\fitchcomind}{2em}
% Line number width
\newlength{\fitchnumwd}
\setlength{\fitchnumwd}{1em}
% Horizontal space between vertical lines (AK added)
\newlength{\fitchsep}
\setlength{\fitchsep}{\fitchindent}
% Horizontal space between numbers and vertical lines (AK added)
\newlength{\fitchnumsep}
\setlength{\fitchnumsep}{\fitchindent}
% Altered from mdwtab.sty: shorter vline, for start of subproof
\makeatletter
\newcommand\fvline[1][\arrayrulewidth]{\vrule\@height.5\fitchlineht\@width#1\relax}
\makeatother
% Ordinary vertical line
\newcommand{\fa}{\hspace*{\fitchsep}\vline\hspace*{\fitchindent}}
% Vertical line, shorter: Use at start of (sub)proof
\newcommand{\fb}{\hspace*{\fitchsep}\fvline\hspace*{\fitchindent}}
% Hypothesis
\newcommand{\fh}{\hspace*{\fitchsep}\fvline%
\makebox[0pt][l]{{%
\raisebox{-1.4ex}[0pt][0pt]{\rule{1.5em}{\arrayrulewidth}}}}%
\hspace*{\fitchindent}}
% Hypothesis, with longer vert line: for >1 hypothesis
\newcommand{\fj}{\hspace*{\fitchsep}\vline%
\makebox[0pt][l]{{%
\raisebox{-1.4ex}[0pt][0pt]{\rule{1.5em}{\arrayrulewidth}}}}%
\hspace*{\fitchindent}}
% Modal subproof: takes argument = operator
\newcommand{\fitchmodal}[1]{%
\hspace*{\fitchsep}\makebox[0pt][r]{${}^{#1}$\,}\fvline\hspace*{\fitchindent}}
\newcommand{\fn}{\fitchmodal{\Box}}% Box subproof
\newcommand{\fp}{\fitchmodal{\Diamond}}% Diamond subproof
% Modal subproof with hypothesis in first line (as in Fitch)
\newcommand{\fitchmodalh}[1]{%
\hspace*{\fitchsep}\makebox[0pt][r]{${}^{\footnotesize #1}$\,}%
\fvline%
\makebox[0pt][l]{{%
\raisebox{-1.4ex}[0pt][0pt]{\rule{1.5em}{\arrayrulewidth}}}}%
\hspace*{\fitchindent}}
\newcommand{\fm}{\fitchmodalh{\Box}}% Box subproof with hypothesis
\newcommand{\fq}{\fitchmodalh{\Diamond}}% Diamond subproof with hypothesis
% Rule: formula introduction marker. \fr with line, \fs without line
\newcommand{\fr}{%
\hspace*{\fitchsep}\makebox[0pt][r]{${\rhd}$\,\,}\vline\hspace*{\fitchindent}}
\newcommand{\fs}{%
\hspace*{\fitchsep}\makebox[0pt][r]{${\rhd}$\,\,}}
% Box around argument, like new variable in ql
\newcommand{\fw}[1]{\fbox{\footnotesize $#1$}}
%
\newcounter{fitchcounter}
\setcounter{fitchcounter}{0}
%To avoid starting from 1, \setboolean{resetfitchcounter}{false}
\newboolean{resetfitchcounter}
\setboolean{resetfitchcounter}{true}
%To avoid increasing numbers, \setboolean{increasefitchcounter}{false}
\newboolean{increasefitchcounter}
\setboolean{increasefitchcounter}{true}
%\formatfitchcounter can be altered if need be, though only once per proof
\newcommand{\formatfitchcounter}[1]{\scriptsize \arabic{#1}}
%Typeset the counter
\newcommand{\fitchcounter}{%
\ifthenelse{\boolean{increasefitchcounter}}{\addtocounter{fitchcounter}{1}}{}
\formatfitchcounter{fitchcounter}}
%A line with a special number -- a tag, e.g. \ftag{\vdots}{}
\newcommand{\ftag}[2]{\multicolumn{1}%
{!{\makebox[\fitchnumwd][r]{\footnotesize $#1$}\hspace{\fitchindent}}>{$}l<{$}@{\hspace{\fitchcomind}}}%
{#2}} % AK put the tag in math mode by default
% Main environments
% AK modified the next two environments by replacing Ml (which is supposed to force math mode, left aligned in mdwtab) with >{$}l<{$}, which has the same effect in tabular
\newenvironment{fitchnum}%
{\ifthenelse{\boolean{resetfitchcounter}}{\setcounter{fitchcounter}{0}}{}
\begin{tabular}{!{\makebox[\fitchnumwd][r]{\fitchcounter}\hspace{\fitchnumsep-\fitchsep}}>{$}l<{$}@{\hspace{\fitchcomind}}l}}%
{\end{tabular}}
\newenvironment{fitchunum}%
{\begin{tabular}{!{\makebox[\fitchnumwd][r]{}\hspace{\fitchnumsep-\fitchsep}}>{$}l<{$}@{\hspace{\fitchcomind}}l}}%
{\end{tabular}}
\newenvironment{fitch}{\renewcommand{\arraystretch}{1.5}
\begin{fitchnum}}{\end{fitchnum}}
\newenvironment{fitch*}{\renewcommand{\arraystretch}{1.5}
\begin{fitchunum}}{\end{fitchunum}}
% The following is useful for giving a numbered formula, then the proof.
\newenvironment{flem}[2]%
{\begin{eqnarray}
\label{#2}\\
&\begin{fitch}}%
{\end{fitch}\notag\end{eqnarray}}
%To write comment field for two consecutive lines, with brace
\newcommand{\ftwocom}[1]{%
\parbox[t]{3cm}{
\raisebox{-.6\baselineskip}[\baselineskip][0pt]{%
$\left.
\begin{aligned}
\,\\ \,
\end{aligned}
\right\}$\quad #1}
}}
Nothing in MathJax3 for Fitch style, unfortunately (and I am unable to fix this).
Last, this pedagogical website is wonderful : https://carnap.io/ and it is mainly based on Fitch style,
1 Like
Yes, it contains proof checkers (in Haskell). https://carnap.io/ is a website to teaching logic: you can submit exercises to students, and they can improve their skills online: the background of the formula to prove is green when the proof is finished and is correct, via a “check” option. For exams, this option can be removed, and grades are automatically given by the website. A wonderful tool that good students appreciate a lot.
1 Like
Have a look on Slaney’s prover :
https://vidal-rosset.net/john_slaneys_prover_for_minimal_and_intuitionistic_propositional_logic.html
Yes. The Axiom comes sooner. That is the main difference with Naoyuki’s classical prover:
------- Ax
p --> p
----------- Rbot
p --> bot,p
------------- R-> --------- Lbot
--> p->bot,p bot --> p
---------------------------- L->
(p->bot)->bot --> p
----------------------- R->
--> ((p->bot)->bot)->p
-------------------------- Ltop
top --> ((p->bot)->bot)->p
And the proof of Peirce Law is :
Sequent Calculus Prover ver 2.0 in Prolog
by Naoyuki Tamura (tamura@kobe-u.ac.jp)
cl(first)> (p -> q) -> p --> p .
(p->q)->p-->p.
Trying to prove with threshold = 0
Succeed in proving (p->q)->p --> p (0 msec.)
pretty:1 =
--------- Ax
p --> q,p
----------- R-> ------- Ax
--> p->q,p p --> p
------------------------ L->
(p->q)->p --> p
yes
It’s based on a stronger law that is Excluded Middle. Note that the step
--> p->q,p
could be
--> p -> bot, p
i.e.
--> ~ p \/ p
LEM is not even derivable from RAA in intuitionistic logic.
Proof via provers.
- RAA is the classical double negation elimination rule that allows the derivation of the conditional in the following proof given by Michel Levy’s Prover :
1 assume --A.
2 A. Raa 1
3 therefore --A => A. =>I 1,2
- It is provable via fCube that LEM is not derivable from RAA:
true
Input Formula:
F ((~~a => a) => (~a | a))
Sign Permanence tried,input formula equivalent to:
F ((~~a => a) => (~a | a));
F->,Main SWFF: F ((~~a => a) => (a | ~a))
T (~~a => a);
F (a | ~a);
Main SWFF: F (a | ~a)
F a;
F ~a;
T (~~a => a);
F non,Main SWFF: F ~a
T a;
Found a backtacking point:
F ~a;
T (~~a => a);
F a;
Right branch of T->not,Main SWFF: T (~~a => a)
T a;
F 1;
Left branch of T->not,Main SWFF: T (~~a => a)
FC a;
1 search result = unprovable (fCube-4.1)
*** The Counter Model (see also the prolog term ) ***
-- root --
-- end world --
F a;
-- end world --
T a;
-- end world --
FC a;
-- end world --
*** Prolog term of the countermodel ***
[[swff(F,a),[swff(T,a)],[swff(FC,a)]]]
631.0 msec.
Our discussion is about logic and not about Prolog. I apologize.
RAA is a classical rule but it can be taken as assumption. LEM cannot be intuitionistically deduced from RAA as assumption. The conclusion of your proof is valid in classical logic, not in intutionistic logic. Therefore it is a fortiori false that LEM is derivable from RAA in minimal logic, because it is even false in intuitionistic logic.
von Plato : “A rule is derivable in a given system of rules it its conclusion is derivable from its premisses in the system”. (Def. 3.4. Elements of logical reasoning)
The proof to which you refer is a proof in classical logic, RAA and LEM being both classical laws, their mutual “derivation” is trivial, because both are on the right of the turnstile while the left of the same turnstile is empty. Again, as soon as you add RAA to minimal logic you get classical logic, just because EFQ is derivable from RAA. It is easier for me to understand this point than to understand how works the lambda-calculus.
Las, in this document about Interpretations of Classical Logic Using λ-calculus, Freddie Agestam wrote, p. 39
Another interesting proposition is that RAA implies the Principle of Ex-
cluded Middle (PEM). Neither RAA nor PEM are derivable in intuitionistic
logic, but when we add the derivation rule double negation elimination (RAA)
to natural deduction and get classical logic, both are derivable. Nonetheless,
“RAA → PEM” is not derivable in intuitionistic logic. This is initially quite
confusing, which is what makes this proposition interesting.
The reason that there is a difference between adding a derivation rule RAA
and showing an implication from RAA, is that the derivation rule really looks
like ∀P.(¬¬P → P ). That is, we may eliminate double negations in any formula,
while the implication from RAA only allows us to eliminate double negations
in front of P . As we see in the inhabitant below, we eliminate double negation
not in front of P , but in front of P ∨ ¬P .
This point is explained much more clearly by von Plato (p. 83 of Elements of Logical Reasoning):
There is thus a difference between the assumption A and the assumption
that A is derivable that can be expressed by:
When we assume A, we assume that there is a hypothetical derivation of A.
When we assume |- A, we assume that there is an actual derivation of A.
The explanation of A ⊃ B in terms of proof was that by a proof of A ⊃ B ,
any proof of A can be turned into some proof of B. With |- A, instead, it is
claimed that there is some proof of A.
When A is assumed, it must be possible to compose a derivation of A
and any derivation from the assumption A. This matter is discussed further
in Section 13.4.
Classical logic is in many ways simpler than intuitionistic logic, because
it does not make the distinction between a proposition and its double nega-
tion. We show, as further examples of classical derivations, that implication
and falsity suffice for defining the rest of the connectives.
End of quotation. Taking again this excellent book, I just realized that it contains a section about lambda-calculus and natural deduction. I am going to study it.
A widespread prejudice which seems to pop up annoyingly often on tik tok as well 
I’m quite messy. If I weren’t, possibly I would have never stumbled in Prolog (which I don’t claim to be neither a positive nor a negative thing…). But of course it might get difficult to discuss with someone like you who is constantly deleting his posts. Good evening