Magidor–Malitz reflection

In this paper we investigate the consistency and consequences of the downward Löwenheim–Skolem–Tarski theorem for extension of the first order logic by the Magidor–Malitz quantifier. We derive some combinatorial results and improve the known upper bound for the consistency of Chang’s conjecture at successor of singular cardinals.     

Non‐elementary speed‐ups in logic calculi

In this paper we show some non‐elementary speed‐ups in logic calculi: Both a predicative second‐order logic and a logic for fixed points of positive formulas are shown to have non‐elementary speed‐ups over first‐order logic. Also it is shown that eliminating second‐order cut formulas in second‐order logic has to increase sizes of proofs super‐exponentially, and the same in eliminating second‐order epsilon axioms. These are proved by relying on results due to P. Pudlák. (© 2008 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

The two‐variable fragment with counting and equivalence

We consider the two‐variable fragment of first‐order logic with counting, subject to the stipulation that a single distinguished binary predicate be interpreted as an equivalence. We show that the satisfiability and finite satisfiability problems for this logic are both NExpTime ‐complete. We further show that the corresponding problems for two‐variable first‐order logic with counting and two equivalences are both undecidable.     

THE FUNDAMENTAL THEOREM OF ULTRAPRODUCT IN PAVELKA'S LOGIC

In [This Zeitschrift 25 (1979), 45-52, 119-134, 447-464], Pavelka systematically discussed propositional calculi with values in enriched residuated lattices and developed a general framework for approximate reasoning. In the first part of this paper we introduce the concept of generalized quantifiers into Pavelka's logic and establish the fundamental theorem of ultraproduct in first order Pavelka's logic with generalized quantifiers. In the second part of this paper we show that the fundamental theorem of ultraproduct in first order Pavelka's logic is preserved under some direct product of lattices of truth values.     

Intuitionistic ϵ- and τ-calculi

There are several open problems in the study of the calculi which result from adding either of Hilbert's ?- or τ-operators to the first order intuitionistic predicate calculus. This paper provides answers to several of them. In particular, the first complete and sound semantics for these calculi are presented, in both a “quasi-extensional” version which uses choice functions in a straightforward way to interpret the ?- or τ-terms, and in a form which does not require extensionality assumptions. Unlike the classical case, the addition of either operator to intuitionistic logic is non-conservative. Several interesting consequences of the addition of each operator are proved. Finally, the independence of several other schemes in either calculus are also proved, making use of the semantics supplied earlier in the paper.     

Logic as a Science and Logic as a Theory: Remarks on Frege, Russell and the Logocentric Predicament

Since its publication in 1967, van Heijenoort??s paper, ??Logic as Calculus and Logic as Language?? has become a classic in the historiography of modern logic. According to van Heijenoort, the contrast between the two conceptions of logic provides the key to many philosophical issues underlying the entire classical period of modern logic, the period from Frege??s Begriffsschrift (1879) to the work of Herbrand, G?del and Tarski in the late 1920s and early 1930s. The present paper is a critical reflection on some aspects of van Heijenoort??s thesis. I concentrate on the case of Frege and Russell and the claim that their philosophies of logic are marked through and through by acceptance of the universalist conception of logic, which is an integral part of the view of logic as language. Using the so-called ??Logocentric Predicament?? (Henry M. Sheffer) as an illustration, I shall argue that the universalist conception does not have the consequences drawn from it by the van Heijenoort tradition. The crucial element here is that we draw a distinction between logic as a universal science and logic as a theory. According to both Frege and Russell, logic is first and foremost a universal science, which is concerned with the principles governing inferential transitions between propositions; but this in no way excludes the possibility of studying logic also as a theory, i.e., as an explicit formulation of (some) of these principles. Some aspects of this distinction will be discussed.     

Horn clause computability

It is proved that a Turing computable functionf is computable in binary Horn clauses, which are a subset of first order logic. Moreover, it is proved that the binary Horn clauses do not need more than one function symbol. The proofs comprise computable relations that can be run efficiently as logic programs on a computer.     

Binary Relations and Permutation Groups

We discuss some new properties of the natural Galois connection among set relation algebras, permutation groups, and first order logic. In particular, we exhibit infinitely many permutational relation algebras without a Galois closed representation, and we also show that every relation algebra on a set with at most six elements is Galois closed and essentially unique. Thus, we obtain the surprising result that on such sets, logic with three variables is as powerful in expression as full first order logic.     

New methods for computing inferences in first order logic

Recent improvements in satisfiability algorithms for propositional logic have made partial instantiation methods for first order predicate logic computationally more attractive. Two such methods have been proposed, one by Jeroslow and a hypergraph method for datalog formulas by Gallo and Rago. We show that they are instances of two general approaches to partial instantiation, and we develop these approaches for a large decidable fragment of first order logic (the fragment).Working Paper 1991-11. Supported in part by the Air Force Office of Scientific Research, Grant number AFOSR-87-0292.     

Finite satisfiability for two‐variable,first‐order logic with one transitive relation is decidable

We consider two‐variable, first‐order logic in which a single distinguished predicate is required to be interpreted as a transitive relation. We show that the finite satisfiability problem for this logic is decidable in triply exponential non‐deterministic time. Complexity falls to doubly exponential non‐deterministic time if the transitive relation is constrained to be a partial order.     

Saturated calculus for Horn-like sequents of a complete class of a linear temporal first order logic

A saturated calculus for the so-called Horn-like sequents of a complete class of a linear temporal logic of the first order is described. The saturated calculus contains neither induction-like postulates nor cut-like rules. Instead of induction-like postulates the saturated calculus contains a finite set of “saturated” sequents, which (1) capture and reflect the periodic structure of inductive reasoning (i.e., a reasoning which applies induction-like postulates); (2) show that “almost nothing new” can be obtained by continuing the process of derivation of a given sequent; (3) present an explicit way of generating the so-called invariant formula in induction-like rules. The saturated calculus for Horn-like sequents allows one: (1) to prove in an obvious way the completeness of a restricted linear temporal logic of the first order; (2) to construct a computer-aided proof system for this logic; (3) to prove the decidability of this logic for logically decidable Horn-like sequents. Bibliography: 15 titles. Translated fromZapiski Nauchnykh Seminarov POMI, Vol. 220, 1995, pp. 123–144. Translated by R. Pliuškevičius.     

Remarks on Martin-Löf's partial type theory

In this paper we discuss Martin-Löf's partial type theory, that is type theory with general recursion, and in particular the consequences of the presence of a fixed point operator. We model Martin-Löf's logical framework domain-theoretically in the category of conditional upper semi lattices and parametrizations thereof. An interpretation of a type of sets in the logical framework, which defines partial type theory with one universe, is finally described.During the preparation of this paper, the first author was supported by the Swedish Natural Science Research Council as a PhD-student in mathematical logic.     

An Algebraic Approach to Knowledge Base Models Informational Equivalence

In this paper we study the notion of knowledge from the positions of universal algebra and algebraic logic. We consider first order knowledge which is based on first order logic. We define categories of knowledge and knowledge base models. These notions are defined for the fixed subject of knowledge. The key notion of informational equivalence of two knowledge base models is introduced. We use the idea of equivalence of categories in this definition. We prove that for finite models there is a clear way to determine whether the knowledge base models are informationally equivalent.     

Sémantique algébrique ďun système logique basé sur un ensemble ordonné fini

In order to modelize the reasoning of an intelligent agent represented by a poset T, H. Rasiowa introduced logic systems called “Approximation Logics”. In these systems a set of constants constitutes a fundamental tool. In this papers, we consider logic systems called L′_T without this kind of constants but limited to the case where T is a finite poset. We prove a weak deduction theorem. We introduce also an algebraic semantics using Hey ting algebra with operators. To prove the completeness theorem of the L′_T system with respect to the algebraic semantics, we use the method of H. Rasiowa and R. Sikorski for first order logic. In the propositional case, a corollary allows us to assert that it is decidable to know “if a propositional formula is valid”. We study also certain relations between the L′_T logic and the intuitionistic and classical logics.     

SO(∀∃*) Sentences and Their Asymptotic Probabilities

We prove a 0‐1 law for the fragment of second order logic SO(∀∃*) over parametric classes of finite structures which allow only one unary atomic type. This completes the investigation of 0‐1 laws for fragments of second order logic defined in terms of first order quantifier prefixes over, e.g., simple graphs and tournaments. We also prove a low oscillation law, and establish the 0‐1 law for Σ¹₄(∀∃*) without any restriction on the number of unary types.     

0–1 laws for maps

A class of finite structures has a 0–1 law with respect to a logic if every property expressible in the logic has a probability approaching a limit of 0 or 1 as the structure size grows. To formulate 0–1 laws for maps (i.e., embeddings of graphs in a surface), it is necessary to represent maps as logical structures. Three such representations are given, the most general being the full cross representation based on Tutte's theory of combinatorial maps. The main result says that if a class of maps has two properties, richness and large representativity, then the corresponding class of full cross representations has a 0–1 law with respect to first‐order logic. As a corollary the following classes of maps on a surface of fixed type have a first‐order 0–1 law: all maps, smooth maps, 2‐connected maps, 3‐connected maps, triangular maps, 2‐connected triangular maps, and 3‐connected triangular maps. ©1999 John Wiley & Sons, Inc. Random Struct. Alg., 14, 215–237, 1999     

On contraction and the modal fragment

We observe that removing contraction from a standard sequent calculus for first‐order predicate logic preserves completeness for the modal fragment. (© 2008 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Negation and partial axiomatizations of dependence and independence logic revisited

In this paper, we axiomatize the negatable consequences in dependence and independence logic by extending the systems of natural deduction of the logics given in [22] and [11]. We prove a characterization theorem for negatable formulas in independence logic and negatable sentences in dependence logic, and identify an interesting class of formulas that are negatable in independence logic. Dependence and independence atoms, first-order formulas belong to this class. We also demonstrate our extended system of independence logic by giving explicit derivations for Armstrong's Axioms and the Geiger-Paz-Pearl axioms of dependence and independence atoms.     

Properties of Tense Logics

Based on the results of [11] this paper delivers uniform algorithms for deciding whether a finitely axiomatizable tense logic

• has the finite model property,
• is complete with respect to Kripke semantics,
• is strongly complete with respect to Kripke semantics,
• is d-persistent,
• is r-persistent.

It is also proved that a tense logic is strongly complete iff the corresponding variety of bimodal algebras is complex, and that a tense logic is d-persistent iff it is complete and its Kripke frames form a first order definable class. From this we obtain many natural non-d-persistent tense logics whose corresponding varieties of bimodal algebras are complex. Mathematics Subject Classification: 03B45, 03B25.     

The expressive power of k-ary exclusion logic

In this paper we study the expressive power of k-ary exclusion logic, EXC[k], that is obtained by extending first order logic with k-ary exclusion atoms. It is known that without arity bounds exclusion logic is equivalent with dependence logic. By observing the translations, we see that the expressive power of EXC[k] lies in between k-ary and ($k+1$)-ary dependence logics. We will show that, at least in the case when $k=1$, both of these inclusions are proper.In a recent work by the author it was shown that k-ary inclusion-exclusion logic is equivalent with k-ary existential second order logic, ESO[k]. We will show that, on the level of sentences, it is possible to simulate inclusion atoms with exclusion atoms, and in this way express ESO[k]-sentences by using only k-ary exclusion atoms. For this translation we also need to introduce a novel method for “unifying” the values of certain variables in a team. As a consequence, EXC[k] captures ESO[k] on the level of sentences, and we obtain a strict arity hierarchy for exclusion logic. It also follows that k-ary inclusion logic is strictly weaker than EXC[k].Finally we use similar techniques to formulate a translation from ESO[k] to k-ary inclusion logic with an alternative strict semantics. Consequently, for any arity fragment of inclusion logic, strict semantics is strictly more expressive than lax semantics.