§4.1 Introducing BCK Games for constructive implication.
A language L for Arithmetic. The judgement tree.
Eloise and Abelard, conjunctive and disjunctive judgements.
Backtracking Games (for intuitionistic logic).
A generic position of the play in tree form.
A generic position of the play in sequent form.
Created by Mathematica (November 11, 2006)