A central issue for spatial reasoning in practice is to formalize reasoning about 3-dimensional space. In this paper, a spatial logic called 3-dimensional spatial logic (3SL), which can appropriately represent the 3-Cartesian product
of the set
of natural numbers, is introduced as a Gentzen-type sequent calculus. 3SL is an extension and generalization of the linear-time temporal logic LTL in which the time domain is
. The completeness and cut-elimination theorems for 3SL are proved.