This article is about Avicenna’s account of syllogisms comprising opposite premises. We examine the applications and the truth conditions of these syllogisms. Finally, we discuss the relation between these syllogisms and the principle of non-contradiction.

A Kripke model for a first order language is called a partially-elementary extension model if its accessibility relation is not merely a submodel relation but a stronger relation of being an elementary submodel with respect to some class of fromulae. As a main result of the paper, we give a characterization of partially-elementary extension Kripke models. Throughout the paper we exploit a generalized version of the hierarchy of first order formulae introduced by W. Burr. We present some applications of partially-elementary (...) extension Kripke models to subtheories of Heyting Arithmetic and provide examples of their models and prove some of their properties. For example, we show that finite models of subtheories in question need not be normal . The presented results show that the properties of models of subtheories of Heyting Arithmetic differ much from the properties of models of the full theory. (shrink)

The aim of this paper is to describe from a semantic perspective the problem of conservativity of classical first-order theories over their intuitionistic counterparts. In particular, we describe a class of formulae for which such conservativity results can be proven in case of any intuitionistic theory T which is complete with respect to a class of T-normal Kripke models. We also prove conservativity results for intuitionistic theories which are closed under the Friedman translation and complete with respect to a class (...) of conversely well-founded Kripke models. The results can be applied to a wide class of intuitionistic theories and can be viewed as generalization of the results obtained by syntactic methods. (shrink)

We study the relations of being substructure and elementary substructure between Kripke models of intuitionistic predicate logic with the same arbitrary frame. We prove analogues of Tarski's test and Löwenheim-Skolem's theorems as determined by our definitions. The relations between corresponding worlds of two Kripke models [MATHEMATICAL SCRIPT CAPITAL K] ⪯ [MATHEMATICAL SCRIPT CAPITAL K]′ are studied.

We present axiom systems, and provide soundness and strong completeness theorems, for classes of Kripke models with restricted extension rules among the node structures of the model. As examples we present an axiom system for the class of cofinal extension Kripke models, and an axiom system for the class of end-extension Kripke models. We also show that Heyting arithmetic is strongly complete for its class of end-extension models. Cofinal extension models of HA are models of Peano arithmetic.

We prove that every infinite rooted narrow tree Kripke model of HA is locally PA.

In the first section of this paper we show that i Π1 ≡ W⌝⌝lΠ1 and that a Kripke model which decides bounded formulas forces iΠ1 if and only if the union of the worlds in any path in it satisflies IΠ1. In particular, the union of the worlds in any path of a Kripke model of HA models IΠ1. In the second section of the paper, we show that for equivalence of forcing and satisfaction of Πm-formulas in a linear Kripke (...) model deciding Δ0-formulas it is necessary and sufficient that the model be Σm-elementary. This implies that if a linear Kripke model forces PEMprenex, then it forces PEM. We also show that, for each n ≥ 1, iΦn does not prove ℋ(IΠn's are Burr's fragments of HA. (shrink)