Schedule

Ross Willard, The decidable discriminator variety problem

This talk is an advertisement for an old, unsolved problem in which universal algebra meets homogeneous structures. An equational class is any class in an algebraic signature (i.e., constants and function symbols only) which is axiomatized by universally quantified equations. Such a class is locally finite if every finitely generated substructure of a member is finite. The problem in question is that of describing all locally finite equational classes with finite signature whose first-order theory is decidable. The work of Burris, McKenzie and Valeriote [1, 3] in the 1980s reduced this problem to two special kinds of equational classes:

• For a given finite ring $R$, the class ${}_R\mathcal M$ of all $R$-modules.
• Locally finite "discriminator varieties" in a finite signature.

What are discriminator varieties? They are equational classes $\mathcal E$ which resemble the class of Boolean algebras in certain ways. In particular, (i) the class $\mathcal S$ of simple algebras in $\mathcal E$ is $\forall_1$-axiomatizable, and (ii) each algebra in $\mathcal E$ has a Stone-like representation via a sheaf over $\mathcal S$. In practice [4, 2], the question of whether a locally finite discriminator variety $\mathcal E$ has a decidable first-order theory hinges on how well-structured are the members of $\mathcal S$, and in particular on the degree to which the countable members of $\mathcal S$ fail to be homogeneous. In this talk I will make this precise and explain the current state of the problem.

References
[1] Stanley Burris and Ralph McKenzie, Decidability and Boolean representations, Memoirs of the American Mathematical Society, vol. 32 (1981), no. 246.
[2] Dejan Delić, Decidable discriminator varieties arising from dihedral varieties of groups, Journal of Pure and Applied Algebra, vol. 198 (2005), no. 1–3, pp. 75–92.
[3] Ralph McKenzie and Matthew Valeriote, The Structure of Decidable Locally Finite Varieties, Progress in Mathematics, Birkhäuser, Boston, 1989.
[4] Ross Willard, Decidable discriminator varieties from unary classes, Transactions of the American Mathematical Society, vol. 336 (1993), no. 1, 311-333.
[Close]

Josh Wiscons, The status of Cherlin's conjecture for primitive structures of relational complexity 2

The relational complexity of a structure $\mathbf{X}$ is the least $k<\omega$ for which the orbits of $\operatorname{Aut}(\mathbf{X})$ on $X^k$ "determine" the orbits of $\operatorname{Aut}(\mathbf{X})$ on $X^n$ for all $n<\omega$. This invariant originated in Lachlan's classification theory for homogeneous finite –and more generally, countable stable– relational structures, but not much was known about the complexities of specific structures until de work of Cherlin, Martin and Saracino in the 1990's. In this talk, I will present some background on relational complexity and discuss recent work on Cherlin's conjecture regarding the classification of the finite primitive structures of complexity 2.
[Close]

David Schrittesser, Definable discrete sets, forcing, and Ramsey theory

Let $\mathcal R$ be a family of finitary relations on a set $X$. A set $A\subseteq X$ is called $\mathcal R$-discrete if no relation $R \in \mathcal R$ relates any elements of $A$; $A$ is called maximal discrete if it is maximal with respect to subset-inclusion among $\mathcal R$-discrete subsets of $X$. For any family of relations $\mathcal R$, maximal $\mathcal R$-discrete sets exist by the axiom of choice; whether such sets can be definable is contentious. Maximal discrete sets have been widely studied: instances are maximal co-finitary groups, maximal almost disjoint families, and maximal orthogonal families of measures. In many (but not all) cases one can show such objects cannot be analytic (i.e. projections of closed sets). On the contrary, certain definable (in fact, co-analytic) maximal discrete sets have been shown to exist under the assumption that every set is constructible. We present some new results, exhibiting definable maximal discrete sets in forcing extensions, e.g. extensions where the continuum hypothesis fails. In most cases, these results rely on Ramsey theoretic considerations.
[Close]

Anush Tserunyan, Integer cost and ergodic actions

A countable Borel equivalence relation $E$ on a probability space can always be generated in two ways: as the orbit equivalence relation of a Borel action of a countable group and as the connectedness relation of a locally countable Borel graph, called a graphing of $E$. Assuming that $E$ is measure-preserving, graphings provide a numerical invariant called cost, whose theory has been largely developed and used by Gaboriau and others in establishing rigidity results. A well-known theorem of Hjorth states that when $E$ is ergodic, treeable (admits an acyclic graphing), and has integer cost $n \ge 1$, then it is generated by an a.e. free measure-preserving action of the free group $\mathbf{F}_n$ on $n$ generators. We give a simpler proof of this theorem and the technique of our proof, combined with a recent theorem of Tucker-Drob, yields a strengthening of Hjorth's theorem: the action of $\mathbf{F}_n$ can be arranged so that each of the $n$ generators acts ergodically.
[Close]

Sam Sanders, The unreasonable effectiveness of Nonstandard Analysis

As suggested by the title, we will uncover the vast computational content of classical Nonstandard Analysis. To this end, we formulate a template $\mathfrak{CI}$ which converts a theorem of `pure' Nonstandard Analysis, i.e. formulated solely with the nonstandard definitions (of continuity, integration, differentiability, convergence, compactness, et cetera), into the associated effective theorem. The latter constitutes a theorem of computable mathematics no longer involving Nonstandard Analysis. The template often produces theorems of Bishop's Constructive Analysis ([1]). \medskip To establish the vast scope of $\mathfrak{CI}$, we apply this template to representative theorems from the Big Five categories from Reverse Mathematics ([3, 5]). The latter foundational program provides a classification of the majority of theorems from `ordinary', that is non-set theoretical, mathematics into the aforementioned five categories. The Reverse Mathematics zoo ([2]) gathers exceptions to this classification, and is studied in [4] using $\mathfrak{CI}$. Hence, the template $\mathfrak{CI}$ is seen to apply to essentially all of ordinary mathematics, thanks to the Big Five classification (and associated zoo) from Reverse Mathematics. Finally, we establish that certain `highly constructive' theorems, called Herbrandisations, imply the original theorem of Nonstandard Analysis from which they were obtained via $\mathfrak{CI}$.
Acknowledgement. This research is generously sponsored by the John Templeton Foundation and the Alexander Von Humboldt Foundation.

References
[1] E. Bishop, D. Bridgess Constructive analysis, Grundlehren der Mathematischen Wissenschaften, vol. 279, Springer, 1985, xii+477
[2] D. Dzhafarov, The Reverse Mathematics zoo, {http://rmzoo.uconn.edu/}
[3] U. Kohlenbach, Higher-order Reverse Mathematics, Lect. Notes Log., Reverse Mathematics 2001, vol. 21, Assoc. Symbol. Logic, La Jolla, CA, 2005, pp. 281-295
[4] S. Sanders, The refining of the taming of the Reverse Mathematics zoo, to appear in Notre Dame Journal for formal logic, 2016
[5] S. Simpson, Subsystems of Second-order Arithmetic, 2nd ed., Perspectives in Logic, Cambridge University Press, Cambridge, 2009
[Close]

David R. Belanger, A computable perfect-set theorem

We gauge the difficulty of finding a perfect subtree in a tree of a given Cantor-Bendixson rank. To simplify the analysis we introduce half-derivative, and extend the definition of rank to include values of the form $n$-and-a-half; each increase of one-half in the rank corresponds to one added jump in the perfect-subtree problem.
[Close]

Jan Hubicka, All those Ramsey classes (Ramsey classes with closures and forbidden homomorphisms)

Class $\mathcal K$ of finite structures is Ramsey class if for every choice of $\mathbf A,\mathbf B\in K$ there exists $\mathbf C\in \mathcal K$ such that for every coloring of its substructures isomorphic to $\mathbf A$ with 2 colors there exists an isomorphic copy of $\mathbf B$ in $\mathbf C$ where all copies of $\mathbf A$ are monochromatic. It is a classical result that for every purely relational language $L$ the class of all finite ordered $L$-structures is Ramsey [5, 1]. We extend this theorem for languages containing both relations and functions. We also give a new sufficient condition for subclass of a Ramsey class to be Ramsey. By verifying this condition we prove Ramsey property of many classes such as convexly ordered $S$-metric spaces (solving an open problem [6]), totally ordered structures (structures with linear order on both vertices and relations), and ordered single constraint Cherlin Shelah Shi classes [2].

References
[1] F. G. Abramson, L. A. Harrington, Models without indiscernibles, Journal of Symbolic Logic, vol. 43 (1978), no. 3, pp. 572–600.
[2] G. Cherlin, S. Shelah, N. Shi, Universal graphs with forbidden subgraphs and algebraic closure, Advances in Applied Mathematics, vol. 22 (1999), no. 4, pp. 454–491.
[3] J. Hubička, J. Nešetřil, Bowtie-free graphs have a {R}amsey lift, arXiv preprint, arXiv:1402.2700.
[4] J. Hubička, J. Nešetřil, All those Ramsey classes (Ramsey classes with closures and forbidden homomorphisms), in preparation.
[5] J. Nešetřil, V. Rödl, Partitions of Finite Relational and Set Systems, Journal Combinatorial Theory, Series A, vol. 22 (1977), no. 3, pp. 289–312.
[6] L. Nguyen Van Thé, Structural {R}amsey Theory of Metric Spaces and Topological Dynamics of Isometry Groups, Memoirs of the American Mathematical Society, American Mathematical Society, 2010.
[Close]

Libor Barto, The algebraic dichotomy conjecture for infinite domain Constraint Satisfaction Problems

We prove that an $\omega$-categorical core structure primitively positively interprets all finite structures with parameters if and only if some stabilizer of its polymorphism clone has a homomorphism to the clone of projections, and that this happens if and only if its polymorphism clone does not contain operations $\alpha$, $\beta$, $s$ satisfying the identity $\alpha s(x,y,x,z,y,z) \approx \beta s(y,x,z,x,z,y)$. This establishes an algebraic criterion equivalent to the conjectured borderline between P and NP-complete CSPs over reducts of finitely bounded homogenous structures, and accomplishes one of the steps of a proposed strategy for reducing the infinite domain CSP dichotomy conjecture to the finite case. Our theorem is also of independent mathematical interest, characterizing a topological property of any $\omega$-categorical core structure (the existence of a continuous homomorphism of a stabilizer of its polymorphism clone to the projections) in purely algebraic terms (the failure of an identity as above). This is a joint work with Michael Pinsker.
[Close]

Nam Trang, Large cardinals, determinacy, and forcing axioms

We discuss some recent progress in descriptive inner model theory. In particular, we discuss some current results concerning connections of the three hierarchies of models: canonical models of large cardinals (pure extender models), canonical models of determinacy, and strategic hybrid models (e.g. HOD of determinacy models). These structural results can be used to improve (lower-bound) consistency strength of strong combinatorial principles such as The Proper Forcing Axiom ($\sf{PFA}$), strong forms of the tree property etc. In particular, I proved that $\sf{PFA}$ implies the existence of a transitive model of ``$\sf{AD}_\mathbb{R} + \Theta$ is regular". Building on this and structural results above, G. Sargsyan and I have constructed models of theory $\sf{LSA} =_{\rm{def}} ``\sf{AD}^+ + $there is an $\alpha$ such that $\Theta=\theta_{\alpha+1} + \theta_\alpha$ is the largest Suslin cardinal" from $\sf{PFA}$. This result is the strongest of its kind and reflects our current understanding of HOD of models of determinacy.
[Close]

Andrew Marks, Borel and measurable matchings

We discuss several results related to the question of when a Borel graph has a Borel matching. Here, the analogue of Hall's matching theorem fails, but there are positive results giving Borel matchings in several contexts if we are willing to discard null or meager sets, or restrict the types of graphs we consider. We also discuss some applications to geometrical paradoxes.
[Close]

Lev Gordeev, On Harvey Friedman's finite phase transitions

Definition (H. Friedman). The proof theoretic integer of formal system $\mathbf{T}$ (abbreviation: $\mathrm{PTI}\left( \mathbf{T}\right) $ ) is the least integer $n$ such that every $\Sigma _{1}^{0}$ sentence \begin{equation*} \exists x_{1}\cdots \exists x_{m}A\left( x_{1},\cdots ,x_{m}\right) \end{equation*} that has a proof in $\mathbf{T}$ with at most $10,000$ symbols, has witnesses $x_{1},\cdots ,x_{m}<n$. (Actually $m=1$ would suffice.)

A good source of examples is in the area surrounding Kruskal's theorem. This talk is devoted to $\mathrm{PTI}\left( \mathbf{T}\right) $'s basic properties, examples, comparisons and related phase transitions.
[Close]

Florian Pelupessy, Ramsey like principles and well-foundedness of $d$-height $\omega$-towers

Recently it has been highlighted by Kreuzer and Yokoyama [1] that, over $\mathrm{RCA}_0$, there are many principles equivalent to the well foundedness of the ordinal $\omega^\omega$. We will observe that there are Ramsey-like principles which are equivalent to the well-foundedness of $\omega_d$, where $\omega_0=1$ and $\omega_{n+1}=\omega^{\omega_n}$. One of these examples is based on the relativised Paris–Harrington principle as mentioned in [1], but for dimension $d$. The more interesting example is the restricton of Friedman's adjacent Ramsey theorem to fixed dimension $d$, which is equivalent to the well-foundedness of $\omega_{d+1}$.

Definition (adjacent Ramsey in dimension $d$). For every $C\colon \mathbb{N}^d \rightarrow \mathbb{N}^r$ there exist $x_0 < \dots < x_{d+1}$ such that $C(x_1, \dots , x_d) \leq C(x_2, \dots , x_{d+1})$, where $\leq$ is the coordinatewise ordering.

References
[1] Alexander P. Kreuzer and Keita Yokoyama, On principles between $\Sigma_1$ and $\Sigma_2$ induction and monotone enumerations, arXiv:1306.1936v5.
[2] Stephen G. Simpson, Subsystems of second order arithmetic, Perspectives in logic (2nd edition), Cambridge University Press, 2009.
[Close]

Patrice Ossona de Mendez, Structural Limits and Clustering near Infinity

Structural limits (including FO-limits and X-limits for various fragments X) arise as a natural generalization of limits of bothe dense and bounded degree graphs, yet having a distinctive model theoretic flavour. It is in a way dual approach which allows to prove distributional limits in a full generality. More recently it leads to clustering which seems to be interesting from both analytic and model theoretic perspective. This can be also outlined as follows: The cluster analysis of very large objects is an important problem, which spans several theoretical as well as applied branches of mathematics and computer science. Here we suggest a novel approach: under assumption of local convergence of a sequence of finite structures we derive an asymptotic clustering. This is achieved by a blend of analytic and geometric techniques, and particularly by a new interpretation of the authors? repre-sentation theorem for limits of local convergent sequences, which serves as a guidance for the whole process. Our study may be seen as an effort to describe connectivity structure at the limit (without having a defined explicit limit structure) and to pull this connectivity structure back to the finite structures in the sequence in a continuous way.
[Close]

Ove Ahlman, Simple structures axiomatized by almost sure theories

Studying simple structures, one of the nicest examples of a simple yet not stable structure is the Rado graph. The Rado graph is the unique countable graph $\mathcal{G}$ which satisfies that for any finite disjoint subsets $A$ and $B$ of $\mathcal{G}$ there is a vertex $c$ such that $c$ is adjacent to all vertices in $A$ and no vertices in $B$. Some of the properties of the Rado graph which makes it especially nice include $\omega-$categoricity (even homogeneity), SU-rank $1$ and trivial algebraic closure.
For each $n\in\mathbb{N}$ let $\mathbf{K}_n$ be a set of finite structures and let $\mu_n$ be the uniform probability measure on $\mathbf{K}_n$, assigning the same probability to each structure. This meas-sure induce a probability measure on first order sentences $\varphi$ by putting $\mu_n(\varphi)=\mu(\{\mathcal{M}\in\mathbf{K}_n: \mathcal{M}\models \varphi\})$. Put $T$ to be the theory, called the almost sure theory, of all first order sentences $\varphi$ such that $\lim_{n\rightarrow\infty} \mu_n(\varphi)= 1$. We directly see that $T$ is complete if and only if each sentence has asymptotic probability $0$ or $1$, in which case we say that the pair $(\mathbf{K}_n,\mu_n)_{n\in\mathbb{N}}$ has a $0-1$ law. Sets which have a $0-1$ law under the uniform probability measure include all finite structures, all finite partial orders, all finite $l-$colorable graphs and many more.
One can easily show that the Rado graph is not only axiomatized by the vertex-extension property described above, but can also be seen as the unique countable structure satisfying the almost sure theory coming from $\mathbf{K}_n$ consisting of all graphs with universe $\{1,\ldots,n\}$. Further more many other almost sure theories, including all of the above mentioned examples, are $\omega-$categorical and simple with $SU-$rank 1. In this talk we will discuss why this connection occurs and see that the binary simple $\omega-$categorical structures with SU-rank $1$ is in direct connection with almost sure theories.
[Close]

Rupert Hölzl, Randomness for computable measures and initial segment complexity

The Levin-Schnorr theorem establishes the equivalence of a certain measure-theoretic notion of typicality for infinite sequences (known as Martin-Löf randomness) with a notion of incompressibility given in terms of Kolmogorov complexity. Although the Levin-Schnorr theorem is usually formulated for sequences that are random with respect to the Lebesgue measure on $2^\omega$, it is well known that the theorem can be generalized to hold for any computable probability measure on $2^\omega$. More specifically, a sequence $X\in2^\omega$ is Martin-Löf random with respect to a computable measure $\mu$ if and only if the initial segment complexity of $X\upharpoonright n$ is bounded from below by $-\log\mu(X\upharpoonright n)$. Thus we see that certain values of the measure $\mu$ constrain the possible values of the initial segment complexities of the $\mu$-random sequences. In this study, we further explore the interaction between computable measures and the initial segment complexity of the sequences that are random with respect to these measures (hereafter, we will refer to those sequences that are random with respect to a computable measure as proper sequences, following the terminology of Zvonkin and Levin [6]). We focus in particular on the growth rates of functions of the form $f(X,n)=-\log\mu(X\upharpoonright n)$ for various computable measures $\mu$ and $\mu$-random sequences $X$. As we demonstrate, these growth rates can vary widely, depending on the choice of the underlying measure $\mu$. In the first half of the paper, we focus on the relationship between a class of sequences known as complex sequences and those sequences that are random with respect to a computable, continuous measure. First studied systematically by Kjos-Hanssen et al. [4] (but also studied earlier by Kanovič [2]), complex sequences are those sequences whose initial segment complexities are bounded below by some computable function. We characterize the complex proper sequences as the sequences that are random with respect to some computable continuous measure. This is done by studying the "removability" of $\mu$-atoms, that is, sequences $X$ such that $\mu(\{X\})>0$. We show that if a sequence $X$ is complex and random with respect to some computable measure $\mu$, we can define a computable, continuous measure $\nu$ such that $X$ is random with respect to $\nu$ by removing the $\mu$-atoms that are in some sense near $X$. It is natural to ask whether this removal of atoms can always be carried out while preserving all non-atomic random sequences simultaneously, again assuming that all of these random sequences are complex. We show that this is not the case. Using this characterization of complex sequences through computable continuous measures, we establish new results on the relationship between the notions of avoidability, hyperavoidability, semigenericity, and not being random for any computable, continuous measure. More specifically, when restricted to the collection of proper sequences, we show that these four notions are equivalent to being complex. We also study the granularity of a computable, continuous measure $\mu$ and show that the inverse of the granularity function provides a uniform lower bound for the initial segment complexity of $\mu$-random sequences. In the second half of the paper, we turn our attention to atomic computable measures, i.e., computable measures $\mu$ that have $\mu$-atoms. First, we study atomic measures $\mu$ with the property that every $\mu$-random sequence is either a $\mu$-atom or is complex. We show that for such measures $\mu$, even though the initial segment complexity of each non-atom $\mu$-random sequence is bounded from below by some computable function, there is in general no uniform computable lower bound for every non-atom $\mu$-random sequence. Next, we construct a computable atomic measure $\mu$ with the property that the initial segment complexity of each $\mu$-random sequence dominates no computable function, and a computable atomic measure $\nu$ with the property that the initial segment complexity of each $\nu$-random sequence is dominated by all computable functions. The former sequences are called infinitely often anti-complex, while the latter are known simply as anti-complex. Lastly, we study two specific kinds of atomic measures: diminutive measures and trivial measures. Here, a measure $\mu$ is trivial if $\mu(\mathrm{Atoms}_\mu)=1$, and diminutive measures are defined as follows.

Definition. Let $\mathcal{C}\subseteq2^\omega$.
(i) $\mathcal{C}$ is diminutive if it does not contain a computably perfect subclass.
(ii) Let $\mu$ be a computable measure, and let $(\mathcal{U}_i)_{i\in\omega}$ be the universal $\mu$-Martin-Löf test. Then we say that $\mu$ is diminutive if $\mathcal{U}_i^c$ is a diminutive $\Pi^0_1$ class for every $i$.

We show that while every computable trivial measure is diminutive, the converse does not hold. The proof of this last statement gives an alternative, priority-free proof of the following known result.

Corollary (Kautz [3]). There is a computable, non-trivial measure $\mu$ such that there is no $\Delta^0_2$, non-computable $X\in\mathrm{MLR}_\mu$.

References
[1] R. Hölzl and C. P. Porter, Randomness for Computable Measures and Initial Segment Complexity, ArXiv e-prints, October 2015, 1510.07202.
[2] Max I. Kanovič, The complexity of the enumeration and solvability of predicates, Doklady Akademii nauk SSSR, vol. 190 (1970), pp. 23–26.
[3] Steven M. Kautz, Degrees of random sets, PhD thesis, Cornell University, 1991.
[4] Bjørn Kjos-Hanssen, Wolfgang Merkle, and Frank Stephan, Kolmogorov complexity and the recursion theorem, Transactions of the American Mathematical Society, vol. 363 (2011), no. 10, pp. 5465–5480.
[5] Christopher Porter, Mathematical and Philosophical Perspectives on Algorithmic Randomness, PhD thesis, University of Notre Dame, 2012.
[6] Alexander K. Zvonkin and Leonid A. Levin, The complexity of finite objects and the basing of the concepts of information and randomness on the theory of algorithms, Uspekhi Matematicheskikh Nauk, vol. 25 (1970), no. 6(156), pp. 85–127.
[Close]

Chris Conidis, New directions in reverse algebra

We will survey some old results in the reverse mathematics of Artinian and Noetherian rings, showing how computability-theoretic insights can give rise to new algebraic techniques. Finally, we will conclude with some new results concerning the reverse mathematics of the (very general) class of Noetherian rings.

References
[1] Conidis, C.J., Chain conditions in computable rings, Transactions of the American Mathematical Society, vol. 362 (2010), no. 12, pp. 6523–6550.
[2] ― The computability, definability, and proof theory of Artinian rings, To appear.
[3] ― The meta-metamathematics of Neotherian rings, In preparation.

[Close]

Volker Halbach, Axiomatizing Kripke's theory of truth in classical and nonclassical logic

We consider axiomatizations of Kripke's [3] theory of truth, more precisely, of all fixed points of Kripke's operator based on Strong Kleene logic over the standard model over arithmetic. We also consider analogous models with gluts as considered by [4]. Feferman [1] axiomatized Kripke's theory in classical logic. Feferman's axiomatization is sound in the sense that whenever $T\ulcorner\phi \urcorner$ is provable then $\phi $ holds in all of Kripke's fixed-point models. Halbach and Horsten [2] provided an axiomatization that is directly sound: $\phi $ holds in all of Kripke's fixed-point models, if $\phi $ is provable in their system. Halbach and Horsten [2] showed that their system is proof-theoretically much weaker than Feferman's system and lacks many arithmetical theorems provable in Feferman's system. There are many sentences such that $T\ulcorner\phi \urcorner$ is provable in Feferman's system, while $\phi $ isn't provable in the Halbach–Horsten system. We pinpoint the source of the deductive weakness of the Halbach–Horsten system in the induction rule. Both systems contain the same rule of induction. If it is removed from both systems, then $T\ulcorner\phi \urcorner$ is provable in Feferman's system iff $\phi $ is provable in the Halbach–Horsten system. Thus the effect of switching from classical logic to the nonclassical logic of the Halbach–Horsten system limits the usability of the mathematical principle of induction. We take this as evidence that the often advocated strategy of restricting classical logic for semantic vocabulary doesn't necessarily affect our semantic reasoning, but it can cripple our mathematical reasoning.

References
[1] Solomon Feferman, Reflecting on incompleteness, Journal of Symbolic Logic, vol. 56 (1991), no. 1, pp. 1–49.
[2] Volker Halbach and Leon Horsten, Axiomatizing Kripke's theory of truth, Journal of Symbolic Logic, vol. 71 (2006), no. 2, pp. 677–712.
[3] Saul A. Kripke, Outline of a Theory of Truth, Journal of Philosophy, vol. 72 (1975), no. 19, pp. 690–716.
[4] Albert Visser, Four-valued semantics and the liar, Journal of Philosophical Logic, vol. 13 (1984), no. 2, pp. 181–212.
[Close]

Lavinia Picollo, Truth, Reference and Disquotation

I first provide intuitively appealing notions of reference, self-reference, and well-foundedness of sentences of the language of first-order Peano arithmetic extended with a truth predicate. They are intended as a tool for studying reference patterns that underlie expressions leading to semantic paradox, and thus to shed light on the debate on whether every paradox formulated in a first-order language involves self-reference or some other vicious reference pattern. I use the new notions to formulate sensible restrictions on the acceptable instances of the T-schema, to carry out the disquotationalist project. Since the concept of reference I put forward is proof-theoretic\textemdash i.e., it turns to the provability predicate rather than the truth predicate\textemdash and, therefore, arithmetically definable, it can be used to provide recursive axiomatizations of truth. I show the resulting systems are $\omega$-consistent and as strong as Tarski's theory of ramified truth iterated up to $\epsilon_0$.
[Close]

Caroline Terry, An application of model theoretic Ramsey theory

Chudnovsky, Kim, Oum, and Seymour recently established that any prime graph contains one of a short list of induced prime subgraphs. In this talk we present joint work with Malliaris, in which we reprove their theorem using many of the same ideas, but with the key model theoretic ingredient of first determining the so-called amount of stability of the graph. This approach changes the applicable Ramsey theorem, improves the bounds, and offers a different structural perspective on the graphs in question.
[Close]

Nathanael Ackerman, Hypergraphons, invariant measures, and model theory

Over the last decade a rich theory of the limits of sequences of dense finite structures has developed. The limiting objects, known as hypergraphons, lie at a crossroads between probability theory, combinatorics and model theory. In particular, hypergraphons are closely tied to $S_\infty$-invariant measures on the space of countable structures, and can be seen as a variant of the Aldous-Hoover-Kallenberg representation of such a measure. In this talk we will review the basic theory of hypergraphons and will discuss the effects the model theoretic assumption of stability can have on their structure. This is joint work with Cameron Freer and Rehana Patel.
[Close]

Andre Nies, Describing finite groups by first-order sentences of polylogarithmic length

I discuss recent research with Katrin Tent [1] that connects group theory, logic, and the idea of Kolmogorov complexity. We call a class of finite structures for a finite first-order signature R-compressible, for an unbounded function $R$ on the natural numbers, if each structure $G$ in the class has a first-order description of length at most $O(R(|G|))$. We show that the class of finite simple groups is $\log$-compressible, and the class of all finite groups is $\log^3$ compressible. The results rely on the classification of finite simple groups, the existence of profinite presentations with few relators for finite groups, and group cohomology. We also indicate why the bounds are close to optimal. A much easier result that still conveys the flavour of our research is the following: for each $n$ there is a first-order sentence of length $O(\log n)$ expressing that a group has size $n$ (see [2]).

References
[1] A. Nies and K. Tent. Describing finite groups by short first-order sentences. Israel J. of Matematics, to appear. Available at arXiv:1409.8390.
[2] A. Nies (editor). Logic Blog 2016. Available at cs.auckland.ac.nz/~nies.
[Close]

Yang Yue, A Computation Model on Real Numbers

The study of computation models on real numbers has a history almost as long as the one of recursion theory. Various models have been proposed, for instance, the type-two theory of effectivity (TTE) based on oracle Turing machines and the Blum-Shub-Smale model of computation (BSS). In this talk I will identify a class of functions over real numbers, which can be characterized by three equivalent ways: by functional schemes similar to the class of partial recursive functions; by master-slave machines which are generalizations of Turing machines; and by $\lambda$-calculus with extra $\delta$-reductions. These equivalent characterizations seem to suggest something intrinsic behind this class of functions. The talk is based on joint work with Keng Meng Ng from Nanyang Technological University, Singapore and Nazanin Tavana from Amirkabir University of Technology, Iran; Duccio Pianigiani and Andrea Sorbi from University of Siena, Italy and Jiangjie Qiu from Renming University, China.
[Close]

Theodora Achourioti, Truth, Intensionality and Paradox

We know since Tarski that the truth of a sufficiently strong first-order theory cannot be captured by means of a truth predicate which satisfies the full $T$-schema. A number of formal theories of type-free truth have been developed that restrict the instances of the $T$-schema in some interesting way so that a consistent theory of truth can be obtained. We present an untyped satisfaction predicate restricted to the geometric fragment of the language and motivated by semantic structures that embody a model of falsification on which the truth of some theory resides. This is a predicate with intensional meaning that it inherits from its semantic environment where the existence of objects and interpretation of predicates depend on what can be seen as some decision process. We show how the consistency of this predicate follows from a certain form of groundedness conditions and we explain what these mean in our context. Finally, we turn to complexity issues and show that even though syntactically severely restricted, this truth predicate does not amount to a simple notion of truth.
[Close]

Roy Cook, Embracing Inference: Three Revenge-Free Deductive Systems for Truth

The Embracing Revenge account, which provides a logical and semantic treatment of the Liar paradox and the revenge phenomena, has been developed in a series of papers by Roy T Cook (2008, 2009), Nicholas Tourville (under review), and Philippe Schlenker (2010). In this paper, after surveying the semantics developed in the most recent such work, I present three deductive systems for the Embracing Revenge view. Each of these three systems reflect distinct ways to "read" the semantics, modelled roughly on many-valued (or "gappy"), dialethic (or "glutty"), and degree-theoretic approaches to semantics.

References
[1] Roy T Cook, Embracing Revenge: On the Indefinite Extensibility of Language, Revenge of the Liar (JC Beall, editors), Oxford University Press 2008, pp. 31–52.
[2] ― What is a Truth Value, and How Many Are There?, Studia Logica, vol. 92 (2009), pp. 183–201.
[3] ― P. Schlenker, Super-Liars, Review of Symbolic Logic, vol. 3 (2010), no. 3, pp. 374–414.
[4] ― N. Tourville and R. Cook, Embracing the Technicalities: Expressive Completeness and Revenge, under review,
[Close]

Hazel Brickhill, A generalisation of closed unbounded sets and square sequences

I will introduce a generalisation of the notion closed unbounded (club) set which ties in with the generalisation of stationary set given in [1]. We can use these $n$-clubs to define a generalisation of Jensen’s $\Box$ sequence below a non-weakly compact (constructed in [2]). The main result is that in $L$ we have such a $\Box^n$ sequence below every cardinal that is $\Pi^1_n$-indescribable but not $\Pi^1_{n+1}$-indescribable. It is interesting to note that construction of the $\Box^n$ sequence does not require fine-structure.

References
[1] Bagaria, J., Magidor, M., and Sakai, H., Reflection and indescribability in the constructible universe., Israel Journal of Mathematics, Vol. 208 (2015), no. 1, pp. 1-11.
[2] Jensen, R. B, The fine structure of the constructible hierarchy., Annals of Mathematical Logic , Vol. 4 (1972), no. 3, pp. 229-308.
[Close]

Sy-David Friedman, Radek Honzik and Sarka Stejskalova, The tree property at the double successor of a singular cardinal with a larger gap

All three authors were supported by FWF/GA{\v C}R grant I 1921-N25.
Starting from a Laver-indestructible supercompact $\kappa$ and a weakly compact $\lambda$ above $\kappa$, we show there is a forcing extension where $\kappa$ is a strong limit singular cardinal with cofinality $\omega$, $2^\kappa = \kappa^{+3} = \lambda^+$, and the tree property holds at $\kappa^{++} = \lambda$. Next we generalize this result to an arbitrary cardinal $\mu$ such that $\kappa <\mathrm{cf}(\mu)$ and $\lambda^+ \le \mu$. This result provides more information about possible relationships between the tree property and the continuum function.
[Close]

Guido Gherardi, Paolo Maffezioli and Eugenio Orlandelli, Interpolation theorem for first-order theories

In this work we prove the interpolation theorem for some first-order theory. Previous results by Negri and von Plato [2] and Dyckhoff and Negri [1] have shown how to prove cut elimination in the presence of non-logical rules. Often cut elimination allows a constructive proof of the interpolation theorem. Thus, the question as to whether and to what extent interpolation holds in first-order theories naturally arises. Our aim is to give an answer to this question. First, we show that the standard Takeuti-Maehara techinique fails when first-order axioms are formulated as rules. Then, using an alternative strategy based on negative normal forms, we identify a class of theories for which interpolation holds. The proof we give is entirely constructive. As a case study, we consider the theory of strict partial orders and we show how to extend the result to linear orders as well.

References
[1] R. Dyckhoff, S. Negri, Geometrization of first-order logic, The Bulletin of Symbolic Logic, vol. 21 (2015), no. 2, pp. 123–163.
[2] S. Negri, J. von Plato, Proof Analysis, Cambridge University Press, 2011.
[Close]

Andreas Weiermann, On generalized Goodstein sequences

The termination property of the classical Goodstein sequences provides a simple number-theoretic assertion which is true but independent of first order Peano arithmetic $\mathrm{P}\mathrm{A}$. In this talk we consider Goodstein sequences which are defined relative to Ackermannian functions. We discuss the following two results. {\bf Theorem A.} When the zero-th branch of the Ackermann function is the successor function then the induced Goodstein principle will be equivalent to the one consistency of PA. {\bf Theorem B.} When the zero-th branch of the Ackermann function is an exponential function $k\mapsto k^b$ then the induced Goodstein principle will be equivalent to the one consistency of $\mathrm{A}\mathrm{T}\mathrm{R}_0$. (Theorem B is joint work with Tosiyasu Arai and Stan Wainer).
[Close]

Roger Villemaire, $\aleph_0$-categorical structures for which Forth suffices

Cantor's original proof that countable dense linear orders are isomorphic maps elements in a single direction. This method has been named Forth by P. J. Cameron, who furthermore showed, answering a question of A. Mathias, that Forth fails to yield an onto mapping for some $\aleph_0$-categorical structures. In Cameron's terminology, Forth does not suffice for those structures. In [1] Cameron gave a sufficient condition for Forth to suffice that was later generalized by McLeish [2]. However, none of these conditions are necessary. A necessary and sufficient condition for Forth to suffice has been given in [3] in terms of an countable ordinal rank on types. While [3] gives, for any countable ordinal $\alpha$, a homogeneous structure with the property that the ranks of its types form $\alpha$, the considered languages are infinite for $\alpha\geq\omega$. These structures are unfortunately not $\aleph_0$-categorical. This talk will present results on the ranks that occur in $\aleph_0$-categorical structures, with an emphasis on the combinatorial constraints that the existence of a rank imposes on types.

References
[1] P. J. Cameron, Oligomorphic Permutation Groups, London Mathematical Society Lecture Note Series, Cambridge University Press, 1990.
[2] S. J. McLeish, The forth part of the back and forth map in countable homogeneous structures, Journal of Symbolic Logic, vol. 62 (1997), no. 3, pp. 873–890.
[3] R. Villemaire, Homogeneity and Fix-Points: Going Forth!, Journal of Symbolic Logic, vol. 80 (2015), no. 2, pp. 636–660, DOI {10.1017/jsl.2014.72}.
[Close]

David Hartman and Jan Hubicka, Towards relational complexity of graphs

Homogeneity of relational structures represents property that every local isomorphism can be extended to an automorphism. This strong symmetry condition usually results in relatively small number of families having this property, see example of undirected graphs [4]. For this reason it is valuable to study a process of extending a language of studied structure via introducing new relations in order to make the resulting extension homogeneous. If we additionally require this extension to preserve the automorphism group of the original structure we get notion of relational complexity. This notion evaluate maximal arity of used relation in described homogenization. Relational complexity has been introduced in slightly modified way in [1] and later reviewed in [2]. Motivated by these results we are interested in relational complexity of finite structures acquiring small values like $1$ or $2$ as well as structure maximizing its value. Another interesting area is that of countable universal structures defined by families of forbidden structures, see some details in [3].

References
[1] Cherlin, G., Martin, G. and Saracino, D., Arities of permutation groups: Wreath products and k-sets, Journal of Combinatorial Theory, Series A, vol. 74 (1996), pp. 249–286.
[2] Cherlin, G., Sporadic Homogeneous Structures, The Gelfand Mathematical Seminars, 1996–1999 (I. M. Gelfand and V. S. Retakh, editors), Birkhäuser Boston, Birkhäuser Publishing Ltd., 675 Massachusetts Avenue, Cambridge, 2000, pp. 15–48.
[3] Hartman, D., Hubička, J. and Nešetřil, J., Complexities of relational structure, Mathematica Slovaca, vol. 65 (2015), no. 2, pp. 229–246.
[4] Lachlan, A. H and Woodrow, R. E., Countable ultrahomogeneous undirected graphs, Transactions of the American Mathematical Society, vol. 262 (1980), pp. 51–94.
[Close]

Samuel Braunfeld, The Lattice of Definable Equivalence Relations in Homogeneous n-Dimensional Permutation Structures

Abstract: In [1], Cameron classified the homogeneous permutations (structures in a language of 2 linear orders). In working toward the classification of the homogeneous n-dimensional permutation structures (structures in a language of n linear orders), consideration of the lattice of definable equivalence relations leads to a generalization of Cameron's structures, giving a large class of new imprimitive examples, and places some constraints on lattices that can appear.

References
[1] Peter Cameron, Homogeneous Permutations, The Electronic Journal of Combinatorics, vol. 9 (2002), no. 2, Research Paper 2.
[Close]

Roman Wencel, Open covers of definable sets in o-minimal structures

It is well known that a set definable in an o-minimal structure is a finite union of pairwise disjoint cells. During my talk I am going to discuss the main ideas of the proof of a theorem saying that an open bounded set definable in an arbitrary o-minimal structure is a union of finitely many open definable cells, not necessarily pairwise disjoint. This generalizes earlier analogous results of A. Wilkie (for o-minimal expansions of real closed fields) and of M. Edmundo, P. Eleftheriou and L. Prelli (for o-minimal expansions of ordered groups).
[Close]

Philip Ehrlich and Elliot Kaplan, Number systems with simplicity hierarchies: a generalization of Conway's theory of surreal numbers II

In [1], the algebraico-tree-theoretic simplicity hierarchical structure of J. H. Conway's ordered field $\bf No$ of surreal numbers was brought to the fore and employed to provide necessary and sufficient conditions for an ordered field to be isomorphic to an initial subfield of $\bf No$, i.e. a subfield of $\bf No$ that is an initial subtree of $\bf No$. In this sequel to [1], which is joint work with Elliot Kaplan, analogous results for ordered abelian groups and ordered domains are established which in turn are employed to characterize the convex subgroups and convex subdomains of initial subfields of ${\bf No}$ that are themselves initial. It is further shown that an initial subdomain of ${\bf No}$ is discrete if and only if it is an initial subdomain of ${\bf No}$'s canonical integer part ${\bf Oz}$ of omnific integers. Finally, extending results of [1], the theories of nontrivial divisible ordered abelian groups and real-closed ordered fields are shown to be the sole theories of nontrivial densely ordered abelian groups and ordered fields all of whose models are isomorphic to initial subgroups and initial subfields of ${\bf No}$.

References
[1] Philip Ehrlich, Number Systems with Simplicity Hierarchies: A Generalization of Conway's Theory of Surreal Numbers, The Journal of Symbolic Logic, vol. 66 (2001), no. 3, pp. 1231-1258.
[Close]

Oliver Kullmann, Understanding (minimal) unsatisfiability

In my talk I want to give an overview on understanding unsatisfiability of propositional CNFs. One application area is where some kind of artefact (for example a car or a Linux system) is requested, using many options, which is translated into CNF, solved by a SAT solver, and where it then turns out the request was inconsistent – now the user wants to "understand" the inconsistency. In general a CNF $F$ can be unsatisfiable for "many reasons", where we treat a \underline{m}inimally \underline{u}nsatisfiable $F' \subseteq F$ as "one reason". In my talk I concentrate on such MUs $F'$ (alone). Another motivation is that such MUs can be considered as the hardest instances for SAT solvers and propositional proof systems (not having additional helper clauses). See [2] for a general overview. The classical paper, which started the investigations, is [1], showing that, using modern terminology, the "deficiency" of an MU is at least $1$, i.e., there is at least one more clause than there are variables. The central conjecture of the field is that for every fixed deficiency all MUs can be described by finitely many patterns. See the extensive introduction of [3] for a recent overview.

References
[1] Ron Aharoni and Nathan Linial, Minimal Non-Two-Colorable Hypergraphs and Minimal Unsatisfiable Formulas, Journal of Combinatorial Theory, Series A, vol. 43 (1986), no. 2, pp. 196–204.
[2] {Hans {Kleine Büning} and Oliver Kullmann}, Minimal Unsatisfiability and Autarkies, Handbook of Satisfiability (Armin Biere and Marijn J.H. Heule and Hans van Maaren and Toby Walsh, editors), IOS Press, 2009, pp. 339–401.
[3] Oliver Kullmann and Xishun Zhao, Bounds for variables with few occurrences in conjunctive normal forms, arXiv:1408.0629, 2016.
[Close]

Olaf Beyersdorff and Ján Pich, Understanding Gentzen and Frege systems for QBF

Recently Beyersdorff, Bonacina, and Chew [1] introduced a natural class of Frege systems for quantified Boolean formulas (QBF) and showed strong lower bounds for restricted versions of these systems. Here we provide a comprehensive analysis of their new extended Frege system, denoted EF+$\forall$red, which is a natural extension of classical extended Frege EF. Our main results are the following: Firstly, we prove that the standard Gentzen-style system $G_1^*$ p-simulates EF+$\forall$red and that $G_1^*$ is strictly stronger under standard complexity-theoretic hardness assumptions. Secondly, we show a correspondence of EF+$\forall$red to bounded arithmetic: EF+$\forall$red can be seen as the non-uniform propositional version of intuitionistic $S^1_2$. Specifically, intuitionistic $S^1_2$ proofs of arbitrary statements in prenex form translate to polynomial-size EF+$\forall$red proofs, and EF+$\forall$red is in a sense the weakest system with this property. Finally, we show that unconditional lower bounds for EF+$\forall$red would imply either a major breakthrough in circuit complexity or in classical proof complexity, and in fact the converse implications hold as well. Therefore, the system EF+$\forall$red naturally unites the central problems from circuit and proof complexity. Technically, our results rest on a formalised strategy extraction theorem for EF+$\forall$red akin to witnessing in intuitionistic $S^1_2$ and a normal form for EF+$\forall$red proofs.

References
[1] O. Beyersdorff, I. Bonacina, L. Chew, Lower bounds: From circuits to QBF proof systems, Proc. ACM Conference on Innovations in Theoretical Computer Science (ITCS), ACM, 2016, pp. 249–260.
[Close]

Murdoch Gabbay, What are variables of first-order logic and the lambda-calculus?

Intuitively, conjunction corresponds to sets intersection; disjunction corresponds to sets union; and negation corresponds to sets complement. If we axiomatise these connectives in universal algebra then we obtain Boolean algebras. Every Boolean algebra can be presented as a field of sets, and in this sense conjunction is sets intersection; disjunction is sets union; and negation is sets complement. First-order logic has variables. The usual approach to variables is to assign them values with a valuation, which is just a lookup table. An alternative is offered by nominal algebra, an extension of universal algebra with nominal-style names and binding. This admits a simple finite axiomatisation of variables and substitution as just another `connective'. That is, substitution is a single logical connective, with an associated standard finite algebraic theory (no axiom-schemes). Furthermore, we can finitely axiomatise quantifiers in nominal algebra, including:

• the $\forall$ universal quantifier of first-order logic,
• the $\lambda$ of the untyped lambda-calculus, and
• the sets comprehension binder in set theory.

Remarkably, we can extend the presentation as a field of sets to these algebraic theories, and even extend Stone duality to give full topological dualities for first-order logic and the untyped lambda-calculus (the treatment of set theory is the topic of a separate abstract). By this account, substitution, quantification, and $\lambda$-abstraction become

• axiomatisations in nominal algebra alongside those for conjunction, disjunction, and negation; and dually, they become
• operations on sets of points of topological spaces–which turn out to be fairly elementary–existing alongside sets intersection, union, and complement.

This approach to semantics differs from what is usually found in the textbooks, and it offers some technical advantages: the axioms for $\forall$ and $\lambda$ do not reference the axioms for substitution, or vice versa, and this decoupling of the algebraic theories is reflected in the concrete proofs and modular constructions. A general method seems to be emerging here. The end results are clean, elegent, non-evident, and suggestive of future work.
[Close]

Noam Zeilberger, Linear lambda terms as invariants of rooted trivalent maps

Recent work on the combinatorics of linear lambda calculus (also known as BCI combinatory logic) has uncovered a variety of surprising connections to the theory of graphs on surfaces (also known as "maps"). The main purpose of the talk will be to convey a simple and conceptual account for one of these connections, namely the correspondence (originally described by Bodini, Gardy, and Jacquot) between $\alpha$-equivalence classes of closed linear lambda terms and isomorphism classes of rooted trivalent maps on compact oriented surfaces without boundary, as an instance of a more general correspondence between linear lambda terms with a context of free variables and rooted trivalent maps with a boundary of free edges. After recalling some basic definitions as well as a familiar diagrammatic representation for linear lambda terms, I'll explain how the "easy" direction of the correspondence is a simple forgetful operation which erases annotations on the diagram of a linear lambda term to produce a rooted trivalent map. The other more surprising direction views linear lambda terms as topological invariants of their underlying rooted trivalent maps, reconstructing the missing information through a Tutte-style recurrence on maps with free edges. As an application in combinatorics, I'll show how to use this analysis to enumerate bridgeless rooted trivalent maps as linear lambda terms containing no closed subterms, and conclude by giving a natural reformulation of the Four Color Theorem as a statement about typing in lambda calculus. \bibliographystyle{abbrvnat}

References
[1] H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, Studies in Logic 103, second, revised edition, North-Holland, Amsterdam, 1984.
[2] O. Bodini, D. Gardy, and A. Jacquot. Asymptotics and random sampling for BCI and BCK lambda terms. Theoretical Computer Science, 502:227–238, 2013.
[3] Sergei K. Lando and Alexander K. Zvonkin. Graphs on Surfaces and Their Applications, Encyclopaedia of Mathematical Sciences 141, Springer-Verlag, 2004.
[4] Noam Zeilberger and Alain Giorgetti. A correspondence between rooted planar maps and normal planar lambda terms. Logical Methods in Computer Science, 11(3:22):1–39, 2015.
[5] Noam Zeilberger. Counting isomorphism classes of $\beta$-normal linear lambda terms. September 25, 2015. arXiv:1509.07596
[6] Noam Zeilberger. Linear lambda terms as invariants of rooted trivalent maps. December 21, 2015. arXiv:1512.06751
[Close]

Paolo Torrini, Dependent Types and Linear Scoping

In languages based on nominal types, a type is characterised by its abstract structure together with its name. In pure languages, an abstract characterisation of nominal types can rely on usual nominal techniques. Things can get more complicated, for instance, when we consider records with mutable fields, where a name refers to a resource and may represent a physical address. This is also the case of class types in object-oriented languages. An abstract characterisation of effectful nominality can be useful in dealing with encapsulation and inheritance, to specify shape transformation, and to express locality of resources with respect to code blocks. In [1] we extended a system of linear dependent types by allowing linear types to depend on locally non-linear terms (L-terms). L-variables and L-terms can be interpreted as addresses of abstract locations. L-variables can also be understood as names, as equivariant renaming is admissible, with the implicit guarantee that the same name cannot be associated with different locations. The evaluation of L-terms is orthogonal to that of value terms. Linear scoping is defined as L-variable binding, based on a linear form of $\Sigma$-types that combines effectfulness and scoping. This notion of binding associates system components, represented as linear types, to the abstract locations they can access, thus enforcing locality of free L-terms. Linear scoping can be used to specify mutable record types compatibly with their nominal characterisation. More generally, this approach could give us a simple way to model abstractly aspects of object orientation and resource virtualisation, by using dependent types to type statically programs that involve dynamic, effectful operations such as reallocation and optimisation of memory use.

References
[1] P. Torrini, Linear types and locality, Journal of Logic and Computation, vol. 24 (2014), no. 3, pp. 655–685.
[Close]

Ryszard Mirek, Renaissance Geometry

Renaissance mathematicians and geometers like Piero della Francesca and Luca Pacioli refers directly or indirectly to Euclidean geometry. For instance, Piero della Francesca in his proofs refers to the similarity of the triangles. In Elements discussion of these issues is in the Book VI, Proposition 4 to 8. There is also no doubt that Piero is familiar with Book XIII of Elements. Piero constructs each of the regular solids from its circumsphere, but unlike Euclid, he gives a numerical value for the diameter of the sphere. In turn, in Proposition I.8 he shows that the perspective images of orthogonals converge to a centric point what follows from Euclid's theorem from the Book VI, Proposition 21. On the other hand, Luca Pacioli provides a direct reference to Elements and the precise information are given to where the result is proved by Euclid.
My goal here is to provide a detailed analysis of the methods of inference that are employed in the Renaissance treatises. For this purpose one can use a formal system EF that seems to present in a precise and visually readable way the geometrical systems.
This research is supported by the NCN research grant 2012/07/B/HS1/01986.
[Close]

Jeff Paris and Alena Vencovska, The Indian Syllogism as analogical reasoning

When H.T.Colebrooke first introduced to the West the so called Indian or Hindu Syllogism from Gotama's Nyaya-Sutra (c.100CE) at his lecture to the Royal Asiatic Society in 1824 it caused a flurry of excitement, not least amongst the main logicians at the time, Babbage, De Morgan, and Boole. For it seemed that here was some independent development of logic within the subcontinent, breaking the Aristotelian monopoly and providing the space for new ideas to develop. Subsequently however a section of Britain's Victorian Society, perhaps reluctant to acknowledge such advanced thinking in what was after all one of its colonies, contemptuously `downgraded' the syllogism to the status of analogy, an example of reasoning from particular to particular without any genuine soundness or even justification. Whilst most commentators today hold this reading to be incorrect I will argue that notwithstanding even when viewed as a schema of analogical reasoning the syllogism has a demonstrably rational justification within the context of Pure Inductive Logic.
[Close]

Sara L. Uckelman, The Logic of Where and While in the 13th and 14th Centuries

Medieval analyses of molecular propositions include many non-truth-func\-tional connectives in addition to the standard modern binary connectives (conjunction, disjunction, and conditional). Two types of non-truthfunctional molecular propositions considered by a number of 13th- and 14th-century authors are temporal and local propositions, which combine atomic propositions with `while' and `where'. Despite modern interest in the historical roots of temporal and tense logic, medieval analyses of `while' propositions are rarely discussed in modern literature, and analyses of `where' propositions are almost completely overlooked. In this paper we introduce 13th- and 14th-century views on temporal and local propositions, and connect the medieval theories with modern temporal and spatial counterparts.
[Close]

Radek Honzik and Sarka Stejskalova, The tree property and the continuum function below $\aleph_\omega$

Both authors were supported by FWF/GAČR grant I 1921-N25.
We say that a regular cardinal $\kappa$, $\kappa> \aleph_0$, has the tree property if there are no $\kappa$-Aronszajn trees; we say that $\kappa$ has the weak tree property if there are no special $\kappa$-Aronszajn trees. Starting with infinitely many weakly compact cardinals, we show that the tree property at every even cardinal $\aleph_{2n}$, $0<n<\omega$, is consistent with an arbitrary continuum function below $\aleph_\omega$ which satisfies $2^{\aleph_{2n}}>\aleph_{2n+1}$, $n<\omega$. Next, starting with infinitely many Mahlo cardinals, we show that the weak tree property at every cardinal $\aleph_n$, $1 < n <\omega$, is consistent with an arbitrary continuum function which satisfies $2^{\aleph_n} > \aleph_{n+1}$, $n<\omega$. Thus the tree property has no provable effect on the continuum function below $\aleph_\omega$ except for the trivial requirement that the tree property at $\kappa^{++}$ implies $2^\kappa>\kappa^+$ for every infinite $\kappa$.
[Close]

Tanmay Inamdar, A fragment of PFA consistent with large continuum

The side condition method of Todorčević is an important technique to build proper partial orders. It has been used to establish several consequences of PFA, the most important of which are the Open Graph Axiom as well as the P-Ideal Dichotomy. Many of these applications can be reformulated to assert that given a graph on an uncountable set, if there is a proper $\sigma$-ideal which is well behaved in a certain way with respect to this graph, then a certain partial order to add an uncountable clique to this graph is proper. On the other hand, in recent years Asperó and Mota have developed new techniques to iterate proper partial orders which have allowed them to establish the consistency of several consequences of PFA with the continuum large. In my talk I shall talk about how using the methods of Asperó and Mota, one can get models where the continuum is arbitrarily large, Martin's Axiom holds, and a certain `side condition forcing axiom' holds for graphs on $\omega_1$ and $\omega_1$-generated $\sigma$-ideals. For example, such models have no S-spaces, $\omega_1 \rightarrow (\omega_1, \alpha)^2$ holds for any countable ordinal $\alpha$, and certain restricted forms of OGA and PID hold.
[Close]

Sherwood Hachtman, Determinacy and admissible reflection

For transitive sets $X$, let $\mathfrak{M}(X)$ denote the least admissible set containing $X$ as an element. Say $\kappa$ reflects admissibly if for any $\Pi_1$ formula $\varphi$ and $A \subseteq V_\kappa$, if $(V_{\kappa+1}, \in, A) \models \varphi$, then for some $\alpha < \kappa$, $(V_{\alpha+1} \cap \mathfrak{M}(V_\alpha), \in, A \cap V_\alpha) \models \varphi$. Note that if we replaced $\mathfrak{M}(V_\alpha)$ with $V_{\alpha+1}$, this would simply be weak compactness of $\kappa$. But admissible reflection is much weaker. Our interest in this principle is due to its use in calibrating the strength of determinacy hypotheses. We show that the minimal model of NBG+"ON reflects admissibly" satisfies clopen, but not open, determinacy for proper class games; this answers a question of Gitman & Hamkins.
[Close]

Philipp Schlicht and Fabiana Castiblanco, Tree forcings and sharps

The Levy-Solovay theorem shows that any measurable cardinal $\kappa$ is preserved by all forcings of size strictly less than $\kappa$, and there are similar results for many other large cardinals. Moreover, many global consequences of large cardinals are preserved by certain forcings. For instance, a sharp for a set of ordinals $x$ states the existence of a non-trivial elementary embedding $j\colon L[x]\rightarrow L[x]$ with $\mathrm{crit}(j)>\sup(x)$. It is well-known that the existence of sharps for all sets of ordinals is preserved by all forcings. In this project, we study interesting consequences of large cardinals in $H(\omega_1)$ and prove that they are preserved under certain proper forcings. In particular, we study the existence of sharps for all sets of ordinals in $H(\omega_1)$, equivalently analytic determinacy. We show that this condition is preserved by various tree forcings, for instance Mathias forcing, Sacks forcing and Laver forcing.
[Close]

Philipp Lücke, The infinite productivity of Knaster properties

Given an uncountable regular cardinal $\kappa$, we say that a partial order $\mathbb{P}$ is $\kappa$-Knaster if every set of $\kappa$-many conditions in $\mathbb{P}$ contains a subset of cardinality $\kappa$ consisting of pairwise compatible conditions. This strengthening of the $\kappa$-chain condition is typically used because of its nice product behavior: finite support products of $\kappa$-Knaster partial orders are $\kappa$-Knaster, and the product of a $\kappa$-Knaster partial order with a partial order satisfying the $\kappa$-chain condition satisfies the $\kappa$-chain condition. Moreover, if $\kappa$ is weakly compact, then the class of $\kappa$-Knaster partial orders is closed under $\nu$-support products for every $\nu<\kappa$. This raises the question whether it is possible that the class of $\kappa$-Knaster partial orders is closed under countable support products and $\kappa$ is not weakly compact. I will present results that show that the axioms of $\mathrm{ZFC}$ do not answer this question. This is partially joint work with Sean Cox (VCU Richmond).
[Close]

Marija Boricic, Natural deduction probabilized

By combining Gentzen's and Prawitz's approach to deductive systems and Carnap–Popper–type probability logic semantics, we introduce a probabilistic version of inference rules of natural deduction $\mathbf{NK}$, denoted by $\mathbf{NKprob}$. Probabilized natural deduction systems have already been considered (see [2], [3] and [4]). For each propositional formula $A$ and each $a,b\in I$, where $I$ is a finite subset of reals $[0,1]$ containing $0$ and $1$, closed under addition, the expression $A[a,b]$ is probabilized formula in $\mathbf{NKprob}$. The meaning of $A[a,b]$ is that 'the probability $c$ of truthfulness of a sentence $A$ belongs to the interval $[a,b]$'. Our system contains at least two inference rules for each connective, one introducing, and the other one eliminating the connective. For example, the following rules are treating the introduction and elimination of disjunction: $$\frac{A[a,b]\quad B[c,d]}{(A\vee B)[\max(a,c),b+d]}(I\vee)\qquad\frac{A[a,b]\quad (A\vee B)[c,d]}{B[c-b,d]}(E\vee)$$ Also, there are specific rules treating inconsistency: $$ \frac{\begin{matrix} \dfrac{\underline{[A[c_1,c_1]]}}{A\emptyset} \dfrac{\underline{[A[c_2,c_2]]}}{A\emptyset} \dots \dfrac{\underline{[A[c_m,c_m]]}}{A\emptyset} \end{matrix} } {A\emptyset}(I\emptyset) \qquad\frac{A\emptyset}{B[a,b]}(E\emptyset)$$ for any propositional formulae $A$ and $B$, and any $a, b \in I=\{c_1, c_2, \dots c_m\}$, where $A\emptyset$ is $A[a,b]$, for $a>b$. Let $\text{For}$ be the set of all propositional formulae. Then any mapping $p:\text{For}\to I$ will be an $\text{\bf NKprob}$–model if it satisfies the following conditions: (i) $p(\top)=1$ and $p(\bot)=0$; (ii) if $p(A\wedge B)=0$, then $p(A\vee B)=p(A)+p(B)$; (iii) if $A\leftrightarrow B$ in classical logic, then $p(A)=p(B)$. We prove that our probabilistic natural deduction system $\mathbf{NKprob}$ is sound and complete with respect to this kind of models (see [1]).

References
[1] M. Boričić, Inference rules for probability logic, Publications de l'Institut Mathématique (to appear)
[2] A. M. Frisch, P. Haddawy, Anytime deduction for probabilistic logic, Artificial Intelligence, vol. 69 (1993), pp. 93–122.
[3] T. Hailperin, Probability logic, Notre Dame Journal of Formal Logic, vol. 25 (1984), pp. 198–212.
[4] C. G. Wagner, Modus tollens probabilized, British Journal for the Philosophy of Science, vol. 54(4) (2004), pp. 747–753.
[Close]

Nobu-Yuki Suzuki, Relations among some weak variants of existence and disjunction properties in intermediate predicate logics

We discuss relationships among the existence property (EP), disjunction property (DP), and their weak variants in the setting of intermediate predicate logics. These weak variants were treated in [1] for constructing intermediate logics having EP but lacking DP. This revealed that EP and DP are independent in intermediate logics. We show the relationships among these properties and their combinations. The properties we discuss are as follows. A(n intermediate predicate) logic $\mathbf{L}$ is said to have EP, if $\mathbf{L} \vdash \exists xA(x)$ implies that there is a variable $v$ such that $\mathbf{L} \vdash A(v)$. A logic $\mathbf{L}$ is said to have DP, if $\mathbf{L} \vdash A \lor B$ implies that $\mathbf{L} \vdash A$ or $\mathbf{L} \vdash B$. A logic $\mathbf{L}$ is said to have the sentential existence property if for every sentence $\exists xA(x)$, $\mathbf{L} \vdash \exists xA(x)$ implies that there exists a fresh variable $v$ such that $\mathbf{L} \vdash A(v)$. A logic $\mathbf{L}$ is said to have the weak existence property, if for every formula $\exists xA(x)$ and every finite non-empty $\{v_1, \dots, v_n\}$ of individual variables such that $FV(\exists xA(x)) \subseteq \{v_1, \dots, v_n\}$, $\mathbf{L} \vdash \exists xA(x)$ implies $\mathbf{L} \vdash A(v_1) \vee \cdots \vee A(v_n)$. Moreover, we introduced a very weak DP called $Z$-normality. The $Z$-normality is important in the consideration of the relation between EP and DP; every $Z$-normal logic with EP has DP.

References
[1] Suzuki, N.-Y., A negative solution to Ono's problem P52: Existence and disjunction properties in intermediate predicate logics, to appear.
[2] Suzuki, N.-Y., Some weak variants of the existence and disjunction properties in intermediate predicate logics, submitted.
[Close]

Bahareh Afshari, Stefan Hetzl and Graham Leigh, Structural representation of Herbrand's theorem

We present recent results on the deepening connection between proof theory and formal language theory. To each first-order proof with cuts of complexity at most $\Pi_n$/$\Sigma_n$, we associate a typed (non-deterministic) tree grammar of order $n$ (equivalently, an order $n$ recursion scheme) that abstracts the computation of Herbrand sets obtained through Gentzen-style cut elimination. Apart from offering a means to compute Herbrand expansions directly from proofs with cuts, these grammars provide a structural counterpart to Herbrand's theorem that opens the door to tackling a number of questions in proof-theory such as proof equivalence, proof compression and proof complexity, which will be discussed. The grammars presented naturally generalise the rigid regular and context-free tree grammars introduced in [2] and [1] that correspond to (respectively) proofs with $\Pi_1$/$\Sigma_1$ and $\Pi_2$/$\Sigma_2$ cuts.

References
[1] Bahareh Afshari, Stefan Hetzl, and Graham E. Leigh, Herbrand disjunctions, cut elimination and context-free tree grammars, 13th International Conference on Typed Lambda Calculi and Applications (Warsaw, Poland), (Thorsten Altenkirch, editor), vol. 38, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2015, pp. 1–16.
[2] Stefan Hetzl, Applying tree languages in proof theory, Language and Automata Theory and Applications: 6th International Conference (A Coruña, Spain), (Adrian-Horia Dediu and Carlos Martín-Vide, editors), vol. 7183, Springer Berlin Heidelberg, 2012, pp. 301–312.
[Close]

Graham Leigh, The simple truth

What is implicit in the acceptance of the Tarskian truth biconditionals? In this talk I will present recent results that characterise the proof- and truth-theoretic content of iterated reflection principles over disquotational theories of truth. In particular, I confirm the conjecture that, modulo reflection, all there is to compositional and Kripke–Feferman truth is captured by simple and natural collections of local truth and falsity biconditionals.
[Close]

Kentaro Sato, Monotone induction can be prolonged by exponential

The usual formulation of induction is the implication from $A(0)$ and $\forall n(A(n)\,{\to}\,A(n{+}1))$ to $\forall xA(x)$. A less popular formulation, called cumulative induction, is formulated by the implication from $\forall n((\forall k\,{<}\,n)B(k)\,{\to}\,B(n))$ to $\forall xB(x)$. Practically, the difference is: in proofs by cumulative induction, we can use all $B(k)$ for $k$ below $n$ in order to show $B(n)$, whereas in those by usual induction we can use only $A(n)$ to show $A(n{+}1)$. However, if we consider these schemata for classes of formulae closed under bounded quantifiers, the difference is, usually, not so important, for we can replace $A(n)$ by $(\forall k\,{<}\,n)B(k)$. Now a natural question is: how about transfinite induction? The trick increases the complexity, as the quantifier $\forall\xi\,{\prec}\,\alpha$ is not bounded. In this talk, I consider a transfinite analogue of the usual formulation of induction, the implication from \[\forall\alpha((\forall\xi\,{\prec}\,\alpha)(\exists\eta\,{\prec}\,\alpha) (\eta\,{\succeq}\,\xi\,{\land}\,A(\eta))\,{\to}\,A(\alpha))\] to $\forall\alpha A(\alpha),$ and compare it with the usual formulation of transfinite induction, which is a straightforward generalization of the cumulative one. Under the monotoneness assumption $\xi\,{\prec}\,\eta\land A(\eta)\,{\to}\,A(\xi)$, both are equivalent. I will show that the supremum of those ordinals along which this "cofinal induction" for $\Delta^0_0$ formulae is provable in ${\bf I}\boldsymbol{\Sigma}_n$ is $\omega_{n+2}$ (including $n\,{=}\,0$) where $\omega_0\,{=}\,1$, $\omega_{k+1}\,{=}\,\omega^{\omega_k}$. This is longer than that for the usual transfinite induction for $\Delta_0$ formulae, by exponential base 2, or, for $n\,{\geq}\,1$, equivalently base $\omega$.
[Close]

David Bradley-Williams, Limits of betweenness relations

Betweenness relations on semilinear orderings, among other tree-like relational stuctures, were studied extensively by Adeleke and Neumann in [3]. Such tree-like structures were also investigated though a host of examples constructed by Cameron in [6]. Adeleke and Macpherson [2] then built on this knowledge to determine that when a transitive permutation group is a Jordan group, it preserves one from a list of various kinds of relational structures. Some of these structures are quite well understood as relational structures, but there are cases in which the invariant structure appears only as an exotic infinite `limit' of more familiar structures. In this talk we will discuss what `limits of betweenness relations' are and how they have been constructed (by Adeleke [1], Bhatacharjee and Macpherson [4] and myself [5]).

References
[1] S. A. Adeleke, On irregular infinite Jordan groups, Communications in Algebra, vol. 41 (2013), no. 4, pp. 1514–1546.
[2] S. A. Adeleke and D. Macpherson, Classification of infinite primitive Jordan permutation groups, Proceedings of the London Mathematical Society, vol. 72 (1996), no. 3, pp. 63–123.
[3] S. A. Adeleke and P. M. Neumann, Relations related to betweenness: their structure and automorphisms, Memoirs of the American Mathematical Society, The American Mathematical Society, \textbf{623}, 1998.
[4] M. Bhattacharjee and D. Macpherson, Jordan groups and limits of betweenness relations, Journal of Group Theory, vol. 9 (2006), no. 1, pp. 59–94.
[5] D. Bradley-Williams, Jordan groups and homogeneous structures, PhD Thesis, University of Leeds, 2015.
[6] P. Cameron, Some treelike objects, The Quarterly Journal of Mathematics, vol. 38 (1987), no. 2, pp. 155–183.
[Close]

Thomas Coleman, Permutation monoids and MB-homogeneous structures

Group embeddable monoids, by their nature, can be represented as a submonoid of permutations contained in some symmetric group Sym$(X)$. As every finite group embeddable monoid is a group, we consider infinite submonoids $B$ of the infinite symmetric group Sym$(\mathbb{N})$ to avoid triviality; such a $B$ is an infinite permutation monoid. Natural examples of these occur via the bimorphism monoid Bi$(\mathcal{A})$ of a structure; that is, the collection of bijective endomorphisms of $\mathcal{A}$. It follows that every automorphism of $\mathcal{A}$ is a bimorphism of $\mathcal{A}$ but in general the converse is not true; and so we have that Aut$(\mathcal{A})\subseteq$ Bi$(\mathcal{A})\subseteq$ Sym$(A)$, where $A$ is the domain of $\mathcal{A}$. Recent work in this field by Cameron and Nešetřil [1] and Lockett and Truss [2] generalizes the idea of homogeneity to several notions of homomorphism-homogeneity. One such example is the property of MB-homogeneity: a structure $\mathcal{A}$ is MB-homogeneous if every monomorphism between finite substructures of $\mathcal{A}$ extends to a bimorphism of $\mathcal{A}$. Lockett and Truss completely classified homomorphism-homogeneous countable posets in [2]. In this talk, connections between permutation monoids and bimorphism monoids of structures are explored in order to develop a notion of oligomorphicity for infinite permutation monoids. In addition to this, a version of Fraïssé's theorem is shown for MB-homogeneous structures, extending work of [1]. Finally, we construct $2^{\aleph_0}$ non-isomorphic examples of MB-homogeneous graphs and take steps towards a classification result. This is joint work with David Evans and Robert Gray during the course of my PhD studies.

References
[1] P. J. Cameron, J. Nešetřil, Homomorphism-homogeneous relational structures, Combinatorics, Probability and Computing, vol. 15 (2006), no. (1-2), pp. 91-103.
[2] D. C Lockett, J. K. Truss, Some more notions of homomorphism-homogeneity, Discrete Mathematics, vol. 336 (2014), pp. 69-79.
[Close]

Daoud Siniora, A dense locally-finite subgroup of the automorphism group of a free homogeneous structure

Consider an amalgamation class of finite relational structures which has the free amalgamation property. We show that the automorphism group of its Fraisse limit has a dense locally-finite subgroup.
[Close]

Dario Garcia, On variations of unimodularity and measurability.

Unimodularity was defined by Hrushovski in [3] where he proved that a unimodular strongly minimal set is one-based, thus generalising Zilber's result that a locally finite strongly minimal set is locally modular. Recently, Hrushovski has re-visited unimodularity in the context of pseudofinite structures, aiming to develop an intersection theory for definable pseudofinite sets. It was claimed in [3] that unimodularity was equivalent to an a priori different notion called functional unimodularity in [1] and [2].
Pillay and Kestner [4] have distinguished two types of functional unimodularity: one for definable sets and one for type-definable sets. They also showed that for strongly minimal theories, unimodularity is equivalent to functional unimodularity for arbitrary types, and is also equivalent to the structures being measurable in the sense of [5].
In this talk we introduce yet another variant called correspondence unimodularity and present a study of the relationship between these different concepts. The main results state that unimodularity is equivalent to both correspondence unimodularity and to functional unimodularity for complete types, and for $\omega$-stable theories unimodularity is also equivalent to both correspondence and functional unimodularity for partial types.
Finally, we showed that all variants of unimodularity coincide for strongly minimal theories, and more generally for non multi-dimensional theories where the dimensions are associated to strongly minimal types.
This is joint work with Frank Wagner (Université Claude Bernard - Lyon 1).

References
[1] R. Elwes, Asymptotic classes of finite structures, Journal of Symbolic Logic, vol. 72 (2007), no. 2, pp. 418–438.
[2] R. Ewes, E. Jaligot, D. Macpherson, M. Ryten, Groups in simple and pseudofinite theories, Proceedings of the London Mathematical Society, vol. 103 (2011), no. 6, pp. 1049–1082.
[3] E. Hrushovski., Unimodular minimal structures., Journal of the London Mathematical Society, vol. 46 (1992), no. 3, pp. 385–396.
[4] C. Kestner, A. Pillay, Remarks on unimodularity, Journal of Symbolic Logic., vol. 76 (2011), no. 4, pp. 1453–1458.
[5] D. Macpherson, C. Steinhorn., Definability in classes of finite structures, Finite and Algorithmic Model Theory. (Javie Esparza, Christian Michaux and Charles Steinhorn, editors), London Mathematical Society, Cambridge University Press, 2011, pp. 140–176.
[Close]

Sylvy Anscombe, Generalised measurable structures with the Tree Property

In [1], Chatzidakis, van den Dries, and Macintyre gave an asymptotic description of the number of points in definable sets in finite fields, building on earlier celebrated work of Lang and Weil, [2], for varieties. Later, in [3], Macpherson and Steinhorn turned these results into the definition of a `one-dimensional asymptotic class'. This is a class $\mathcal{C}$ of finite structures in which, given a definable set $X$, there is a real number $r$ and a natural number $d$ such that the number of points in $X$ in a structure $M\in\mathcal{C}$ is approximately equal to $r\,|M|^{d}$. Moreover, the pair $(r,d)$ may be chosen somewhat uniformly, if $X$ is allowed to vary through a definable family. Taking ultraproducts of such classes, yields a `measurable structure': an infinite structure equipped with a function \begin{align*} \mathrm{Def}(M)&\longrightarrow\mathbb{R}_{\geq0}\times\mathbb{N}
X&\longmapsto(r,d) \end{align*} satisfying certain natural axioms which correspond to the intuition that $r$ is the `measure' and $d$ is the `dimension' of $X$. In particular, the fact that dimension takes values in the natural numbers implies that any measurable structures is supersimple, of finite rank. In joint work between the speaker and Macpherson, Steinhorn, and Wolf, we have broadened this framework to allow more exotic measures and dimensions. We call such structures `generalised measurable'. In this talk we describe several key examples of generalised measurable structures, including the generic triangle-free graph which has the Tree Property of the First Kind.

References
[1] Zoe Chatzidakis, Lou van den Dries, and Angus Macintyre", Definable sets over finite fields", Journal fur die Reine und Angewandte Mathematik, vol. 427 (1992), pp. 107–136.
[2] Serge Lang and Andre Weil, Number of points of varieties in Finite Fields", American Journal of Mathematics, vol. 76 (1954), pp. 819–827.
[3] Dugald Macpherson and Charles Steinhorn, One-dimensional asymptotic classes of finite structures", Transactions of the American Mathematical Society, vol. 360 (2008), pp. 411–448.
[Close]

Alireza Mofidi, Some symbolic dynamical views in model theory

The topological dynamical aspects of model theory in particular stability theory has been recently investigated in several papers such as [2], [3] and [4]. We will have a symbolic dynamical and ergodic theoretical point of view, two other essential point of views in the theory of dynamical systems, to the action of automorphisms and definable groups on certain model theoretic objects, such as stone spaces, models, etc, in particular in the presence of invariant measures. Note that applications of measures as a technique in stability theory are extensively studied in several papers such as [1]. We borrow the notion of symbolic representation from dynamical systems theory and develop it in the context of model theory. In particular, the symbolic representations of actions on spaces of types will be under consideration. We generalize this notion in a way that deals with some standard definition of products of types (studied in for example [3]) as well as product of measures. In the particular case of the action of the group $\mathbb{Z}$ (which includes the case of action of single automorphisms), we characterize some stability theoretic hierarchies in particular NIP. Moreover, we make connections between the symbolic representations of spaces of types and certain mathematical notions such as the rotation number of circle homeomorphisms, Bohr sets and some additive number theoretic definitions.

References
[1] E. Hrushovski and A. Pillay, On NIP and invariant measures, Journal of the European Mathematical Society, vol.13 (2011), pp.1005–1061.
[2] L. Newelski, Topological dynamic of definable group actions, Journal of Symbolic Logic, 74 (2009), pp. 50-72.
[3] L. Newelski, Model theoretic aspects of the Ellis semigroup, Israel J. Math, 190(2012), 477-507.
[4] A. Pillay, Topological dynamics and definable groups, J. Symbolic Logic, 78 (2013), no. 2, 657-666.
[Close]

Alexandre Ivanov, Sofic metric groups and continuous logic

Let us consider the class $\mathcal{G}$ of all continuous structures which are metric groups $(G,d)$ with bi-invariant metrics $d\le 1$. Let $\mathcal{G}_{sof} \subset \mathcal{G}$ be the subclass of all closed metric subgroups of metric ultraproducts of finite symmetric groups with Hamming metrics. We call metric groups from $\mathcal{G}_{sof}$ sofic metric groups. The class $\mathcal{G}_{w.sof}$ of weakly sofic continuous metric groups, consists of continuous metric groups $(G,d)$ which embed into metric ultraproducts of finite metric groups with invariant metrics bounded by 1. In a similar way we define the classes $\mathcal{G}_{l.sof}$ and $\mathcal{G}_{hyplin}$ of continuous metric groups which are linear sofic and hyperlinear as metric groups. We study relationship among the classes of the collection $$ \{ \mathcal{G} , \mathcal{G}_{sof} , \mathcal{G}_{w.sof} , \mathcal{G}_{hyplin}, \mathcal{G}_{l.sof} \} . $$ All of them are axiomatizable in continuous logic. It is clear that $\mathcal{G}_{sof} \subseteq \mathcal{G}_{w.sof} \subseteq \mathcal{G}$. Moreover, by some arguments of Arzhantseva and Päunescu $\mathcal{G}_{l.sof} \subseteq \mathcal{G}_{w.sof}$. We show that the class $\mathcal{G}_{w.sof} \setminus (\mathcal{G}_{sof} \cup \mathcal{G}_{hyplin} \cup \mathcal{G}_{l.sof})$ is not empty. We emphasize that in these classes groups are considered together with metrics. Thus Gromov's problem if any group is sofic [1] still remains open. We also show that the question of all possible inclusions above is reduced to discrete members of these classes.

References
[1] V.Pestov, Hyperlinear and sofic groups: a brief guide, Bulletin of Symbolic Logic, vol. 14 (2008), no. 4, pp. 449–480.
[Close]

Juan de Vicente, Locally $\mathbb{C}$-Nash groups

Locally $\mathbb{C}$-Nash groups are analytic groups which also carry a semialgebraic structure –- seing $\mathbb{C}$ as $\mathbb{R}^2$. For example, the universal coverings of algebraic groups are locally C-Nash groups. The definition of the latter is based on the concept of $\mathbb{C}$-Nash map, which has been studied –- with may be other names –- by different authors (see e.g. [1],[2]). In this talk we give a classification of abelian locally $\mathbb{C}$-Nash groups of dimension one and two. (Joint work with E. Baro and M. Otero.)

References
[1] J. Adamus and S. Randriambololona, Tameness of holomorphic closure dimension in a semialgebraic set, Mathematische Annalen, vol.355 (2013), no.3, pp.985–1005.
[2] Y. Peterzil and S. Starchenko, Complex analytic geometry in a nonstandard setting, Model theory with applications to algebra and analysis. Vol. 1 (Z. Chatzidakis, D. Macpherson, A. Pillay, A. Wilkie, editors), Cambridge Univ. Press, 2008, pp. 117–165.
[3] E. Baro, J. de Vicente, M. Otero, Locally $\mathbb{C}$-Nash groups, In preparation.
[Close]

Nurlan Kogabaev, Freely generated projective planes with finite computable dimension

In [1] it was proved that every countable free projective plane has computable dimension either $1$ or $\omega$. Futhermore, such a plane is computably categorical if and only if it has finite rank. Hence the natural question arises: can we extend the above results to the case of freely generated projective planes? In particular, we are interested in the existence question of computably categorical freely generated projective plane of infinite rank. We also investigate the realizability of finite computable dimension $n>1$ in the class of freely generated projective planes. In [2] it was shown that the class of symmetric irreflexive graphs is complete in the following computable-model-theoretic sense: for every countable structure $\mathcal{A}$, there exists a countable symmetric irreflexive graph $\mathcal{G}$ which has the same degree spectrum as $\mathcal{A}$, the same $\mathbf{d}$-computable dimension as $\mathcal{A}$ (for each degree $\mathbf{d}$), the same computable dimension as $\mathcal{A}$ under expansion by a constant, and which realizes every degree spectrum $\mathrm{DgSp}_{\mathcal{A}}(R)$ (for every relation $R$ on $\mathcal{A}$) as the degree spectrum of some relation on $\mathcal{G}$. In the present paper we construct an effective coding of symmetric irreflexive graphs into freely generated projective planes preserving most computable-model-theoretic properties and obtain the following result.

Theorem. The class of freely generated projective planes is complete with respect to degree spectra of nontrivial structures, $\mathbf{d}$-computable dimensions, expansion by constants, and degree spectra of relations. In particular, for every natural $n\geqslant 1$ there exists a freely generated projective plane of infinite rank with computable dimension $n$.

This work was supported by RFBR (grant 14-01-00376-a) and by the Grants Council under RF President for State Aid of Leading Scientific Schools (grant NSh-6848.2016.1).

References
[1] N.T.Kogabaev, The class of projective planes is noncomputable, Algebra and Logic, vol. 47 (2008), no. 4, pp. 242–257.
[2] D.R.Hirschfeldt, B.Khoussainov, R.A.Shore, A.M.Slinko, Degree spectra and computable dimensions in algebraic structures, Annals of Pure and Applied Logic, vol. 115 (2002), no. 1-3, pp. 71–113.
[Close]

Ruslan Kornev, Reducibilities of computable metrics on the real line

We are concerned with a natural computable-model-theoretic question for uncountable metric spaces: do there exist computable metric spaces, equivalent in some standard sense but not computably equivalent? Pour-El and Richards [2] considered different countable dense substructures of a given Banach space up to computable isometries; see also more recent papers [3] and [4]. In contrast, our goal is to construct computably inequivalent metrics on a separable space with fixed dense subset. In this talk, two notions of computable reducibility of metrics are discussed. One of them is induced by reducibility of Cauchy representations. Namely, let $\rho$ and $\rho'$ be complete metrics on a separable space $X$, let $W$ be a countable dense subset of $X$, enumerated by integers. We say that the metric $\rho$ is computably reducible to the metric $\rho'$ (and denote this as $\rho\leq_c\rho'$) if the Cauchy representation $\delta_\rho$ of effective metric space $(X, \rho, W)$ is computably reducible to the representation $\delta_{\rho'}$ of the space $(X, \rho', W)$; precise definitions can be found in [1]. It is possible to characterize $\leq_c$ in the following terms: $\rho\leq_c\rho'$ iff the identity homeomorphism $\text{id}_X$ is $(\delta_\rho,\delta_{\rho'})$-computable. Based on this, we introduce weak reducibility of metrics: we say $\rho\leq_{ch}\rho'$ if there exists a $(\delta_\rho,\delta_{\rho'})$-computable autohomeomorphism of $X$. Clearly, $c$-reducibility implies $ch$-reducibility. The results obtained are mainly related to the case $X=\mathbb{R}$ with the standard real line topology and $W=\mathbb{Q}$.

Theorem. All convex (i.e., admitting midpoints) computable metrics on the reals are $c$-equivalent.

Theorem. Any countable tree $T$ can be isomorphically embedded into the ordering of computable metrics on the reals under $c$-reducibility.

Theorem. There exists a countable sequence of computable metrics on $\mathbb{R}$ which are not $ch$-reducible to each other. Informally, copies of the real line, equipped with these metrics, are pairwise homeomorphic, but not computably homeomorphic.

References
[1] K. Weihrauch, Computable Analysis. An Introduction, Springer-Verlag, Berlin/Heidelberg, 2000.
[2] M. B. Pour-El, J. I. Richards, Computability in Analysis and Physics, Springer-Verlag, Berlin, 1989.
[3] Z. Iljazović, Isometries and Computability Structures, Journal of Universal Computer Science, vol. 16 (2010), no. 18, pp. 2569–2596.
[4] A. G. Melnikov, Computably Isometric Spaces, Journal of Symbolic Logic, vol. 78 (2013), no. 4, pp. 1055–1085.
[Close]

Nikolay Bazhenov, Effective categoricity for polymodal algebras

Let $\mathbf{d}$ be a Turing degree. A computable structure $\mathcal{A}$ is $\mathbf{d}$-computably categorical if for every computable structure $\mathcal{B}$ isomorphic to $\mathcal{A}$, there is a $\mathbf{d}$-computable isomorphism from $\mathcal{A}$ onto $\mathcal{B}$. The categoricity spectrum of $\mathcal{A}$ is the set $$ CatSpec(\mathcal{A}) = \{ \mathbf{d} \,\colon \mathcal{A} \text{ is } \mathbf{d} \text{-computably categorical} \}. $$ The results of [1] imply that not every categoricity spectrum is the categoricity spectrum of a Boolean algebra. A natural question that arises is the following: how does expanding the language of Boolean algebras affect categoricity spectra and other related properties? Hirschfeldt, Khoussainov, Shore, and Slinko [2] introduced the notion of a class which is complete with respect to degree spectra of nontrivial structures, effective dimensions, expansion by constants, and degree spectra of relations. For brevity, we call such classes HKSS-comp\-lete. If a class $K$ is HKSS-complete, then for every computable structure $\mathcal{S}$, there is a structure $\mathcal{A}_{\mathcal{S}}\in K$ with the property $CatSpec(\mathcal{A}_{\mathcal{S}}) = CatSpec(\mathcal{S})$. Khoussainov and Kowalski [3] proved that the class of Boolean algebras with operators is HKSS-complete. They also asked whether the similar result is true for polymodal algebras. Here we give the positive answer to the question:

Theorem. The class of Boolean algebras with four distinguished modalities is HKSS-complete.

In particular, this result implies that every categoricity spectrum is the categoricity spectrum of some polymodal algebra. This work was supported by the Grants Council (under RF President) for State Aid of Leading Scientific Schools (grant NSh-6848.2016.1).

References
[1] N.A. Bazhenov, $\Delta^0_2$-categoricity of Boolean algebras, Journal of Mathematical Sciences, vol. 203 (2014), no. 4, pp. 444–454.
[2] D.R. Hirschfeldt, B. Khoussainov, R.A. Shore, A.M. Slinko, Degree spectra and computable dimensions in algebraic structures, Annals of Pure and Applied Logic, vol. 115 (2002), no. 1–3, pp. 71–113.
[3] B. Khoussainov, T. Kowalski, Computable isomorphisms of Boolean algebras with operators, Studia Logica, vol. 100 (2012), no. 3, pp. 481–496.
[Close]

Sergey Goncharov, Nikolay Bazhenov and Margarita Marchuk, Autostability relative to strong constructivizations of computable 2-step nilpotent groups

For a class K of structures, closed under isomorphism, the index set is the set I(K) of all indices for computable members of K in a universal computable numbering of all computable structures for a fixed computable language. We study the complexity of the index set of class of computable structures, which are autostable relative to strong constructivizations. A computable model $\mathcal{M}$ is called strongly constructivizable if there exists a decidable model $\mathcal{N}$ such that $\mathcal{N}$ is isomorphic to $\mathcal{M}$. A strongly constructivizable model $\mathcal{M}$ is autostable relative to strong constructivizations if for any decidable copies $\mathcal{N}_0$ and $\mathcal{N}_1$ of the model $\mathcal{M}$, there is a computable isomorphism $f : \mathcal{N}_0 \rightarrow \mathcal{N}_1$. Using the result of [1] for rings and a coding of rings into groups due to Mal'cev [2] we prove the following theorem.

Theorem. The index set $SCAut(Gr)$ of computable 2-step nilpotent groups, which are autostable relative to strong constructivizations is $m$-complete $\Sigma^{0}_3(\emptyset^{\omega})$.

This work was supported by RFBR (grant 14-01-00376) and by the Grants Council (under RF President) for State Aid of Leading Scientific Schools (grant NSh-6848.2016.1). The second author was supported by RFBR (research project No. 16-31-60058 mol\_a\_dk).

References
[1] S. S. Goncharov, N. A Bazhenov., M. I. Marchuk, The index set of Boolean algebras autostable relative to strong constructivizations, Siberian Mathematical Journal, vol. 56 (2015), no. 3, pp. 393–404.
[2] A. Malícev, On a correspondence between rings and groups, American Mathematical Society Translations, series 2, vol. 45 (1965), pp. 221–232.
[Close]

Birzhan Kalmurzaev, Note on cardinality of Rogers semilattices

It is easy to show that

• For every family $\mathcal{S}$ on $n$-c.e. sets, if the Rogers semilattice $\mathcal{R}_m^{-1}(\mathcal{S})$ is infinite for some $m\geq n$ then $\mathcal{R}_m^{-1}(\mathcal{S})$ is infinite for all $k\geq m$.
• For every two-element family of $n$-c.e. sets $\mathcal{S}=\{A,B\}$, the Rogers samilattices $\mathcal{R}_m^{-1}(\mathcal{S})$ is infinite if $m>2n$. If $n$ is even, then this statement is true for $m=2n$.

All known Rogers semilattices of the family in the hierarchy of Ershov are either one-element or infinite. Theorem ([1]). For every nonzero $n\in \omega \cup \{\omega\}$, and for every ordinal notation $a$ of a nonzero ordinal, there exists a $\Sigma_a^{-1}$-computable family $\mathcal{A}$ of exactly $n$ sets such that $|\mathcal{R}_a^{-1}(\mathcal{A})|=1$. Main result: Theorem. For every nonzero $n\in \omega$, there exist $n$-c.e. sets $A$ and $B$ such that $$|\mathcal{R}_n^{-1}(A,B)|=|\mathcal{R}_{n+1}^{-1}(A,B)|=\ldots=|\mathcal{R}_{2n}^{-1}(A,B)|=1   \text{if}  n  \text{is odd},$$ $$|\mathcal{R}_n^{-1}(A,B)|=|\mathcal{R}_{n+1}^{-1}(A,B)|=\ldots=|\mathcal{R}_{2n-1}^{-1}(A,B)|=1  \text{if}  n  \text{is even}.$$ Corollary. For every nonzero $n\in \omega$ and for every $n<m\leq2n$, there exist $n$-c.e. sets $A$ and $B$ such that $$1=|\mathcal{R}_n^{-1}(A,B)|=\ldots=|\mathcal{R}_{m-1}^{-1}(A,B)|<|\mathcal{R}_{m}^{-1}(A,B)|.$$ Question. Does there exist a family of sets in some level of the hierarchy of Ershov whose Rogers semilattice consists of $2, 3, \ldots$ elements?

References
[1] Serikzhan A. Badaev, Mustafa Manat, Andrea Sorbi, Rogers semilattices of families of two embedded sets in the Ershov hierarchy, Mathematical Logic Quarterly, vol. 58 (2012), no. 4-5, pp. 366–376.
[Close]

Dimitris Tsementzis, A Syntactic Characterization of Morita Equivalence

We characterize Johnstone's [2] topos-theoretic notion of Morita equivalence of theories in terms of an extended notion of a common definitional extension developed by Barrett and Halvorson [3]. We thus provide a purely syntactic characterization of the relation between two theories that have equivalent categories of models naturally in any Grothendieck topos. Our investigation may be understood as an inversion of the work of Awodey-Forsell [1] and Makkai [5]. There the question is asked: what extra structure do we need to impose on the category of models of a theory in order to recover the theory up to logical equivalence? Here, we answer the following: if we identify a theory with its category of models, then from a syntactic point of view what can we recover it up to? We will first describe in detail the proof in the coherent fragment of (many-sorted) first-order logic. Then we will describe how to extend our method to regular, cartesian, geometric and full first-order theories. Finally, as an application, we provide a new proof (originally in [4]) that $\omega$-categoricity for complete geometric theories is invariant under Morita equivalence.

References
[1] S. Awoday, H. Forsell, First-Order Logical Duality, Annals of Pure and Applied Logic, vol. 164 (2013), no. 3, pp. 319–348.
[2] P. Johnstone, Sketches of an Elephant: A Topos Theory Compendium, Oxford University Press, 2003.
[3] T. Barrett and H. Halvorson, Morita Equivalence, Available at http://arxiv.org/abs/1506.04675
[4] O. Caramello, Atomic Toposes and Countable Categoricity, Applied Categorical Structures, vol. 4 (2012), pp. 379–391.
[5] M. Makkai, Stone Duality for First-Order Logic, Advances in Mathematics, vol. 65 (1987), no. 2 pp. 97–170.
[Close]

Ian Orton and Andrew Pitts, Axioms for modelling cubical type theory in a topos

The homotopical approach to intensional type theory views proofs of equality as paths. We explore what is required of an interval-like object $\mathtt{I}$ in a topos to give a model of type theory in which elements of identity types are morphisms from $\mathtt{I}$. Cohen, Coquand, Huber and Mörtberg give such a model using a particular category of presheaves [1]. We investigate the extent to which their model construction can be expressed in the internal type theory of any topos and identify a collection of quite weak axioms for this purpose. This clarifies the definition and properties of the notion of Kan filling that lies at the heart of their constructive interpretation of Voevodsky's univalence axiom. Furthermore, since our axioms can be satisfied in a number of different ways, we show that there is a range of topos-theoretic models of homotopy type theory in this style. This work presented in this talk is described in more detail in [2]

References
[1] C. Cohen, T. Coquand, S. Huber and A. Mörtberg, Cubical Type Theory: a Constructive Interpretation of the Univalence Axiom, Preprint, Dec, 2015.
[2] I. Orton and A. Pitts, Axioms for Modelling Cubical Type Theory in a Topos, Preprint, April, 2016.
[Close]

Eric Faber, Relative computability in realisability toposes

When the effective topos was first devised in [3], Martin Hyland cunningly revealed the remarkably rich structure of its lattice of local operators: this admits an embedding of the Turing degrees. Consequently, a Turing degree represented by a function $f: \mathbb{N} \rightarrow \mathbb{N}$ corresponds to a subtopos $\mathit{Eff}_f$ of the effective topos. In [1], Jaap van Oosten and the author show a partial converse to this result; namely that restricted to the category of realisability toposes, the subtoposes of $\mathit{Eff}$ are precisely those of the form $\mathit{Eff}_f$ for a partial function $f$. Here, a realisability topos $\text{rt}(A)$ is a topos constructed from a tripos on a partial combinatory algebra (pca) $A$. The partial converse seems particular to the effective topos, but Hylands observation can be extended to realisability toposes. For any pca $A$ and partial map $f: A \rightarrow A$, there is a corresponding subtopos $\text{rt}(A)_f$ of $\text{rt}(A)$, which is a realisability topos, and for total functions $f$ this is the largest subtopos in which $f$ is computable, or realised. In [2], we exhibit a technique to force a functional $F: A^A \rightarrow A$ to be internally realised. The resulting class of subtoposes $\text{rt}(A)_F$ relative to a functional $F$ happens to be contained in the class of subtoposes $\text{rt}(A)_f$ relative to a partial function $f$. In the effective topos, the technique can be used to force internal functionals on the natural numbers object. This theory is related to the theory on effective operations. With this work we aim to extract the computational content from local operators, which one can now regard as "generalised oracles". Examples of local operators not captured by the above show that there is still a lot to be understood.

References
[1] Faber, E. and van Oosten, J., More on geometric morphisms between realizability toposes, Theory and Applications of Categories, vol. 29 (2014), pp. 874–895.
[2] ― Effective operations of type 2 in PCAs, Computability, vol. 5 (2016), no. 2, pp. 127–146.
[3] Hyland, J.M.E., The effective topos, The L.E.J. Brouwer Centenary Symposium (Noordwijkerhout, 1981), Studies in Logic and the Foundations of Mathematics, vol. 110, North-Holland, Amsterdam-New York, 1982, pp. 165–216.
[Close]

Jacopo Emmenegger and Erik Palmgren, Exact completion and constructive theories of sets

In [2] Palmgren proposed a constructive and predicative version of Lawvere's Elementary Theory of the Category of Sets (ETCS), called CETCS, which provides a structuralist foundation for constructive mathematics in the style of Bishop. As shown in [2], a CETCS category is precisely a well-pointed locally cartesian closed pretopos with a natural number object and enough projectives. In both the intended models of CETCS categories, namely setoids in Martin-Löf type theory and sets in Aczel's CZF, sets can be seen as quotients of projective sets and can thus be regarded as exact completions. We generalise this approach to CETCS categories and characterise them in terms of weaker properties of their projective covers. In particular, it seems that Carboni and Rosolini's characterisation of local closure [1] in terms of weak closure of the maximal projective cover cannot be applied in this case, because splitting of idempotents is undecidable in Martin-Löf type theory. We solve this issue providing an alternative characterisation of local closure that applies to any projective cover. We apply this characterisation to the category of small types in Martin-Löf type theory with a universe and basic type formers, obtaining as a consequence that the category of setoids is a CETCS category.

References
[1] {A. Carboni and G. Rosolini}, {Locally cartesian closed exact completions}, {Journal of Pure and Applied Algebra}, vol. 154 (2000), no. 1–3, pp. 103–116.
[2] {E. Palmgren}, {Constructivist and structuralist foundations: Bishop's and Lawvere's theories of sets}, {Annals of Pure and Applied Logic}, vol. 163 (2012), no. 10, pp. 1384–1399.
[Close]

Maria Emilia Maietti, Fabio Pasquali and Giuseppe Rosolini, When the tripos-to-topos construction factors through the elementary quotient completion

Maietti and Rosolini in [4] generalized the notion of exact completion on a weakly lex category in [3] to that of elementary quotient completion of a Lawvere's elementary doctrine. From the logic point of view a Lawvere's elementary doctrine, denoted with $(\mathbb{C},P)$, can be seen as a many sorted conjunctive logic $P$ with equality depending on sorts which are objects of a category $\mathbb{C}$. The elementary quotient completion of $(\mathbb{C},P)$, denoted by $(\mathbb{C}_q,P_q)$, is a way to obtain a new elementary doctrine whose base is closed under effective quotients of equivalence relations expressed in the logic $P_q$.
In this talk we focus on triposes, which are a special class of Lawvere's elementary doctrines introduced in [1] to build elementary toposes by mean of the so-called tripos-to-topos construction. We characterize when the tripos-to-topos construction factors through an elementary quotient completion by using a result in [5].
Our main result is that an elementary topos arising from a tripos $(\mathbb{C},P)$ is the elementary quotient completion of the free full comprehension of the starting tripos $(\mathbb{C},P)$ if and only if the tripos $(\mathbb{C},P)$ validates a form of rule of choice inspired by Hilbert epsilon operator and introduced in [2].

References
[1] J.M.E. Hyland, P.T. Johnstone, A.M.Pitts, Tripos theory, Mathematical Proceedings of the Cambridge Philosophical Society, vol. 88 (1980), no. 2, pp. 205–232.
[2] F. Pasquali, Hilbert's {$\epsilon$}-operator in doctrines, IfCoLog Journal of Logics and their Applications, To appear.
[3] A. Carboni, R. Celia Magno, The free exact category on a left exact one, Journal of the Australian Mathematical Society, vol. 33 (1982), no. 3, pp. 295–301.
[4] M.E.Maietti, G. Rosolini, Elementary quotient completion, Theory and applications of categories, vol. 27 (2013), no. 17, pp. 445–463.
[5] M. E. Maietti, G. Rosolini, Relating quotient completions via categorical logic, In Dieter Probst and Peter Schuster (eds.), "Concepts of Proof in Mathematics, Philosophy, and Computer Science". Ontos Mathematical Logic. Walter de Gruyter, Berlin., To appear.
[Close]

Anupam Das, Intuitionistic bounded arithmetic and monotone proof complexity

This work concerns the relationship between weak theories of arithmetic and the complexity of proofs in propositional logic. We introduce a hierarchy of intuitionistic theories of bounded arithmetic, based on Buss' second-order (classical) theories $U^1_2$ and $V^1_2$ [2] as developed in [3], by controling the type-level of induction formulae, i.e. the nesting to the left of an implication symbol. We calibrate a Paris-Wilkie style propositional translation from bounded arithmetic with a Brouwer-Heyting-Kolmogorov interpretation of implication as transformation of proofs. As a result, we obtain a general translation from arbitrary proofs of $\Pi^0_1$ sentences in intuitionistic bounded arithmetic to monotone propositional proofs, i.e. proofs free of negation. In the case of type-level 1 the complexity of the transformation is quasipolynomial-time. In order to deal with second-order existential quantifiers we prove a sort of witnessing theorem, reducing the interaction between induction and comprehension to a form of iterated comprehension, thereby sidestepping the need for extension variables that may introduce complications with respect to negation. Finally we show that this amount of negation, type-level 1, is sufficient to prove a converse result, the soundness of monotone propositional proofs, thereby establishing a full correspondence. This talk is based on work appearing in [1].

References
[1] Anupam Das, From positive and intuitionistic bounded arithmetic to monotone proof complexity, LICS '16 Accepted. 2016.
[2] Samuel R. Buss. Bounded arithmetic, Bibliopolis, Naples, 1986.
[3] Jan Krajíček. Bounded arithmetic, propositional logic, and complexity theory, Cambridge University Press, New York, 1995.
[Close]

Robert Lubarsky, D-Fan and c-Fan

Brouwer's Fan Theorem – that every binary tree with no infinite path is finite – is an important principle in constructive mathematics. Various fragments of the Fan Theorem, which limit the trees to which it applies, have been of interest over the years, because they are equivalent to basic principles of analysis. These weakenings of Fan are easily seen to be implicationally linear: \begin{equation*} \textrm{FAN}_{\mathrm{full}} \Rightarrow \textrm{FAN}_{\Pi^{0}_{1}} \Rightarrow \textrm{FAN}_{c} \Rightarrow \textrm{FAN}_{\Delta}. \end{equation*} The obvious question is whether those implications are strict. Some of them were shown over the years to be strict, by a variety of methods; in [4], they were all shown to be strict, by a fairly uniform method. Here I provide a new proof that Decidable Fan ($\textrm{FAN}_{\Delta}$) does not imply c-Fan ($\textrm{FAN}_{c}$). The argument is a mixture of realizability, Heyting-valued models, and Kripke models. It remains possible, yet still unknown, that the same method will separate the other implications.

References
[1] Michael Beeson, Foundations of Constructive Mathematics, Springer, 1985
[2] Josef Berger, A separation result for varieties of Brouwer's Fan Theorem, in Proceedings of the 10th Asian Logic Conference (ALC 10), Kobe University in Kobe, Hyogo, Japan, September 1-6, 2008 (Arai et al., eds.), World Scientific, 2010, p. 85 - 92
[3] Michael Fourman and J.M.E. Hyland, Sheaf models for analysis, in Applications of Sheaves, Lecture Notes in Mathematics 753 (Fourman, Mulvey and Scott, eds.), Springer, 1979, p. 280 - 301
[4] Robert Lubarsky and Hannes Diener, Separating the Fan Theorem and Its Weakenings, Journal of Symbolic Logic, 79 (2014), pp. 792-813, doi: 10.1017/jsl.2014.9
[Close]

Tatsuji Kawai and Matthew de Brecht, Interactions between powerlocales and Scott topology on locally compact locales

We study interactions between three powerlocales on a locally compact locale $X$: upper powerlocale $\mathrm{P_U}(X)$; lower powerlocale $\mathrm{P_L}(X)$; and Scott topology $\mathbb{S}^{X}$, where $\mathbb{S}^{X}$ is the exponential over the Sierpinski locale $\mathbb{S}$. It is well known that upper and lower powerlocales commute [1], and that composition of upper and lower powerlocales coincides with taking Scott topology twice [3], i.e. $\mathrm{P_U}(\mathrm{P_L}(X)) \cong \mathrm{P_L}(\mathrm{P_U}(X)) \cong \mathbb{S}^{\mathbb{S}^{X}}$. In this talk, we show that three powerlocales commute in a mixed way, i.e. $\mathrm{P_U}(\mathbb{S}^{X}) \cong \mathbb{S}^{\mathrm{P_L}(X)}$ and $\mathrm{P_L}(\mathbb{S}^{X}) \cong \mathbb{S}^{\mathrm{P_U}(X)}$. This gives us a complete picture of how these powerlocales on locally compact locales interact with each other. The result is obtained in the setting of formal topology [2]. This work was supported by JSPS Core-to-Core Program, A. Advanced Research Networks. The first author was supported by JSPS KAKENHI Grant Number 15K15940.

References
[1] P. T. Johnstone and S. Vickers, Preframe presentations present, Category Theory, (A. Carboni, M. Pedicchio, and G. Rosolini, editors), Lecture Notes in Mathematics, vol. 1488, Springer, Berlin Heidelberg, 1991, pp. 193–212.
[2] G. Sambin, Intuitionistic formal spaces –- a first communication, Mathematical Logic and its Applications, vol. 305, (D. Skordev, editor), Plenum Press, New York, 1987, pp. 187–204.
[3] S. Vickers, The double powerlocale and exponentiation: A case study in geometric logic, Theory and Applications of Categories, vol. 12 (2004), no. 13, pp. 272–422.
[Close]

Tin Lok Wong, A new construction of models of the Weak K\"onig Lemma

The subsystem $\mathrm{WKL}_0$ of second-order arithmetic occupies a prominent position in reverse mathematics. Nonstandard models of $\mathrm{WKL}_0$ are typically constructed using forcing arguments in which conditions are trees. Recently, Enayat and I [1] found an alternative construction based on the Arithmetized Completeness Theorem (ACT), which is a formalization of Gödel's Completeness Theorem in arithmetic. In the talk, I will demonstrate how to enhance our method to perform more delicate constructions in Simpson–Tanaka–Yamazaki [2]. In particular, I will present a new proof of the conservativity of $\mathrm{WKL}_0$ over $\mathrm{RCA}_0$ for sentences of the form $\forall X \exists!Y \theta(X,Y)$, where $\theta(X,Y)$ is an arithmetical formula. The heart of our construction is a forcing argument in which conditions are theories. This research is joint with Ali Enayat, University of Gothenburg, Sweden.

References
[1] Ali Enayat and Tin Lok Wong, Model theory of $\mathrm{WKL}_0^*$, Preprint available at http://www.logic.univie.ac.at/~wongt9/papers/ew-wkl0star.pdf.
[2] Stephen G. Simpson, Kazuyuki Tanaka, and Takeshi Yamazaki, Some conservation results on Weak König's Lemma, Annals of Pure and Applied Logic, vol. 118 (2002), no. 1–2, pp. 87–114.
[Close]

Bruno Dinis and Fernando Ferreira, Interpreting weak König's lemma in nonstandard theories of arithmetic

A number of nonstandard versions of Gödel's system T (introduced in [4]) were recently developed. These systems are based on Nelson's IST version of nonstandard analysis [5]. Not without surprise, these developments pointed out relations between constructive notions and nonstandard ones. We show that weak König's lemma can be interpreted in the nonstandard theories presented in [3] and in [1]. These interpretations provide yet another route for proving Friedman's conservation theorem of ${\sf WKL}_0$ over ${\sf RCA}_0$. This work was done in collaboration with Fernando Ferreira [2].

References
[1] B. van den Berg, E. Briseid, and P. Safarik, A functional interpretation for nonstandard arithmetic, Annals of Pure and Applied Logic, vol. 163(2012), pp. 1962–1994.
[2] B. Dinis, F. Ferreira, Interpreting weak König's lemma in nonstandard theories of arithmetic. Manuscript in preparation.
[3] F. Ferreira and J. Gaspar, Nonstandardness and the bounded functional interpretation, Annals of Pure and Applied Logic, vol. 166(2015), pp. 701–712.
[4] K. Gödel, Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes, Dialectica, vol. 12(1958), pp. 280–287.
[5] E. Nelson, Internal set theory: A new approach to nonstandard analysis, Bulletin of the American Mathematical Society, vol. 83(1977), pp. 1165–1198.
[Close]

Emanuele Bottazzi, A nonstandard generalization of the space of distributions and the Schwartz impossibility theorem

In 1954, L. Schwartz proved that there is no differential algebra $(A, +, \otimes, D)$ in which the real distributions $\mathcal{D}'$ can be embedded and the following conditions are satisfied:

• $\otimes$ extends the product over $C^0$ functions;
• $D$ extends the distributional derivative $\partial$;
• the product rule holds: $D(u\otimes v) = (Du)\otimes v + u\otimes(Dv)$.

However, $\mathcal{D}'$ can be embedded in a space of functions of nonstandard analysis in a way that conditions 1.–3. are satisfied with only an infinitesimal perturbation. Let $^\ast\mathbb{R}$ be a set of hyperreals of nonstandard analysis, let $\varepsilon\in\,\! ^\ast\mathbb{R}$ be a positive infinitesimal, and let $(^\ast\mathbb{R}^\Lambda, +, \cdot)$ be the vector space of $^\ast\mathbb{R}$-valued functions defined on $\Lambda = \{ n\varepsilon : n \in ^\ast{\mathbb{Z}} \}$, with pointwise sum and product. Let $\mathfrak{D}$ be the finite difference operator defined by $$ \mathfrak{D} u(x) = \frac{u(x+\varepsilon)-u(x)}{\varepsilon} $$ for all $u \in \,\! ^\ast\mathbb{R}^\Lambda$. We prove that there is an embedding $\iota : \mathcal{D}' \rightarrow\, ^\ast\mathbb{R}^\Lambda$ and a projection $\pi:\, ^\ast\mathbb{R}^\Lambda \rightarrow \mathcal{D}'$ satisfying:

 0. for all $T \in \mathcal{D}'$, $\pi(\iota(T)) = T$;
 1. the product over $^\ast\mathbb{R}^\Lambda$ extends the product over $\iota(C^0(\mathbb{R}))$;
 2'. $\mathfrak{D}$ extends the distributional derivative $\partial$ in the sense that, for all $T \in \mathcal{D}'$, $$ \pi (\mathfrak{D}(\iota (T))) = \partial T; $$
 3'. for all $u, v \in\,\! ^\ast\mathbb{R}^\Lambda$, the following discrete product rule holds: $$ \mathfrak{D}(u v)(x) = (\mathfrak{D}u(x)) v(x) + u(x+\varepsilon)(\mathfrak{D}v(x)). $$

Thus, $(^\ast\mathbb{R}^\Lambda, +, \cdot, \mathfrak{D})$ provides a non-trivial generalization of the space of distributions.
[Close]

Imme van den Berg, Complete arithmetical solids and nonstandard analysis

A neutrix is a convex additive subgroup of a nonstandard model of the real numbers. Obvious neutrices are £, the external set of of limited numbers and $\oslash $, the external set of infinitesimals, as groups they are not isomorphic. The set of non-isomorphic neutrices is at least countable [1]. An external number $ \alpha $ is the sum $\alpha =a+A$ of a nonstandard real number $a$ and a neutrix $A$. Due to the stability by some shifts, external numbers may be seen as mathematical models of vague transitions of Sorites type, orders of magnitude, or errors of measurement [3]. The external numbers form a completely regular commutative semigroup (union of groups) for addition and multiplication. The distributive law holds up to a neutrix. The order relation is total and respects the operations [3][2]. Dedekind completeness is valid in a model which is sufficiently saturated for Nelson's reduction algorithm [4] to hold: definable halflines either are cofinal with an external number, or there is an external number just beyond. The structure is Archimedean for nonstandard natural numbers. In a joint work with B.Dinis, University of Lisbon, we present a first-order axiomatics for the external numbers in the language $\{+,\cdot ,\leq \}$, using algebraic, analytic and arithmetical axioms. A model is called a complete arithmetical solid. Its precise numbers ($A=\{0\}$) must be contained in a nonstandard model for the real number system.

References
[1] I.P. van den Berg, A decomposition theorem for neutrices, Annals of Pure and Applied Logic, vol. 161 (2010), no. 7, pp. 851–865.
[2] B. Dinis, I. P. van den Berg, Algebraic properties of external numbers, Journal of Logic and Analysis, vol. 3:9 (2011), pp. 1–30.
[3] F. Koudjeti, I.P. van den Berg, Neutrices, external numbers and external calculus, Nonstandard Analysis in Practice (F. Diener and M. Diener, editors), Springer Universitext, Berlin-Heidelberg, 1995, pp. 145–170.
[4] E. Nelson, The syntax of nonstandard analysis, Annals of Pure and Applied Logic, vol. 38 (1988), no. 2, pp. 123–134.
[Close]

Neil Barton, (Sub)systems of second-order set theory

Much of set-theoretic practice concerns questions that are, at first blush, second-order in content. The study of the construction of inner models (such as Woodin's Ultimate-$L$ conjecture and the construction of the Steel Core Model), the investigation of embedding principles (for example large cardinals and Kunen's Theorem that there is no $j: V \longrightarrow V$), and examination of certain kinds of maximality principle (such as Friedman's Inner Model Hypothesis), are all naturally understood as concerning second-order classes rather than sets. Understandably, given the pleasant metalogical properties of first-order $\mathbf{ZFC}$, many set theorists work hard to render their second-order interests in first-order terms. However, increasingly set theorists have become engaged in questions that are greater than first-order (good examples being the results concerning embeddings in [8], the study of open determinacy for class games in [5], and the consistency of principles in [7]). In the philosophical literature, there is a debate concerning how to characterise proper classes within the framework of there being a unique, maximal proper class model of set theory. Traditionally, talk of proper classes in set theory was understood as shorthand for statements definable in terms of first-order formulae with parameters. However, in the last forty years, philosophical conceptions of proper classes have been proposed which aim to capture this essentially second-order character of set-theoretic practice. In particular, [4] and [3] develop a paraphrase in terms of plural quantification, where [2] provides a mereological conception of proper classes. In this paper, we examine what can be extracted from particular philosophical conceptions of classes, focussing on the plural conception. First (\S1), we provide some motivating considerations for the choice of the plural paraphrase. In particular, we argue that the plural paraphrase meshes better with the foundational role many have seen for set theory. Next (\S2), we note that this conception of classes has been viewed to motivate one of two class theories, either (1.) $MK$ (as in [4]) or (2.) $NBG$ (on the basis of recent work by [1]). We argue that this is a false dichotomy; just as in the case of subsystems of second-order arithmetic, we should expect there to be various philosophical motivations for different strengths of class theories both intermediate between $NBG$ and $MK$, and above $MK$. Finally (\S3), we examine some of the relevant technical literature, and draw some philosophical conclusions. We argue that naturalistic considerations motivate the use of some non-definable class talk. In particular, we argue for two conclusions (1.) $\Pi^1_1$-comprehension for classes is motivated by its having many independently justified consequences made clear in the work of [5], and (2.) given a stronger naturalism we can justify the use of strong choice principles for classes extending $MK$ on the basis of work in [6]. We conclude that a detailed philosophical and mathematical study of (sub)systems of second-order set theory is in order, including some which extend $MK$.

References
[1] S. Florio and \O. Linnebo, On the Innocence and Determinacy of Plural Quantification, Noûs, vol. 49 (2015), no. 1, pp. 1–19.
[2] L. Horsten and P. Welch, Reflecting on absolute infinity, Journal of Philosophy, Forthcoming.
[3] G. Uzquiano, Plural quantification and classes, Philosophia Mathematica, vol. 11 (2003), no. 1, pp. 67–81.
[4] G. Boolos, To be is to be a value of a variable (or to be some values of some variables), Journal of Philosophy, vol. 81 (1984), no. 8, pp. 430–449.
[5] V. Gitman and J. Hamkins, Open determinacy for class games, arXiv:1509.01099 [math.LO],
[6] V. Gitman and J. Hamkins and T. Johnstone, Kelley-Morse set theory and choice principles for classes, Unpublished,
[7] S. Friedman, Internal consistency and the inner model hypothesis, Bulletin of Symbolic Logic, vol. 12 (2006), no. 4, pp. 591–600.
[8] J. Vickers and P. Welch, On elementary embeddings from an inner model to the universe, Journal of Symbolic Logic, vol. 66 (2006), no. 3, pp. 1090–1116.
[Close]

Jaykov Foukzon, Inconsistent countable set in second order ZFC and unexistence of the strongly inaccessible cardinals

In this article we derived an important example of the inconsistent countable set in second order $ZFC$ $(ZFC_{2})$ with the full second-order semantic. Main results is:
(i) $\lnot Con(ZFC_{2})$.
(ii) Let $\kappa$ be an inaccessible cardinal and $H_{\kappa}$ is a set of all sets having hereditary size less then $\kappa$, then $\lnot Con(ZFC+(V=H_{\kappa})).$
[Close]

Michael Lieberman and Jiri Rosicky, Abstract tameness from large cardinals, via accessible categories

Tameness of types in an abstract elementary class–the principle that distinct types over large models can be distinguished by restrictions to a submodel of fixed small size–appears as a necessary condition in nearly all of the major classification-theoretic results for AECs. By a theorem of [1], tameness of AECs is known to follow from the existence of a proper class of (almost) strongly compact cardinals. The authors reprove this result in [3] by entirely different methods, namely by reducing tameness to the accessibility of the (powerful) image of a certain accessible functor. We show that this method extends naturally to prove that the metric analogue of tameness holds for metric AECs (analyzed as in [4]) under the same cardinal assumption. While this fact is already known, having been proven by different means in [2], we note that our analysis provides a template for the analysis of tameness more broadly. As in the metric case, we may consider notions of tameness intrinsic to the ambient category of objects over which an abstract class' structures are built–the characterization via accessible images provides a natural, unified framework in which to address these generalized notions.

References
[1] W. Boney, Tameness from large cardinal axioms, Journal of Symbolic Logic, vol. 79 (2014), no. 4, pp. 1092–1119.
[2] W. Boney and P. Zambrano, Around the set-theoretical consistency of d-tameness of abstract elementary classes, arXiv:1508.05529.
[3] M. Lieberman and J. Rosick\'y, Classification theory for accessible categories, Journal of Symbolic Logic, vol. 81 (2016), no. 1, pp. 151–165.
[4] ―, Metric abstract elementary classes as accessible categories, arXiv:1504.02660.
[Close]

Ali Enayat, Paul Gorbow and Zachiri McKenzie, Feferman's forays into the foundations of category theory

This talk is primarily concerned with assessing a set-theoretical system, $S^*$, for the foundations of category theory suggested by Solomon Feferman. $S^*$ is an extension of NFU, and may be seen as an attempt to accommodate unrestricted categories such as the category of all groups (without any small/large restrictions), while still obtaining the benefits of ZFC on part of the domain. A substantial part of the paper is devoted to establishing an improved upper bound on the consistency strength of $S^*$. The assessment of $S^*$ as a foundation of category theory is framed by the following general desiderata (R) and (S). (R) asks for the unrestricted existence of the category of all groups, the category of all categories, the category of all functors between two categories, etc., along with natural implementability of ordinary mathematics and category theory. (S) asks for a certain relative distinction between large and small sets, and the requirement that they both enjoy the full benefits of the ZFC axioms. $S^*$ satisfies (R) simply because it is an extension of NFU. By means of a recursive construction utilizing the notion of strongly cantorian sets, we argue that it also satisfies (S). Moreover, this construction yields a lower bound on the consistency strength of $S^*$. We also exhibit a basic positive result for category theory internal to NFU that provides motivation for studying NFU-based foundations of category theory.
[Close]

Jeffrey Bergfalk, Homological characterizations of ``small'' cardinals

We consider a number of homological invariants of the "small" cardinals $\omega_n$. We show, for example, that $\omega_n$ is the least ordinal whose $n$th sheaf cohomology group is nonzero. The best-understood case is that of $n=1$: here the nonzero group is that of nontrivial coherent families of functions on $\omega_1$. We consider what the (ZFC) existence of analogous, higher-dimensional families corresponding to higher nonzero homology groups begins to tell us about the combinatorics of higher $\omega_n$.
[Close]

Jan Walker, Finitism, truth, and reflection

Let $\mathsf{S}$ be a theory in a language $\mathcal{L}$. Define $\mathsf{Ref}(\mathsf{S})$ as the theory in $\mathcal{L} \cup \{ T \}$ which is obtained by adding to $\mathsf{S}$: first, for all formulae containing $T$, the corresponding substitution instances of axiom schemas and rules of $\mathsf{S}$; second, axioms to the effect that $T$ denotes partial truth in the sense of Saul Kripke [2]. In a seminal article, Solomon Feferman [1] proposed to identify the statements in $\mathcal{L}$ which are derivable in $\mathsf{Ref}(\mathsf{S})$ as the statements in $\mathcal{L}$ one ought to accept if one has accepted $\mathsf{S}$. My talk is inspired by Feferman's approach, but takes a different direction. It starts off with the assumption that only theorems of finitist arithmetic ought to be accepted and aims at answering truth-theoretic questions such as: How to adapt (the axioms for) Kripke's account of truth to what is acceptable from the finitist perspective? How to adapt other prominent conceptions of truth? What features do finitist conceptions of truth have in common? In the sequel of my talk, I will turn to a proof-theoretic analysis of (Turing-like) progressions in which reflection (or formal soundness) principles are successively added to theories in a language of iterated finitist truth.

References
[1] Solomon Feferman, Reflecting on incompleteness, The Journal of Symbolic Logic, vol. 56 (1991), no. 1, pp. 1–49.
[2] Saul Kripke, Outline of a theory of truth, The Journal of Philosophy, vol. 72 (1975), no. 19, pp. 690–716.
[Close]

Anton Freund, The slow reflection hierarchy

We generalize the notion of slow consistency, due to S.-D. Friedman, Rathjen and Weiermann [3], to obtain slow (uniform) reflection statements of arbitrary arithmetical complexity. The resulting hierarchy over Peano Arithmetic is incomparable with the hierarchy of usual reflection principles: No single one of the usual reflection statements implies all slow reflection statements. Interestingly, though, slow reflection is much weaker when it comes to $\Pi_1$-consequences: Any $\Pi_1$-formula that is provable in the slow reflection hierarchy already follows from the (usual) consistency of Peano Arithmetic. For detailed proofs we refer to [2]. Henk and Pakhomov [4] independently establish similar results. A more computational viewpoint is adopted in [1], where we determine the provably total functions of slow $\Sigma_1$-reflection.

References
[1] Anton Freund, Proof lengths for instances of the Paris-Harrington Principle, arXiv:1601.08185 (preprint).
[2] ― Slow reflection, arXiv:1601.08214 (preprint).
[3] Sy-David Friedman, Michael Rathjen, Andreas Weiermann, Slow consistency, Annals of Pure and Applied Logic, vol. 164 (2013), no. 3, pp. 382–393.
[4] Paula Henk, Fedor Pakhomov, Slow and ordinary provability for Peano Arithmetic, arXiv:1602.01822.
[Close]

Andrei Sipos, Proof mining and positive-bounded logic

Proof mining is a research program introduced by U. Kohlenbach in the 1990s ([3] is a comprehensive reference), which aims to obtain explicit quantitative information (witnesses and bounds) from proofs of an apparently ineffective nature. This paradigm in applied logic has successfully led so far to obtaining some previously unknown effective bounds, primarily in nonlinear analysis and ergodic theory. A large number of these are guaranteed to exist by a series of logical metatheorems which cover general classes of bounded or unbounded metric structures. In order to apply these metatheorems, the structures are typically formalized in higher-order systems of arithmetic and analysis, using appropriate codings of real numbers and related operations. The classes for which metatheorems have already been proven include normed spaces and hyperbolic spaces. Recently, Günzel and Kohlenbach [1] have shown that, in principle, one could obtain metatheorems for a plethora of classes of structures, provided that they are formalized in positive-bounded logic (in the sense of Henson and Iovino [2]) and that some preparation of the axioms is undertaken beforehand. We aim to show how this process may be carried out in some additional classes suggested by the two authors above. We illustrate it with some concrete applications.

References
[1] Daniel Günzel and Ulrich Kohlenbach, Logical metatheorems for abstract spaces axiomatized in positive bounded logic, Advances in Mathematics, vol. 290, pp. 503-551 (2016).
[2] C. Ward Henson and Jose Iovino, Ultraproducts in Analysis, in Analysis and Logic, London Math. Soc. Lecture Note Ser., vol. 262, Cambridge Univ. Press, pp. 1–115 (2002).
[3] Ulrich Kohlenbach, Applied proof theory: Proof interpretations and their use in mathematics, Springer Monographs in Mathematics, Springer-Verlag, Berlin-Heidelberg (2008).
[Close]

Leroy Chew, Olaf Beyersdorff and Ilario Bonacina, Lower bounds: from circuits to QBF proof systems

A general and long-standing belief in the proof complexity community asserts that there is a close connection between progress in lower bounds for Boolean circuits and progress in proof size lower bounds for strong propositional proof systems. Although there are famous examples where a transfer from ideas and techniques from circuit complexity to proof complexity has been effective [4], a formal connection between the two areas has never been established so far. Here we provide such a formal relation between lower bounds for circuit classes and lower bounds for $\mathsf{Frege}$ systems for quantified Boolean formulas (QBF). Starting from a propositional proof system $P$ we exhibit a general method how to obtain a QBF proof system $P+\forall$red, which is inspired by the transition from resolution to Q-resolution. For us the most important case is a new and natural hierarchy of QBF $\mathcal{C}$-$\mathsf{Frege}$ systems $\mathcal{C}$-$\mathsf{Frege+}\forall\mathsf{red}$ that parallels the well-studied propositional hierarchy of $\mathcal{C}$-$\mathsf{Frege}$ systems, where lines in proofs are restricted to a circuit class $\mathcal{C}$. Building on earlier work for resolution [1] we establish a lower bound technique via strategy extraction that transfers arbitrary lower bounds for the circuit class $\mathcal{C}$ to lower bounds in $\mathcal{C}$-$\mathsf{Frege+}\forall\mathsf{red}$. By using the full spectrum of state-of-the-art circuit lower bounds [3, 5, 6, 2], our new lower bound method leads to very strong lower bounds for QBF \FREGE systems:

• exponential lower bounds and separations for $\mathsf{AC}^0[p]$-$\mathsf{Frege+}\forall\mathsf{red}$ for all primes $p$;
• an exponential separation of $\mathsf{AC}^0[p]$-$\mathsf{Frege+}\forall\mathsf{red}$ from $\mathsf{TC}^0[p]$-$\mathsf{Frege+}\forall\mathsf{red}$;
• an exponential separation of the hierarchy of constant-depth systems $\mathsf{AC}^0_d$-$\mathsf{Frege+}\forall\mathsf{red}$ by formulas of depth independent of $d$.

In the propositional case, all these results correspond to major open problems.

References
[1] Olaf Beyersdorff, Leroy Chew, and Mikolás Janota. Proof complexity of resolution-based QBF calculi. In 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015), pages 76–89, 2015a.
[2] Ravi B. Boppana and Michael Sipser. Handbook of theoretical computer science (vol. {A}). chapter The Complexity of Finite Functions, pages 757–804. MIT Press, Cambridge, MA, USA, 1990.
[3] Johan Håstad. Almost optimal lower bounds for small depth circuits. In Proc. 18th STOC, pages 6–20. ACM Press, 1986.
[4] Jan Krajíček. Interpolation theorems, lower bounds for proof systems and independence results for bounded arithmetic. The Journal of Symbolic Logic, 62 (2): 457–486, 1997.
[5] Alexander A. Razborov. Lower bounds for the size of circuits of bounded depth with basis $\{ \&, \oplus \}$. Math. Notes Acad. Sci. USSR, 41 (4): 333–338, 1987.
[6] Roman Smolensky. Algebraic methods in the theory of lower bounds for Boolean circuit complexity. In Proc. of 19th ACM STOC, pages 77–82, 1987.
[Close]

Carlo Nicolai, Transfinite induction and reflection for some systems of truth in basic De Morgan logic

Semantic paradoxes force us to question our naïve intuition about truth, encompassed in the schema `$\phi$' is true if and only if $\phi$. They may be approached by giving up the naïve truth schema and retain classical logic; alternatively, one may retain our naïve intuition and abandon classical logic. It has been argued that the latter approach severely cripples our capability of employing mathematical – or more generally extra-semantic – patterns of reasoning in semantics [3]. This is usually motivated by the different amount of transfinite induction that is provable in the classical axiomatization of the fixed point construction of [2] – due to [1] and known as $\mathsf{KF}$ – and the corresponding nonclassical system $\mathsf{PKF}$ formulated in a logic $\mathsf{B}$ featuring only introduction and elimination rules for positive connectives (and their negations) [4]. In the talk we consider several subsystems or extensions of $\mathsf{PKF}$: we focus on (i) a basic disquotational theory extending $\mathsf{B}$ with arithmetical axioms and the basic principles `if $\phi$, then `$\phi$' is true', and `if `$\phi$' is true, then $\phi$' for all sentences in the language with the truth predicate; (ii) a variant of $\mathsf{PKF}$ with no semantic induction; (iii) the extension of $\mathsf{PKF}$ with a rule of transfinite induction up to $\varepsilon_0$ for the entire vocabulary. We first measure the strength of the systems by comparing them to the sentences provably true in $\mathsf{KF}$ and variants thereof. We then consider a strategy for employing – suitably adjusted – reflection principles to climb up, in a rather natural way, from (i) to (iii) via (ii). We conclude by examining the role of reflection and induction in the debate between advocates of the classical and the nonclassical approaches sketched above.

References
[1] Solomon Feferman, Reflecting on incompleteness, The Journal of Symbolic Logic, vol. 56, no. 1 (1991), 1–49.
[2] Saul Kripke, Outline of a Theory of Truth, Journal of Philosophy, no. 72 (1975): 690–712.
[3] Volker Halbach, Axiomatic Theories of Truth. Revised Edition, Cambridge University Press, 2014.
[4] Volker Halbach and Leon Horsten, Axiomatizing Kripke's theory of Truth, The Journal of Symbolic Logic, vol. 71, no. 2 (2006), 677–712.
[Close]

Michael Kompatscher and Trung Van Pham, Constraint satisfaction problems of reducts of the random poset

We present a dichotomy result for computational problems of the form Poset-SAT($\Phi$). In these problems the input consists of variables and constraints about them which have to be taken from $\Phi$, a fixed finite set of quantifier-free formulas in the language of orders. The decision problem is whether the variables can be assigned elements of a partial order so that all constraints are satisfied. We show that Poset-SAT($\Phi$) is NP-complete or solvable in polynomial time. All problems Poset-SAT($\Phi$) can be stated as constraint satisfaction problems of reducts of the random poset, the Fraïssè-limit of all finite partial orders. By studying their polymorphism clones with the help of methods developed by Bodirsky and Pinsker, we show the following result: Either the polymorphism clone contains a weak nu-term (modulo endomorphism) and the CSP is in P, or the problem is NP-complete.
[Close]

Dana Bartosova, Combinatorics of ultrafilters on automorphism groups

For a topological group $G,$ an ambit is a compact pointed space $(X,x_0)$ with a (jointly) continuous action of $G$ on $X$ with the orbit $Gx_0=\{gx_0:g\in G\}$ dense in $X.$ The greatest ambit of $G$, denoted by $S(G),$ is an ambit that has every ambit as its quotient preserving the distringuished points. We will study $S(G)$ for $G$ an automorphism group of a countable first order structure as a space of ultrafilters, describe how the multiplication in $G$ extends to $S(G)$ and show a couple of results about combinatorics and algebra in $S(G).$ This is partially a joint work with Andrew Zucker (CMU).
[Close]

Bektur Baizhanov, Olzhas Umbetbayev and Tatyana Zambarnaya, The properties of linear orders defined on the classes of convex equivalence of 1-formulas

In the report we consider small countable theories with an $\emptyset$-definable binary relation of linear order. Let $A$ be a finite subset of a countable saturated model $N$, and $ H(x)$ and $\Theta (x)$ be $A$-definable $1$-formulas such that $H(N) \subset \Theta(N) $. Define $E _{H,\Theta }(x,y):=H(x)\land H(y)\land (x < y\to\forall z((x < z< y\land\Theta (z))\to H(z)))\land (y<x\to\forall z((y < z < x\land\Theta (z))\to H(z))$. $E_{H,\Theta}(x,y)$ is an $A$-definable relation of equivalence on $H(N)$ such that any $E_{H,\Theta}$-class is convex in $\Theta(N)$. We say that an ordered theory $T$ has the property of finiteness of discrete chains convex equivalences (FDCCE) if for every two one-formulas $H(x)$ and $\Theta (x)$ such that $H(N)\subset \Theta(N)$, for any $k$ ($1<k < \omega$) every discrete chain of convex $E_{H,\Theta}$-classes is finite. We say that the set of $A$-definable one-formulas $C\subset F_1(A)$ is a $BH-algebra$ if it is closed under the following logical operations: $\land$, $\neg$, $\lor$, $\triangleleft^i_k$ ($0<i<k$, $1<k <\omega$).

Theorem. Let $T$ be a small ordered theory with FDCCE, $A$ be a finite subset of a countable saturated model $N$ of the theory $T$. Then for every finite set of $A$-definable one-formulas $\{\phi_1(x), \dots , \phi_n(x)\}$, $n<\omega$ the $BH$-algebra generated by this set is finite.

An ordered theory $T$ is a theory of a pure order if it is in a language $L=\{=,<\}$.

Theorem. Let $T$ be a small theory of a pure order. Then $T$ is $\omega$-categorical if and only if it has FDCCE.

Corollary. Let $T$ be a non-$\omega$-categorical small theory of a pure order. Then there is $\emptyset$-definable $1$-formula $\phi(x)$ such that for some elements $\alpha,\beta \in \phi(N)$ ($\alpha <\beta$), $(\alpha,\beta)\cap \phi(N)$ is an infinite discrete chain.

Corollary. Let $T$ be a countable complete ordered theory in a language $L$ and $T_0\subset T$ be a complete theory in a language $L_0: =\{=,< \}\subset L$. If $T_0$ is non-$\omega$-categorical then $I(T,\omega)=2^{\omega}.$

References
[1] M. Rubin, Theories of linear order, Israel Journal of Mathematics, vol. 17 (1974), pp. 392–443.
[2] S. Shelah, End extensions and numbers of countable models, Journal of Symbolic Logic, vol. 43 (1978), pp. 550–562.
[Close]

Natasha Dobrinen, Claude Laflamme and Norbert Sauer, Rainbow Ramsey simple structures

We prove that the Rado graph $\mathcal{R}$ has the rainbow Ramsey property. This means that given any finite graph $G$, any finite number $k$, and any coloring of the copies of $G$ in the Rado graph, $\mathcal{R}$, where each color appears no more than $k$ times, there is a subgraph $\mathcal{R}'\le \mathcal{R}$ which is also a Rado graph in which the copies of $G$ use each color at most once. More generally, we show that a class of binary relational structures generalizing the Rado graph are rainbow Ramsey. By compactness, it follows that for all finite graphs $B$ and $C$ and any finite number $k$, there is a graph $A$ so that for every coloring of the copies of $C$ in $A$ such that each color is used at most k times, there is a copy $B'$ of $B$ in $A$ in which each copy of $C$ has a different color. This is joint work with Claude Laflamme and Norbert Sauer.
[Close]

Sebastien Vasey, A proof of Shelah's eventual categoricity conjecture in universal classes

Abstract elementary classes (AECs) are an axiomatic framework encompassing classes of models of an $\mathbb{L}_{\infty, \omega}$ theory, as well as numerous algebraic examples. They were introduced by Saharon Shelah forty years ago. Shelah focused on generalizations of Morley's categoricity theorem and conjectured the following eventual version: An AEC categorical in a high-enough cardinal is categorical on a tail of cardinals. I will present my proof of the conjecture for universal classes. They are a special case of AECs (studied by Shelah in a milestone 1987 paper [1]) corresponding to classes of models of a universal $\mathbb{L}_{\infty, \omega}$ theory. An instance of our result is:

Theorem. If $\psi$ is a universal $\mathbb{L}_{\omega_1, \omega}$ sentence that is categorical in some $\lambda \ge \beth_{\beth_{\omega_1}}$, then $\psi$ is categorical in all $\lambda' \ge \beth_{\beth_{\omega_1}}$.

The proof combines Shelah's earlier work on universal classes with a study of AECs that have amalgamation and are tame (a locality property isolated by Grossberg and VanDieren which says roughly that orbital types are determined by their small restrictions).

References
[1] Saharon Shelah, Universal classes, Classification Theory (Proceedings of the U.S.-Israel Workshop on Model Theory in Mathematical Logic held in Chicago, Dec. 15-19, 1985), (John T. Baldwin, editor), vol. 1292, Springer Berlin Heidelberg, 1987, pp. 264–418.
[Close]

Lubna Shaheen, On $\mathbb{F}_1$-geometry and model theory.

(Joint work with Boris Zilber and John Alexander Cruz Morales)
The geometric motivation of the object $\mathbb{F}_1$," the field with one element" came from the work of Jack Tits in 1956, where he explained how one can define the Chevalley group of characteristic un to obtain some interesting geometries such that the symmetric groups happens to be the Weyl group of the corresponding Lie groups. In the last two decades there have been a lot of development, with motivation coming from Arakelov theory and some ideas relating the notion to the Riemann zeta function. We interpret fields of characteristic $1$ and algebras over fields of characteristic $1$ as {\bf multiplicative monoids with a shadow addition} by which we mean structures of the form $(R; \cdot, 0,1, D_1^{m_1,p_1},D_2^{m_2,p_2},\ldots)$ where $(R;\cdot,0,1)$ is a multiplicative commutative monoid with $0$ and $D_k^{m_k,p_k}$ is an $m_k$-ary relation, $p_k$ a prime number or $0$, which we will write in a more suggestive form as a divisor equality $$ n_1x_1+\ldots+n_mx_m\equiv 0\, \mbox{mod}\, p$$ The initial object in the category of $\mathbb{F}_1$-algebras is $\mathbb{F}_1=\{0,1\}$ the field with one element. We define the cyclotomic extensions $\mathbb{F}_{1^{n}}$ of $\mathbb{F}_1$ as the $\mathbb{F}_{1}$-algebra where $R= 0 \cup \mu_{n}.$ We set $\mathbb{F}_1^{alg}=\bigcup_{n\in \mathbb{N}} \mathbb{F}_{1^n}$ (with the universe $\mu_{\infty}\cup \{ 0\}$) and formulate a conjecture that such an object is $\omega$-stable.
[Close]

Gwyneth Harrison-Shermoen, Independence, via limits

The concept of an independence relation (a ternary relation among sets, satisfying certain properties) generalises that of linear independence in vector spaces and algebraic independence in fields, and gives us a way to determine what behaviour is "generic" in a given theory. Kim and Pillay showed [1] that if a theory has an abstract independence relation satisfying an extra property (the "independence theorem over a model"), then the theory is simple and the independence relation is non-forking independence. There are, however, non-simple theories with relations that satisfy quite a few of the desired properties for a notion of independence. Given a large model M of some theory T, and following work of N. Granger [2] (on two-sorted theories of infinite-dimensional vector spaces over an algebraically closed field and with a bilinear form), we describe a method of lifting independence relations from the (tame) theories of substructures of M to a reasonably well-behaved notion of independence in M. This talk is based on work from the author's PhD thesis [3].

References
[1] Byunghan Kim and Anand Pillay, Simple theories, Annals of Pure and Applied Logic, vol. 88 (1997), no. 2–3, pp. 149–164.
[2] Nicolas Granger, Stability, simplicity, and the model theory of bilinear forms, PhD thesis, University of Manchester, 1999.
[3] Gwyneth Harrison-Shermoen, Independence relations in theories with the tree property, PhD thesis, University of California, Berkeley, 2013.
[Close]

Tim Zander, Higher amalgamation in stable theories

Amalgamating types is an essential tool in stable and simple theories. For example the reason to consider imaginaries in stable theories was exactly done to obtain uniqueness of $2$-Amalgamation over algebraic closed sets. The Independence Theorem in simple theory is nothing more than $3$-Amalgamation over models. But $n$-Amalgamation for $n>3$ can fail in stable theories. But if one expands the theory by certain finite covers (see (called generalised imaginaries) we can still obtain $n$-Amalgamation over the empty set for every $n$ (see 4.11 in [1]). Now if forking is easy enough (SU-rank $1$) this directly translates to Amalgamation over parameters. In general this does not need to hold. This is part of my unpublished PhD-research.

References
[1] Hrushovski, Ehud, Groupoids, imaginaries and internal covers, Turkish Journal of Mathematics, 36(2), pp.173-198.
[Close]

Andrea Sorbi and Uri Andrews, Uniformly effectively inseparable equivalence relations

A computably enumerable equivalence relation (ceer) $R$ is called uniformly effectively inseparable (u.e.i.) if it is nontrivial and there is a computable function $p(a,b)$ such that the partial computable function $\varphi_{p(a,b)}$ witnesses effective inseparability of the pair $([a]_R, [b]_R)$, whenever $a$ and $b$ are non-$R$-equivalent. It is shown in [1] that any u.e.i. ceer $R$ is universal, i.e. for every ceer $S$ there exists a computable function $f$ such that, for all $x,y$, $x \mathrel{R} y$ if and only if $f(x) \mathrel{S} f(y)$. Despite universality, and unlike Smullyan's classical theorem establishing computable isomorphism of any two pairs of effectively inseparable c.e. sets, the u.e.i. ceers do not fall into a unique computable isomorphism type. The previously known largest class of u.e.i. ceers was the class of the uniformly finitely precomplete (u.f.p.) ceers, which can be characterized as those ceers which are computably isomorphic to nontrivial c.e. extensions of the relation $\sim_{PA}$ of provable equivalence in Peano Arithmetic. Answering a question in [1], we show:

Theorem. There exist u.e.i. ceers that are not u.f.p.

Among the u.f.p. ceers, $\sim_{PA}$ itself can be characterized (up to computable isomorphim) as the unique ceer $R$ which has a diagonal function, i.e. a computable function $d$ such that, for all $x$, $x$ and $d(x)$ are non-$R$-equivalent, [2], or equivalently (up to computable isomorphim) as the unique ceer $R$ which has a strong diagonal function, i.e. a computable function $d$ such that for every finite set $D$, $d(D)$ is non-$R$-equivalent to any element in $D$. We show:

Theorem. Every u.e.i. ceer $R$ with a strong diagonal function is computably isomorphic to $\sim_{PA}$.

References
[1] U. Andrews, S. Lempp, J. S. Miller, K. M. Ng, L. San Mauro, and A. Sorbi. Universal computably enumerable equivalence relations. Journal Symbolic Logic, 79(1):60–88, March 2014.
[2] C. Bernardi and F. Montagna. Equivalence relations induced by extensional formulae: Classifications by means of a new fixed point property. Fundamenta Mathematicae, 124:221–232, 1984.
[Close]

Serikzhan Badaev, A Chain of weekly precomplete computably enumerable equivalence relations

A computably enumerable equivalence relation (ceer) $E$ on $\omega$ is weakly precomplete if and only if $E$ has no computable diagonal function. The class of weakly precomplete ceers include the important classes of precomplete ceers and uniformly finitely precomplete (u.f.p.) ceers. In [1], it was shown that there are infinitely many computable isomorphism types of universal weakly precomplete (in fact u.f.p.) ceers; and there are infinitely many computable isomorphism types of non-universal weakly precomplete ceers. We consider ceers relatively to the following well known reduction: a ceer $R$ is said to be reducible to a ceer $S$, if there is a computable function $f$ such that, for all $x$ and $y$, $x R y \iff f (x) S f(y)$. We construct an infinite $\omega$-chain of non-equivalent weakly precomplete ceers under this reduction.

References
[1] Serikzhan Badaev and Andrea Sorbi, Weakly precomplete computably enumerable equivalence relations, Mathematical Logic Quarterly, vol. 62 (2016), no. 1, pp. 111–127.
[Close]

Michał Tomasz Godziszewski, Marek Czarnecki and Dariusz Kalociński, Learnability in the Limit meets the Church Thesis

We consider the notion of intuitive learnability and its relation to intuitive computability. We briefly discuss the Church's Thesis. We formulate the Learnability Thesis. Further we analyse the proof of the Church's Thesis presented by M. Mostowski. We indicate which assumptions of the Mostowski's argument implicitly include that the Church's Thesis holds. The impossibility of this kind of argument is strengthened by showing that the Learnability Thesis does not imply the Church's Thesis. Specifically, we show a natural interpretation of intuitive computability under which intuitively learnable sets are exactly algorithmically learnable but intuitively computable sets form a proper superset of recursive sets.
[Close]

Luca San Mauro, Complexity of Relations via Computable Reducibility

Computable reducibility provides a natural way of ranking binary relations on $\omega$ according to their complexity. Let $R$ and $S$ be two binary relations, we say that $R$ is computably reducible to $S$ iff there is a computable function $f$ such that, for all $x,y \in \omega$, the following holds: \[ xRy \Leftrightarrow f(x)Sf(y). \] Computable reducibility has been object of study for decades, being mostly applied to the case of equivalence relations. In particular, a prominent problem in the area has been that of characterizing universal equivalence relations, i.e. relations to which all others relations, of a given complexity, can be computably reduced. In this talk, we address the problem of universality for a more general context than that of equivalence relations. First, we prove that, contrary to the case of equivalence relations and preorders, for each level of the arithmetical hierarchy there is a universal binary relation. Then, we define natural examples of universal $\Sigma^0_n$ binary relations and of universal $\Pi^0_n$ binary relations. More precisely, let $U^{\in}_n$ be the following $\Sigma^0_n$ binary relation, \[ xU^{\in}_n y \Leftrightarrow x\in W^{\emptyset^{(n-1)}}_y, \] and, for $n>2$, let $U^\subseteq_n$ be the following binary relation \[ xU^\subseteq_n y \Leftrightarrow W_x \subseteq W^{(n-2)}_y. \]. We show that:

• For all $n$, $U^\in_n$ is a universal $\Sigma^0_n$ binary relation;
• There exists a total computable function $f$ such that the following binary relation \[ xU^\subseteq_2 y \Leftrightarrow W_x \subseteq W_{f(y)} \] is a universal $\Pi^0_2$ binary relation;
• For $n>2$, $U^\subseteq_n$ is a universal $\Pi^0_n$ binary relation.

References
[1] Uri Andrews, Steffen Lempp, Joseph S. Miller, Keng Meng Ng, Luca San Mauro, Andrea Sorbi, Universal computably enumerable equivalence relations, The Journal of Symbolic Logic, vol. 79 (2014), no. 1, pp. 60–88.
[2] Egor Ianovski, Russell Miller, Keng Meng Ng, André Nies, Complexity of equivalence relations and preorders from computability theory, The Journal of Symbolic Logic, vol. 79 (2015), no. 3, pp. 859–881.
[Close]

Andrew Swan, Identity types in algebraic model structures

The original Bezem-Coquand-Huber cubical set model promised to give a constructive model of homotopy type theory. However, in its original form there was a notable shortcoming: one of the definitional equalities usually included in type theory, the J computation rule was absent. One way to fix this is to use an alternative definition of identity type in which we keep track more carefully of degenerate paths. The new identity type has a nice presentation in the setting of algebraic model structures. To model identity types what we need is very good path objects: a factorisation of each diagonal as a trivial cofibration followed by a fibration. I'll show a general way to create very good path objects from path objects in the weaker sense of factorisations of diagonals as weak equivalence followed by fibration, and that under certain reasonable conditions on an ams this can be carried out "stably and functorially" allowing us to satisfy the Garner-van den Berg notion of "stable functorial choice of diagonal factorisation." These can then be used to model identity types.
[Close]

Steve Awodey, Natural models of type theory

The notion of a natural model of type theory provides an entirely algebraic description of a system of dependent type theory with an operation of context extension, and can serve as a flexible notion of a model of type theory. We give the main definition, originally stated in [1], make the algebraic character explicit, and then sketch the proof that this notion is equivalent to that of a category with families in the sense of Dybjer [2].

References
[1] S. Awodey, Natural models of homotopy type theory, arXiv, 1406.3219v2.
[2] P. Dybjer, Internal type theory, LNCS, vol. 1158 (1996), pp. 120–134.
[Close]

Clive Newstead, Categories of natural models of type theory

Natural models of type theory (see [1]) provide an algebraic setting for the interpretation of dependent type theory. First, we define homomorphisms of natural models of type theory with a basic type and context extension, and prove that the syntactic category of contexts is initial in this category. We then extend our construction to allow for dependent sums and products. Time permitting, we prove that, in this latter case, the polynomial functor associated with a given natural model is a polynomial monad. This is joint work with Steve Awodey.

References
[1] Steve Awodey, Natural models of homotopy type theory, eprint arXiv:1406.3219v2 (2015)
[Close]

Egbert Rijke and Ulrik Buchholtz, The real projective spaces in HoTT

We construct the real projective spaces as certain higher inductive types in Homotopy Type Theory. The classical definition of $\mathbb{R}\mathrm{P}^n$, as the quotient space where the antipodal points of the $n$-sphere are identified, does not translate directly to Homotopy Type Theory. Instead, we define $\mathbb{R}\mathrm{P}^n$ by induction on $n$ simultaneously with its tautological bundle. As the base case, $\mathbb{R}\mathrm{P}^{-1}$ is taken to be the empty type. In the inductive step, $\mathbb{R}\mathrm{P}^{n+1}$ is taken to be the mapping cone of the projection map of the tautological bundle. It is then possible to define the tautological bundle on $\mathbb{R}\mathrm{P}^{n+1}$ using the universal property of $\mathbb{R}\mathrm{P}^{n+1}$ and the univalence axiom. With this definition, one can use the descent theorem to show that the total space of the tautological bundle of $\mathbb{R}\mathrm{P}^n$ is the $n$-sphere. Hence one can retrieve the description of $\mathbb{R}\mathrm{P}^{n+1}$ as $\mathbb{R}\mathrm{P}^n$ with an $(n+1)$-disk attached to it. The infinite dimensional real projective space $\mathbb{R}\mathrm{P}^\infty$, defined as the sequential colimit of $\mathbb{R}\mathrm{P}^n$ with the canonical inclusion maps, is equivalent to $K(\mathbb{Z}/2\mathbb{Z},1)$, and the tautological bundles of the finite dimensional real projective spaces factor through $\mathbb{R}\mathrm{P}^{n+1}$ as expected. Indeed, the infinite dimensional projective space classifies the $0$-sphere bundles – which one can think of as synthetic line bundles – and using the join connectivity theorem one can then show that the tautological bundle of $\mathbb{R}\mathrm{P}^n$ is an $(n-1)$-connected map into $\mathbb{R}\mathrm{P}^\infty$.
[Close]

Peter Aczel, On Type Theory and the Philosophy of Mathematics

This talk is intended to advocate the basics of Per Martin-Lof's dependent type theory as a general purpose tool in the philosophy of mathematics that is an improvement on the traditional uses of first order logic.
[Close]

Joan Casas-Roma, Antonia Huertas and M. Elena Rodríguez, Towards a semantics for Dynamic Imagination Logic

Imagining alternative ways the reality could be is something we do almost everyday in our lives: when we wonder how things would be if I was to win the lottery or if I were working in another company, when we read a book that describes a reality different than ours, when we "log in" to a virtual world and we incarnate our alter-ego, or even when we consider more recent technological developments like virtual reality: while wearing a pair of VR goggles, we start experiencing a new, different reality in which we accept some things to be different, in which we are someone else, and in which we embrace new rules that we know they would be impossible in our reality but which are, nonetheless, possible in that alternative one. We define and present the syntax and semantics of the Dynamic Imagination Logic: this system models an epistemic agent who is able to deal with issues involving imagination in a dynamic way, and perform actions such as imagining "whether $\varphi$ could be the case, provided everything else stays the same", or even imagining "how different things should be in order for $\varphi$ to be the case". These actions are processed in a dynamic way that expands the model by creating new and different "spaces" that represent alternative realities the agent thinks about; moreover, the model is expanded in such a way that every imagination step can be fully traced to see what the agent imagined and from where, which alternative realities are generated by each imagination step, and what would the agent come to know or ignore in each of these alternatives.

\textbf{Acknowledgements:} This work has been supported by a doctoral grant from the Universitat Oberta de Catalunya (UOC) and the funding for the project "Hybrid Intensional Logic" (with reference FFI2013-47126-P) given by the Spanish Ministry of Economy and Competitiveness.
[Close]

Hao-Cheng Fu, On the problem of higher order vagueness

It is well-known that the higher order vagueness is an arguable phenomenon while we want to construct an adequate semantics for vagueness. Timothy Williamson has taken the phenomenon of higher order vagueness to refute some attempts to revise the semantics of classical logic. In other words, Williamson claimed that best way to dissolve the problem of higher order vagueness is the epistemic theory rather than trying to amend the logical system such as three-valued, many-valued, continuum valued and supervaluationist's theories. When we consider Williamson's strategy to refute these theories, it seems there is a more basic problem which we need to contemplate. Is the phenomenon of higher order vagueness real or just verbal? So, I must say that we have to distinguish two different problems about the confusion of higher order vagueness. Of course the first one is to ask whether the phenomenon is real and the other one is to inquire whether the phenomenon does matter or not? I shall argue that the phenomenon of higher order vagueness is real but we needn't to be afraid because the phenomenon would not threaten supervaluationism as Williamson contended.
[Close]

Edoardo Rivello, A revision-theoretic general theory of definitions

The classical theory of definitions bans so-called circular definitions, namely, definitions of, say, a unary predicate $P$ based on stipulations of the form \[ P(x) =_{\mathsf{Df}} \Phi(P, x), \] where $\Phi$ is a formula of a fixed first-order language and the definiendum $P$ occurs into the definiens $\Phi$. In their seminal book The Revision Theory of Truth [1], Gupta and Belnap claim that "General theories of definitions are possible within which circular definitions [...] make logical and semantic sense" [p. IX]. In order to sustain their claim, they develop in this book one general theory of definitions (in some variants) based on revision sequences, namely, ordinal-length iterations of the operator which is induced by the (possibly circular) definition of the predicate. Gupta-Belnap's approach to circular definitions has been criticised, among others, by Martin [2] and McGee [3]. Their criticisms point on the logical complexity of revision sequences, on their relations with ordinary mathematical practice, and on their merits relative to alternative approaches. In my talk I will present an alternative general theory of definitions, based on a combination of supervaluation and $\omega$-length revision, which aims to address some issues raised by Martin and McGee while preserving the philosophical and mathematical core of revision.

References
[1] Anil Gupta and Nuel Belnap, The Revision Theory of Truth, A Bradford Book, MIT Press, 1993.
[2] Donald A. Martin, Revision and its rivals, Philosophical Issues, vol. 8 (1997), pp. 387–406.
[3] Vann McGee, Revision, Philosophical Issues, vol. 8 (1997), pp. 407–418.
[Close]

Simon Hewitt, Indefinite extensibility and set-theoretic relativity

Following Dummett, several authors have responded to the set-theoretic paradoxes by claiming that the concept set is indefinitely extensible [1]. One way of understanding this is in terms of ontological extensibility: however many sets there are, it is always possible that there be more. Recent work by Gabriel Uzquiano provides an alternative characterisation of indefinite extensibility, laying out an account of set-formation within a fixed domain modal logic [2]. The modality is interpreted linguistically, in terms of possible expansions of the extensions of predicates. We review Uzquiano's proposal, and make clear the underlying philosophical picture of set-theoretic ontology. We argue that this picture sits uncomfortably with widespread convictions about the nature of sets. More seriously, we call into question whether the proponent of a linguistic account of indefinite extensibility is entitled to assume a sufficiently large cardinality of objects to recover set-theory.

References
[1] Michael Dummett, Frege: Philosophy of Mathematics, Duckworth, 1991.
[2] Gabriel Uzquiano, Varieties of Indefinite Extensibility, Notre Dame Journal of Formal Logic, vol.56 (2015), no.1, pp.147-166.
[Close]

Farshad Badie and Hans Götzsche, Towards Logical Analysis of Occurrence Values in Truth-Functional Independent Occurrence Logic

The human beings never really understood how truth could be recognised as the centrepiece of philosophy. The idea of truth vs. falsity is based on the assumption that the truth-value of statements about things beyond actual settings can, indisputably, be determined (‘false’ statements about settings are just counterfactuals). In this discussion, we will rely on our alternative kind of logic: Occurrence Logic (Occ Log), which is not based on truth functionality, see [1]. The Occ Log $z ^\circ{>} y$ expression denotes the fact that ‘$y$ occurs in case and only in case $z$ occurs’. Note that '$z ^\circ{>} y$' does not by itself express any kind of truth-value semantics. We will see that the Occurrences as the main building blocks of our approach are independent from truth-values, but they are strongly dependent on the occurrence values. The fact that '$y$ would only occur [and would only have an occurrence value] in case $z$ occurs [and has an occurrence value]', has been represented by Occ Log expression $z ^\circ{>} y$. We shall stress that what is in logic often called ‘states of affairs’ (including ‘events’) of the real world could be called Local Universes that are made of Entities and Properties. Focusing on the events $z$ and $y$ we can justifiably say that “in case, and only in case, the local universe of $z$ differs from the local universe of $y$ regarding at least one but not all Entities and Properties, one of them can, potentially, be said to be a change of the other”. \begin{thebibliography}
[1] Götzsche, Hans, Deviational Syntactic Structures. London / New Delhi / New York / Sydney: Bloomsbury Academic, 2013.
[Close]

Michał Tomasz Godziszewski, Short elementary cuts in recursively saturated models of arithmetic

We study certain model-theoretic properties of countable recursively saturated models of arithmetic. Our primary inspiration for examining mathematical features of such structures, and recursively saturated in particular, is that every countable recursively saturated model of Peano Arithmetic supports a great variety of nonstandard satisfaction classes that can serve as models for formal theories of truth - those models allow to investigate the role of arithmetic induction in semantic considerations. In the other direction, nonstandard satisfaction classes are used as a tool in model theoretic constructions providing answers to questions in the model theory of formal arithmetic and often allow to solve problems that do not explicitly involve nonstandard semantics. Due to the fact that a for a countable model of arithmetic, it is equivalent to admit a full satisfaction class (i.e. satisfy the formal theory of compositional truth) and to be recursively saturated, the project can be thought of as an investigation into structure of possible interpretations for theory of compositional, arithmetical truth. It needs to be underlined that the purpose of our research is to examine model-theoretic but purely arithmetical properties of models admitting satisfaction classes. In particular, we study various substructures of recursively saturated models of PA, and we focus on the cofinal extensions of models of PA. First-order theories of pairs $(N,M)$, where $N\models PA$ and $M$ is an elementary cofinal submodel of $M$ reveal great diversity and demand systematic study. The case of models admitting satisfaction classes is of particular interest in this respect: all countable recursively saturated models of PA have continuum many nonisomorphic cofinal submodels, and after acknowledging the variety of the abovementioned pairs for $N$ being countable recursively saturated, the next goal is to consider isomorphism types and first-order theories for pairs of models $(N, M)$ for a fixed countable recursively saturated model $N$ and a fixed isomorphism type of $M$. The method that has already been shown quite effective in this direction is the method of gaps (also called skies). We present briefly the gap terminology and explain why it is useful. Skolem terms, also called simply definable functions\footnote{with a slight abuse of terminology that is unimportant to our investigations}, are paramter-free definable and PA-provably total functions. Let $\mathcal{M}$ be a nonstandard model of arithmetic and let $\mathcal{F}$ be some family of Skolem terms $f : M \rightarrow M$ such that $\forall x,y \in M \: x <y \Rightarrow x \leq f(x) \leq f(y)$. There is a partition of $M$ into sets, which we call $\mathcal{F}$-gaps. For any $a \in M$, $gap_{\mathcal{F}}(a)$ is the smallest set $C \subseteq M$ such that $a \in C$ and: $ \forall b \in C \: \forall f \in \mathcal{F} \: \forall x \in M\: \: b \leq x \leq f(b) \: \vee \: x \leq b \leq f(x)) \Rightarrow x \in C.$ This is a natural generalization of an idea of partitioning the universe of a nonstandard model into $\mathbb{Z}$-blocks around each element (then, each such block is $gap_{\mathcal{F}}(a)$ for some $a$, where $\mathcal{F}$ consists only of the successor function $s$). The gap of $a \in M$, denoted by $gap(a)$, is the $\mathcal{F}$-gap of $a$, where $\mathcal{F}$ is the family of \textbf{all} such definable functions, i.e. $\mathcal{F} = \{f : M \rightarrow M: f \: \: \text{is definable and} \: \: \forall x,y \in M \: x <y \Rightarrow x \leq f(x) \leq f(y)\}.$ Every model $\mathcal{M}$ has the least gap, the $gap(0)$. Let $A \subseteq M$. Then, we denote $sup(A) = \{x \in M : \exists y \in A \: x \leq y\}$. If for some $a \in M$, $M =sup(gap(a))$, then we call $gap(a)$ the \textbf{last gap of $\mathcal{M}$}. A model with a last gap is called \textbf{short}. If $\mathcal{M} \preceq_{cut} \mathcal{N}$ (i.e. $\mathcal{M}$ is an elementary cut of $\mathcal{N}$), we say that $\mathcal{M}$ is \textbf{short elementary cut} of $\mathcal{N}$ if $\mathcal{M}$ is short - in other words, if by $Scl(a)$ we denote the set $\{t(a): \text{ $t$ is a Skolem term of PA}\}$ $\mathcal{M}$ is short if there is such an element $a \in M$ that its Skolem closure in $\mathcal{M}$ is cofinal in $\mathcal{M}$, i.e. for all $x \in M$ there is $b \in Scl(a)$ such that $x <_{\mathcal{M}} b$. An elementary cut is \textbf{coshort} if $\mathcal{N} \setminus \mathcal{M}$ has the least gap, i.e. there is $a \in N \setminus M$ s.t. $M = inf(gap(a))$, where $inf(A) = \{x \in M : \forall y \in A \: x \leq y\}$. Now, to clarify the gap terminology, if we put: $\mathcal{M}(a) = sup(Scl(a))$, and $\mathcal{M}[a] = \{b \in M: \: \forall t \in Scl(b) \: t(b) < a\}$, then the set $[a) = \mathcal{M}(a) \setminus \mathcal{M}[a]$ is exactly the $gap(a)$. It can be shown that $\mathcal{M}(a)$ is the smallest elementary cut of $\mathcal{M}$ containing $a$, and that $\mathcal{M}[a]$ is empty if and only if everey elementary cut of $\mathcal{M}$ contains $a$. Gap terminology is particularly useful in the study of recursively saturated models of PA (see e.g. [5] for a reference to many methods and properties). One of the interesting and natural questions conerning pairs for countable recursively saturated models of arithmetic and its cofinal submodels is the following big question of our particular interest:

• Let $\mathcal{M} \models PA$ be a countable recursively saturated model and let $\mathcal{K}, \mathcal{K}'$ be elementary cuts of $\mathcal{M}$. Suppose that $(\mathcal{M}, \mathcal{K}) \equiv (\mathcal{M}, \mathcal{K}')$. Does it follow that $(\mathcal{M}, \mathcal{K}) \cong (\mathcal{M}, \mathcal{K}')$?

Another way to put it is: under what conditions, does the identity of theories of such pairs imply their isomoprhism? It is known that the answer to the big question above is negative, if $\mathcal{K}$ and $\mathcal{K}'$ in question are coshort, as shown by R. Kossak and J. Schmerl in [6]. However, it remains open (and is considered to be difficult) what is the answer for the case in which $\mathcal{K}$ and $\mathcal{K}'$ are short elementary cuts of $\mathcal{M}$, i.e. are of the form $\mathcal{M}(a)$ and $\mathcal{M}(b)$ for some $a, b \in M$. Since it is not hard to prove the equivalence that there exists an automorphism of such $\mathcal{M}$ if and only if $tp(a) = tp(b)$ (in the purely arithmetical language $\mathcal{L}$), where $tp(a) =\{\varphi(x): \mathcal{M} \models \varphi(a)\}$ is the set of formulae satisfied in $\mathcal{M}$ by $a \in M$, the natural way to proceed is to consider the definable sets in $(\mathcal{M}, \mathcal{M}(a))$ and complete types realized in the last gap of $\mathcal{M}$. We might then first ask under what circumstances there is an element $c \in gap(a)$ such that $tp(c) \in Def(\mathcal{M}, \mathcal{M}(a))$ for $\mathcal{M}$ being a countable recursively saturated model of PA. Using results of Smorynski from [12] and working with gaps and standard systems $SSy(\mathcal{M})$ of $\mathcal{M}$, i.e. the family of all subsets of $\mathbb{N}$ that are coded in $\mathcal{M}$\footnote{It turns out that the standard system tells you a lot about the model; for example, any two countable recursively saturated models of the same completion of PA with the same standard system are isomorphic.} we show that

Theorem (Tin Lok Wong, MTG). Let $\mathcal{M} \models PA$ be a countable recursively saturated model and let $a, b \in M$. Suppose that $(\mathcal{M}, \mathcal{M}(a)) \equiv (\mathcal{M}, \mathcal{M}(b))$ (recall that $\mathcal{M}(a)$ and $\mathcal{M}(b)$ are short). If $SSy(\mathcal{M}) \subseteq Def(\mathbb{N})$, then $(\mathcal{M}, \mathcal{M}(a)) \cong (\mathcal{M}, \mathcal{M}(b))$.

As the project is essentially in progress, we end with perspective paths for further work. The conceptual import of the result is that taking a nonstandard model of compositional truth such that all its coded sets are already definable in the standard model, we are able to identify isomorphic cofinal short elementary cuts of the model just by looking on the arithmetical theory of both pairs considered.

References
[1] J. Barwise, J. Schlipf, An introduction to recursively saturated and resplendent models, Journal of Symbolic Logic, vol. 41 (1976), pp. 531–536.
[2] A. Enayat, A. Visser, New constructions of satisfaction classes, Unifying the Philosophy of Truth (T. Achourioti, H. Galinon, J. Martinez Fernandez and K. Fujimoto, editors), Springer-Verlag, Publisher's address, 2015, pp. X–XX.
[3] F. Engström, Satisfaction classes in nonstandard models of first-order arithmetic, Chalmers University of Technology and Göteborg University, Göteborg, vol. XX (2002), no. X, pp. XXX–XXX.
[4] R. Kaye, Models of Peano Arithmetic, Oxford University Press, Oxford, 1991.
[5] R. Kossak, J. Schmerl, The structure of models of Peano Arithmetic, Clarendon Press, Oxford, 2006.
[6] R. Kossak, J. Schmerl, On Cofinal Submodels and Elementary Interstices, Notre Dame Journal of formal Logic, vol. 53 (2012), pp. 267–287.
[7] H. Kotlarski, S. Krajewski, A. Lachlan, Construction of satisfaction classes for nonstandard models, Canadian Mathematical Bulletin, vol. 24 (1981), pp. 283–293.
[8] H. Kotlarski, Full satisfaction classes: a survey, Notre Dame Journal of Formal Logic, vol. 32 (1991), pp. 573–579.
[9] S. Krajewski, Nonstadard satisfaction classes, Set Theory and Hierarchy Theory (W. Marek, M. Srebrny and A. Zarach, editors), Editorial, Heidelberg, 1976, pp. X–XX.
[10] A. Lachlan, Full satisfaction classes and recursive saturation, Canadian Mathematical Bulletin, vol. 42 (1981), pp. 295–297.
[11] A. Robinson, On languages based on non-standard arithmetic, Nagoya Mathematical Journal, vol. 22 (1963), pp. 83–107.
[12] C. Smorynski, Cofinal extensions and nonstandard models of arithmetic, Notre Dame Journal of formal Logic, vol. 2 (1981), pp. 133–144.
[13] C. Smorynski, Elementary extensions of recursively saturated models of arithmetic, Notre Dame Journal of formal Logic, vol. 2 (1981), pp. 193–203.
[14] C. Smorynski, Recursively saturated nonstandard models of arithmetic, Journal of Symbolic Logic, vol. 46 (1981), pp. 259–286.
[Close]

Jana Glivická, Skolem arithmetic, its extensions and their properties

Skolem arithmetic (SA) is the theory of the structure $(\mathbb{N}-\{0\},\cdot)$. This structure, its standard model, can be viewed as an infinite direct sum of the standard model $(\mathbb{N},+)$ of Presburger arithmetic. SA is known to be decidable [3], with explicit complete axiomatization and simple elimination set [1]. We are interested in extensions of SA, in some enriched language, that have similar properties and thus are, in this sense, still very far from Peano arithmetic. To obtain such extensions, we first prove a general theorem on substructures of infinite direct products. The setting is as follows: For every $p \in \mathbb{N}$, $\mathcal{M}_p$ is a structure for language $\mathcal{L}$ with constant symbol $0$. We impose certain technical conditions on $\mathcal{L}$ and $\mathcal{M}_p$. $\mathcal{M}$ is an $\mathcal{L}$-structure with $\coprod_{p \in \mathbb{N}} \mathcal{M}_p \subseteq \mathcal{M} \subseteq \prod_{p \in \mathbb{N}} \mathcal{M}_p$, where $\coprod$ denotes direct sum and $\prod$ direct product. We say that $\mathcal{M}$ has uniform witnessing property if, for any $\mathcal{L}$-formula $\varphi(\bar{x},y)$ such that $\varphi(\bar{0},0)$ is true in all $\mathcal{M}_p$ and any $\bar{a} \in \mathcal{M}$, the following holds true $$(\forall p \in \mathbb{N}) \mathcal{M}_p \vDash \exists y \varphi(\bar{a}(p),y) \Rightarrow (\exists b \in \mathcal{M})(\forall p \in \mathbb{N}) \mathcal{M}_p \vDash \varphi(\bar{a}(p),b(p)).$$ Suppose $\mathcal{M}$ has the uniform witnessing property and for any $\bar{a} \in \mathcal{M}$ there are infinitely many $p \in \mathbb{N}$ such that $\bar{a}(p) = \bar{0}$. We prove that $\coprod_{p \in \mathbb{N}} \mathcal{M}_p$ is then an elementary substructure of $\mathcal{M}$. The two conditions are sufficient, but provably not necessary. It is possible to express the uniform witnessing property in the language of SA. It allows us to "lift" results about extensions of Presburger arithmetic to extensions of SA. We show how to obtain natural complete axiomatizations of theories extending SA. Moreover, we show how to lift properties such as decidability, quantifier elimination, existence of simple elimination set and so on. A prominent example of such a lifting is the theory $SA^a$, Skolem arithmetic with a "slice" of exponentiation (function thought of as $f(x) = x^a$, where $a$ is nonstandard). Here, we use results on certain extensions of Presburger arithmetic called linear arithmetics [2].

References
[1] P. Cegielski, Theorie elementaire de la multiplication des entiers naturels,Lecture notes in mathematics, vol. 890, pp. 44–89.
[2] P. Glivický, Study of Arithmetical Structures and Theories with Regard to Representative and Descriptive Analysis, PhD. thesis,Charles University in Prague, 2013.
[3] A. Mostowski, On direct product of theories, Journal of symbolic logic, vol. 36, pp. 1–31.
[Close]

Michal Garlik, Models of bounded arithmetic and a restricted ultrapower construction

It is well known that some problems in complexity theory can be reformulated as problems of constructions of expanded extensions of models of bounded arithmetic. Usually, these models are required to satisfy some form of bounded induction and at the same time not to introduce any new lengths. It seems that modifications of the ultrapower construction could make it easier to meet the last requirement. Our attempt in this direction is a construction by a restricted reduced power. The construction starts with a model $M$ of true arithmetic, a nonstandard element $n$ of $M$, and an index set $\Omega$ which is a subset of numbers of length $n$. It uses straight-line programs defined in $M$ to build the universe of a new model $N$. The construction assumes a hypothesis that there is a formula $\psi(x,y)$ such that for each straight-line program $f$ of size $m^s$ the formula $\psi(x,f(x))$ is true in $M$ for at most $q$ fraction of the time when $x$ ranges over $\Omega$. Using these parameters, which are moreover required to satisfy $qn^{m^i}<1$ for each $i\in \mathbb{N}$, the construction proceeds by defining a filter on the powerset of $\Omega$ and a suitable subset of straight-line programs of size $m^s$. This is done in countably many stages and the crucial step is to ensure induction. The resulting model $N$ then satisfies the theory $strict R^1_2$, agrees with $M$ on lengths and contains an element which falsifies $\psi$. We use the construction to separate theories $R^1_2(g)$ and $strict R^1_2(g)$ assuming that $g$ is a one-way permutation hard against polynomial-size circuits. We add further applications of the construction.
[Close]

Murdoch Gabbay, Consistency of Quine's NF using nominal techniques

Naive set theory has one rule; naive sets comprehension:

• If $\phi$ is a predicate, then $\{a\mid \phi(a)\}$ is a set (the $a$ such that $\phi$).

This is inconsistent by Bertrand Russell's famous observation of 1901 that $\{a\mid a{\not\in} a\}\in\{a\mid a{\not\in} a\}$ if and only if $\{a\mid a{\not\in} a\}\not\in\{a\mid a{\not\in} a\}$. Solutions proposed included Zermelo-Fraenkel set theory, simple type theory, and Quine's New Foundations (NF). Zermelo-Fraenkel set theory restricts comprehension so we can only form comprehension within an existing set. Simple type theory imposes a type system. Quine's NF weakens comprehension by restricting it to stratifiable formulae; formulae in which variables can be assigned `levels', which are natural numbers, such that if $a\in b$ occurs in a formula and $a$ has level $n$, then $b$ must have level $n{+}1$. Russell's example is clearly ruled out because $a\in a$ cannot be stratified. Consistency of NF has been an open problem since it was proposed by Quine in 1937. I will present a claimed proof of consistency of Quine's NF, based on ideas previously developed to extend duality theory to logics with quantifiers (the paper is available on my webpage and on arXiv). In the paper:

• Stratifiability corresponds to a simple normalisability property on terms,
• substitution corresponds to both a nominal algebra axiomatisation and a renormalisation procedure,
• universal quantification corresponds to a colimit in nominal lattices, and to a form of the nominal new-quantifier (and existential quantification to its dual),
• sets comprehension corresponds to nominal atoms-abstraction, and
• extensionality corresponds to a non-evident transfinite construction which amounts to saturating an equality theory with all possible equalities to ensure that extensionality holds.

The end result is a points-based representation of NF in which predicates correspond to sets of points, and points are deductively closed sets of predicates subject to some interesting filter-style conditions.
[Close]

Alessandro Vignati, Forcing axioms and automorphisms of C*-algebras

In the last decade Farah developed the study of the group of automorphisms of coronas C*-algebras. He and Coskey conjectured that under CH there are wild automorphisms of corona algebras, while under PFA the situation is conjectured to be quite rigid. McKenney and I recently verified the conjecture in the case of PFA for a large class of algebras, although very much remains open. After a brief introduction of the objects, we present the current situation of the conjecture, and then we focus on some of the difficulties stopping us from expanding our results.
[Close]

Dorottya Sziraki, A dichotomy for infinitely many $\mathbf{\Sigma}^0_2(\kappa)$ relations on the $\kappa$-Baire space

As an initial step in studying dichotomies about independent sets with respect to certain (sets of) definable relations on the $\kappa$-Baire space ${}^\kappa\kappa$, we examine the case of a set $\mathcal R$ of $\kappa$ many $\mathbf{\Sigma}^0_2(\kappa)$ relations (of arbitrary finite arity). By considering games introduced by Jouko Väänänen [4] which allow trees to play, for the $\kappa$-Baire space, a role analogous to that of Cantor-Bendixson ranks in the classical case and by restricting the allowed strategies for these games, we show that the $\kappa$-version of a recent result of Martin Doležal and Wies\l{}aw Kubiś [1] (see also [2]) holds under $\Diamond_\kappa$. Namely, for a set $\mathcal R$ of relations as above, if the $\kappa$-Baire space has $\mathcal R$-independent subsets of "arbitrary Cantor-Bendixson rank", then there exists a $\kappa$-perfect $\mathcal R$-independent subset. For $\kappa$ inaccessible, this is true already in ZFC. As a corollary, we obtain (the slightly more general version of) a recent theorem of Jouko Väänänen and the author [3].

References
[1] M. Doležal, W. Kubiś, Perfect independent sets with respect to infinitely many relations, submitted.
[2] W. Kubiś, Perfect cliques and $G_\delta$ colorings of Polish spaces, Proceedings of the American Mathematical Society, vol. 131 (2003), no. 2, pp. 619–623.
[3] D. Sziráki, J. Väänänen, A dichotomy for the generalized Baire space and elementary embeddability at uncountable cardinals, submitted.
[4] J. Väänänen, A {Cantor-Bendixson} theorem for the space $\omega_1^{\omega_1}$, Fundamenta Mathematicae, vol. 137 (1991), no. 3, pp. 187–199.
[Close]

Makoto Fujiwara, Effective computability and constructive provability for existence sentences

Along the line of [1], we investigate the relationship between effective computability and constructive provability for existence sentences. We show the following. Here $\mathsf{E\mbox{-}PA^{\omega}}$ (resp. $\mathsf{E\mbox{-}HA^{\omega}}$) is the finite type extension of $\mathsf{ PA}$ (resp. $\mathsf{ HA}$), $\mathsf{EL}$ is the system of elementary analysis, $AC$ (resp. $\mathrm{AC_{00}}, \mathrm{\Pi^0_1\text{-}AC_{00}} $) is the axiom of choice in all finite types (resp. the axiom of countable choice, that for purely universal formulas), $IP^\omega_{ef}$ is the independence of premise for $\exists$-free formulas, $ \mathrm{\Sigma^0_2\text{-}DNS^0}$ is the fragment of double negation shift principle: $$\forall \alpha^1 (\forall x^0 \neg \neg \exists y^0 \forall z^0 \alpha (x,y,z)=0 \to \neg \neg \forall x^0 \exists y^0 \forall z^0 \alpha (x,y,z)=0 ).$$

Theorem. For every sentence $\forall \xi^1 (A(\xi) \rightarrow \exists \zeta^1 B (\xi, \zeta))$ where $A(\xi)$ is $\exists$-free and $B(\xi, \zeta)\in \mathrm{\Gamma_1}$, if $$\mathsf{E\mbox{-}HA^{\omega}} + AC+IP^\omega_{ef}+ \mathrm{\Sigma^0_2\text{-}DNS^0} \vdash \forall \xi (A(\xi) \rightarrow \exists \zeta B (\xi, \zeta)),$$ then there exists a term $t^{1\to 1}$ of $\mathsf{E\mbox{-}PA^{\omega}}$ such that $$\mathsf{E\mbox{-}PA^{\omega}} +\mathrm{\Pi^0_1\text{-}AC_{00}} \vdash \forall \xi (A(\xi) \rightarrow \exists \zeta B (\xi, t\xi)).$$

The classes $\mathcal{A}$, $\mathcal{B}$ of formulas in $\mathcal{L}(\mathsf{E\mbox{-}HA^{\omega}}) $ are defined simultaneously by

• $P$, $A_1\wedge A_2$, $A_1\vee A_2$, $\forall x A_1$, $\exists x A_1$, $B_1\to A_1$ are in $\mathcal{A}$;
• $P$, $B_1\wedge B_2$, $\forall x B_1$, $A_1\to B_1$ are in $\mathcal{B}$;

where $P$, $A_i$, $B_i$ range over prime formulas, formulas in $\mathcal{A}$, $\mathcal{B}$ respectively.

Theorem. For every sentence $\forall \xi^1 (A(\xi) \rightarrow \exists \zeta^1 B (\xi, \zeta))$ where $A(\xi)\in \mathcal{A}$ and $B(\xi, \zeta)\in \mathcal{B}$, if there exists a term $t^{1\to 1}$ of $\mathsf{E\mbox{-}PA^{\omega}}$ such that $$\mathsf{E\mbox{-}PA^{\omega}} +\mathrm{\Pi^0_1\text{-}AC_{00}} \vdash \forall \xi (A(\xi) \rightarrow \exists \zeta B (\xi, t\xi)),$$ then $$\mathsf{EL}+\mathrm{\Pi^0_1\text{-}AC_{00}} + \mathrm{\Sigma^0_2\text{-}DNS^0} \vdash \forall \xi (A(\xi) \rightarrow \exists \zeta B (\xi, \zeta)).$$

Corollary. For every sentence $\forall \xi^1 (A(\xi) \rightarrow \exists \zeta^1 B (\xi, \zeta))$ where $A(\xi)$ and $B(\xi, \zeta)$ are $\exists$-free, there exists a term $t^{1\to 1}$ of $\mathsf{E\mbox{-}PA^{\omega}}$ such that $$\mathsf{E\mbox{-}PA^{\omega}} +\mathrm{\Pi^0_1\text{-}AC_{00}} \vdash \forall \xi (A(\xi) \rightarrow \exists \zeta B (\xi, t\xi))$$ if and only if $$\mathsf{EL}+\mathrm{AC_{00}} + \mathrm{\Sigma^0_2\text{-}DNS^0} \vdash \forall \xi (A(\xi) \rightarrow \exists \zeta B (\xi, \zeta)).$$

These also hold for $\mathsf{\widehat {E\mbox{-}PA}^\omega \hspace{-.4em}\upharpoonright}$, $\mathsf{\widehat {E\mbox{-}HA}^\omega \hspace{-.4em}\upharpoonright}$ and ${\sf EL_0}$, which are the restrictions of corresponding systems to primitive recursion of type $0$ and quantifier-free induction, instead of $\mathsf{E\mbox{-}PA^{\omega}}$, $\mathsf{E\mbox{-}HA^{\omega}}$ and $\mathsf{EL}$. Note that $\mathsf{\widehat {E\mbox{-}PA}^\omega \hspace{-.4em}\upharpoonright} +\mathrm{\Pi^0_1\text{-}AC_{00}}$ contains arithmetical comprehension, which allows to develop most of ordinary mathematics. It is known that most of Bishop's constructive mathematics can be formalized in $\mathsf{EL}+\mathrm{AC_{00}}$.

References
[1] Makoto Fujiwara, Intuitionistic Provability versus Uniform Provability in $\mathsf{RCA}$, Lecture Notes in Computer Science, vol. 9136 (2015), pp. 186–195.
[Close]

Franco Parlamento and Flavio Previale, The Cut Elimination and Nonlengthening Property for Gentzen's Sequent Calculus for First Order Logic with Equality

Leibniz's indiscernibility principle, in the framework of second order logic, leads to a sequent calculus for first order logic with equality, that satisfies the cut elimination theorem, but cut free derivations may not satisfy the subformula property. We note that instead, the path described by von Plato in his historical reconstruction of Gentzen's discovery of the sequent calculus in [2], leads to a calculus that is fully satisfactory. In addition to the reflexivity axiom $\Rightarrow t=t$, it has the following two left introduction rules for $=$: \[ \frac{\Gamma\Rightarrow\Delta, F\{v/r\}}{\Gamma, r=s\Rightarrow\Delta, F\{v/s\}}=_1\quad \frac{ \Gamma \Rightarrow\Delta, F\{v/s\} }{\Gamma, r=s\Rightarrow\Delta, F\{v/r\}}=_2 \] Other satisfactory calculi can be obtained by taking into account the following other rules: \[ \frac{\Gamma, F\{v/r\} \Rightarrow\Delta}{\Gamma, F\{v/s\}, r=s \Rightarrow\Delta}=^l_1 \quad \frac{ \Gamma , F\{v/s\} \Rightarrow\Delta}{\Gamma, F\{v/r\}, r=s \Rightarrow\Delta}=^l_2 \] We give a very simple proof that cut elimination holds for a calculus obtained by adding to the reflexivity axiom some of the above four rules if and only if it contains (at least) $ =_1$ and $ =_2$ or $=_1$ and $ =_1^l$ or $ =_2$ and $ =_2^l$. The admissibility results that are used, can be refined and extended in order to show that if (and only if) all the above four rules are added, then every derivation can be trasformed into one that is cut-free and satisfies the nonlenthening property of [1].

References
[1] A.V. Lifschitz, Specialization of the form of deduction in the predicate calculus with equality and function symbols, The Calculi of Symbolic Logic I ( V.P. Orevkov, editor), Proceedings of the Steklov Institute of Mathematics 98, 1971, pp. 1–23.
[2] J. von Plato,, Gentzen's Proof Systems: Byproducts in a Work of Genius, The Bulletin of Symbolic Logic , vol. 18 (2012), no. 3, pp. 317–367
[Close]

Bartosz Wcisło, Models of positive truth

We study axiomatic theories of truth, i.e. extensions of theories such as Peano arithmetic $\textrm{PA}$ or Zermelo-Fränkel set theory $\textrm{ZFC}$ with a fresh predicate $T(x)$ with the intended reading '$x$ is a (code of a) true sentence' from the model-theoretic perspective. One of the most natural axiom systems, which we call $\textrm{CT}^-$ consists of the Tarskian compositional clauses for the truth predicate. It is a classical theorem of Lachlan that all models of $\textrm{PA}$ which admit an expansion to a model of $\textrm{CT}^-$ are recursively saturated (see e.g. [2]). In effect not every model of $\textrm{PA}$ admits an expansion to a model of $\textrm{CT}^-$. In such situation we say that $\textrm{CT}^-$ is not model-theoretically conservative over $\textrm{PA}.$ One of the theories studied in the literature is $\textrm{PT}^-$: a theory of truth whose axioms consist of positive compositional clauses, i.e. the usual compositional clauses for the conjunction, disjunction, the universal and the existential quantifier, but with no clause for the negation. Instead of it, clauses for double negations and de Morgan clauses for negated conjunctions, disjunctions, quantifiers and negated atomic sentences are introduced. A routine argument shows that unlike $\textrm{CT}^-$ its positive counterpart sis model-theoretically conservative over $\textrm{PA}.$ In our joint work with Cezary Cieśli\'nski and Mateusz \L{}e\l{}yk we study models of various natural extensions of $\textrm{PT}^-$ proof-theoretically conservative over $\textrm{PA}$ (which means that they do not prove any arithmetical sentences not provable in $\textrm{PA}$ alone). In particular, we will focus on the principles which may be spelled out informally in the following way:

• For every arithmetical formula $\phi$ the set of $x$ such that $T(\phi(x))$ holds is either empty or has the least element (the internal induction principle).
• For every arithmetical formula $\phi,$ if $\phi$ is total, i.e. for every $x$ either $T (\phi(x))$ or $T (\neg \phi(x))$ holds, then the set of $x$ such that $T (\phi(x)$ is either empty or has the least element (internal induction for total formulae).

It turns out that adding any of these principles to $\textrm{PT}^-$ result in a theory which is not model-theoretically conservative. Moreover, the models of the fist theory are recursively saturated, whereas all recursively saturated models (including the uncountable ones) admit an expansion to a model of the second theory. If time allows, we will also discuss a variant of $\textrm{PT}^-$ called $\textrm{WPT}^-$ (weak $\textrm{PT}^-$), whose axioms are modelled after weak Kleene logic rather than the strong one (e.g. a disjunction is true if and only if both disjuncts are true or false and at least one of them is true). The latter theory extended with the internal induction principle is still a model-theoretically conservative extension of $\textrm{PA}.$ We will also discuss our current knowledge on the relationships between the models of theories of positive truth and the models of the theories based on the classical notion of truth.

References
[1] Fischer, Martin, Minimal Truth and Interpretability, The Review of Symbolic Logic, vol. 2 (2009), no. 4, pp.779–815.
[2] Halbach, Volker, Axiomatic Theories of Truth, Cambridge University Press, 2011.
[Close]

Mateusz Łełyk, Principles equivalent to $\Delta_0-$induction for the compositional truth predicate

Our talk concerns study of the proof-theoretic strength of compositional theories of truth. The theories we study are obtained via augmenting Peano arithmetic $\textrm{PA}$ with a fresh unary predicate $T(x)$ with the intended reading "$x$ is a (code of a) true (arithmetical) sentence". Then we study various axiom systems trying to capture the most natural properties of the notion of arithmetical truth. One of the basic conditions a satisfactory truth theory may be expected to meet is compositionality. Rather surprisingly, it turns out that if the compositionality is the only thing we demand from the truth predicate, then the resulting theory (usually denoted $\textrm{CT}^-$) is conservative over $\textrm{PA}$ (as shown by Enayat–Visser (in [2]) and Leigh (in [4]), with a similar results being proved much earlier by Kotlarski, Krajewski and Lachlan). On the other hand a theory of compositional truth with full induction for formulae of the extended language (known as $\textrm{CT}$) is obviously non-conservative over $\textrm{PA},$ since we may show that all instances of the induction scheme are true (in the sense of our truth predicate) and then show by induction on the length of derivations in $\textrm{PA}$ that every sentence provable in $\textrm{PA}$ is true (reconstructing the usual proof of soundness of First Order Logic inside our theory). In our research we tried to understand which natural principles for the truth predicate make this notion non-conservative over the arithmetic. It turned out that all the natural principles whose strength we were able to understand thus far are either conservative over $\textrm{PA}$ or are equivalent over $\textrm{CT}^-$ to the principle of global reflection over $\textrm{PA}$. More precisely, we can show that over $\textrm{CT}^-$ the following sets of axioms are equivalent:

• "Axioms of $\textrm{PA}$ are true and sentences provable in First Order Logic from true premises are true as well." (principle of global reflection)
• "Sentences provable from true premises in First Order Logic are true."
• "Sentences provable from true premises in Propositional Logic are true."
• "Sentences valid in First Order Logic are true."
• "A disjunction is true if and only if one of its disjuncts is and axioms of $\textrm{PA}$ are true."
• $\Delta_0$-induction scheme for sentences containing the truth predicate.

The fact that the theory in question admits the listed characterisations is even more striking taking into account that the principle "Axioms of $\textrm{PA}$ are true" by itself, when added to the theory of compositional truth over $\textrm{PA}$ is still conservative, as shown independently by Enayat–Visser (unpublished) and Leigh (in [4]). Some important parts of the result presented above have been proved by Cieśli\'nski and Enayat (both in published papers (see [1]) and in unpublished notes). Our main contribution consists in showing that $\textrm{CT}^-$ with $\Delta_0$-induction for the truth predicate is enough for proving that the truth predicate commutes with blocks of quantifiers (of the same type) of arbitrary length. By proving this we fix a gap which was discovered in 2008 by Heck and Visser (independently) in an old proof by Kotlarski (see [3]). Since then the problem whether $\textrm{CT}^-$ augmented with $\Delta_0-$induction proves the principle of global reflection over $\textrm{PA}$ remained (to our best knowledge) open.

References
[1] Cezary Cieśliński, Deflationary Truth and Pathologies, Journal of Philosophical Logic, vol. 39 (2010), no. 3, pp. 325–337.
[2] Ali Enayat, Albert Visser, New Constructions of Satisfaction Classes, Unifying the Philosophy of Truth (Theodora Achourioti, Henri Galinon, José Martínez Fernández, Kentaro Fujimoto, editors), Springer, Dordrecht, 2015, pp. 321–337.
[3] Henryk Kotlarski, Bounded Induction and Satisfaction Classes, Mathematical Logic Quarterly, vol. 32 (1986), no. 31-34, pp. 531–544.
[4] Graham Leigh, Conservativity for theories of compositional truth via cut elimination, Journal of Symbolic Logic, vol. 80 (2015), no. 03, pp. 825–865.
[Close]

Susumu Yamasaki, A semantics for multi-modal mu-calculus with interaction on Heyting algebra

As regards a human interaction to implementation in programming languages, abstraction of interactive states should be formulated in computer science logic. Communications (for interaction) and ($\lambda$-)terms motivate multi-modality in logic of action ([2]). The syntax of the logical formulas is now given by BNF (Backus Naur Form) into some modification of modal mu-calculus: \[ \begin{array}{l} \varphi :: = \mbox{tt} \mid p \mid \neg \varphi \mid \mathop\sim \varphi \mid \varphi \vee \varphi \mid \langle c \rangle \varphi \mid \mu x. \varphi \mid \varphi\rangle t \rangle \end{array} \] where a prefix modality $\langle c \rangle$ (for communications), a postfix one $\rangle t \rangle$ (for terms), and a negation $\mathop\sim$ (denoting incapability of interaction) are taken, in addition to truth $\mbox{tt}$, propositions $p$, the logical negation $\neg$ and a least fixed point operator $\mu$. To represent the meaning of (a formula) $\varphi$ at a state, receiving communication $c$ (requirement), and being followed by term $t$ (effect), we here have the state sets $[\![\varphi]\!]_{pos}$, $[\![\varphi]\!]_{inter}$ and $[\![\varphi]\!]_{neg}$ for the formula (condition) to be positively, interactively and negatively modeled, respectively, in a transition system. This is an extended semantics for logic of action, from the version of [3]. The state sets are applicable to a triplet of $\langle c \rangle \varphi$, $\varphi$ and $\varphi \langle t \langle$, concerned with communication requirement and term effect. We then adopt a Heyting algebra $H$ $=$ $(\{ 0, 1/2, 1 \}, \leq, \bigvee, \bigwedge, 0, 1)$, equipped with a binary operation $\longrightarrow$ such that $c \bigwedge a \leq b$ iff $c \leq a \longrightarrow b$. With $H$, we define a semantic function $Deno$: $\Phi \rightarrow S \rightarrow \{ 0, 1/2, 1 \}$, to see the positive, interactive, or negative states for the formula (condition) to be at, where $\Phi$ and $S$ are the set of formulas and the set of states, respectively. A semiring structure ([1]) is related to, with multiplicative inverse, if the alternation of applying postfix modal operators is regarded as addition, and the composition is interpreted as multiplication. Kleene star can be included as in star semiring, with relevance to a state constraint system ([4]).

References
[1] M. Droste, W. Kuich and H. Vogler, editors. Handbook of Weighted Automata, Springer, 2009.
[2] M. Hennessy and R. Milner, Algebraic laws for nondeterminism and concurrency, Journal of the ACM, vol. 32 (1985), no. 1, pp.137–161.
[3] A. Kucera and J. Esparza, A logical viewpoint on process-algebraic quotients, Journal of Logic and Computation, vol. 13 (2003), no. 6, pp.863–880.
[4] S. Yamasaki, State constraint system applicable to adjusting, CLMPS Book of Abstracts (Ilona Nevalainen, Mikko Virtanen and Paivi Seppala, editors), printed at University of Helsinki, 2015, pp. 409–410.
[Close]

Alexander Roberts, Modal Expansionism

In arguing that a certain situation is metaphysically possible, philosophers frequently employ recombinatorial principles. Such principles articulate the idea that some possible individuals satisfying certain properties can be recombined into a single possibility at which they all satisfy those properties. Indeed, the theoretical plausibility of many recombinatorial principles is often taken for granted, since rejecting them would equate to imposing unwelcome arbitrary limits on the extent of modal space. However, an apparent paradox due to Kit Fine (2002, pp.223-224), later reformulated by Peter Fritz (manuscript), is seen to allegedly demonstrate that two plausible recombinatorial principles are inconsistent with one another and cannot therefore both feature in modal theory. The more widely known `Kaplan's paradox' due to David Kaplan (1995) also might be taken to undermine another similar recombinatorial principle. Nevertheless, the paper offers a solution to all aforementioned paradoxes in the form of a novel conception of metaphysical modality, according to which for any metaphysical modality there will always be some further, more-inclusive metaphysical modality; or, in other words, the expression `metaphysically necessary' and its interdefinable notions are indefinitely extensible–call this view modal expansionism. In accordance with recent modal treatments of the indefinite extensibility of set-theoretic expressions (see Fine (2006); Linnebo (2010); Studd (2013), and Uzquiano (2015)), where the modality used to explicate indefinite extensibility is interpretational, the paper thus provides a semantics for a quantified bimodal logic containing metaphysical and interpretational modal operators. This semantics is used to more precisely articulate the modal expansionist's diagnoses of the apparent paradoxes.

References
[1] K. Fine, Problem of Possibilia, Modality and Tense: Philosophical papers (K. Fine), Oxford Clarendon Press, 2005.
[2] K. Fine, Relatively Unrestricted Quantification, Absolute Generality (A. Rayo, G. Uzquiano, editors), Clarendon Press, Oxford, 2006.
[3] P. Fritz, A Purely Recombinatorial Puzzle, Unpublished manuscript. Hosted at https://dl.dropboxusercontent.com/u/15106063/drafts/A%20Purely%20Recombinatorial%20Puzzle.pdf
[4] D. Kaplan, A problem in Possible-World Semantics, Modality, Morality, and Belief: Essays in Honour of Ruth Barcan Marcus. (W. Sinnot-Armstrong, editor), Cambridge University Press, Cambridge, 1995.
[5] Ø. Linnebo, Pluralities and Sets, Journal of Philosophy, vol. 107 (2010), pp. 144–164.
[6] J. Studd, The Iterative Conception of Set: A (Bi-)Modal Axiomatisation, The Journal of Philosophical Logic, vol. 42 (2013), pp. 697–725.
[7] G. Uzquiano, Varieties of Indefinite Extensibility, Notre Dame Journal of Formal Logic, vol. 56 (2015), pp. 147–166.
[Close]

William Stafford, On the modal analogue of Frege’s theorem

Frege’s Theorem says that a second-order system (Hume’s Principle), equipped with a type-lowering “number of” operator, interprets full second-order Peano arithmetic (cf. [1] Chapter 1, [4] Chapter 4). This implies, among other things, that all models of this system must have infinite domains. Some have thought that this is inconsistent with the logicism which Frege, Wright, and Hale hoped to secure by means of this theorem. We examine the obstacles to, and resources required, for establishing a version of Frege’s Theorem in a modal setting, where it is consistent that each world contains only finitely many objects. The particular resources we consider are higher-order logic and resources for cross-world predication (cf. [3]). Further, we consider the relation of all this to (i) Hodes’ suggestion that “mathematics is higher-order modal logic” ([2]) and (ii) recent work by Linnebo [4] and Studd [5], which similarly embeds set theories and abstraction principles within the framework of higher-order modal logic.

References
[1] John P. Burgess, Fixing Frege, Princeton Monographs in Philosophy, Princeton University Press, Princeton, 2005.
[2] Harold Hodes, Logicism and the Ontological Commitments of Arithmetic, The Journal of Philosophy, vol. 81 (1984), no. 3, pp. 123–149.
[3] Alex Kocurek, The problem of cross-world predication, Journal of Philosophical Logic, 2016.
[4] \O{}ystein Linnebo, The Potential Hierarchy of Sets, The Review of Symbolic Logic, vol. 6 (2013), no. 2, pp. 205–228.
[5] James P Studd, Abstraction reconceived, The British Journal for the Philosophy of Science, 2015.
[6] Crispin Wright, Frege’s Conception of Numbers as Objects, Scots Philosophical Monographs, Aberdeen University Press, Aberdeen, 1983.
[Close]

Sławomir Kost, Connected frames for fusions of multimodal logics

Most of monomodal logics are characterized by classes of frames. It is even possible to use single connected frames for some logics. The additional modalities make the problem of seeking one connected frame more demanding. Let us consider multimodal logics $L_1$ and $L_2$. We assume that $L_1$ is characterized by a class $\mathcal{C}_1$ of connected $n$-frames and $L_2$ is characterized by a class $\mathcal{C}_2$ of connected $m$-frames. Classes $\mathcal{C}_1'$ and $\mathcal{C}_2'$ are closures of $\mathcal{C}_1$ and $\mathcal{C}_2$, respectively, under the formation of disjoint unions and isomorphic copies. It is already known that fusion $L_1\oplus L_2$ is characterized by the class $\mathcal{C}_1'\oplus \mathcal{C}_2'$ (see e.g. [2]). Let $\mathcal{C}=\{\mathfrak{F}_i;i\in I\}$ be the family of connected frames and $\mathfrak{F}$ be a connected frame. A point $x_0$ from $\mathfrak{F}$ is a $\mathcal{C}$-starting point if every mapping $f:\{x_0\}\to \mathfrak{F}_i$ can be extend to a $p$-morphism $f:\mathfrak{F}\to \mathfrak{F}_i$, for $i\in I$. We assume that there exists a $L_1$-frame $\mathfrak{F}^1$ with $\mathcal{C}_1$-starting point and there exists a $L_2$-frame $\mathfrak{F}^2$ with $\mathcal{C}_2$-starting point. Using isomorphic copies of the frames $\mathfrak{F}^1$ and $\mathfrak{F}^2$ we construct a connected frame $\mathfrak{F}^s$ characterizing the fusion $L_1\oplus L_2$. The obtained frame has some useful properties. Among others, $\mathfrak{F}^s$ is countable if both $\mathfrak{F}^1$ and $\mathfrak{F}^2$ are countable. Moreover, the frame $\mathfrak{F}^s$ has a $CS(\mathcal{C}_1'\oplus \mathcal{C}_2')$-starting point, where $CS(\mathcal{C}_1'\oplus \mathcal{C}_2')$ is a subclass of $\mathcal{C}_1'\oplus \mathcal{C}_2'$ such that $$L_1\oplus L_2=\mbox{Log}\{ \mathcal{C}_1'\oplus \mathcal{C}_2' \}=\mbox{Log}\{CS(\mathcal{C}_1'\oplus \mathcal{C}_2')\}.$$

References
[1] Patrick Blackburn, Maarten De Rijke, Yde Venema, Modal Logic, Cambridge Tracts in Theoretical Computer Science (No.53), Cambridge University Press, 2001.
[2] Edited by D.M. Gabbay, A. Kurucz, F. Wolter and M. Zakharyaschev. Many-Dimensional Modal Logics: Theory and Applications, Elsevier, 2003.
[3] Kit Fine, Gerhard Schurz, Transfer Theorems for Multimodal Logics, Logic and Reality, Cambridge University Press, 1996, pp. 169–213.
[Close]

Zofia Kostrzycka, On interpolation in Brouwer modal logics

We study the Brouwer modal logic $\mathbf{KTB}$ and its normal extensions, which are determined by a class of reflexive and symmetric Kripke frames with a given degree of branching. Hence we consider logics ${\bf KTBAlt(n)}:=\mathbf{KTB}\oplus alt_n$, where \begin{eqnarray*} &&alt_n:=\Box p_1 \vee \Box( p_1 \to p_2)\vee ...\vee \Box(( p_1 \wedge ... \wedge p_n) \to p_{n+1}),\;\;\;\;n\ge 3. \end{eqnarray*} For $n=3$ we get a linear Brouwer logic ${\bf KTBAlt(3)}$. It is proved in [1],[2] that all logics from $NEXT(\mathbf{KTBAlt(3)})$ have finite model property and are finitely axiomatizable. It is easily seen by the above theorem that the cardinality of the class $NEXT({\bf KTBAlt(3)})$ is only countably infinite. On the other side it is known that the cardinality of the class $NEXT({\bf KTBAlt(4)})$ is uncountably infinite [3]. We shall look for locally finite logics from $NEXT(\mathbf{KTB.Alt(n)})$ that have Craig interpolation property or at least interpolation property for deducibility. To do this, we shall characterize Halldén complete logics since there is an important connection between the Craig interpolation property and Halldén completeness of modal logics, see G. F. Schumm [6]. Among Halldén complete and locally finite logics from $NEXT(\mathbf{KTB.Alt(n)})$ we shall characterize the logics which have (CIP) or (IPD).

References
[1] Byrd, M., Ullrich, D. The extensions of $BAlt_3$, Journal of Philosophical Logic, vol. 6 (1977), pp. 109–117.
[2] Byrd, M., The extensions of $BAlt_3$ - revisited, Journal of Philosophical Logic, vol. 7 (1978), pp. 407–413.
[3] Kostrzycka, Z., {Miyazaki, Y.}, Normal modal logics determined by aligned clusters, submitted.
[4] Kostrzycka, Z., On Halldén completeness of modal logics determined by homogeneous Kripke frames, Bulletin of the Section of Logic, vol. 44 (2015), no. 3/4, pp. 1–20.
[5] Maksimowa, L., Amalgamation and Interpolation in Normal Modal Logics, Studia Logica, vol. 50 (1991), no. 3/4, pp. 457–471.
[6] Schumm, G. F., Some failures of interpolatin in modal logic, Notre Dame Journal of Formal Logic, vol. 27 (1986), no. (1), pp. 108–110.
[Close]

Martin Bays and Jonathan Kirby, Exponential-algebraic closedness and quasiminimality

It is well-known that the complex field $\mathbb C$, considered as a structure in the ring language, is strongly minimal: every definable subset of $\mathbb C$ itself is finite or co-finite. Zilber conjectured that the complex exponential field $\mathbb{C}_\mathrm{exp}$ is quasiminimal, that is, every subset of $\mathbb C$ definable in this structure is countable or co-countable. He later showed that if Schanuel's conjecture of transcendental number theory is true and $\mathbb{C}_\mathrm{exp}$ is strongly exponentially-algebraically closed then his conjecture holds [1]. Schanuel's conjecture is considered out of reach, and proving strong-exponential algebraic closedness involves finding solutions of certain systems of equations and then showing they are generic, the latter step usually done using Schanuel's conjecture. We show that if $\mathbb{C}_\mathrm{exp}$ is exponentially-algebraically closed then it is quasiminimal. Thus Schanuel's conjecture can be dropped as an assumption, and strong exponential-algebraic closedness can be weakened to exponential-algebraic closedness which requires certain systems of equations to have solutions, but says nothing about their genericity.

References
[1] Boris Zilber, Pseudo-exponentiation on algebraically closed fields of characteristic zero, Annals of Pure and Applied Logic, vol. 132 (2005), no. 1, pp. 67–95.
[Close]

Dimitra Hobitaki and Thanases Pheidas, Undecidability of the existential theory of the ring of exponential sums

Define the set of exponential sums, EXP($\mathbb{C}$), to be the the set of expressions \begin{equation} a=\alpha _0+\alpha _1e^{\mu_1z}+\dots +\alpha _Ne^{\mu_Nz} \end{equation} where $\alpha_i, \mu _j \in \mathbb{C}$. We ask whether the positive existential first order theory of EXP($\mathbb{C}$), as a structure of the language $$ {\bf L}=\{ +,\mathbb{C}dot, 0,1,e^z\} $$ is decidable or undecidable. In a recent unpublished paper P. D Aquino, Th. Pheidas and G. Terzo have proven a negative answer (actually they prove a stronger result), even for the positive theory, pending on a number theoretic hypothesis that is still being checked, We provide a new proof, based on theirs, but using different tools (`Pell Equations' instead of Elliptic Curves). Our approach has been suggested by A. Macintyre. Our result may be considered as an analogue of Hilbert's Tenth Problem for this structure and as a step to answering the similar problem for the ring of `exponential polynomials', which is still open. We prove: {\bf Theorem 1:} The solutions of the equation \begin{equation}\label{MD} (e^{2z}-1)y^2=x^2-1 \end{equation} where the unknowns $x$ and $y$ range over EXP($\mathbb{C}$) are given by \begin{equation} (x,y)=m\mathbb{C}dot (\pm e^z,1)\oplus n\mathbb{C}dot (\pm e^{-z},\i e^{-z}) \end{equation} where, for any solutions $(a_1,b_1)$, $(a_2,b_2)$ of (2) the law $\oplus$ is defined by $(a_1,b_1)\oplus (a_2,b_2)=(a_1a_2+(e^{2z}-1)b_1b_2, a_1b_2+a_2b_1)$. The proof uses techniques of [4], [1] and [3]. From this, by adapting techniques of [2] we are able to prove {\bf Theorem 2:} The ring of rational integers $\mathbb{Z}$ is positive existentially definable over EXP($\mathbb{C}$), as an ${\bf L}$-structure. Hence the positive existential theory of this structure is undecidable.

References
[1] T. Pheidas, P. D'Aquino, G. Terzo, Undecidability of the diophantine theory of exponential sums, manuscript
[2] J. Denef, The diophantine problem for polynomial rings and fields of rational functions, Transactions of the American Mathematical Society, vol. 242 (1978), pp. 391–399.
[3] Th. Pheidas and K. Zahidi , Undecidable existential theories of polynomial rings and function fields, Communications in Algebra, vol. 27 (1999), no. 10, pp. 4993–5010.
[4] L. van den Dries, Exponential rings, exponential polynomials and exponential functions, Pacific Journal of Mathematics, vol. 113 (1984), no. 1, pp. 51–66.
[Close]

Erick Garcia Ramirez, Tangent cones and stratifications in real closed valued fields

We show that for a definable set $X$ in a real closed valued field, the stratifications defined in [1] induce stratifications of the same nature on the tangent cones of $X$. This shows in particular that those stratifications are stronger than classical Whitney stratifications (introduced in [2]), as the latter do not induce (Whitney) stratifications on tangent cones.

References
[1] I. Halupczok, Non-archimedean Whitney stratifications, Proceedings of the London Mathematical Society, (2013), no. 109, pp. 1304–1362.
[2] H. Whitney Tangents to an analytic variety, Annals of Mathematics, Second Series, vol. 81 (1965), no. 3, pp. 496–549.
[Close]

Aibat Yeshkeyev and Olga Ulbrikht, Cosemanticness and JSB-property for Abelian Groups

We will give some model-theoretic results of Abelian groups in the frame of Jonsson theories. In the [1] John Goodrick gave necessary and sufficient conditions of the Schroder-Bernstein (SB) property for complete theories of Abelian groups. We consider Jonsson analogue of Theorem 1 from [1].
Jonsson theory $T$ has the Schroder-Bernstein (JSB) property if for any two models $A, B\in E_T$ from the fact that they are mutually isomorphically embeddable each other follows that they are isomorphic.
We know that theory of Abelian groups will be a Jonsson theory and also perfect.
In connection with this concept, we got the result that the following theorem is true:

Theorem. Let $T$ be a Jonsson theory of Abelian groups, then the following conditions are equivalent:
(1) $T$ is $J-\omega-$stable;
(2) $T^*$ is $\omega-$stable;
(3) $T$ has JSB property.

Let $A\in Mod$ $\sigma_{AG}$, where $\sigma_{AG}=\langle +,-, 0\rangle$, i.e. our considered theories are universal. Denote through $JSp(A)$ Jonsson spectrum of Abelian group $A$, where $JSp(A)=\{T | T$ is a Jonsson theory in language $\sigma_{AG}$ and $A\in Mod T\}$.
We say that $T_1$ is cosemantic to $T_2$ ($T_1\bowtie T_2$) if $C_{T_1}=C_{T_2}$, where $C_{T_i}$ is semantic model of $T_i$, $i=1, 2$. Then it is easy to notice that $JSp(A)/_{\bowtie}$ is a factor set by relation $\bowtie$ and let its power equals $\mu$, i.e. $|JSp(A)/_{\bowtie}|=\mu$.

Theorem. Let $T$ is Jonsson theory of Abelian groups then $C_T\in E_T$ and $C_T$ is divisible group and its a Shmelev's standart group is $\underset{\kappa}\oplus\mathbb{Z}_{p^\infty}\underset{\kappa}\oplus\mathbb{Q}$, where $\kappa=|C|$.

Let's call a pair $(\alpha,\beta)^A_C$ as Jonsson invariant of Abelian group $A$ if a Shmelev's standart group of a group $A$ is a group of the following form $\underset{\alpha}\oplus\mathbb{Z}_{p^\infty}\underset{\beta}\oplus\mathbb{Q},$ where $C$ is semantic model of $[T]\in JSp(A)/_{\bowtie}$.
The following result is a Jonsson analogue of the well-known Shmelev's theorem about the elementary classification of Abelian groups.

Theorem. Let $A,B\in Mod$ $\sigma_{AG}$ then $A \bowtie B \Leftrightarrow (\alpha,\beta)^A_{C_i}=(\alpha,\beta)^B_{C_i}$, $i\in I$, $|I|=\mu$.

All additional information regarding Jonsson theories can be found in [2].

References
[1] Goodrick J., The Schroder-Bernstein property for theories of abelian groups, arXiv.org $>$ math $>$ arXiv:0705.1850v1, 2007.
[2] Yeshkeyev A.R., Jonsson Theories, Publisher of the Karaganda state university, 2009.
[Close]

Dino Rossegger and Ekaterina Fokina, Enumerable functors

We propose a new notion of reducibility between structures, enumerable functors, inspired by the recently investigated notion of computable functors [1], [2]. An enumerable functor from a structure $\mathcal{A}$ to a structure $\mathcal{B}$ is a pair $(\Psi, \Phi)$ where $\Psi$ is an enumeration operator transforming every presentation of $\mathcal{A}$ to a presentation of $\mathcal{B}$ and $\Phi$ is a Turing functional transforming every isomorphism between two presentations of $\mathcal{A}$ to an isomorphism of their image. Our main results are that enumerable functors preserve $\Sigma_n$–spectra [3] and that they are equivalent to a restricted version of effective interpretability. We also extend this equivalence to effective bi-interpretability and reducibility between classes of structures by effective bi-interpretability.

References
[1] Matthew Harrison-Trainor, Alexander Melnikov, Russel Miller, and Antonio Montalbán, Computable functors and effective interpretability, submitted for publication
[2] Russel Miller, Bjorn Poonen, Hans Schoutens, and Alexandra Shlapentokh, A computable functor from graphs to fields, submitted for publication
[3] Ekaterina Fokina, Pavel Semukhin, and Daniel Turetsky, Degree spectra of sructures under equivalence relations, in preparation
[Close]

Sergey Ospichev, Minimal numberings of partial computable functionals

One of the main questions in numbering theory is studying extremal elements of Rogers semilattices of different families. Here we concentrate our interest on partial computable functionals of finite types. Let's define \textsl{functional type}. Let $T$ will be the set of all types. 1. $0\in{T}$; 2. if $\sigma$,$\tau$ are types, then $(\sigma\times\tau)$ and $(\sigma|\tau)$ are also types; 3. $T$ - minimal set, satisfying 1 and 2. Now we define \textsl{partial computable functionals}. Let $C_\sigma$ be family of all partial computable functionals of type $\sigma$. Let $C_0$ be the family of all partial computable functions or the family of all computable enumerable sets. If $C_\sigma$ and $C_\tau$ are already defined, then $C_{(\sigma\times\tau)}\rightleftharpoons C_\sigma\times C_\tau$ and $C_{(\sigma|\tau)}\rightleftharpoons\mathfrak{Mor}(C_\sigma,C_\tau)$. Any $C_\sigma$ has natural universal numbering $\nu_\sigma$ by definition. So we call numbering $\mu$ $\sigma$-computable if $\mu$ is reducible to $\nu_\sigma$. In work are proven

Theorem. For any $\sigma\in{T}$ there are infinitely many nonequivalent $\sigma$-computable friedberg numberings of family $C_\sigma$.

Theorem. For any $\sigma\in{T}$ there are infinitely many nonequivalent $\sigma$-computable positive undecidable numberings of family $C_\sigma$.

Theorem. For any $\sigma\in{T}$ there is infinite $\sigma$-computable family $\mathcal{S}\subset C_\sigma$ without $\sigma$-computable friedberg numberings.

The reported study was partially supported by RFBR, research project No. 14-01-00376 and by the Grants Council (under RF President) for State Aid of Leading Scientific Schools (grant NSh-6848.2016.1).
[Close]

Arno Pauly, Computability on the space of countable ordinals

While there is a well-established notion of what a computable ordinal is, the question which functions on the countable ordinals ought to be computable has received less attention so far (but cf. [1]). In order to remedy this, we explore various potential representations (in the sense of computable analysis [6, 3]) of the set of countable ordinals. An equivalence class of representations is then suggested as a standard, as it offers the desired closure properties. This class is characterized exactly by the computability of four specific operations. We show that the supremum of a continuous function from Baire space into the countable ordinals can be computed from a name of such function. The binary infimum is also a computable operation, and with some caveat regarding finite values, even countable infima are computable. With a decent notion of computability on the space of countable ordinals in place, we can then state and prove a computable uniform version of the Hausdorff-Kuratowski theorem. We can also show yet another proof of the computable Lusin separation theorem (cf. [2]). A preprint is available on the arXiv [5], and a preliminary version appeared as [4].

References
[1] Zhenhao Li and Joel D. Hamkins, On effectiveness of operations on countable ordinals, unpublished notes.
[2] Author's Name, Classical descriptive set theory as a refinement of effective descriptive set theory, Annals of Pure and Applied Logic, vol. 162 (2010), pp. 243–255.
[3] Arno Pauly, On the topological aspects of the theory of represented spaces, Computability, to appear (2016), available at http://arxiv.org/abs/1204.3763.
[4] ― Computability on the Countable Ordinals and the Hausdorff-Kuratowski Theorem (Extended Abstract), Mathematical Foundations of Computer Science 2015 (G. Italiano and G. Pighizzini and D. Sannella) Lecture Notes in Computer Science, vol. 9234, Springer, 2015.
[5] ―, Computability on the countable ordinals and the {H}ausdorff-{K}uratowski theorem, arXiv 1501.00386, 2015.
[6] Klaus Weihrauch, Computable Analysis, Springer, 2000.
[Close]

Christian Espindola, Completeness of Infinitary Intuitionistic Logics

Completeness theorems for infinitary classical logics $\mathcal{L}_{\kappa, \kappa}$ (for, say, an inaccessible $\kappa$) have been known for decades. When removing excluded middle, however, the situation is more difficult to analyze even in the propositional case, as the main difficulty in studying infinitary intuitionistic logics is the huge variety of non-equivalent formulas that one can obtain. Completeness results for the propositional fragment $\mathcal{L}_{\omega_1, 0}$ have been obtained, but the general case has not been addressed. The purpose of this talk is to outline set-theoretical and category-theoretical techniques that allow the study of completeness theorems for infinitary intuitionistic logics in the general case, both for propositional and first-order logics, in terms of an infinitary Kripke semantics. We will also analyze to what extent the use of large cardinal axioms (more precisely, the condition that $\kappa$ be weakly compact) is necessary, and some applications of the completeness results will be presented.

References
[1] P. Johnstone,Sketches of an Elephant - A Topos Theory Compendium - Vol I and II, Oxford University Press, 2002.
[2] A. Kanamori,The higher infinite, Springer Verlag, 1994.
[3] C. Karp,Languages with expressions of infinite length, North-Holland Publishing Co, 1964.
[4] S. Maclane, I. Moerdijk,Sheaves in geometry and logic, Springer Verlag New York, 1994.
[5] M. Makkai,A theorem on Barr-exact categories, with an infinite generalization,Annals of Pure and Applied Logic,vol. 47 (1990), pp. 225–268.
[6] M. Nadel,Infinitary intuitionistic logic from a classical point of view,Annals of Mathematical Logic, vol. 14 (1978), no. 2, pp. 159–191.
[Close]

Henrik Forssell, Constructive reflection principles for regular theories

Classically, any structure for a signature $\Sigma$ may be completed to a model of a desired regular theory $\mathbb{T}$ by means of the chase construction or small object argument. Moreover, this exhibits $\operatorname{Mod}({\mathbb{T}})$ as weakly reflective in $\operatorname{Str}({\Sigma})$. We investigate this in the constructive setting. The basic construction is unproblematic; however, it is no longer a weak reflection. Indeed, we show that various reflection principles for models of regular theories are equivalent to choice principles in the ambient set theory. However, the embedding of a structure into its chase-completion still satisfies a conservativity property, which suffices for applications such as the completeness of regular logic with respect to Tarski (i.e. set) models. We also consider the extent to which this analysis can be carried over to stronger fragments of first-order logic, notably involving disjunctions. Unlike most constructive developments of predicate logic, we do not assume that equality between symbols in the signature is decidable. This is joint work with Peter LeFanu Lumsdaine.
[Close]

Henning Urbat, Eilenberg-Reiterman Theory for a Monad

Algebraic language theory investigates machine behaviours by relating them to algebraic structures. Its core result is Eilenberg's variety theorem [2]: varieties of languages (classes of regular languages closed under boolean operations, derivatives, and preimages of monoid morphisms) correspond to pseudovarieties of monoids (classes of finite monoids closed under quotients, submonoids, and finite products). This together with Reiterman's theorem [3], stating that pseudovarieties can be specified by profinite equations, establishes a firm connection between automata, regular languages, and algebra. In the meantime, numerous further Eilenberg-type correspondences have been discovered, either dealing with classes of regular languages with weaker closure properties, or considering other types of languages such as languages of infinite words, tree languages, or cost functions. This plethora of similar results has spurred interest in categorical approaches to algebraic language theory, putting a common roof over the various developments. In this talk, we present a general Eilenberg-Reiterman theorem [1, 4] that achieves the desired unification. The idea is to model languages, and the algebras recognizing them, by monads on some algebraic category. Then Stone-type dualities are used to relate pseudovarieties of finite algebras to profinite equational theories and classes of recognizable languages. Our framework covers the bulk of Eilenberg-Reiterman theorems in the literature, and produces new correspondences for free.

References
[1] L.-T. Chen, J. Adámek, S. Milius, and H. Urbat. Profinite monads, profinite equations and Reiterman’s theorem. Proc. FoSSaCS’16. LNCS 9634, Springer, 2016.
[2] S. Eilenberg. Automata, Languages, and Machines, Vol. B, Academic Press, New York, 1976.
[3] J. Reiterman. The Birkhoff theorem for finite algebras. Algebra Universalis, 14(1):1–10, 1982.
[4] H. Urbat, J. Adámek, L.-T. Chen, and S. Milius. One Eilenberg theorem to rule them all. Preprint: http://arxiv.org/abs/1602.05831, 2016.
[Close]

Richard Lawrence, Concepts and objects in game-theoretical semantics

Frege's distinction between objects and concepts represents an important break he makes from the earlier logical tradition, and it has had an outsized influence ever since: it is the basis of the distinction between first- and second-order logic, as well as the type system used in studying natural language semantics. But the distinction is also the source of some of Frege's most puzzling remarks. I will re-examine the distinction, offering a new interpretation of it based on game-theoretical semantics. A standard reading construes Frege's distinction as a distinction between two ontological categories: objects are `saturated' entities, while concepts are `unsaturated' entities. This reading faces serious interpretive challenges, however. A better interpretation conceives objects and concepts as epistemological roles: something belongs to one category or the other depending on how it is apprehended in scientific thought. Unfortunately, Frege's metaphors are little help in deciding when something plays one role or the other. Clearer criteria can be derived from Hintikka's game-theoretical semantics for first-order logic. We can understand the distinction between objects and concepts in terms of their different roles in a semantic game that defines truth in a model. An object is what players seek, find, and specify when executing quantifier moves in this game. A concept is what guides a player as she makes such moves: it distinguishes a strategic choice from a non-strategic one. This characterization of objects and concepts has the virtue of ontological neutrality, offering a clear sense in which numbers, colors, and planets all count as objects, without committing us to finding anything common in their ontologies. It also suggests a new understanding of second-order quantification.
[Close]

Jonathan Dittrich, The inadequacy of nontransitive solutions to paradox

[1] has argued that a nontransitive substructural logic (NT) provides both a solution to semantic paradoxes and preserves full classical logic. Here we argue that NT fulfils these goals only inadequately. We distinguish between weak and strong inconsistency: A language is weakly inconsistent for some formula $\phi$ iff it proves both    $\vdash \phi$ and $\phi \vdash$   . It is strongly inconsistent iff it proves the empty sequent. Although NT is strongly consistent, it remains weakly inconsistent. For even without Cut, NT derives both    $\vdash$ T($\ulcorner \lambda \urcorner$) and T($\ulcorner \lambda \urcorner$) $\vdash$    for the Liar sentence $\lambda$. According to Ripley, the characteristic of any paradoxical sentence $\psi$ is that both    $\vdash \psi$ and $\psi \vdash   $ are provable. However, one can show that NT is weakly inconsistent for many central theorems of classical logic as well; including the law of non-contradiction, excluded middle and identity. This is straightforward in first-order logic when these principles are understood in terms of the Truth-predicate. With second-order logic, this can be extended to hold of these theorems understood with arbitrary predicates. There are two problems. First, NT fails to provide an adequate distinction between paradoxical and non-paradoxical sentences. For classical theorems bear the characteristic of paradoxes. Second, it casts doubt on the classicality of NT. Intuitively, it is not sufficient to merely prove all theorems of classical logic. For even an inconsistent system with explosion will do this. One would further have to ensure that the system does not prove anything weakly inconsistent with these theorems - again, NT fails to do so.

References
[1] David Ripley, Conservatively Extending Classical Logic with Transparent Truth, Review of Symbolic Logic, vol. 5 (2012), no. 2, pp. 354–378.
[Close]

Malte Kließ, Strong Predicate Exchangeability in Inductive Logic

In Pure Inductive Logic we study the consequences for an agent's rational belief function given that she assumes a list of rational principles [4], in the framework following Carnap's Inductive Logic [1]. The Principle of Strong Predicate Exchangeability, or SPx, is a rational principle stating that an agent's belief in a sentence $\phi$ should be the same as that in the statement $\psi$, where $\psi$ is obtained from $\phi$ by permuting the atoms occurring in $\phi$ freely as long as the number of negations remains fixed. The principle was discovered during work on Predicate Exchangeability [2],[3]. The principle is in strength between Predicate Exchangeability and Atom Exchangeability, in the sense that each probability function satisfying a stronger principle also satisfies the weaker one, but not vice versa. Representation Theorems for SPx show a remarkable similarity to those for Atom Exchangeability. In terms of justification, we can obtain SPx both through a generalization of Atom Exchangeability and a weakening of Johnson's Sufficientness Postulate. We will give an outline of the representation theorems and show the relation between the rational principles.

References
[1] Rudolf Carnap, A Basic System of Inductive Logic, Studies in Inductive Logic and Probability (R. Carnap and R.C. Jeffrey, editors), University of California Press, 1971, pp. 33–165.
[2] Malte S. Kließ, The Principle of Predicate Exchangeability in Pure Inductive Logic, PhD Thesis, University of Manchester, 2013.
[3] Malte Kließ and Jeff Paris, Predicate Exchangeability and Language Invariance in Pure Inductive Logic, Logique & Analyse, vol. 57 (2014), no. 228, pp. 513–540.
[4] Jeffrey Paris and Alena Vencovská, Pure Inductive Logic, Perspectives in Logic, Cambridge University Press, 2015.
[Close]

Eric Epstein, Component contexts, reference determination, and the Liar Paradox

Consider the following:
(A) Sentence A is not true.
Reflection on this sentence leads quickly to contradictions. This is the Liar paradox. I develop a diagnosis and solution for this paradox. There is no contradiction, because sentences like A fail to say what they appear to say. This is because the key occurrence of the word 'true' in any such sentence fails to refer to truth. Instead of referring to truth, such occurrences are indeterminate in reference as between two other truth-like properties, a-truth and d-truth, discussed by (Scharp 2013). It is therefore indeterminate whether a Liar sentence like A says of itself that it is not a-true or that it is not d-true. Still, one needn't hold that Liar sentences are meaningless. Rather, they come quite close to saying of themselves that they are not true, since a-truth and d-truth are very similar to truth. Contextualist and indexicalist approaches to the Liar paradox also maintain that certain problematic sentences containing the truth-predicate fail to express propositions. Unlike those approaches, mine does not take the truth-predicate to refer to different properties across different contexts of use. Instead, I take it to be sensitive to its linguistic context of occurrence. My view better navigates the difficulties raised for contextualist and indexicalist approaches. E.g., my solution allows for unrestricted quantification over contexts, and better respects the linguistic data about how `true' behaves in non-paradoxical sentences. On my view, the word `true' refers to truth, but its occurrence in any Liar sentence does not. Therefore, sometimes an occurrence of an expression differs in reference from the expression of which it is an occurrence. This may seem surprising, but compared to the demands of alternative approaches it is a small price to pay.

References
[1] Kevin Scharp, Replacing Truth, Oxford University Press 2013.
[Close]

Diana Costa, Manuel A. Martins and João Marcos, Inconsistent accessibility relation in Hybrid logic

.
[1] Besnard, P. and Hunter, A., Quasi-classical logic: Non-trivializable classical reasoning from inconsistent information, Symbolic and Quantitative Approaches to Reasoning and Uncertainty – Lecture Notes in Computer Science vol.946, (Froidevaux, C. and Kohlas, J., editors), Springer Berlin Heidelberg, 1995, pp.44-51.
[2] Blackburn, P., Representation, reasoning, and relational structures: A hybrid logic manifesto, Logic Journal of the IGPL, vol.8 (2000), no.3, pp.339–365.
[Close]

Yuna Won, Chisholm's Paradox Revisited: A Dynamic Implementation of Kratzer Semantics for Deontic `Ought's

Chisholm's Paradox is one of the most famous puzzles in the deontic logic literature. It is commonly believed that the Chisholm's Paradox arises only in Standard Deontic Logic (SDL), but not in ordering semantics, which is now the orthodox semantics for conditionals and modals. Although ordering semantics is free from this classic puzzle, I argue that ordering semantics fails to meet the real challenge raised by Chisholm's example, which is about the nature of contrary-to-duty (CTD) obligations\textemdash a type of obligations that takes effect when a corresponding primary obligation is violated. To show that ordering semantics cannot provide an adequate formal representation of CTD obligations, I put forward a new puzzle, the CTD trilemma, extending the familiar example from Chisholm's Paradox. The source of their limitation will be identified, and possible resistance to the CTD trilemma will be carefully examined. To solve this new puzzle and adequately capture the notion of CTD obligations in a formal system, I maintain that we need to acknowledge two different normative uses of deontic modal sentences corresponding to the world-to-word direction of fit and the word-to-world direction of fit; I call the former type the axiological use of `ought'-statements and the latter the deontological use of `ought'-statements. Finally, I propose a dynamic approach which accounts for these two meanings of `ought's based on Kratzer semantics and show how it solves the CTD trilemma.
[Close]

Anahit Chubaryan, Artur Khamisyan and Arman Tshitoyan, Some new proof systems for a version of many-valued logics and proof complexities in it

Some method for construction a deductive full propositional calculi for some version of $k$-valued ($k\geq 3$.) logic is described in the paper. The propositional connectives are defined as follows: conjunction is min, disjunction is max, negation is defined by permuting the truthvalues cyclically. We use as literals the propositional variables, variables with negation, with double negations, with triple negations etc. We generalize the notions of determinative conjunct and determinative disjunctive normal form (dDNF), introduced by first coauthor for two-valued Boolean functions in [1], and on the base of it construct the systems $E_k$, axioms of which are not fixed. Each conjunct from some dDNF of given formula can be considered as an axiom . The elimination rule ($e$-rule) infers conjunct $K'\cup K"\cup K"'\cup\cdots$ from conjuncts $K'\cup \{p\}$, $K"\cup \{^{\sim}p\}$, $K"'\cup \{^{\sim\sim}p\}$ etc. for a propositional variable $p$. $E_k$-proof is defined as usually. It is obvious that some DNF $D=\{K_1, K_2, \ldots, K_i\}$ is $k$-valued tautology iff using $e$-rule we can derive the empty conjnct from axioms $\{K_1, K_2, \ldots, K_i\}$. We prove also that for every $k$ there is some sequence of $k$-valued tautologies, which have in described systems the same by order upper and lower bounds for the main proof complexity characteristics: exponential for lines and size, polynomial for space and width.

References
[1] An. Chubaryan, Arm. Chubaryan, A new conception of Equality of Tautologies, L{&}PS, Triest, Italy, Vol. V, No 1, 2007, pp. 3-8.
[Close]

Hubert Bożek, Analysis of functional expressions in Leon Chwistek's elementary semantics and $\lambda$-calculus by Alonzo Church

In my presentation I wish to discuss some similarities between Leon Chwistek's elementary semantics (ES) and $\lambda$-calculus introduced by Alonzo Church, both systems dating back to early 1930's (1, 2, 3, 4, 5) Chwistek: 1929, 1932, 1933 ; Church: 1932, 1936). Instead of comprehensive comparison of the two formal systems, I will focus on the representations of functional expressions they offer. My goal is to demonstrate that both construction and transformation rules of the systems in question are in fact mutually reducible or interchangeable, at least, when applied to functions of the same assumed logical type.

References
[1] Leon Chwistek, Neue Grundlagen der Logik und Mathematik, Mathematische Zeitschrift, vol.30 (1929), pp.704-724.
[2] ―, Neue Grundlagen der Logik und Mathematik. Zweite Mitteilung, Mathematische Zeitschrift, vol.34 (1932), pp.527-534.
[3] ―, Die nominalistische Grundlegung der Mathematik, Erkenntnis, vol.3(1933), no. 4-6, pp. 367-388.
[4] Alonzo Church, A Set of Postulates for the Foundation of Logic, Annals of Mathematics, vol.33 (1932), no.2, pp.346–366.
[5] ―, An Unsolvable Problem of Elementary Number Theory, American Journal of Mathematics, vol.58 (1936), pp. 354-363.
[Close]

İbrahim Şentürk, Tahsin Oner and Urfat Nuriyev, Completeness of Categorical Syllogisms By Means of Diagrammatic Method

In this study, our goal is to show the completeness of categorical syllogisms by means of diagrammatic method. For this, we firstly construct a formal system SLCD (Syllogistic Logic with Caroll Diagrams), which gives us a formal approach to logical reasoning with diagrams, for representations of the fundamental Aristotelian categorical propositions and show that they are closed under the syllogistic criterion of inference which is the deletion of middle term. Therefore, it is implemented to let the formalism comprise synchronically bilateral and trilateral diagrammatical appearance and a naive algorithmic nature. And also, there is no need specific knowledge or exclusive ability to understand as well as to use it. In other respects, we scrutinize algebraic properties of categorical syllogisms together with a representation of syllogistic arguments by using sets in SLCD. To this end, we explain quantitative relation between two terms by means of bilateral diagrams. Thereupon, we enter the data, which are taken from bilateral diagrams, on the trilateral diagram. With the help of elemination method, we obtain a conclusion which is transformed from trilateral to bilateral diagram. A categorical syllogistic system consists of 256 syllogistic moods, 15 of which are unconditionally and 9 are conditionally; in total 24 of them are valid. Those syllogisms in the conditional group are also said to be strengthened, or valid under existential import, which is an explicit assumption of existence of some S, M or P. So, we add a rule, which is Some X is X when $X$ exists, to SLCD. Therefore, we obtain the formal system SLCD$^\dagger$ from SLCD. Finally, we show that syllogism is valid if and only if it is provable in SLCD and strengthened syllogism is valid if and only if it is provable in SLCD$^\dagger$. This means that SLCD is sound and complete.

References
[1] Lewis Caroll. Symbolic Logic, Clarkson N. Potter, 1896.
[2] Jan \L{}ukasiewicz. Aristotle's Syllogistic From the Standpoint of Modern Logic, Clarendon Press, Oxford, 1951.
[3] I. Pratt-Hartmann and L. S. Moss, On the Computational Complexity of the Numerically Definite Syllogistic and Related Logics, Review of Symbolic Logic, vol.2, no.4, pp.647–683, 2009.
[4] Ruggero Pagnan, A Diagrammatic Calculus of Syllogisms, journal of logic language and information, no.21, pp.347–364, 2012.
[5] A. E. Kulinkovich, Algorithmization of Resoning in Solving Geological Problems, Proceedings of the Methodology of Geographical Sciences Naukova Dumka, 1979, pp. 145–161.
[6] Ibrahim Senturk, Tahsin Oner, Urfat Nuriyev, An Algebraic Approach to Categorical Syllogisms By Using Bilateral Diagrams, Theoretical and Applied Aspects of Cybernetics. Proceedings of the 5th International Scientific Conference of Students and Young Scientists ( Kyiv-Ukraine), 2015, pp. 14–21.
[Close]

Pavel Semukhin and Igor Potapov, Decidability of reachability problems in $\mathrm{SL}(2,\mathbb{Z})$

The vector reachability problem for semigroups in $\mathrm{SL}(2,\mathbb{Z})$ is defined as follows: Given two vectors $\mathbf{x}$ and $\mathbf{y}$ with integer coefficients and a finite collection of matrices $M_1,\ldots,M_n$ from $\mathrm{SL}(2,\mathbb{Z})$, decide whether there exists a matrix $M$ from the semigroup $\langle M_1,\ldots,M_n\rangle$ generated by the matrices $M_1,\ldots,M_n$ such that $M\mathbf{x}=\mathbf{y}$. Similarly, we define reachability problem by fractional linear transformations in $\mathrm{SL}(2,\mathbb{Z})$: Given two rational numbers $x$ and $y$ and a finite collection of matrices $M_1,\ldots,M_n$ from $\mathrm{SL}(2,\mathbb{Z})$, decide whether there exists a matrix $\begin{bmatrix} a & b\\ c & d \end{bmatrix}\! \in\! \langle M_1,\ldots,M_n\rangle$ such that $\dfrac{ax+b}{cx+d}=y$. In this talk we present a proof that the above-mentioned reachability problems in $\mathrm{SL}(2,\mathbb{Z})$ are decidable. Our approach to solving these problems relies on the translation of numerical questions on matrices into computational problems on words and regular languages. We will also consider a geometric interpretation of reachability paths and use this technique to prove decidability of a special case of the {\sl scalar reachability problem} in $\mathrm{SL}(2,\mathbb{Z})$, which can be viewed as a generalization of the vector reachability problem.
[Close]

Christoph-Simon Senjak, A Theory of Parsers

Parsing is an essential problem in Computer Science, and especially since streaming of data has become popular, parsing data "online" and getting partial results as fast as possible with a reasonably small amount of memory is a main objective. There are several formal approaches to this problem (e.g. the pi calculus). We present an approach that uses relations between input and output of a parser, and properties that, when proved about those relations, make them well-suited for parsing, and usually lead to efficient parsers by program extraction. We present some monad-style combinators that we use to build up more complex relations from simpler ones. We used our approach to write an implementation of Deflate (compression standard) in Coq, which shows that it is not only theoretically beautiful but also practically usable. While our own research only uses Coq, it should be easily adaptable to any dependently typed programming language.
[Close]

Svetlana Aleksandrova and Nikolay Bazhenov, Automatic and tree-automatic list structures

Moore and Russell introduced their formal theory of linear lists in [1]. Generalizing this theory, Goncharov [2] constructed the axiomatic theory of linear lists over the elements of a given data type.
In this talk we will discuss algorithmic complexity of models of this theory of lists. We exhibit automatic properties of different classes of list structures using the framework of automatic and tree-automatic structures. In particular, we show that list structures over certain sets do not have automatic copies but have tree-automatic presentations, while stronger hereditarily finite list superstructure is not tree-automatically presentable.
We will also explore properties of list structures with respect to ordinal-automatic structures introduced by Schlicht and Stephan [3].

References
[1] D.J. Moore and B. Russell, Axiomatic Data Type Specifications: a First Order Theory of Linear Lists, Acta Informatica, 15(3):193-207, 1981.
[2] S.S. Goncharov, A Theory of Lists and Its Models, Vychisl. Sistemy, 114:84-95, 1986 (In Russian).
[3] Ph. Schlicht and F. Stephan, Automata on ordinals and automaticity of linear orders, Annals of Pure and Applied Logic, 164(5):523 527, 2013.
Supported by the Grants Council (under RF President) for State Aid of Leading Scientific Schools (grant NSh-6848.2016.1)
[Close]

Joshua Blinkhorn, Dependency schemes and soundness in QBF calculi

The tremendous success of SAT solvers in recent years is motivating advances in quantified Boolean formula (QBF) solving. Afforded by its PSPACE-completeness, QBF allows natural and compact encodings of real-world problems [4], due to the addition of a quantifier prefix to the propositional formula. The quantifier prefix of a QBF imposes a linear order on the variables, in which a given variable may depend upon any preceding variable. It need not, however, necessarily depend on all the preceding variables. A dependency scheme is an algorithm that attempts to identify cases of independence by appeal to the syntactic form of an instance, producing a partial order on the variables that describes the dependency structure more accurately. Harnessing independence in this way, a solver enjoys greater freedom to navigate the search space, and frequently solves the instance faster despite the computational overhead incurred in computing the dependency scheme [2]. Whereas there is potential to implement independence further in QBF solving, a major concern is whether the use of a given scheme preserves the correctness of the solving method [3]; that is, does the underlying proof system remain sound when parametrised by the dependency scheme? To that end, we show how to implement dependency schemes in stronger `long-distance' QBF calculi, and demonstrate that the notion of `full exhibition', which is a property of dependency schemes, is sufficient for soundness in all the resulting systems. Further, we show that the reflexive resolution path dependency scheme is fully exhibited, thereby proving a conjecture of Slivovsky [1].

References
[1] Slivovsky, F., Stucture in \#SAT and QBF, PhD thesis (2015), Vienna University of Technology.
[2] Lonsing, F., Dependency shemes and search-based QBF solving: theory and practice, PhD thesis (2012), Johannes Kepler University.
[3]Room Slivovsky, F., Szeider, S., Soundness of Q-resolution with dependency schemes, Theoretical Computer Science, vol. 612 (2016), pp. 83–101.
[4] Benedetti, M., Mangassarian, H., QBF-based formal verification: experience and perspectives, Satisfiability, Boolean Modeling and Computation, vol. 5 (2008), nos. 1–4, pp. 133–191.
[Close]