§5.2 BCK Games for Intuitionistic Logic, Constructive Implication and Cut.

Intuitionistic Logic with Cut rule: rational numbers are dense.
∀x.∀y.(x<y⇒∃z.(x<z∧z<y))

Created by Mathematica  (November 11, 2006)