A new decidable Horn fragment of predicate calculus

We describe an extension of the class ∀∃ of Horn formulas in predicate calculus. We prove the decidability of this class. We describe complexity characteristics such that fixing them splits this extended class into polynomially decidable subclasses. Fixing the maximum arity of predicates splits our class into subclasses belonging to NP. Bibliography: 11 titles. __________ Translated from Zapiski Nauchnykh Seminarov POMI, Vol. 316, 2004, pp. 147–162.     

Primitive recursive estimate of strong normalization for predicate calculus

The strong normalization theorem asserts that any sequence of reductions (standard steps of cut elimination) stops at an object in normal form, i.e., at an object to which further reductions are inapplicable. The most intuitive proofs of strong normalization for various systems, including first- and second-order arithmetic, use, essentially, the concept of hereditary normalizability of an object. This concept, for objects of unbounded complexity, cannot be expressed in the language of arithmetic, so that the proofs mentioned leave its domain. Howard's proof for arithmetic, using nonunique assignment of ordinals, apparently, can be modified so as to get a primitive recursive proof of strict normalizability for the -fragment of the intuitionistic predicate calculus, but the author of the present paper has not succeeded in overcoming the combinatorial difficulties. Our goal is to give an intuitive proof for the predicate calculus, from which one can extract a primitive recursive estimate of the number of reductions, and a proof in primitive recursive arithmetic of the fact that this estimate is proper. The proof of normalizability, that is, the construction of a special reduction sequence stopping at a normal term, is well known. In this sequence one first converts subterms of the highest levell, and first the innermost of them. (Corresponding to this, in the proof one can apply reduction with respect to level.) Here the number of convertible terms of maximal level, suitable for reduction, is lowered and the newly arising convertible terms have lower level.Translated from Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im. V. A. Steklova AN SSSR, Vol. 88, pp. 131–135, 1979.     

Constructing integer programming models by the predicate calculus

A modelling language for Integer Programming (IP) based on the Predicate Calculus is described. This is particularly suitable for building models with logical conditions. Using this language a model is specified in terms of predicates. This is then converted automatically by a series of transformation rules into a normal form from which an IP model can be created. There is also some discussion of alternative IP formulations which can be incorporated into the system as options. Further practical considerations are discussed briefly concerning implementation language and incorporation into practical Mathematical Programming Systems.     

Decidability of a portion of the predicate calculus

We show decidability of the existence of a model (a finite model) for sentences with the string of quantifiers ∀x(∃y ₁...y _n), for a language with equality, one one-place function, predicates and constants. I would like to thank the Israel Academy of Science and Humanities for partially supporting this research by a grant.     

Completeness of two systems of illative combinatory logic for first-order propositional and predicate calculus

Illative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants (and corresponding axioms and rules) intended to capture inference. The paper considers 4 systems of illative combinatory logic that are sound for first-order propositional and predicate calculus. The interpretation from ordinary logic into the illative systems can be done in two ways: following the propositions-as-types paradigm, in which derivations become combinators, or in a more direct way, in which derivations are not translated. Both translations are closely related in a canonical way. In a preceding paper, Barendregt, Bunder and Dekkers, 1993, we proved completeness of the two direct translations. In the present paper we prove completeness of the two indirect translations by showing that the corresponding illative systems are conservative over the two systems for the direct translations. In another version, DBB (1997), we shall give a more direct completeness proof. These papers fulfill the program of Church and Curry to base logic on a consistent system of -terms or combinators. Hitherto this program had failed because systems of ICL were either too weak (to provide a sound interpretation) or too strong (sometimes even inconsistent). Received: February 15, 1996     

A measure-theoretic axiomatization of fuzzy sets

Using measurement theory, this paper examines three empirical structures that underlie the representation of fuzzy sets: the fuzzy membership structure, the fuzzy component structure, and the fuzzy system structure. These qualitative structures justify the use of the standard min-max system to represent fuzzy sets. The results of this study facilitate the development of a sound measurement-theoretic axiomatization of fuzzy systems.     

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.