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}
$$