Can I use fitch.sty by Johan Klüwer in MathJax?

[Jean-Luc-Picard-2021]

Is your feature request related to a problem? Please describe.
Can I use fitch.sty by Johan Klüwer in MathJax?
https://www.actual.world/resources/tex/sty/kluwer/edited/fitch.sty

Describe the solution you'd like
It would be swell if fitch.sty could be used just like bussproofs.
bussproofs are on the extension list:
https://docs.mathjax.org/en/latest/input/tex/extensions/bussproofs.html
But I didn't find fitch.sty by Johan Klüwer.

Describe alternatives you've considered
Jump from a bridge.

Additional context
Screenshots of the results from rendering mathematical proofs with
fitch.sty are for example found in this document:
Proofs in LaTeX, Alexander W. Kocurek, June 8, 2019 (version 3)
https://www.actual.world/resources/tex/doc/Proofs.pdf

[dpvc]

We do not have an implementation of the fitch package for MathJax. It doesn't look like it would be too hard to do, but our resources are currently going toward getting the official v4 released (it is now in beta release). There are several other projects that are scheduled after that, so any work on this would be a ways down to road. It is something that a third-party programmer would be able to, however, so perhaps someone in the MathJax community may want to take that one. You might try posting to the MathJax user's forum or the developer's forum to see if there are any takers.

This is a diplicate of #2289.

[Jean-Luc-Picard-2021]

Not sure whether its really a duplicate. Since
the other ticket asks for a different package adopted.

These are two different packages:

by Johan Klüwer (asked here)
https://www.actual.world/resources/tex/sty/kluwer/edited/fitch.sty

by Peter Selinger (asked there)
https://www.mathstat.dal.ca/~selinger/fitch/

Klüwer fitch.sty could be easier maybe? Don't know what Selinger is
using. Had a look at Klüwer, it seems it uses texmacros I. I already found
texmacros as a package for MathJax. But tabular and length def

macros are also used, I guess these are missing in MathJax.

[dpvc]

You are right, sorry. I didn't recognize the difference.

the conversion to MathJax would not be a direct translation of the original LaTeX code, but a new js version that produces the MathJax internal format (basically MathML), so things like tabular and length macros would not be used.

[hebozhe]

I've got a prototype in the raw that works for both LaTex and MathJax, but it's not a standard by any stretch.

Here's a sample proof in it:

$$ \begin{array}{|ll|r} ~1. & \forall x (Kx \vee Nx) & Ax.1 \\ ~2. & \forall x(\forall \phi (Sx«\phi» \rightarrow \phi) \leftrightarrow Kx) & Ax.2 \\ ~3. & \forall x(\forall \phi(Sx«\phi» \rightarrow \neg \phi) \leftrightarrow Nx) & Ax.3 \\ \hline & \begin{array}{|~ll|r} 4. & \boxed a & SM \forall I \\ \hline 5. & Ka \vee Na & \forall E, 1 \\ 6. & \forall \phi (Sa«\phi» \rightarrow \phi) \leftrightarrow Ka & \forall E, 2 \\ 7. & \forall \phi(Sa«\phi» \rightarrow \neg \phi) \leftrightarrow Na & \forall E, 3 \\ 8. & Ka \rightarrow \forall \phi (Sa«\phi» \rightarrow \phi) & \leftrightarrow E, 6 \\ 9. & Na \rightarrow \forall \phi (Sa«\phi» \rightarrow \neg \phi) & \leftrightarrow E, 7 \\ & \begin{array}{|~ll|r} 10. & Sa«Na» & SM \neg I \\ \hline & \begin{array}{|~ll|r} 11. & Ka & SM \neg I \\ \hline 12. & \forall \phi (Sa«\phi» \rightarrow \phi) & \rightarrow E, 8, 11 \\ 13. & Sa«Na» \rightarrow Na & \forall E, 12 \\ 14. & Na & \rightarrow E, 13, 10 \\ 15. & \forall \phi (Sa«\phi» \rightarrow \neg \phi) & \rightarrow E, 9, 14 \\ 16. & Sa«Na» \rightarrow \neg Na & \forall E, 15 \\ 17. & \neg Na & \rightarrow E, 16, 10 \\ 18. & \bot & \bot I, 14, 17 \\ \end{array} & & \\ 19. & \neg Ka & \neg I, 11 - 18 \\ 20. & Na & DS, 5, 19 \\ 21. & \forall \phi (Sa«\phi» \rightarrow \neg \phi) & \rightarrow E, 9, 20 \\ 22. & Sa«Na» \rightarrow \neg Na & \forall E, 21 \\ 23. & \neg Na & \rightarrow E, 22, 10 \\ 24. & \bot & \bot I, 20, 23 \\ \end{array} & & \\ 25. & \neg Sa«Na» & \neg I, 10 - 24 \\ \end{array} & & \\ 26. & \forall x \neg Sx«Nx» & \forall I, 4 - 25 \\ \end{array} $$

And here's the code:

$$
\begin{array}{|ll|r}
~1. & \forall x (Kx \vee Nx) & Ax.1 \\
~2. & \forall x(\forall \phi (Sx«\phi» \rightarrow \phi) \leftrightarrow Kx) & Ax.2 \\
~3. & \forall x(\forall \phi(Sx«\phi» \rightarrow \neg \phi) \leftrightarrow Nx) & Ax.3 \\
\hline
&
\begin{array}{|~ll|r}
4. & \boxed a & SM \forall I \\
\hline
5. & Ka \vee Na & \forall E, 1 \\
6. & \forall \phi (Sa«\phi» \rightarrow \phi) \leftrightarrow Ka & \forall E, 2 \\
7. & \forall \phi(Sa«\phi» \rightarrow \neg \phi) \leftrightarrow Na & \forall E, 3 \\
8. & Ka \rightarrow \forall \phi (Sa«\phi» \rightarrow \phi) & \leftrightarrow E, 6 \\
9. & Na \rightarrow \forall \phi (Sa«\phi» \rightarrow \neg \phi) & \leftrightarrow E, 7 \\
&
\begin{array}{|~ll|r}
10. & Sa«Na» & SM \neg I \\
\hline
&
\begin{array}{|~ll|r}
11. & Ka & SM \neg I \\
\hline
12. & \forall \phi (Sa«\phi» \rightarrow \phi) & \rightarrow E, 8, 11 \\
13. & Sa«Na» \rightarrow Na & \forall E, 12 \\
14. & Na & \rightarrow E, 13, 10 \\
15. & \forall \phi (Sa«\phi» \rightarrow \neg \phi) & \rightarrow E, 9, 14 \\
16. & Sa«Na» \rightarrow \neg Na & \forall E, 15 \\
17. & \neg Na & \rightarrow E, 16, 10 \\
18. & \bot & \bot I, 14, 17 \\
\end{array}
& & \\
19. & \neg Ka & \neg I, 11 - 18 \\
20. & Na & DS, 5, 19 \\
21. & \forall \phi (Sa«\phi» \rightarrow \neg \phi) & \rightarrow E, 9, 20 \\
22. & Sa«Na» \rightarrow \neg Na & \forall E, 21 \\
23. & \neg Na & \rightarrow E, 22, 10 \\
24. & \bot & \bot I, 20, 23 \\
\end{array}
& & \\
25. & \neg Sa«Na» & \neg I, 10 - 24 \\
\end{array}
& & \\
26. & \forall x \neg Sx«Nx» & \forall I, 4 - 25 \\
\end{array}
$$

[Hemki]

This is my current workaround (similar approach to the above and also not perfect by any means):

(Included as a picture because Github refuses to draw \hlineproperly)

Code:

\begin{matrix}
\begin{aligned} 1  \\[2pt] 2  \\[2pt] 3 \\[2pt] 4 \\[2pt] 5 \\[2pt] 6 \\\end{aligned}
\quad\begin{array}{|l}
   A \to B \\
   B \to C \\
   \hline
   \quad \left. \begin{array}{|l} A \\\hline B \\ C\end{array} \right. \\ 
   A\to C \\ 
\end{array} \qquad
\begin{aligned} \\[2pt] \\[2pt] \\[2pt] 
&(\to E)\space1,3 \\[2pt] 
&(\to E) \space 2,4 \\[2pt]
&(\to I)\space3\text{ - }5
\end{aligned}
\end{matrix}

or if you prefer using \newcommand for increased readability:

\newcommand{\fitch}[3]{\begin{matrix}\begin{aligned}#1\end{aligned}\quad\begin{array}{|l}#2\end{array}\qquad\begin{aligned}#3\end{aligned}\end{matrix}}
\newcommand{\subproof}[1]{\quad \left. \begin{array}{|l} #1 \end{array} \right. \\}
\newcommand{\num}[2]{#1 \\[#2]}
\newcommand{\rule}[3]{&(#1) \space #2 \\[#3]}
\newcommand{\skip}[1]{\\[#1]}

\fitch{
\num{1}{2pt}
\num{2}{2pt}
\num{3}{2pt}
\num{4}{2pt}
\num{5}{2pt}
\num{6}{2pt}
}{
A\to B \\
B \to C \\
\hline
\subproof{
		A \\
		\hline
		B  \\
		C
	}
A \to C
}{
\skip{2pt}
\skip{2pt}
\skip{2pt}
\rule{\to E}{1,3}{2pt}
\rule{\to E}{2,4}{2pt}
\rule{\to I}{3\text{ - }5}{2pt}
}

I'm not very familiar with MathJax, so there's probably quite a few improvements that can be done here.