Fitch Proof Constructor

Premises		Conclusion
	⊢

Formula:	Rule:	SI/TI Rule:	Depth	Lines:

Check the whole proof before exporting:
	Plain	Pretty Print	LaTexify

[+] Syntax

NOTE: the program will accept formulas with a binary connective as the main connective without the outermost parentheses. The program will accept lowercase letters both as individual constants and as variables, so one could e.g. have '(Ea)Fa' or '(Fx>Gy)', but in practice it's best to notationally distinguish them as per the guidelines below. Since 'v' is used for disjunction, it can't be used as a variable/constant.

Logical Symbols
Negation	~
Conjunction	&
Disjunction	v
Conditional	>
Biconditional	<>
Existential Quantifier	E
Universal Quantifier	A
Identity Relation	=
Absurdity	#

Non-Logical Symbols
Individual Constants	a,b,c,d,e,f
Individual Variables	u,w,x,y,z
Propositional Constants	A ... Z
Predicate Constants (any arity)	A ... Z

Sample Wffs
P
((GvH)>F)
(#>P)
Fa
(Fa & Rab)
(Ex)Rxb
(Ex)(Ay)(Rxy <> Ryx)
(Ax)((Fx & (Ey)Rxy) > (Ey)(Fy v Ryx))
((Ax)(Fx > (Ey)Rxy) > (Ey)Gy)

[+] Rules for Sentential Logic

NOTE: the order in which rule lines are cited is important for multi-line rules. For example, in an application of conditional elimination with citation "j,k →E", the line j must be the conditional, and the line k must be its antecedent, even if line k actually precedes line j in the proof. The only multi-line rules which are set up so that order doesn't matter are &I and #I.

Rule of &I
j	p
	:
k	q
	:
	p & q	j,k &I

Rule of &E
j	p & q
	:
	p	j &E

Rule of ∨I
j	p
	:
	p ∨ q	j ∨I

Rule of ∨E
g	p ∨ q
	:
h	p
	:
i	r

j	q
	:
k	r
	r	g,h-i,j-k ∨E

Rule of ~I
j	p
	:
k	⋏
	~p	j-k ~I

Rule of ⋏I
j	~p
	:
k	p
	:
	⋏	j,k ⋏I

Rule of ~E
j	~~p
	:
	p	j ~E

Rule of →I
j	p
	:
k	q
	p → q	j-k →I

Rule of →E
j	p → q
	:
k	p
	:
	q	j,k →E

Rule of ↔I
h	p
	:
i	q

j	q
	:
k	p
	p↔q	h-i,j-k ↔I

Rule of ↔E
j	p ↔ q
	:
k	p
	:
	q	j,k ↔E

Rule of EFQ
j	⋏
	:
	p	j EFQ

[+] Rules for Quantificational Logic

NOTE: as with the propositional rules, the order in which lines are cited matters for multi-line rules.

Rule of ∀I
j	t	Flag
	:
k	φt
m	(∀v)φv	j-k ∀I

where t does not occur in (∀v)φv or any line available to line m.

Rule of ∀E
j	(∀v)φv
	:
	φt	j ∀E

Rule of ∃I
j	φt
	:
	(∃v)φv	j ∃I

Rule of ∃E
j	(∃v)φv
k	φt
	:
l	ψ
m	ψ	j,k-l ∃E

where t does not occur in ψ or any line available to line m.

Rule of =I
j	t=t	=I

Rule of =E
j	t₁=t₂
	:
k	φt₁
	:
	φt₂	j,k =E

[+] Examples

Some (importable) sample proofs in the "plain" notation are here.

Note that proofs can also be exported in "pretty print" notation (with unicode logic symbols) or LaTex. See this pdf for an example of how Fitch proofs typeset in LaTex look. To typeset these proofs you will need Johann Klüwer's fitch.sty. (If you don't want to install this file, you can just include it in the the same directory as your tex file.)