Gazzari provides a mathematical theory of occurrences and of substitutions, which are a generalisation of occurrences constituting substitution functions. The dissertation focusses on term occurrences in terms of a first order language, but the methods and results obtained there can easily be carried over to arbitrary kinds of occurrences in arbitrary kinds of languages.

The aim of the dissertation is twofold: first, Gazzari intends to provide an adequate formal representation of philosophically relevant concepts (not only of occurrences and substitutions, but also of substitution functions, of calculations as well as of intuitively given properties of the discussed entities) and to improve this way our understanding of these concepts; second, he intends to provide a formal exploration of the introduced concepts including the detailed development of the methods needed for their adequate treatment.

The dissertation serves as a methodological fundament for consecutive research on topics demanding a precise treatment of occurrences and as a foundation for all scientific work dealing with occurrences only informally; the formal investigations are complemented by a brief survey of the development of the notion of occurrences in mathematics, philosophy and computer science.

The notion of occurrences. Occurrences are determined by three aspects: an occurrence is always an occurrence of a syntactic entity (its shape) in a syntactic entity (its context) at a specific position. Context and shape can be any meaningful combination of well-known syntactic entities as, in logic, terms, formulae or formula trees. Gazzari’s crucial idea is to represent the position of occurrences by nominal forms, essentially as introduced by Schütte [2]. The nominal forms are a generalisation of standard syntactic entities in which so called nominal symbols $*_k$ may occur. The position of an occurrence is obtained by eliminating the intended shape in the context, which means to replace the intended shape by suitable nominal symbols.

Standard occurrences. Central tool of the theory of nominal terms (nominal forms generalising standard terms) is the general substitution function mapping a nominal term $\mathtt {t}$ and a sequence $\vec {\mathtt {t}}$ of them to the result $\mathtt {t}[\vec {\mathtt {t}}]$ of replacing simultaneously the nominal symbols $*_k$ in the first argument by the respective entries $\mathtt {t}_k$ of the second argument.

A triple $\mathfrak {o}=\langle {t,s,\mathtt {t}} \rangle $ is a standard occurrence, if an application of the general substitution function on the position $\mathtt {t}$ and the shape s results in the context t of that occurrence. As $*_0$ can occur more than once in $\mathtt {t}$ , arbitrary many single occurrences in the context t of the common shape s can be subsumed in $\mathfrak {o}$ .1 Gazzari illustrates the appropriateness of his approach by solving typical problems (counting formally the number of specific occurrences, deciding whether an occurrence lies within another) which are not solvable without a good theory of occurrences.

Multi-shape occurrences. The multi-shape occurrences $\mathfrak {o}=\langle {t,\vec s,\mathtt {t}} \rangle $ are the generalisation of standard occurrences, where the shape $\vec s$ is a sequence of standard terms. Such occurrences subsume arbitrary non-overlapping single occurrences in the context t.

Gazzari addresses the non-trivial identity of such occurrences and their independence. The latter represents formally the idea of non-overlapping occurrences and is a far-reaching generalisation of disjointness as discussed by Huet with respect to single occurrences. Independent occurrences can be merged into one occurrence; an occurrence can be split up into independent occurrences.

Substitutions. A substitution $\mathbf s=\langle {t,\vec s,\mathtt {t},{\vec s}',t'} \rangle $ satisfies that both $\mathfrak {o}=\langle {t,\vec s,\mathtt {t}} \rangle $ and $\mathfrak {o}'=\langle {t',{\vec s}',\mathtt {t}} \rangle $ are occurrences such that the shapes have the same length. Such a substitution represents the replacement of $\vec s$ in t at $\mathtt {t}$ by $\vec s'$ resulting in $t'$ . This means that a substitution is understood as a process and not as a (specific type of a) function.

Identity and independence are addressed again, using and extending the methods developed for occurrences; as before, independent substitutions can be merged and substitutions can be split up into sequences of independent substitutions. Substitutions are used to represent formally calculations (as found in everyday mathematics) and to investigate them.

Sets of substitutions turn out to be set-theoretic functions mapping the affected occurrences $\mathfrak {o}$ and the inserted shapes ${\vec s}'$ to the result $t'$ of a substitution $\mathbf s$ . Such sets are called explicit substitution functions. In order to qualify functions which are usually understood as substitution functions (and which are not formulated in a theory of occurrences) as substitution functions, Gazzari develops the concept of an explication method transforming such functions into explicit substitution functions. The appropriateness and the (philosophical) limitations of this concept are illustrated with example functions.

Conclusion. Gazzari’s theory of occurrences is strong (not restricted to single occurrences), canonical (nominal forms are a canonical generalisation of the underlying syntactic entities) and general (presupposing the grammar for the underlying syntactic entities, suitable nominal forms are easily defined and the theory of occurrences is immediately carried over). Another advantage is a kind of methodological pureness: positions are generalised syntactic entities (and not extraneous, as sequences of natural numbers) and can be treated, in particular, with the well-known methods developed for the underlying syntactic entities.

Abstract prepared by René Gazzari.

E-mail: [email protected]

URL: http://doi.org/10.15496/publikation-47553

Invariance criteria are widely accepted as a means to demarcate the logical vocabulary of a language. In previous work, I proposed a framework of “semantic constraints” for model-theoretic consequence which does not rely on a strict distinction between logical and nonlogical terms, but rather on a range of constraints on models restricting the interpretations of terms in the language in different ways. In this paper I show how invariance criteria can be generalized so as to apply to semantic constraints on models. Some obviously unpalatable semantic constraints turn out to be invariant under isomorphisms. I shall connect the discussion to known counter-examples to invariance criteria for logical terms, and so the generalization will also shed light on the current existing debate on logicality. I analyse the failure of invariance to fulfil its role as a criterion for logicality, and argue that invariance conditions should best be thought of as merely methodological meta-constraints restricting the ways the model-theoretic apparatus should be used.

The article approaches cut elimination from a new angle. On the basis of an arbitrary inference relation among logically atomic formulae, an inference relation on a language possessing logical operators is defined by means of inductive clauses similar to the operator-introducing rules of a cut-free intuitionistic sequent calculus. The logical terminology of the richer language is not uniquely specified, but assumed to satisfy certain conditions of a general nature, allowing for, but not requiring, the existence of infinite conjunctions and disjunctions. We investigate to what extent structural properties of the given atomic relation are preserved through the extension to the full language. While closure under the Cut rule narrowly construed is not in general thus preserved, two properties jointly amounting to closure under the ordinary structural rules, including Cut, are.

Attention is then narrowed down to the special case of a standard first-order language, where a similar result is obtained also for closure under substitution of terms for individual parameters. Taken together, the three preservation results imply the familiar cut-elimination theorem for pure first-order intuitionistic sequent calculus.

In the interest of conceptual economy, all deducibility relations are specified purely inductively, rather than in terms of the existence of formal proofs of any kind.

In 1932, von Neumann proposed classifying the statistical behavior of differentiable systems. Joint work of B. Weiss and the author proved that the classification problem is complete analytic. Based on techniques in that proof, one is able to show that the collection of recursive diffeomorphisms of the 2-torus that are isomorphic to their inverses is $\Pi ^0_1$-hard via a computable 1-1 reduction. As a corollary there is a diffeomorphism that is isomorphic to its inverse if and only if the Riemann Hypothesis holds, a different one that is isomorphic to its inverse if and only if Goldbach’s conjecture holds and so forth. Applying the reduction to the $\Pi ^0_1$-sentence expressing “ZFC is consistent” gives a diffeomorphism T of the 2-torus such that the question of whether $T\cong T^{-1}$ is independent of ZFC.

Satisfaction systems and reductions between them are presented as an appropriate context for analyzing the satisfiability and the validity problems. The notion of reduction is generalized in order to cope with the meet-combination of logics. Reductions between satisfaction systems induce reductions between the respective satisfiability problems and (under mild conditions) also between their validity problems. Sufficient conditions are provided for relating satisfiability problems to validity problems. Reflection results for decidability in the presence of reductions are established. The validity problem in the meet-combination is proved to be decidable whenever the validity problem for the components are decidable. Several examples are discussed, namely, involving modal and intuitionistic logics, as well as the meet-combination of $\textrm {K}$ modal logic and intuitionistic logic.

I describe several ways in which forcing arguments can be used to yield clean and conceptual proofs of nonreducibility, ergodicity and other results in the theory of analytic equivalence relations. In particular, I present simple Borel equivalence relations E, F such that a natural proof of nonreducibility of E to F uses the independence of the Singular Cardinal Hypothesis at ℵω.

There are Π5 formulas in the language of the Turing degrees, D, with ≤, ⋁ and ⋀, that define the relations x″ ≤ y″, x″ = y″ and so x ∈ L2(y) = {x ≥ y ∣ x″ = y″} in any jump ideal containing 0(ω). There are also Σ6 & Π6 and Π8 formulas that define the relations w = x″ and w = x′, respectively, in any such ideal I. In the language with just ≤ the quantifier complexity of each of these definitions increases by one. On the other hand, no Π2 or Σ2 formula in the language with just ≤ defines L2 or x ∈ L2(y). Our arguments and constructions are purely degree theoretic without any appeals to absoluteness considerations, set theoretic methods or coding of models of arithmetic. As a corollary, we see that every automorphism of I is fixed on every degree above 0″ and every relation on I that is invariant under double jump or joining with 0″ is definable over I if and only if it is definable in second order arithmetic with set quantification ranging over sets whose degrees are in I. Similar direct coding arguments show that every hyperjump ideal I is rigid and biinterpretable with second order arithmetic with set quantification ranging over sets with hyperdegrees in I. Analogous results hold for various coarser degree structures.

Suppose that we have a method which estimates the conditional probabilities of some unknown stochastic source and we use it to guess which of the outcomes will happen. We want to make a correct guess as often as it is possible. What estimators are good for this? In this work, we consider estimators given by a familiar notion of universal coding for stationary ergodic measures, while working in the framework of algorithmic randomness, i.e., we are particularly interested in prediction of Martin-Löf random points. We outline the general theory and exhibit some counterexamples. Completing a result of Ryabko from 2009 we also show that universal probability measure in the sense of universal coding induces a universal predictor in the prequential sense. Surprisingly, this implication holds true provided the universal measure does not ascribe too low conditional probabilities to individual symbols. As an example, we show that the Prediction by Partial Matching (PPM) measure satisfies this requirement with a large reserve.

We prove a number of elementary facts about computability in partial combinatory algebras (pca’s). We disprove a suggestion made by Kreisel about using Friedberg numberings to construct extensional pca’s. We then discuss separability and elements without total extensions. We relate this to Ershov’s notion of precompleteness, and we show that precomplete numberings are not 1–1 in general.