All Finitely Axiomatizable Tense Logics of Linear Time Flows Are CoNP-complete

We prove that all finitely axiomatizable tense logics with temporal operators for ‘always in the future’ and ‘always in the past’ and determined by linear fows time are coNP-complete. It follows, for example, that all tense logics containing a density axiom of the form ■ⁿ⁺¹_F p → ⁿ_F p, for some n ≥ 0, are coNP-complete. Additionally, we prove coNP-completeness of all ∩-irreducible tense logics. As these classes of tense logics contain many Kripke incomplete bimodal logics, we obtain many natural examples of Kripke incomplete normal bimodal logics which are nevertheless coNP-complete.     

Normal Modal Logics Determined by Aligned Clusters

We consider the family of logics from NExt(KTB) which are determined by linear frames with reflexive and symmetric relation of accessibility. The condition of linearity in such frames was first defined in the paper [9]. We prove that the cardinality of the logics under consideration is uncountably infinite.     

A Splitting Logic in NExt(KTB)

It is shown that the normal modal logic of two reflexive points jointed with a symmetric binary relation splits the lattice of normal extensions of the logic KTB. By this fact, it is easily seen that there exists the third largest logic in the class of all normal extensions of KTB. Presented by Michael Zakharyaschev Received February 17, 2006     

Multi-Modal CTL: Completeness,Complexity, and an Application

We define a multi-modal version of Computation Tree Logic (ctl) by extending the language with path quantifiers E ^δ and A ^δ where δ denotes one of finitely many dimensions, interpreted over Kripke structures with one total relation for each dimension. As expected, the logic is axiomatised by taking a copy of a ctl axiomatisation for each dimension. Completeness is proved by employing the completeness result for ctl to obtain a model along each dimension in turn. We also show that the logic is decidable and that its satisfiability problem is no harder than the corresponding problem for ctl. We then demonstrate how Normative Systems can be conceived as a natural interpretation of such a multi-dimensional ctl logic. Presented by Jacek Malinowski     

On Permutation in Simplified Semantics

This note explains an error in Restall’s ‘Simplified Semantics for Relevant Logics (and some of their rivals)’ (Restall, J Philos Logic 22(5):481–511, 1993) concerning the modelling conditions for the axioms of assertion A → ((A → B) → B) (there called c6) and permutation (A → (B → C)) → (B → (A → C)) (there called c7). We show that the modelling conditions for assertion and permutation proposed in ‘Simplified Semantics’ overgenerate. In fact, they overgenerate so badly that the proposed semantics for the relevant logic R validate the rule of disjunctive syllogism. The semantics provides for no models of R in which the “base point” is inconsistent. This problem is not restricted to ‘Simplified Semantics.’ The techniques of that paper are used in Graham Priest’s textbook An Introduction to Non-Classical Logic (Priest, 2001), which is in wide circulation: it is important to find a solution. In this article, we explain this result, diagnose the mistake in ‘Simplified Semantics’ and propose two different corrections.     

Cut-free tableau calculi for some propositional normal modal logics

We give sound and complete tableau and sequent calculi for the prepositional normal modal logics S4.04, K4B and G ⁰(these logics are the smallest normal modal logics containing K and the schemata A A, A A and A ( A); A A and AA; A A and ((A A) A) A resp.) with the following properties: the calculi for S4.04 and G ⁰are cut-free and have the interpolation property, the calculus for K4B contains a restricted version of the cut-rule, the so-called analytical cut-rule.In addition we show that G ⁰is not compact (and therefore not canonical), and we proof with the tableau-method that G ⁰is characterised by the class of all finite, (transitive) trees of degenerate or simple clusters of worlds; therefore G ⁰is decidable and also characterised by the class of all frames for G ⁰.Research supported by Fonds zur Förderung der wissenschaftlichen Forschung, project number P8495-PHY.Presented by W. Rautenberg     

Decidable and enumerable predicate logics of provability

Predicate modal formulas are considered as schemata of arithmetical formulas, where is interpreted as the standard formula of provability in a fixed sufficiently rich theory T in the language of arithmetic. QL _T(T) and QL _T are the sets of schemata of T-provable and true formulas, correspondingly. Solovay's well-known result — construction an arithmetical counterinterpretation by Kripke countermodel — is generalized on the predicate modal language; axiomatizations of the restrictions of QL _T(T) and QL _T by formulas, which contain no variables different from x, are given by means of decidable prepositional bimodal systems; under the assumption that T is ₁-complete, there is established the enumerability of the restrictions of QL _T(T) and QL _T by: 1) formulas in which the domains of different occurrences of don't intersect and 2) formulas of the form ⁿ A.     

Kripke Incompleteness of Predicate Extensions of the Modal Logics Axiomatized by a Canonical Formula for a Frame with a Nontrivial Cluster

We generalize the incompleteness proof of the modal predicate logic Q-S4+ p p + BF described in Hughes-Cresswell [6]. As a corollary, we show that, for every subframe logic Lcontaining S4, Kripke completeness of Q-L+ BF implies the finite embedding property of L.     

A 2-categorial Generalization of the Concept of Institution

After defining, for each many-sorted signature Σ = (S, Σ), the category Ter(Σ), of generalized terms for Σ (which is the dual of the Kleisli category for \mathbb T_S{\mathbb {T}_{\bf \Sigma}}, the monad in Set ^S determined by the adjunction T_S \dashv G_S{{\bf T}_{\bf \Sigma} \dashv {\rm G}_{\bf \Sigma}} from Set ^S to Alg(Σ), the category of Σ-algebras), we assign, to a signature morphism d from Σ to Λ, the functor d_à{{\bf d}_\diamond} from Ter(Σ) to Ter(Λ). Once defined the mappings that assign, respectively, to a many-sorted signature the corresponding category of generalized terms and to a signature morphism the functor between the associated categories of generalized terms, we state that both mappings are actually the components of a pseudo-functor Ter from Sig to the 2-category Cat. Next we prove that there is a functor Tr^Σ, of realization of generalized terms as term operations, from Alg(Σ) × Ter(Σ) to Set, that simultaneously formalizes the procedure of realization of generalized terms and its naturalness (by taking into account the variation of the algebras through the homomorphisms between them). We remark that from this fact we will get the invariance of the relation of satisfaction under signature change. Moreover, we prove that, for each signature morphism d from Σ to Λ, there exists a natural isomorphism θ ^d from the functor Tr^L °(Id ×d_à){{{\rm Tr}^{\bf {\bf \Lambda}} \circ ({\rm Id} \times {\bf d}_\diamond)}} to the functor Tr^S °(d^* ×Id){{\rm Tr}^{\bf \Sigma} \circ ({\bf d}^* \times {\rm Id})}, both from the category Alg(Λ) × Ter(Σ) to the category Set, where d* is the value at d of the arrow mapping of a contravariant functor Alg from Sig to Cat, that shows the invariant character of the procedure of realization of generalized terms under signature change. Finally, we construct the many-sorted term institution by combining adequately the above components (and, in a derived way, the many-sorted specification institution), but for a strict generalization of the standard notion of institution.     

Some results on the Kripke sheaf semantics for super-intuitionistic predicate logics

Some properties of Kripke-sheaf semantics for super-intuitionistic predicate logics are shown. The concept ofp-morphisms between Kripke sheaves is introduced. It is shown that if there exists ap-morphism from a Kripke sheaf ₁ into ₂ then the logic characterized by ₁ is contained in the logic characterized by ₂. Examples of Kripke-sheaf complete and finitely axiomatizable super-intuitionistic (and intermediate) predicate logics each of which is Kripke-frame incomplete are given. A correction to the author's previous paper Kripke bundles for intermediate predicate logics and Kripke frames for intuitionistic modal logics (Studia Logica, 49(1990), pp. 289–306 ) is stated.Dedicated to Professor Takeshi Kotake on his 60th birthdayThis research was partially supported by Grant-in-Aid for Encouragement of Young Scientists No. 03740107, Ministry of Educatin, Science and Culture, Japan.     

Second order propositional operators over cantor space

We consider propositional operators defined by propositional quantification in intuitionistic logic. More specifically, we investigate the propositional operators of the formA* :p q(p A(q)) whereA(q) is one of the following formulae: (¬¬q q) V ¬¬q, (¬¬q q) (¬¬q V ¬q), ((¬¬q q) (¬¬q V ¬q)) ((¬¬q q) V ¬¬q). The equivalence ofA*(p) to ¬¬p is proved over the standard topological interpretation of intuitionistic second order propositional logic over Cantor space.We relate topological interpretations of second order intuitionistic propositional logic over Cantor space with the interpretation of propositional quantifiers (as the strongest and weakest interpolant in Heyting calculus) suggested by A. Pitts. One of the merits of Pitts' interpretation is shown to be valid for the interpretation over Cantor space.Presented byJan Zygmunt     

Non-Adjunctive Inference and Classical Modalities

The article focuses on representing different forms of non-adjunctive inference as sub-Kripkean systems of classical modal logic, where the inference from □A and □B to □A∧B fails. In particular we prove a completeness result showing that the modal system that Schotch and Jennings derive from a form of non-adjunctive inference in (Schotch and Jennings, 1980) is a classical system strictly stronger than EMN and weaker than K (following the notation for classical modalities presented in Chellas, 1980). The unified semantical characterization in terms of neighborhoods permits comparisons between different forms of non-adjunctive inference. For example, we show that the non-adjunctive logic proposed in (Schotch and Jennings, 1980) is not adequate in general for representing the logic of high probability operators. An alternative interpretation of the forcing relation of Schotch and Jennings is derived from the proposed unified semantics and utilized in order to propose a more fine-grained measure of epistemic coherence than the one presented in (Schotch and Jennings, 1980). Finally we propose a syntactic translation of the purely implicative part of Jaśkowski's system D₂ into a classical system preserving all the theorems (and non-theorems) explicilty mentioned in (Jaśkowski, 1969). The translation method can be used in order to develop epistemic semantics for a larger class of non-adjunctive (discursive) logics than the ones historically investigated by Jaśkowski.     

A Routley-Meyer affixing style semantics for logics containing Aristotle's Thesis

We provide a semantics for relevant logics with addition of Aristotle's Thesis, ∼(A→∼A) and also Boethius,(A→B)→∼(A→∼B). We adopt the Routley-Meyer affixing style of semantics but include in the model structures a regulatory structure for all interpretations of formulae, with a view to obtaining a lessad hoc semantics than those previously given for such logics. Soundness and completeness are proved, and in the completeness proof, a new corollary to the Priming Lemma is introduced (c.f.Relevant Logics and their Rivals I, Ridgeview, 1982).     

Henkin Quantifiers and the Definability of Truth

Henkin quantifiers have been introduced in Henkin (1961). Walkoe (1970) studied basic model-theoretical properties of an extension L _* ¹(H) of ordinary first-order languages in which every sentence is a first-order sentence prefixed with a Henkin quantifier. In this paper we consider a generalization of Walkoe's languages: we close L _* ¹(H) with respect to Boolean operations, and obtain the language L ¹(H). At the next level, we consider an extension L _* ²(H) of L ¹(H) in which every sentence is an L ¹(H)-sentence prefixed with a Henkin quantifier. We repeat this construction to infinity. Using the (un)-definability of truth – in – N for these languages, we show that this hierarchy does not collapse. In addition, we compare some of the present results to the ones obtained by Kripke (1975), McGee (1991), and Hintikka (1996).     

Some Results on Mean Square Error for Factor Score Prediction

For the confirmatory factor model a series of inequalities is given with respect to the mean square error (MSE) of three main factor score predictors. The eigenvalues of these MSE matrices are a monotonic function of the eigenvalues of the matrix Γ _p = Φ ^1/2 Λ _p ′Ψ _p ⁻¹ Λ _p Φ ^1/2. This matrix increases with the number of observable variables p. A necessary and sufficient condition for mean square convergence of predictors is divergence of the smallest eigenvalue of Γ _p or, equivalently, divergence of signal-to-noise (Schneeweiss & Mathes, 1995). The same condition is necessary and sufficient for convergence to zero of the positive definite MSE differences of factor predictors, convergence to zero of the distance between factor predictors, and convergence to the unit value of the relative efficiencies of predictors. Various illustrations and examples of the convergence are given as well as explicit recommendations on the problem of choosing between the three main factor score predictors. The author is obliged to Maarten Speekenbrink and Peter van Rijn for their assistance with plotting the figures. In addition, I am obliged to the referees for their stimulating remarks.     

The Pentus Theorem for Lambek Calculus with Simple Nonlogical Axioms

The Lambek calculus introduced in Lambek [6] is a strengthening of the type reduction calculus of Ajdukiewicz [1]. We study Associative Lambek Calculus L in Gentzen style axiomatization enriched with a finite set Γ of nonlogical axioms, denoted by L(Γ).It is known that finite axiomatic extensions of Associative Lambek Calculus generate all recursively enumerable languages (see Buszkowski [2]). Then we confine nonlogical axioms to sequents of the form p → q, where p and q are atomic types. For calculus L(Γ) we prove interpolation lemma (modifying the Roorda proof for L [10]) and the binary reduction lemma (using the Pentus method [9] with modification from [3]). In consequence we obtain the weak equivalence of the Context-Free Grammars and grammars based on L(Γ).     

An axiomatization of the modal theory of the veiled recession frame

The veiled recession frame has served several times in the literature to provide examples of modal logics failing to have certain desirable properties. Makinson [4] was the first to use it in his presentation of a modal logic without the finite model property. Thomason [5] constructed a (rather complicated) logic whose Kripke frames have an accessibility relation which is reflexive and transitive, but which is satisfied by the (non-transitive) veiled recession frame, and hence incomplete. In Van Benthem [2] the frame was an essential tool to find simple examples of incomplete logics, axiomatized by a formula in two proposition letters of degree 2, or by a formula in one proposition letter of degree 4 (the degree of a modal formula is the maximal number of nested occurrences of the necessity operator in ). In [3] we showed that the modal logic determined by the veiled recession frame is incomplete, and besides that, is an immediate predecessor of classical logic (or, more precisely, the modal logic axiomatized by the formula pp), and hence is a logic, maximal among the incomplete ones. Considering the importance of the modal logic determined by the veiled recession frame, it seems worthwhile to ask for an axiomatization, and in particular, to answer the question if it is finitely axiomatizable. In the present paper we find a finite axiomatization of the logic, and in fact, a rather simple one consisting of formulas in at most two proposition letters and of degree at most three.The paper was written with support of the Netherlands organization for the Advancement of Pure Research (Z.W.O.).     

Undecidability and intuitionistic incompleteness

Let S be a deductive system such that S-derivability (s) is arithmetic and sound with respect to structures of class K. From simple conditions on K and s, it follows constructively that the K-completeness of s implies MP(S), a form of Markov's Principle. If s is undecidable then MP(S) is independent of first-order Heyting arithmetic. Also, if s is undecidable and the S proof relation is decidable, then MP(S) is independent of second-order Heyting arithmetic, HAS. Lastly, when s is many-one complete, MP(S) implies the usual Markov's Principle MP.An immediate corollary is that the Tarski, Beth and Kripke weak completeness theorems for the negative fragment of intuitionistic predicate logic are unobtainable in HAS. Second, each of these: weak completeness for classical predicate logic, weak completeness for the negative fragment of intuitionistic predicate logic and strong completeness for sentential logic implics MP. Beth and Kripke completeness for intuitionistic predicate or sentential logic also entail MP.These results give extensions of the theorem of Gödel and Kreisel (in [4]) that completeness for pure intuitionistic predicate logic requires MP. The assumptions of Gödel and Kreisel's original proof included the Axiom of Dependent Choice and Herbrand's Theorem, no use of which is explicit in the present article.     

Modal logic and model theory

We propose a first order modal logic, theQS4E-logic, obtained by adding to the well-known first order modal logicQS4 arigidity axiom schemas:A → □A, whereA denotes a basic formula. In this logic, thepossibility entails the possibility of extending a given classical first order model. This allows us to express some important concepts of classical model theory, such as existential completeness and the state of being infinitely generic, that are not expressibile in classical first order logic. Since they can be expressed in -logic, we are also induced to compare the expressive powers ofQS4E and . Some questions concerning the power of rigidity axiom are also examined.     

Omega-consistency and the diamond

G is the result of adjoining the schema (qAA)qA to K; the axioms of G* are the theorems of G and the instances of the schema qAA and the sole rule of G* is modus ponens. A sentence is -provable if it is provable in P(eano) A(rithmetic) by one application of the -rule; equivalently, if its negation is -inconsistent in PA. Let -Bew(x) be the natural formalization of the notion of -provability. For any modal sentence A and function mapping sentence letters to sentences of PA, inductively define A by: p = (p) (p a sentence letter); = ; (AB)su}= (A B); and (qA)= -Bew(A )(S) is the numeral for the Gödel number of the sentence S). Then, applying techniques of Solovay (Israel Journal of Mathematics 25, pp. 287–304), we prove that for every modal sentence A, _G A iff for all , _PA A ; and for every modal sentence A, _G* A iff for all , A is true.I should like to thank David Auerbach and Rohit Parikh.