One of the important thoughts in mathematical logic is the way of formalization for practical statements. This paper just adopts the method to make formalization for granular computing. Based on this logical method, formulas of a particular kind are constructed on a universal set U. The structure consisting of the universal set, and the all-formula set, is defined as a granular space. Through a formula on the granular space, a semantic set can be separated from U n(n1). This derives the definition of granules on the granular space. On the basis of the granular space and the granules, granular computing is defined through correspondences which connect some granules with another granule or with an object. This arrives at the goal of formalization for granular computing.