Modified realizability and predicate logic

Semantics of predicate formulas based on the notion of modified realizability for arithmetic formulas and interpretations of the language of arithmetic in all finite types are considered. For a number of natural constructive interpretations, the corresponding predicate logic of modified realizability is proved to be nonarithmetical. Translated fromMatematicheskie Zametki, Vol. 61, No. 2, pp. 259–269, February, 1997. This research was supported by the Russian Foundation for Basic Research under grant No. 95-01-00416 and by the International Science Foundation under grant No. NFQ000. Translated by V. N. Dubrovsky     

On arithmetic complexity of certain constructive logics

A constructive arithmetical theory is an arbitrary set of closed arithmetical formulas that is closed with respect to derivability in an intuitionsitic arithmetic with the Markov principle and the formal Church thesis. For each arithmetical theory T there is a corresponding logic L(T) consisting of closed predicate formulas in which all arithmetic instances belong to T. For so-called internally enumerable constructive arithmetical theories with the property of existentiality, it is proved that the logic L(T) is II₁ ^T -@#@ complete. This implies, for example, that the logic of traditional constructivism is II₂ ⁰-complete.Translated from Matematicheskie Zametki, Vol. 52, No. 1, pp. 94–104, July, 1992.     

Interpolation in superintuitionistic predicate logics with equality

It is shown that the Craig interpolation property and the Beth property are preserved under passage from a superintuitionistic predicate logic to its extension via standard axioms for equality, and under adding formulas of pure equality as new axioms. We find an infinite independent set of formulas which, though not equivalent to formulas of pure equality, may likewise be added as new axiom schemes without loss of the interpolation, or Beth, property. The formulas are used to construct a continuum of logics with equality, which are intermediate between the intuitionistic and classical ones, having the interpolation property. Moreover, an equality-free fragment of the logics constructed is an intuitionistic predicate logic, and formulas of pure equality satisfy all axioms of the classical predicate logic. Supported by RFFR grant No. 96-01-01552. Translated fromAlgebra i Logika, Vol. 36, No. 5, pp. 543–561, September–October, 1997.     

一阶模糊谓词逻辑公式的解释模型真度理论及其应用

基于一阶模糊谓词逻辑公式的有限和可数解释真度的理论,引入了一阶模糊谓词逻辑公式的解释模型及解释模型真度的概念,并讨论了它们的一系列性质及其在近似推理中的应用.     

Arithmetical realizability and basic logic

Absolute arithmetical realizability of predicate formulas is introduced. It is proved that the intuitionistic logic is not correct with this semantics, but the basic logic is correct.     

A method of epsilon substitution for the predicate logic with equality

The method of epsilon substitution was defined for arithmetic with interpretation of αxA(x) as the least x satisfying A(x). It proceeds by a series of finite approximations “from below” to a solution of a fixed system of critical formulas. For the predicate logic only approach “from above” similar to cut-elimination was available. We present a definition of epsilon substitution for the predicate logic, prove the termination of the substitution process, and derive the corresponding Herbrand-type theorem. Bibliography: 18 titles. Translated fromZapiski Nauchnykh Seminarov POMI, Vol. 220, 1995, pp. 93–122. Translated by G. E. Mints.     

On the completeness and the decidability of strictly monadic second-order logic

Regarding strictly monadic second-order logic (SMSOL), which is the fragment of monadic second-order logic in which all predicate constants are unary and there are no function symbols, we show that a standard deductive system with full comprehension is sound and complete with respect to standard semantics. This result is achieved by showing that in the case of SMSOL, the truth value of any formula in a faithful identity-standard Henkin structure is preserved when the structure is “standardized”; that is, the predicate domain is expanded into the set of all unary relations. In addition, we obtain a simpler proof of the decidability of SMSOL.     

TOPOS BASED SEMANTIC FOR CONSTRUCTIVE LOGIC WITH STRONG NEGATION

The aim of the paper is to show that topoi are useful in the categorial analysis of the constructive logic with strong negation. In any topos ? we can distinguish an object Λ and its truth-arrows such that sets ?(A, Λ) (for any object A) have a Nelson algebra structure. The object Λ is defined by the categorial counterpart of the algebraic FIDEL-VAKARELOV construction. Then it is possible to define the universal quantifier morphism which permits us to make the first order predicate calculus. The completeness theorem is proved using the Kripke-type semantic defined by THOMASON .     

The classical decision problem and partial functions

We consider the decision problem for sets of sentences of first-order logic when instead of interpreting function symbols as total functions over the universe of a model (henceforth referred to as the usual interpretation) we interpret them as partial functions.We consider only standard classes, which are certain sets of prenex sentences specified by restrictions on the prefix and on the numbers ofk-place predicate and function symbols for eachk1. Standard classes are introduced in [1] and it is proved there that the decision problem for any set of prenex sentences specified by such restrictions reduces to that for the standard classes.We solve the decision problem completely for standard classes with at least one function symbol and both with and without equality.This problem was suggested to me by my supervisor, Professor Yuri Gurevich who was confident that the results would be very similar to those for the usual interpretation and could be achieved by similar techniques.     

Glivenko sequent classes in the light of structural proof theory

In 1968, Orevkov presented proofs of conservativity of classical over intuitionistic and minimal predicate logic with equality for seven classes of sequents, what are known as Glivenko classes. The proofs of these results, important in the literature on the constructive content of classical theories, have remained somehow cryptic. In this paper, direct proofs for more general extensions are given for each class by exploiting the structural properties of G3 sequent calculi; for five of the seven classes the results are strengthened to height-preserving statements, and it is further shown that the constructive and minimal proofs are identical in structure to the classical proof from which they are obtained.     

A Weak Constructive Second-Order Arithmetic with Extraction of Algorithms Computable in Polynomial Time

In this paper, a family of weak constructive theories, containing arithmetic and a theory of natural-valued functions of natural arguments, is suggested. The functions are polynomially bounded and computable in time bounded by polynomials in their arguments. The languages of these theories contain functional constants for addition and multiplication and the equality predicate. Other functional constants are also allowed, provided that the corresponding functions satisfy the above conditions of polynomial boundedness. From the proofs of the theories considered witness functions for provable formulas, computable in polynomial time, can algorithmically be extracted. If an argument of a witness is a function, then the latter is used in the witness algorithm as an oracle. Bibliography: 2 titles.__________Translated from Zapiski Nauchnykh Seminarov POMI, Vol. 304, 2003, pp. 7–12.     

A survey of predicate realizability logic

The paper contains a survey of the results and methods of studying interpretations of predicate formulas based on constructive semantics of the first-order language of arithmetic and its extensions.     

The atomic theory of multiplication and division of semiring ideals

We consider two-sided ideals of semirings. More precisely, we study the theory of two-sided ideals in the signature consisting of the predicate symbol ⊆ and three function symbols that denote the multiplication, right division, and left division of ideals. We prove that the set of those atomic formulas in this signature that are valid for all semirings and all valuations is decidable.     

Refined hierarchy of formulas

In this paper a hierarchy of predicate logic which refines the hierarchy by the number of quantor alterations is introduced and studied. Theorem 1 shows that the hierarchy constructed is the most refined in a certain sense. Theorem 2 describes hierarchy classes in terms of properties of the corresponding models. In Theorems 3 and 4, the connection between the hierarchy of formulas and the hierarchy of sets presented in [1] and the index sets is studied.Translated from Algebra i Logika, Vol. 30, No. 5, pp. 568–582, September–October, 1991.     

The atomic theory of division of semiring ideals

We consider two-sided ideals of semirings. More precisely, we study the theory of two-sided ideals in the signature consisting of the predicate symbol ⊆ and two function symbols that denote the right and left division of ideals. We prove that the set of those atomic formulas in this signature that are valid for all semirings and all valuations is decidable. __________ Translated from Fundamentalnaya i Prikladnaya Matematika, Vol. 12, No. 2, pp. 201–208, 2006.     

On interplay of quantifiers in Gödel-Dummett fuzzy logics

Axiomatization of Gödel-Dummett predicate logics S2G, S3G, and PG, where PG is the weakest logic in which all prenex operations are sound, and the relationships of these logics to logics known from the literature are discussed. Examples of non-prenexable formulas are given for those logics where some prenex operation is not available. Inter-expressibility of quantifiers is explored for each of the considered logics.     

Advances in the ŁΠ and logics

 The ŁΠ and logics were introduced by Godo, Esteva and Montagna. These logics extend many other known propositional and predicate logics, including the three mainly investigated ones (G?del, product and Łukasiewicz logic). The aim of this paper is to show some advances in this field. We will see further reduction of the axiomatic systems for both logics. Then we will see many other logics contained in the ŁΠ family of logics (namely logics induced by the continuous finitely constructed t-norms and Takeuti and Titani's fuzzy predicate logic). Received: 1 October 2000 / Revised version: 27 March 2002 / Published online: 5 November 2002 Partial support of the grant No. A103004/00 of the Grant agency of the Academy of Sciences of the Czech Republic is acknowledged. Key words or phrases: Fuzzy logic – Łukasiewicz logic – Product logic     

The Skolemization of prenex formulas in intermediate logics

The skolem class of a logic consists of the formulas for which the derivability of the formula is equivalent to the derivability of its Skolemization. In contrast to classical logic, the skolem classes of many intermediate logics do not contain all formulas. In this paper it is proven for certain classes of propositional formulas that any instance of them by (independent) predicate sentences in prenex normal form belongs to the skolem class of any intermediate logic complete with respect to a class of well-founded trees. In particular, all prenex sentences belong to the skolem class of these logics, and this result extends to the constant domain versions of these logics.