Though this be madness…

Fitch diagrams are a way of constructing formal logic proofs in sentential logic or in predicate logic. The script on this page page (open script in separate tab) allows users to constuct these proofs and check its validity automatically.

The script allows the use of the logical connectives listed in the table below. In addition, the script allows for the use of predicates, functions, variables, and constants. The only restrictions on these is that they must start with a letter and consist only of letters, numbers, and the underscore (_) character. In particular, the typical restrictions that predicates must start with uppercase letters, while functions and variables must start with lowercase letters, is not enforced.

Logical connective	Logic symbol	Script symbol
Equality	=	=
Conjunction	∧	&, ^
Disjunction	∨	|
Negation	¬	~, !
Absurdity	⊥	#
Implication	→	>
Biconditional	↔	<
Universal quantifier	∀	@
Existential quantifier	∃	?

Rules

Each statement in a proof has to be justified by a rule. Below, we describe each of the possible rules in more detail. In some cases, the rule alone justifies the use of a certain statement. In general, however, a rule refers to previous statements and/or subproofs. Single statements are referred to through their line number, while subproofs are referred to by the first and last line of the subproof, separated by a dash (e.g. 4-6). If a rule refers to more than one statement and/of subproof, they are separated by a comma (e.g. 3, 4-5, 7). The script on this page will automatically check whether rules are applied correctly. Below, we look at each of the supported rules in more detail.

Premise

Premises are the statements that are assumed to be true, and from which we want to derive the goal or conclusion. As a result, premise rules are always allowed, except that they must appear as a single block at the start of the proof. That is, you cannot slip in an extra premise halfway through the proof: it must appear at the top.

Assumption

Assumptions, as the name suggests, are assumed to be true. However, unlike premises, assumptions are temporary. In essence, an assumption starts a subproof that has a single premise (the assumption). While a subproof can refer to any statement in proofs that contain it, there are only a few ways in which the main proof can interact with subproofs. We will visit these rules below.

Flag

A flag is like an assumption, except that a flag assumes that some constant exists rather than that some statement is true. Note that this must be a new constant, it may not already exist in some statement before the flag statement. The flag rule is only needed to introduce a universal quantifier (∀).

Tautology

A tautology rule introduces a statement that is logically true (e.g. P ∨ ¬ P). In general, you should avoid introducing tautologies this way, and instead use Fitch to derive the tautologies you need. After all, if you can derive Q from premises P₁, …, P_n, then (P₁ ∧ … ∧ P_n) → Q is a tautology. Using this tautology to prove Q, however, would miss the point of making a proof that Q does indeed follow from premises P₁, …, P_n.

When you do introduce a tautology this way, the script will check whether the formula you provided actually is a tautology. However, this check may fail for formulas that contain certain combinations of universal and existential quantifiers. If this happens, the script will trust your judgment on whether or not the formula is a tautology.

Reiteration

Reiteration repeats a previously derived statement. You can only reiterate statements that are in the same subproof, or a subproof containing the reiteration. Note that you never need to use reiteration, it is simply there to make the proof more readable.

Equality (=) rules

The equality symbol (=) indicates that the left-hand side is the same as the right-hand side. In terms of Fitch proofs, equality is not the same as mathematical equality. From a statement a=b, it does not follow that b=a.

= Introduction

k

a = a

= Introduction

Any constant or variable equals itself.

= Elimination

k		P(a)
		⋮
m		a = b
		⋮
n		P(b)	= Elimination: k, m

An equality a=b allows any occurence of the left-hand side (a) of the equation to be replaced by the right-hand side (b).

Conjunction (∧) rules

The conjunction symbol (∧) indicates that both the left-hand side and the right-hand side of a statement are true.

∧ Introduction

k		P
		⋮
m		Q
		⋮
n		P ∧ Q	∧ Introduction: k, m

For any two derived formulas P and Q, their conjunction P ∧ Q can also be derived.

∧ Elimination

k		P ∧ Q
		⋮
m		P	∧ Elimination: k

Whenever a conjunction P ∧ Q is derived, both the left-hand side (P) and the right-hand side (Q) can also be derived.

Disjunction (∨) rules

The disjunction symbol (∨) indicates that of the left-hand side and the right-hand side of a statement, at least one of them is true (and possible both). Subproofs are needed to eliminate a disjunction: to show that R follows from P ∨ Q, you must show that R follows from assuming P, and that R also follows from assuming Q.

∨ Introduction

k		P
		⋮
m		P ∨ Q	∨ Introduction: k

Any disjunction in which either the left-hand side or the right-hand side is a derived formula can also be derived.

∨ Elimination

g		P ∨ Q
		⋮
h			P
			⋮
j			R
		⋮
k			Q
			⋮
m			R
		⋮
n		R		∨ Elimination: g, h-j, k-m

Formula R can be derived from a disjunction P ∨ Q if R follows from assuming the left-hand side (P) of a disjunction, but also from assuming the right-hand side (Q) of the same disjunction.

Negation (¬) rules

The negation symbol (¬) indicates that the underlying statement is not true. Introducing a negation relies on a subproof: if assuming P results in inconsistencies, then ¬P can be derived.

¬ Introduction

k			P
			⋮
m			⊥
		⋮
n		¬ P		¬ Introduction: k-m

Whenever absurdity can be derived in a subproof, the assumption of that subproof can be derived to be false.

¬ Elimination

k		¬ ¬ P
		⋮
m		P	¬ Elimination: k

A double negation can be eliminated.

Absurdity (⊥) rules

Absurdity (⊥) is the result of two contradicatory statements. From absurdity, any statement can be derived.

⊥ Introduction

k		P
		⋮
m		¬ P
		⋮
n		⊥	⊥ Introduction: k, m

Aburdity follows when both a formula and its negation can be derived.

⊥ Elimination

k		⊥
		⋮
m		P	⊥ Elimination: k

Any formula follow froms absurdity.

Implication (→) rules

The implication symbol (→) indicates that whenever the left-hand side can be derived, the right-hand side must also be true.

→ Introduction

k			P
			⋮
m			Q
		⋮
n		P → Q		→ Introduction: k-m

If formula Q can be derived from assuming P, then the corresponding conditional can be derived.

→ Elimination

k		P → Q
		⋮
m		P
		⋮
n		Q	→ Elimination: k, m

If Q follows from P, and P is derived, then Q can be derived.

Biconditional implication (↔) rules

The biconditional implication symbol (↔) indicates an implication that works both ways. That is, a biconditional implication P ↔ Q means that when P is true, Q can be derived, but also that if Q is true, P can be derived.

↔ Introduction

g			P
			⋮
h			Q
		⋮
k			Q
			⋮
m			P
		⋮
n		P ↔ Q		↔ Introduction: g-h, k-m

If formula Q follows from assuming P, and P follows from assuming Q, then the corresponding biconditional can be derived.

↔ Elimination

k		P ↔ Q
		⋮
m		Q
		⋮
n		P	→ Elimination: k, m

If P can be derived if and only if Q can be derived, then P follows from Q, and Q follows from P.

Universal quantifier (∀) rules

The universal quantifier (∀) indicates that some statement holds for all possible constants. For example, if we know that ∀x P(x) is true and that c is some constant, then P(c) is true. But be careful: a universal quantifier does not imply that a constant actually exists.

∀ Introduction

k			a
			⋮
m			P(a)
		⋮
n		∀x P(x)		∀ Introduction: k-m

If a formula can be derived for a randomly chosen constant, it holds universally.

∀ Elimination

k		∀x P(x)
		⋮
m		P(a)	∀ Elimination: k

If a formula holds universally, it holds for any (existing) constant.

Existential quantifier (∃) rules

The existential quantifier (∃) indicates that a statement holds for at least one constant, though it gives no information about the identity of that constant. For example, if you know that ∃x P(x), this tells you that there is some constant c so that P(c) holds, but it gives no information at all about whether or not for a given constant b, P(b) holds.

∃ Introduction

k		P(a)
		⋮
m		∃x P(x)	∃ Introduction: k

If a formula holds for some constant (a), there exists a constant for which the formula holds.

∃ Elimination

k		∃x P(x)
		⋮
m		P(a)	∃ Introduction: k

If a formula holds for some constant, give that constant a name that has not previously been used.