  In 1938, Tarski proved that a formula is not intuitionistically valid if, and
only if, it has a counter-model in the Heyting algebra of open sets of some
topological space. In fact, Tarski showed that any Euclidean space R^n with n
>= 1 suffices, as does e.g. the Cantor space. In particular, intuitionistic
logic cannot detect topological dimension in the frame of all open sets of a
Euclidean space. By contrast, we consider the lattice of open subpolyhedra of a
given compact polyhedron P \subseteq R^n, prove that it is a locally finite
Heyting subalgebra of the (non-locally-finite) algebra of all open sets of R^n,
and show that intuitionistic logic is able to capture the topological dimension
of P through the bounded-depth axiom schemata. Further, we show that
intuitionistic logic is precisely the logic of formul{\ae} valid in all Heyting
algebras arising from polyhedra in this manner. Thus, our main theorem
reconciles through polyhedral geometry two classical results: topological
completeness in the style of Tarski, and Jaskowski's theorem that
intuitionistic logic enjoys the finite model property. Several questions of
interest remain open. E.g., what is the intermediate logic of all closed
triangulable manifolds?
