Boolean reflection

Boolean reflection is the technique of encoding logical propositions as computable boolean predicates, enabling proof assistants to use computation as a reasoning strategy. In the Coq proof assistant, boolean reflection bridges the gap between the boolean world of decidable computation and the propositional world of logical proof. A proposition P is 'reflected' into a boolean b such that b = true if and only if P holds. This allows tactics in SSReflect to simplify goals through computation — running programs to discharge proof obligations — rather than through purely symbolic manipulation. The technique is central to the Mathematical Components library, where it enables proofs that are simultaneously logical arguments and executable programs.

Boolean reflection is not a convenience. It is a philosophical commitment: that computation and reasoning are the same activity viewed from different angles.