fitch.sty module (Küwer's fitch.sty, improved by Kocurek).

Feature request: support for fitch.sty (Fitch-style natural deduction proofs)

Summary

MathJax 4 supports bussproofs for tree-style proofs. I would like to request support for fitch.sty by Johan W. Klüwer — the other major proof notation used in logic, known as Fitch-style or "flag notation" natural deduction.

The package and its syntax

The reference implementation is Klüwer's original fitch.sty (2001), improved by Alexander W. Kocurek (debugged, lighter dependencies):

• Kocurek's improved version: https://www.actual.world/resources/tex/sty/kluwer/edited/fitch.sty
• Kocurek's LaTeX resources page (with documentation): https://www.actual.world/latex/

Note: this is not the fitch package on CTAN (https://ctan.org/pkg/fitch), which is a more complex reimplementation by Peter Selinger and Richard Zach (OpenLogicProject). Klüwer's design is minimalist: a thin layer over tabular, with a handful of commands that map almost directly to visual elements:

Command	Meaning
\fa	Continuation line (vertical scope line)
\fh	Hypothesis (short vertical line + flag underneath)
\fj	Additional premise (full vertical line + flag)
\fb	Start of subproof (short vertical line, no flag)
&	Separator between formula and justification

Nesting is determined by how many \fa/\fh/\fj commands precede the formula on each line. Here is a complete example:

\begin{fitch}
\fh $P \to Q$ & $AS$ \\
\fa\fh $Q \to R$ & $AS$ \\
\fa\fa\fh $P$ & $AS$ \\
\fa\fa $Q$ & $\to E\,1,3$ \\
\fa\fa $R$ & $\to E\,2,4$ \\
\fa $P \to R$ & $\to I\,3\text{-}5$ \\
$(Q \to R) \to (P \to R)$ & $\to I\,2\text{-}6$ \\
$(P \to Q) \to ((Q \to R) \to (P \to R))$ & $\to I\,1\text{-}7$
\end{fitch}

This is structurally simpler than bussproofs, which requires explicit tree construction with \AxiomC, \UnaryInfC, \BinaryInfC, etc. The simplicity makes it a realistic target for a MathJax extension.

Real-world use case: G4+ theorem prover

I am a professor of logic at the Université de Lorraine (Nancy, France) and the developer of G4+, a theorem prover for minimal, intuitionistic, and classical first-order logic that produces human-readable proofs. G4+ is integrated into Geoff Sutcliffe's SystemOnTPTP and runs entirely in the browser via SWI-Prolog's WebAssembly build.

G4+ outputs proofs in three formats:

1. G4 sequent calculus — rendered natively with bussproofs in MathJax ✅
2. Tree-style natural deduction — rendered natively with bussproofs in MathJax ✅
3. Fitch-style natural deduction — no MathJax support ❌

Because of this gap, I had to build a custom SVG renderer that parses the fitch.sty LaTeX output, draws scope lines and flags in SVG, and delegates formula rendering to MathJax via foreignObject. It works, but it is a fragile workaround.

Live demo (press Ctrl+M to toggle rendering): 🔗 https://g4-mic.vidal-rosset.net/wasm/tinker#A4Jw9gbgpgFDwAIC8A+BBHAIMtd04RG1QXgKM0wDog

<!-- INSERT SCREENSHOT: Fitch proof rendered with the custom SVG workaround -->

Who would benefit

• Logic courses using web-based tools (carnap.io, online textbooks, LMS integrations)
• Automated theorem provers with web interfaces
• Philosophy and computer science departments teaching natural deduction in Fitch style
• Any MathJax-enabled platform (Jupyter notebooks, Stack Exchange, academic blogs) where authors currently have no way to typeset Fitch proofs

Adding fitch.sty support would complete MathJax's coverage of the two standard proof notations in logic. The demand is niche but real, and growing as logic education moves online.

Thank you for considering this request.

# Feature request: support for `fitch.sty` (Fitch-style natural deduction proofs)

Summary

MathJax 4 supports bussproofs for tree-style proofs. I would like to request support for fitch.sty by Johan W. Klüwer — the other major proof notation used in logic, known as Fitch-style or "flag notation" natural deduction.

The package and its syntax

The reference implementation is Klüwer's original fitch.sty (2001), improved by Alexander W. Kocurek (debugged, lighter dependencies):

• Kocurek's improved version: https://www.actual.world/resources/tex/sty/kluwer/edited/fitch.sty
• Kocurek's LaTeX resources page (with documentation): https://www.actual.world/latex/

Note: this is not the fitch package on CTAN (https://ctan.org/pkg/fitch), which is a more complex reimplementation by Peter Selinger and Richard Zach (OpenLogicProject). Klüwer's design is minimalist: a thin layer over tabular, with a handful of commands that map almost directly to visual elements:

Command	Meaning
\fa	Continuation line (vertical scope line)
\fh	Hypothesis (short vertical line + flag underneath)
\fj	Additional premise (full vertical line + flag)
\fb	Start of subproof (short vertical line, no flag)
&	Separator between formula and justification

Nesting is determined by how many \fa/\fh/\fj commands precede the formula on each line. Here is a complete example:

\begin{fitch}
\fh $P \to Q$ & $AS$ \\
\fa\fh $Q \to R$ & $AS$ \\
\fa\fa\fh $P$ & $AS$ \\
\fa\fa $Q$ & $\to E\,1,3$ \\
\fa\fa $R$ & $\to E\,2,4$ \\
\fa $P \to R$ & $\to I\,3\text{-}5$ \\
$(Q \to R) \to (P \to R)$ & $\to I\,2\text{-}6$ \\
$(P \to Q) \to ((Q \to R) \to (P \to R))$ & $\to I\,1\text{-}7$
\end{fitch}

This is structurally simpler than bussproofs, which requires explicit tree construction with \AxiomC, \UnaryInfC, \BinaryInfC, etc. The simplicity makes it a realistic target for a MathJax extension.

Real-world use case: G4+ theorem prover

I am a professor of logic at the Université de Lorraine (Nancy, France) and the developer of G4+, a theorem prover for minimal, intuitionistic, and classical first-order logic that produces human-readable proofs. G4+ is integrated into Geoff Sutcliffe's [SystemOnTPTP](https://www.tptp.org/cgi-bin/SystemOnTPTP) and runs entirely in the browser via SWI-Prolog's WebAssembly build.

G4+ outputs proofs in three formats:

1. G4 sequent calculus — rendered natively with bussproofs in MathJax ✅
2. Tree-style natural deduction — rendered natively with bussproofs in MathJax ✅
3. Fitch-style natural deduction — no MathJax support ❌

Because of this gap, I had to build a custom SVG renderer that parses the fitch.sty LaTeX output, draws scope lines and flags in SVG, and delegates formula rendering to MathJax via foreignObject. It works, but it is a fragile workaround.

Live demo (press Ctrl+M to toggle rendering):
🔗 https://g4-mic.vidal-rosset.net/wasm/tinker#A4Jw9gbgpgFDwAIC8A+BBHAlMtd04RG1QXgKM0wDog

Who would benefit

• Logic courses using web-based tools ([carnap.io](https://carnap.io), online textbooks, LMS integrations)
• Automated theorem provers with web interfaces
• Philosophy and computer science departments teaching natural deduction in Fitch style
• Any MathJax-enabled platform (Jupyter notebooks, Stack Exchange, academic blogs) where authors currently have no way to typeset Fitch proofs

Adding fitch.sty support would complete MathJax's coverage of the two standard proof notations in logic. The demand is niche but real, and growing as logic education moves online.

Thank you for considering this request.

No implementation file or test is named. Start by reviewing MathJax's existing bussproofs support and the supplied fitch.sty commands and example. Done means the requested Fitch-style syntax renders correctly, including nested scope lines, flags, formulas, and justifications.