Rule specifications
Introduction rules
^I (And Introduction)
From x, y deduce x ^ y
1 x [...]
2 y [...]
3 x ^ y [^I(1,2)]->I (Implication Introduction)
From "assuming x deduces y", deduce x -> y
1 x [ass]
<hard struggle>
2 y [...]
3 x -> y [->I(1,2)]/I (Or Introduction)
From x deduce x / ? or ? / x
1 x
2 x / y [/I(1)]~I (Not Introduction)
From "assuming original deduces bottom" deduce its negation
1 x [ass]
<hard struggle>
2 F [...]
3 ~x [~I(1,2)]~~I (Double Negation Introduction)
From x deduce ~~x
1 x [...]
2 ~(~(x)) [~~I(1)]FI (Falsity Introduction)
From x and ~x deduce F
1 x [...]
2 ~x [...]
3 F [FI(1,2)]TI (Truth Introduction)
From nothing deduces T (but why would you do that 😏)
1 T [TI]<->I (Equivalence Introduction)
From x -> y and y -> x deduce x <-> y
1 x -> y [...]
2 y -> x [...]
3 x <-> y [<->I(1,2)]existsI (Exists Introduction)
From 𝝓(x) deduce ∃a 𝝓(a)
1 𝝓(x) [...]
2 exists x. (𝝓(x)) [existsI(1)]forallI (Forall Introduction)
From "c deduces f(c)" deduce ∀x f(x)
1 c [forall I const]
<hard struggle>
2 f(c) [...]
3 forall x. (f(x)) [forallI(1,2)]Elimination
^E (And Elimination)
From x ^ y deduce x (or y)
1 x ^ y [...]
2 x [^E(1)]->E (Emplication Elimination)
From x -> y and x deduce y
1 x [...]
2 x -> y [...]
3 y [->E(1,2)]/E (Or Elimination)
From x1 / x2, "assuming x1 deduces y", "assuming x2 deduces y", deduce y
1 x1 / x2 [...]
2 x1 [ass]
<hard struggle>
3 y [...]
4 x2 [ass]
<hard struggle>
5 y [...]
6 y [/E(1,2,3,4,5)]~E (Not Elimination)
From x and ~x deduces F (same as FI)
1 x [...]
2 ~x [...]
3 F [~E(1,2)]~~E (Double Negation Elimination)
From ~~x deduce x
1 ~~x [...]
2 x [~~E(1)]FE (Falsity Elimination)
From F deduce anything
1 F [...]
2 anything [FE(1)]<->E (Equivalence Elimination)
From x <-> y and either side, deduce the other side
1 x <-> y [...]
2 y [...]
3 x [<->E(1,2)]existsE (Exists Elimination)
From ∃a 𝝓(a) and "𝝓(c) for some c deduces x", deduce x
1 exists a. (𝝓(a)) [...]
2 𝝓(c) [ass]
<hard struggle>
3 x [...]
4 x [existsE(1,2,3)]forallE (Forall Elimination)
From ∀x f(x) deduce f[x/c]
1 forall x. (f(x)) [...]
2 f(c) [forallE(1)]forall->E (Forall Implication Elimination)
From ∀x f(x) -> g(x) and f(c), deduces g(c)
1 forall x. (f(x) -> g(x)) [...]
2 f(c) [...]
3 g(c) [forall->E(1,2)]Special
LEM (Law of Excluded Middle)
From nothing deduce p / ~p
1 x / ~x [LEM]MT (Modus Tollens)
From x -> y and ~y, deduce ~x
1 x -> y [...]
2 ~y [...]
3 ~x [MT(1,2)]PC (Proof by Contradiction)
From "assuming x deduces F", deduce ~x
1 x [...]
<hard struggle>
2 F [...]
3 ~x [PC(1,2)]refl (rule of Reflection)
From nothing deduce x = x
1 x = x [refl]=sub (Equality Substitution)
From a = b and f(a), deduce f(b)
1 a = b [...]
2 f(a) [...]
3 f(b) [=sub(2,1)]sym (rule of Symmetry)
From a = b deduce b = a
1 a = b [...]
2 b = a [sym(1)]forall I const
Introduces a new free variable
1 c [forall I const]given (Given)
Given proposition
1 x [given]premise (Premise)
Given proposition
1 x [premise]ass (Assumption)
Assume proposition / formula
1 x [...]
2 x -> y [ass]
3 result [...]
4 conclusion [...]tick (Tick)
From x deduce x (syntactic flag), see syntax gotcha for more details
1 x [...]
2 y [...]
3 result1 [...]
4 result1 [tick(3)] # Must tick here to signify ending of block
5 z [...]
6 result2 [...]
7 conclusion [...]