We prove completeness and decidability results for the temporal logic CTL in Coq/Ssreflect. Our main result is a constructive proof that for every formula one can obtain either a finite model satisfying the formula or a proof in a Hilbert system certifying the unsatisfiability of the formula. The small model property of CTL and completeness of the Hilbert system follow as corollaries. Our proofs mostly refine the mathematical proofs given by Emerson and Halpern. One important deviation is our use of an inductive semantics for CTL to avoid reasoning about infinite paths. On finite models the inductive semantics agrees constructively with the standard path semantics. The proof amounts to the verification of a simple model checking algorithm. For general models, the agreement between the inductive semantics and the path semantics requires excluded middle and dependent choice.
This is an extended and revised version of the ITP 2014 paper.