This chapter presents a new semantics for inductive empirical knowledge. The epistemic agent is represented concretely as a learner who processes new inputs through time and who forms new beliefs from those inputs by means of a concrete, computable learning program. The agent’s belief state is represented hyper-intensionally as a set of time-indexed sentences. Knowledge is interpreted as avoidance of error in the limit and as having converged to true belief from the present time onward. Familiar topics are re-examined within (...) the semantics, such as inductive skepticism, the logic of discovery, Duhem’s problem, the articulation of theories by auxiliary hypotheses, the role of serendipity in scientific knowledge, Fitch’s paradox, deductive closure of knowability, whether one can know inductively that one knows inductively, whether one can know inductively that one does not know inductively, and whether expert instruction can spread common inductive knowledge—as opposed to mere, true belief—through a community of gullible pupils. (shrink)

The Craig Interpolation Theorem is intimately connected with the emergence of abstract logic and continues to be the driving force of the field. I will argue in this paper that the interpolation property is an important litmus test in abstract model theory for identifying “natural,” robust extensions of first order logic. My argument is supported by the observation that logics which satisfy the interpolation property usually also satisfy a Lindström type maximality theorem. Admittedly, the range of such logics is small.

Gaifman's normal form theorem showed that every first-order sentence of quantifier rank n is equivalent to a Boolean combination of “scattered local sentences”, where the local neighborhoods have radius at most 7n−1. This bound was improved by Lifsches and Shelah to 3×4n−1. We use Ehrenfeucht–Fraïssé type games with a “shrinking horizon” to get a spectrum of normal form theorems of the Gaifman type, depending on the rate of shrinking. This spectrum includes the result of Lifsches and Shelah, with a more (...) easily understood proof and with the bound on the radius improved to 4n−1. We also obtain bounds for a normal form theorem of Schwentick and Barthelmann. (shrink)

Inexpressibility results in Finite Model Theory are often proved by showing that Duplicator, one of the two players of an Ehrenfeucht game, has a winning strategy on certain structures.In this article a new method is introduced that allows, under certain conditions, the extension of a winning strategy of Duplicator on some small parts of two finite structures to a global winning strategy.As applications of this technique it is shown that • — Graph Connectivity is not expressible in existential monadic second-order (...) logic , even in the presence of a built-in linear order,• — Graph Connectivity is not expressible in MonNP even in the presence of arbitrary built-in relations of degree n0, and• — the presence of a built-in linear order gives MonNP more expressive power than the presence of a built-in successor relation. (shrink)

When a structure or class of structures admits an unbounded induction, we can do arithmetic on the stages of that induction: if only bounded inductions are admitted, then clearly each inductively definable relation can be defined using a finite explicit expression. Is the converse true? We examine evidence that the converse is true, in positive elementary induction . We present a stronger conjecture involving the language L consisting of all L∞ω formulas with a finite number of variables, and examine a (...) combinatorial property equivalent to “all L-definable relations are elementary”. (shrink)

In this paper, we initiate the study of Ehrenfeucht–Fraïssé games for some standard finite structures. Examples of such standard structures are equivalence relations, trees, unary relation structures, Boolean algebras, and some of their natural expansions. The paper concerns the following question that we call the Ehrenfeucht–Fraïssé problem. Given nω as a parameter, and two relational structures and from one of the classes of structures mentioned above, how efficient is it to decide if Duplicator wins the n-round EF game ? We (...) provide algorithms for solving the Ehrenfeucht–Fraïssé problem for the mentioned classes of structures. The running times of all the algorithms are bounded by constants. We obtain the values of these constants as functions of n. (shrink)

We show in this paper that the theory of ordinal addition of any fixed ordinal ωα, with α less than ωω, admits a quantifier elimination. This in particular gives a new proof for the decidability result first established in 1965 by R. Büchi using transfinite automata. Our proof is based on the Ehrenfeucht games, and we show that quantifier elimination go through generalized power.RésuméOn montre ici que, pour tout ordinal α inférieur à ωω, la théorie additive de ωα admet une (...) élimination des quantificateurs. On obtient ainsi une nouvelle preuve de la décidabilité de ces théories . On utilise ici les jeux d'Ehrenfeucht, avec un formalisme à la Ferrante et Rackoff, et on montre que le fait d'admettre une élimination des quantificateurs se transmet par produit généralisé. (shrink)

Khoussainov and Nerode [14] posed various open questions on model-theoretic properties of automatic structures. In this work we answer some of these questions by showing the following results: There is an uncountably categorical but not countably categorical theory for which only the prime model is automatic; There are complete theories with exactly 3,4,5,…3,4,5,… countable models, respectively, and every countable model is automatic; There is a complete theory for which exactly 2 models have an automatic presentation; If LOGSPACE=PLOGSPACE=P then there is (...) an uncountably categorical but not countably categorical theory for which the prime model does not have an automatic presentation but all the other countable models are automatic; There is a complete theory with countably many countable models for which the saturated model has an automatic presentation but the prime model does not have one. (shrink)

This paper develops the model theory of ordered structures that satisfy Keisler’s regularity scheme and its strengthening REF ${(\mathcal{L})}$ (the reflection scheme) which is an analogue of the reflection principle of Zermelo-Fraenkel set theory. Here ${\mathcal{L}}$ is a language with a distinguished linear order <, and REF ${(\mathcal {L})}$ consists of formulas of the form $$\exists x \forall y_{1} < x \ldots \forall y_{n} < x \varphi (y_{1},\ldots ,y_{n})\leftrightarrow \varphi^{ < x}(y_1, \ldots ,y_n),$$ where φ is an ${\mathcal{L}}$ -formula, φ (...) shrink)

We establish a general hierarchy theorem for quantifier classes in the infinitary logic L∞ωωon finite structures. In particular, it is shown that no infinitary formula with bounded number of universal quantifiers can express the negation of a transitive closure.This implies the solution of several open problems in finite model theory: On finite structures, positive transitive closure logic is not closed under negation. More generally the hierarchy defined by interleaving negation and transitive closure operators is strict. This proves a conjecture of (...) Immerman.We also separate the expressive power of several extensions of Datalog, giving new insight in the fine structure of stratified Datalog. (shrink)

We develop a variant of Least Fixed Point logic based on First Orderlogic with a relaxed version of guarded quantification. We develop aGame Theoretic Semantics of this logic, and find that under reasonableconditions, guarding quantification does not reduce the expressibilityof Least Fixed Point logic. But we also find that the guarded version ofa least fixed point algorithm may have a greater time complexity thanthe unguarded version, by a linear factor.

We study a generalization of the standard syntax and game-theoretic semantics of logic, which is based on a duality between two players, to a multiplayer setting. We define propositional and modal languages of multiplayer formulas, and provide them with a semantics involving a multiplayer game. Our focus is on the notion of equivalence between two formulas, which is defined by saying that two formulas are equivalent if under each valuation, the set of players with a winning strategy is the same (...) in the two respective associated games. We provide a derivation system which enumerates the pairs of equivalent formulas, both in the propositional case and in the modal case. Our approach is algebraic: We introduce multiplayer algebras as the analogue of Boolean algebras, and show, as the corresponding analog to Stone’s theorem, that these abstract multiplayer algebras can be represented as concrete ones which capture the game-theoretic semantics. For the modal case we prove a similar result. We also address the computational complexity of the problem whether two given multiplayer formulas are equivalent. In the propositional case, we show that this problem is co-NP-complete, whereas in the modal case, it is PSPACE-hard. (shrink)

This book illustrates the program of Logical-Informational Dynamics. Rational agents exploit the information available in the world in delicate ways, adopt a wide range of epistemic attitudes, and in that process, constantly change the world itself. Logical-Informational Dynamics is about logical systems putting such activities at center stage, focusing on the events by which we acquire information and change attitudes. Its contributions show many current logics of information and change at work, often in multi-agent settings where social behavior is essential, (...) and often stressing Johan van Benthem's pioneering work in establishing this program. However, this is not a Festschrift, but a rich tapestry for a field with a wealth of strands of its own. The reader will see the state of the art in such topics as information update, belief change, preference, learning over time, and strategic interaction in games. Moreover, no tight boundary has been enforced, and some chapters add more general mathematical or philosophical foundations or links to current trends in computer science. The theme of this book lies at the interface of many disciplines. Logic is the main methodology, but the various chapters cross easily between mathematics, computer science, philosophy, linguistics, cognitive and social sciences, while also ranging from pure theory to empirical work. Accordingly, the authors of this book represent a wide variety of original thinkers from different research communities. And their interconnected themes challenge at the same time how we think of logic, philosophy and computation. Thus, very much in line with van Benthem's work over many decades, the volume shows how all these disciplines form a natural unity in the perspective of dynamic logicians (broadly conceived) exploring their new themes today. And at the same time, in doing so, it offers a broader conception of logic with a certain grandeur, moving its horizons beyond the traditional study of consequence relations. (shrink)

We introduce a generalization of Independence Friendly logic in which Eloise is restricted to a finite amount of information about Abelard’s moves. This logic is shown to be equivalent to a sublogic of first-order logic, to have the finite model property, and to be decidable. Moreover, it gives an exponential compression relative to logic.

In this paper we develop an Ehrenfeucht‐Fraïssé game for. Unlike the standard Ehrenfeucht‐Fraïssé games which are modeled solely after the behavior of quantifiers, this new game also takes into account the behavior of connectives in logic. We prove the adequacy theorem for this game. We also apply the new game to prove complexity results about infinite binary strings.

The algebraic recursive structure of countable languages of classical first-order logic with equality is analysed. all languages of finite undecidable similarity type are shown to be algebraically and recursively equivalent in the following sense: their boolean algebras of formulas are, after trivial factors involving the one element models of the languages have been excepted, recursively isomorphic by a map which preserves the degree of recursiveness of their models.

An overview of different versions and applications of Lorenzen’s dialogue game approach to the foundations of logic, here largely restricted to the realm of manyvalued logics, is presented. Among the reviewed concepts and results are Giles’s characterization of Łukasiewicz logic and some of its generalizations to other fuzzy logics, including interval based logics, a parallel version of Lorenzen’s game for intuitionistic logic that is adequate for finite- and infinite-valued Gödel logics, and a truth comparison game for infinite-valued Gödel logic.

The classical Feferman–Vaught Theorem for First Order Logic explains how to compute the truth value of a first order sentence in a generalized product of first order structures by reducing this computation to the computation of truth values of other first order sentences in the factors and evaluation of a monadic second order sentence in the index structure. This technique was later extended by Läuchli, Shelah and Gurevich to monadic second order logic. The technique has wide applications in decidability and (...) definability theory. Here we give a unified presentation, including some new results, of how to use the Feferman–Vaught Theorem, and some new variations thereof, algorithmically in the case of Monadic Second Order Logic MSOL . We then extend the technique to graph polynomials where the range of the summation of the monomials is definable in MSOL . Here the Feferman–Vaught Theorem for these polynomials generalizes well known splitting theorems for graph polynomials. Again, these can be used algorithmically. Finally, we discuss extensions of MSOL for which the Feferman–Vaught Theorem holds as well. (shrink)

The first-order logical theory Th $({\mathbb{N}},x + 1,F(x))$ is proved to be complete for the class ATIME-ALT $(2^{O(n)},O(n))$ when $F(x) = 2^{x}$ , and the same result holds for $F(x) = c^{x}, x^{c} (c \in {\mathbb{N}}, c \ge 2)$ , and F(x) = tower of x powers of two. The difficult part is the upper bound, which is obtained by using a bounded Ehrenfeucht–Fraïssé game.

Inquisitive first-order logic, InqBQ, is a system which extends classical first-order logic with formulas expressing questions. From a mathematical point of view, formulas in this logic express properties of sets of relational structures. This paper makes two contributions to the study of this logic. First, we describe an Ehrenfeucht–Fraïssé game for InqBQ and show that it characterizes the distinguishing power of the logic. Second, we use the game to study cardinality quantifiers in the inquisitive setting. That is, we study what (...) statements and questions can be expressed in InqBQ about the number of individuals satisfying a given predicate. As special cases, we show that several variants of the question how many individuals satisfy α(x) are not expressible in InqBQ, both in the general case and in restriction to finite models. (shrink)

We say that a first order sentence A defines a graph G if A is true on G but false on any graph non-isomorphic to G. Let L ) denote the minimum length of such a sentence. We define the succinctness function s ) to be the minimum L ) over all graphs on n vertices.We prove that s and q may be so small that for no general recursive function f we can have f)≥n for all n. However, for (...) the function q*=maxi≤nq, which is the least nondecreasing function bounding q from above, we have q*=)log*n, where log*n equals the minimum number of iterations of the binary logarithm sufficient to lower n to 1 or below.We show an upper bound qshrink)

A linear order is -decidable if its universe is and the relations defined by formulas are uniformly computable. This means that there is a computable procedure which, when applied to a formula and a sequence of elements of the linear order, will determine whether or not is true in the structure. A linear order is decidable if the relations defined by all formulas are uniformly computable. These definitions suggest two questions. Are there, for each , -decidable linear orders that are (...) not -decidable? Are there linear orders that are -decidable for all but not decidable? The former was answered in the positive by Moses in 1993. Here we answer the latter, also positively. (shrink)