We study the problem of finding a basis for all rules admissible in the intuitionistic propositional logic IPC. The main result is Theorem 3.1 which gives a basis consisting of all rules in semi-reduced form satisfying certain specific additional requirements. Using developed technique we also find a basis for rules admissible in the logic of excluded middle law KC.

Let equation image denote the inverse limit of all finite cyclic groups. Let F, G and H be abelian groups with H ≤ G. Let FβH denote the abelian group , where +βis defined by +β = + β — β) for a certain β : F → G linear mod H meaning that β = 0 and β + β — β ∈ H for all a, b in F. In this paper we show that the following hold: The (...) additive group of any nonstandard model ℤ* of the ring ℤ is isomorphic to βH for a certain β : ℤ*+/H → equation image linear mod H. equation image is isomorphic to βH for some β : equation image/H →ℚ linear mod H, though equation image is not the additive group of any model of Th and the exact sequence H → equation image → equation image/H is not splitting. (shrink)

In [5] Phillips proved that one can obtain the additive group of any nonstandard model *ℤ of the ring ℤ of integers by using a linear mod 1 function h : F ℚ, where F is the α-dimensional vector space over ℚ when α is the cardinality of *ℤ. In this connection it arises the question whether there are linear mod 1 functions which are neither addition nor quasi-linear. We prove that this is the case.