The finite model property for ${\bf MIPQ}$ and some consequences.
Gisèle Fischer-Servi · Notre Dame Journal of Formal Logic · 1978
The proof given in [l] that MIPQ has the finite model property is shown to be erroneous.Through the use of slightly different techniques we prove that this property nonetheless does hold.We then prove a representation theorem for finite Monadic Heyting algebras which, together with the finite model property for MIPQ, yields an algebraic proof of a theorem concerning a translation map from MIPQ to a bimodal calculus (S4, S5)-C (see [3]). MIPQ has the finite model propertyFollowing a suggestion of Prior, R. A. Bull considers in [l] a modal calculus (MIPQ) which contains as its base the intuitionist propositional calculus (IC) instead of the usual classical logic.For reasons that will become clear in section 2, from here on this calculus will be called S5-IC.Hence S5-IC contains IC and the following rules:For this modal extension of IC, R. A. Bull shows completeness with respect to canonical models.We recall that in a canonical model (A, B, U, Π, -*, 0,1, K,l>, A is a Heyting algebra, B is a relatively complete subalgebra of A and K, I are two operators on A such that Kx = Min {ye B: x ^ y} and \x= Maχ{yeB: y ^ x}.In [1] it is proven that S5-IC is characterized by finite models,but it appears that the proof in question is wrong ~ >r, starting from a canonical model, the author uses a construction whic > opposed to what is maintained, does not yield a finite canonical model.Let us consider the argument in [1]: given a canonical model {A, B, u, Π, -», 0, 1, K, I)