Intensional models for the theory of types

In this paper we define intensional models for the classical theory of types, thus arriving at an intensional type logic ITL. Intensional models generalize Henkin's general models and have a natural definition. As a class they do not validate the axiom of Extensionality. We give a cut-free sequent calculus for type theory and show completeness of this calculus with respect to the class of intensional models via a model existence theorem. After this we turn our attention to applications. Firstly, it is argued that, since ITL is truly intensional, it can be used to model ascriptions of propositional attitude without predicting logical omniscience. In order to illustrate this a small fragment of English is defined and provided with an ITL semantics. Secondly, it is shown that ITL models contain certain objects that can be identified with possible worlds. Essential elements of modal logic become available within classical type theory once the axiom of Extensionality is given up.

Systematization of finite many-valued logics through the method of tableaux

This paper presents a unified treatment of the propositional and first-order many-valued logics through the method of tableaux. It is shown that several important results on the proof theory and model theory of those logics can be obtained in a general way.We obtain, in this direction, abstract versions of the completeness theorem, model existence theorem (using a generalization of the classical analytic consistency properties), compactness theorem and Löwenheim-Skolem theorem.The paper is completely self-contained and includes examples of application to particular many-valued formal systems.

Model existence theorem in algorithmic logic with non-deterministic programs1

The paper is a continuation of the considerations connected with non-deterministic algorithmic logic. We will formulate a Hilbert style axiomatization basing on the analogous one defined for algorithmic logic. The main result is the theorem asserting that every consistent non-deterministic algorithmic theory possesses a model.

Fragments of first order logic, I: universal Horn logic

Let L be any finitary language. By restricting our attention to the universal Horn sentences of L and appealing to a semantical notion of logical consequence, we can formulate the universal Horn logic of L. The present paper provides some theorems about universal Horn logic that serve to distinguish it from the full first order predicate logic. Universal Horn equivalence between structures is characterized in two ways, one resembling Kochen's ultralimit theorem. A sharp version of Beth's definability theorem is established for universal Horn logic by means of a reduced product construction. The notion of a consistency property is relativized to universal Horn logic and the corresponding model existence theorem is proven. Using the model existence theorem another proof of the definability result is presented. The relativized consistency properties also suggest a syntactical notion of proof that lies entirely within the universal Horn logic. Finally, a decision problem in universal Horn logic is discussed. It is shown that the set of universal Horn sentences preserved under the formation of homomorphic images (or direct factors) is not recursive, provided the language has at least two unary function symbols or at least one function symbol of rank more than one.This paper begins with a discussion of how algebraic relations between structures can be used to obtain fragments of a given logic. Only two such fragments seem to be under current investigation: equational logic and universal Horn logic. Other fragments which seem interesting are pointed out.