ABSTRACT. In first-order theories of arithmetic, the only ``official'' objects are natural numbers. However, much of the expressive power of these theories comes from the fact that we may also work with finite sets of numbers by means of bounded definable sets (or even to encode such sets by numbers where possible). In many applications of finite sets in arithmetic, it is crucial that we can count their cardinalities. The most straightforward way to do that requires the totality of the exponentiation function.

In weaker fragments of arithmetic that lack exponentiation (variants of bounded arithmetic), exact counting of bounded definable sets is not possible. Nevertheless, impromptu rough comparison of set sizes could be sometimes achieved by ad~hoc use of combinatorial principles available in these theories, most notably variants of the weak pigeonhole principle (WPHP).

By exploiting the power of the weak pigeonhole principle in a systematic way, we can in fact develop a general framework for approximate counting of bounded definable sets in fragments of bounded arithmetic~\cite{ej:dwphp,ej:apx,ej:hash}.

Approximate counting has various applications within bounded arithmetic. The original motivations were, first, that it can be used to handle randomized algorithms in bounded arithmetic, and to develop the basic theory of probabilistic complexity classes such as BPP; second, to facilitate proofs of combinatorial or number-theoretic statements that rely on counting and probabilistic arguments. Somewhat unexpectedly, approximate counting has been recently employed to show the collapse of the bounded depth proof hierarchy for propositional proof systems using mod-$p$ gates~\cite{bkz}.

ABSTRACT. This will be a three part tutorial: 1. General introduction to Stone duality 2. Applications in semantics 3. Applications in formal languages: automata and beyond

ABSTRACT. Towards the development of more reliable computerized systems, expressive models are designed, targetting application to automatic verification (model-checking). As part of this effort, timed automata have been proposed in the early nineties [2] as a powerful and suitable model to reason about (the correctness of) real-time computerized systems. Timed automata extend finite-state automata with several clocks, which can be used to enforce timing constraints between various events in the system. They provide a convenient formalism and enjoy reasonably-efficient algorithms (e.g. reachability can be decided using polynomial space), which explains the enormous interest that they provoked in the community of formal methods. Timed games [4] extend timed automata with a way of modelling systems interacting with external, uncontrollable components: some transitions of the automaton cannot be forced or prevented to happen. The reachability problem then asks whether there is a strategy (or controller) to reach a given state, whatever the (uncontrollable) environment does. This problem can also be decided, in exponential time. Timed automata and games are not powerful enough for representing quantities like resources, prices, temperature, etc. The more general model of hybrid automata [14] allows for accurate modelling of such quantities using hybrid variables. The evolution of these variables follow differential equations, depending on the state of the system, and this unfortunately makes the reachability problem undecidable, even in the very restricted case of stopwatches (stopwatches are clocks that can be stopped, and hence, automata with stopwatches only are the simplest hybrid automata one can think of). Weighted (or priced) timed automata [3, 5] and games [15, 1, 9] have been proposed in the early 2000’s as an intermediary model for modelling resource consumption or allocation problems in real-time systems (e.g. optimal scheduling [6]). As opposed to (linear) hybrid systems, an execution in a weighted timed model is simply one in the underlying timed model: the extra quantitative information is just an observer of the system, and it does not modify the possible behaviours of the system. In this tutorial, we will present basic results concerning timed automata and games, and we will further investigate the models of weighted timed automata and games. We will present in particular the important optimal reachability problem: given a target location, we want to compute the optimal (i.e. smallest) cost for reaching a target location, and a corresponding strategy. We will survey the main results that have been obtained on that problem, from the primary results of [3, 5, 16, 13, 8, 17, 7] to the most recent developments [11, 10]. We will also mention our new tool TiAMo, which can be downloaded at https://git.lsv.fr/colange/tiamo. We will finally show that weighted timed automata and games have applications beyond that of model- checking [12].

ABSTRACT. Joint work with Kobi Peterzil. We consider the group $\operatorname{SO}_3^{00}$ of infinitesimal rotations in the non-standard reals. We show that it is bi-interpretable with the valued field structure of the standard part map, and hence that the structure of definable sets in the group is as rich as possible.

ABSTRACT. Transseries such as LE series arise when dealing with certain asymptotic expansions of real analytic function. Most transseries, though, are not convergent, and cannot represent real analytic functions, if only just for cardinality reasons.

On the other hand, we can show that LE series do induce germs of non-standard analytic functions on the surreal line. More generally, call “omega-series” the surreal numbers that can be generated from the real numbers and the ordinal omega by closing under exponentiation, logarithm and infinite sum. Then omega-series form a proper class of transseries including LE series.

It turns out that all omega-series induce (germs of) surreal analytic functions. Moreover, they can be composed and differentiated in a way that is consistent with their interpretation as functions, extending the already known composition and derivation of LE series, and the derivation coincides with the simplest one on surreal numbers.

This is joint work with A. Berarducci.

ABSTRACT. NIP is a model-theoretic dividing line which was introduced in Shelah's classification theory programme. As with any combinatorial property, it is a natural question to ask whether it corresponds to some well-known algebraic notion when one considers the class of NIP fields. An open conjecture by Shelah states that every NIP field is either real closed or separably closed or `like the $p$-adic numbers'. In this talk, I will explain the conjecture and discuss some recent developments around it.

ABSTRACT. There is is a strong analogy between stationary sets and weakly compact sets. However, by a theorem of Kunen there are models in which non-weakly compact sets can become weakly compact after forcing, whereas nonstationary sets can never be forced to become stationary. Thus, proofs about the ideal of non-weakly compact sets often require a finer analysis than their counterparts for the nonstationary ideal. Many questions whose analogues have been answered for the nonstationary ideal remain open for the weakly compact ideal, and higher order $\Pi^1_n$-indescribability ideals. This talk will survey what is known in this area and will include a discussion of some recent results on the weakly compact reflection principle, which is a generalization of a certain stationary reflection principle. We say that the weakly compact reflection principle holds at $\kappa$ and write $\text{Refl}_{\text{wc}}(\kappa)$ if and only if $\kappa$ is a weakly compact cardinal and every weakly compact subset of $\kappa$ has a weakly compact proper initial segment. The weakly compact reflection principle at $\kappa$ implies that $\kappa$ is $\omega$-weakly compact, and in this talk we will discuss a proof that the converse of this statement can be false. Moreover, if $\kappa$ is $(\alpha+1)$-weakly compact where $\alpha<\kappa^+$ then there is a forcing extension in which there is a weakly compact set $W\subseteq\kappa$ having no weakly compact proper initial segment, the class of weakly compact cardinals is preserved and $\kappa$ remains $(\alpha+1)$-weakly compact.

ABSTRACT. Classically, many partition relations involving $\omega_1$ and countable ordinals were shown to fail from $\mathsf{CH}$. In joint work with Shimon Garti and Thilo Weinert, we prove that having certain cardinal characteristics equal to $\aleph_1$ causes the failure of partition relations such as $\omega_1\rightarrow (\omega_1,\omega+2)^2_2$ and $\omega_1^2\rightarrow (\omega_1\omega,4)^2_2$. Most often, we use the hypothesis $\mathfrak{d}=\aleph_1$, but this seems quite strong. In an effort to use weaker hypotheses, we consider how partition relations behave under the stick principle, and with certain values of invariants for category, evasion and prediction.

ABSTRACT. Analytic sets enjoy a classical representation theorem based on well-founded relations. I will explain a similar representation theorem for $\mathbf{\Sigma}^1_2$ sets due to Marcone (1993) which is based on an intriguing topological graph: the Shift Graph. The chromatic number of this graph is $2$, but its Borel chromatic number is infinite. We use this representation theorem to show that the Shift Graph is not minimal among the graphs of Borel functions which have infinite Borel chromatic number. While this answers negatively the primary outstanding question from (Kechris, Solecki and Todorcevic; 1999), our proof unfortunately does not construct any explicit example of a Borel function whose graph has infinite Borel chromatic number and admits no homomorphism from the Shift Graph.

ABSTRACT. Abstract: Few things can better illustrate the unity of mathematics than the homotopy interpretation of Martin-L\"of type theory (Awodey-Warren, Voevodsky) and the discovery of the univalence axiom (Voevodsky). {\it Homotopy Type Theory} is the new field of mathematics springing from these discoveries. The creation of the definitive formalism may not lie so far in the future. There are good evidences that Hott can contribute effectively to homotopy theory and to higher topos theory: non-trivial homotopy groups of spheres were computed by Brunerie and a new proof of a fundamental result of homotopy theory (the Blakers-Massey theorem) was found (and verified in Agda) by Favonia, Finster, Licata and Lumsdane. The theorem was generalised by Anel, Biedermann, Finster and the author, and applied to Goodwillie's calculus [arxiv/1703.09050/1703.09632]. The [ABFJ] papers are written in {\it creole}, a blend of category theory, type theory and infty-category theory, but a formal verification in Agda by Finster and Licata is on the way. It is clear that category theory serves as an intermediate between type theory and homotopy theory [CCHM/arxiv/1611.02108][ALV/arxiv/1705.04310][LS/arxiv/1705.07088]. The basic aspects of the theory of infty-categories were recently formalised in Hott by Riehl and Shulman. The syntaxic category of type theory happens to be a {\it path category} in the sense of Van den Berg. The notion of {\it tribe} introduced independantly by the author and Shulman is somewhat simpler, but not every path category is a tribe. However, every fibration category is equivalent (in the sense of Dwyer-Kan) to a tribe by a construction of Cisinski and by the work of Szumilo and of Kapulkin. I will sketch the homotopy theory of tribes and of {\it simplicial tribes}.

ABSTRACT. Engineers and scientists have reinvented an approximation of topos theory for their modeling languages. Modeling languages in the UML family have constructions for operations with multiple arguments (products), multivalued operations (powers), operations with operations are arguments (exponentials), as well as images of operations and subtypes. These languages are missing constructions which are needed for applications, and they do not have any accepted formal semantics. However, these languages, together with special purpose sublanguages are used to design complex systems and analyze their behavior in an operational setting. With a formal semantics a topos based modeling language can serve as the foundation for a new generation of modeling language tools which integrate automated reasoning with simulation.

Axiomatic topos theory as developed by Lawvere, including rule axioms for products and powers, goes a long way to providing an axiomatic modeling language suitable for science and engineering. Subobjects (subtypes) play an extensive role in system modeling. The topos subobject classification axiom is not very suitable for mechanization. Further, arbitrary set theoretic toposes are more general than is appropriate for modeling semantics. A generalized rule axiom is given as a replacement for subobject classification in the context of axiomatic Cartesian closed categories with powers. The resulting toposes have canonical subobjects.

By using an axiomatic topos formalism descriptive models as developed in engineering modeling languages can be embedded within axiom sets which generate toposes with canonical subobjects. The theory of a descriptive model can be represented where the types are sheaves defined on the spectrum of the terminal object and the maps are sheaf maps when the models have constructions for dynamics. The interpretations of these models are strict logical functors. A simulation is an interpretation. This provides a formal basis for simulation correctness.

ABSTRACT. The concept of names as studied in the theory of nominal sets has been proven useful in various parts of mathematical logic and computer science. A notable instance is the work presented in [1], which exposes cubical sets as nominal sets equipped with nominal restriction operations. As is well-known, this underlying name-dependending structure has been incorporated into subsequent formulations of cubical type theory.

Following a suggestion of Pitts, the author observed that there are many more examples of toposes, including simplicial sets, that admit a representation as categories of finitely supported M-sets, for a `monoid of substitutions' M, which is to be taken quite generally. We study these toposes as such and compare them using the theory of classifying toposes. Our findings feed back into this theory by allowing for a nominal presentation of syntactic categories that does not rely on alpha-equivalence. More examples show how this nominal viewpoint offers a useful paradigm for studying aspects of topos theory. Potential applications include not only the semantics of names in type theory, but also categorical formulations of models of intuitionistic set theory.

ABSTRACT. See pdf-file.

ABSTRACT. Makkai's reconstruction result allows to recover a first-order theory, up to pretopos completion, from its category of models by equipping it with appropriate structure and considering set-valued functors preserving this structure. One of the difficulties in extending this result to the infinitary case is that the Keisler-Shelah isomorphism theorem, which asserts that elementarily equivalent models have isomorphic ultrapowers, does not hold for infinitary logic. However, we will see that the theory of accessible categories can provide extra structure, under appropriate large cardinal assumptions, to recover the theory from its category of models up to a notion of infinitary pretopos-completion. More precisely, the plan of Makkai of endowing the categories of models with extra structure coming from ultraproducts can be readily generalized to the infinitary case in the presence of a compact cardinal, by means of which an infinitary version of Los theorem is possible. Makkai's use of Keisler-Shelah theorem allows him to regulate the behaviour of subfunctors of set-valued functors from the category of models, while the use of Vopenka's principle in our case, in the form "every subfunctor of an accessible functor is accessible" will provide the desired effect. For the reconstruction result, one more large cardinal axiom needs to be assumed, namely that the class of ordinals Ord is weakly compact. With these assumptions, a duality theory arises for the infinitary case that generalizes the one exposed by Makkai.

ABSTRACT. Recent work in abstract model theory (see [2], [3], and [4]) has highlighted the highly desirable properties of abstract classes under large cardinals axioms, chiefly the assumption of a proper class of strongly (or almost strongly) compact cardinals. There are parallel results for accessible categories (see [5] and [6]), in addition to earlier work of [1] concerning Vopenka's Principle. We here consider the other end of the spectrum: pathological behavior of accessible categories assuming that there is only a set of measurable cardinals or, indeed, that V=L. The pathological examples, which are built directly out of the cumulative set-theoretic hierarchies, include the non-co-well-powered accessible category considered in [1] and [7], as well as an example tucked away in [8], which we have newly adapted to this context.

[1] J. Adamek and J. Rosicky, Locally presentable and accessible categories. LMS Lecture Note Series 189, Cambridge UP, 1994. [2] J. Baldwin and W. Boney, Hanf numbers and presentation theorems in AECs, to appear in Beyond First Order Model Theory (J. Iovino, editor), CRC Press, 2017. [3] W. Boney, Tameness from large cardinal axioms, Journal of Symbolic Logic, vol.163 (2012), pp. 2008–2017. [4] W. Boney and S. Unger, Large cardinal axioms from tameness in AECs, to appear in Proceedings of the American Mathematical Society. [5] M. Lieberman and J. Rosicky ́, Classification theory for accessible categories, Journal of Symbolic Logic, vol. 81 (2016), no. 1, pp. 151–165. [6] --------, Hanf numbers via accessible images, arXiv:1610.07816v4. [7] M. Makkai and R. Pare, Accessible Categories: The Foundations of Cat- egorical Model Theory, Contemporary Mathematics 104, AMS, 1989. [8] S. Shelah, Model theory for a compact cardinal. arXiv:1303.5247v3.

ABSTRACT. In this paper I want to show that the traditional characterization of the notion of paradox —an apparently valid argument with apparently true premises and an apparently false conclusion— is too narrow; there are paradoxes that do not satisfy it. After discussing and discarding some alternatives, a paradox is found to be an argument that seems valid —in the sense that rejecting its validity would imply giving up some core intuitions about the notion of logical consequence— but such that the commitment to the conclusion that stems from the acceptance of the premises and the validity of the argument should not be there. Something even stronger can be said to be the case: apparently, there is no commitment at all. In the last sections, some consequences and some objections are discussed.

ABSTRACT. We focus on the problem of constructing of some standard Hilbert style proof systems for any version of many valued propositional logic. The generalization of Kalmar’s proof of deducibility for two valued tautologies inside classical propositional logic gives us a possibility to suggest for any version of 3-valued logic some method for defining of two types axiomatic systems, completeness of which is easy proved directly, without of loading into two valued logic. This method i) can be base for direct proving of completeness for all well-known axiomatic systems of k-valued (k≥3) logics and may be for fuzzy logic also, ii) can be base for constructing of new Hilbert-style axiomatic systems for all mentioned logics.

ABSTRACT. A monotonic function on a set S is a ⊆-preserving mapping on 2^S, that is, a function C such that C(A) ⊆ C(A∪B), for every A,B ⊆ S.  Tarski's fixpoint theorem guarantees the existence of the least and of the greatest fixpoints for monotonic functions.  The latter have a variety of applications, in particular in providing a foundation for inductive and co-inductive definitions, and the proof methods associated therewith.  A Tarskian closure operator on S is a monotonic function on S that is also inflationary (i.e. A ⊆ C(A)) and idempotent (i.e. C(C(A)) = C(A)); it is a generalization of the notion of topological closure, axiomatized by Kuratowski.  A closure operator on S is called structural when it commutes with endomorphisms on S.  (Structural) Tarskian closure operators are known [3] to be characterizable by a family of so-called logical matrices, viz. structures containing sets of 'algebraic' truth-values, some of which are distinguished.  Their inflationary and idempotent character also guarantees that they may be characterized by (at most) two 'logical' values (cf. Chap. 4 of [4]).  In the present contribution we will show how a generalized notion of closure and a two-dimensional notion of logical matrix (resp. B-closure and B-matrix) may be used to characterize any given monotonic function on a set S, recovering a theme earlier explored at [2] in the context of symmetrical consequence relations involving two potentially distinct languages.  We will also show that any B-matrix may be alternatively characterized by (at most) four logical values [1].  A brief discussion of inferential many-valuedness and its connections with bilattice-based reasoning, from a metalogical perspective, will ensue.

[1] Carolina Blasio and João Marcos and Heinrich Wansing, An inferentially many-valued two-dimensional notion of entailment, to appear in the Bulletin of the Section of Logic, 2017.
[2] Lloyd Humberstone, Heterogeneous logic, Erkenntnis, vol. 29 (1988), pp. 395-435.
[3] Ryszard Wójcicki, Some remarks on the consequence operation in sentential logics, Fundamenta Mathematicae, vol. 68 (1970), pp. 269-279.
[4]Grzegorz Malinowski, Many-Valued Logics, Oxford, 1993.

ABSTRACT. Belnap-Dunn type bivalent semantics is the semantics originally defined for interpreting Anderson and Belnap's ``First Degree Entailment Logic'' (cf. [1] and references therein). On the other hand, the notion of a ``natural implication'' is understood as it is defined in [2]. According to this notion, there are exactly 24 natural implicative expansions of Kleene's strong three-valued matrix with 1 and 1/2 as designated values. Some of these expansions characterize interesting logics such as paraconsistent expansions of the three-valued extensions of the positive fragments of Lewis' S5 and three-valued G\"{o}del logic G3.

The aim of this paper is to define a Belnap-Dunn type bivalent semantics for the logics determined by each one of these 24 implicative expansions.

ABSTRACT. Routley-Meyer semantics, originally introduced for interpreting relevance logic, is a highly malleable semantics capable of modelling families of non-classical logics very different from each other. Let us now understand the notion of a ``natural implication'' following [2]. Then, there are exactly six natural implicative expansions of Kleene's strong three-valued matrix with 1 as the sole designated value.

The aim of this paper is to endow each one of the logics characterized by these six expansions with a Routley-Meyer type ternary relational semantics. There are well-known logics among those determined by these six expansions. \L ukasiewicz three-valued logic \L 3 is an example.

ABSTRACT. The study of the algebraic semantics of Łukasiewicz logic, also known as MV-algebras, has shown deep connections with piece-wise linear geometry: finite theories correspond to rational polyhedra and formulas correspond to piece-wise linear functions with integer coefficients. The Diophantine restriction on the coefficients gives rise to complex and interesting phenomena. This talk is about an extension of Łukasiewicz logic by scalars taking values in the unit interval of any ring A such that Z< A< R. The main results are a completeness theorem in the style of C. C. Chang and a characterisation in the style of R. McNaughton of the formulas in this logic. Together, these results leads to a geometric interpretation of this logic similar to the aforementioned one, but where the coefficients are bound to take values in A, rather than in Z.

ABSTRACT. Okada and Takemura (\cite{ot}) introduced phase semantics for $\lambda$-terms of Laird's dual affine/intuitionistic $\lambda$-calculus, whose types are composed from intuitionistic implication $\to$, linear implication $\multimap$ and linear additive product $\&$. The validity in this semantics has several key features of the validity in proof-theoretic semantics (PTS), which was introduced by Prawitz (\cite{pr}) and analyzed by Schroeder-Heister (\cite{sch}), so one can provide Okada-Takemura's semantics with a PTS-style foundation. This poses the following question: Can one supply Okada-Takemura's semantics with an interpretation of disjunction, keeping the connection to PTS?

First, we introduce a Okada-Takemura-style semantics for the term-calculus $\mathsf{M}_{\to \land \lor}$ of minimal propositional logic with the connectives $\to ,\land$ and $\lor$. Our interpretation of disjunction $\lor$ is inspired by Sandqvist's (\cite{san}) and keeps the connection to PTS. Next, we prove the completeness of $\mathsf{M}_{\to \land \lor}$ in the following sense: Every valid term in our semantics is typable. Finally, we note that strong normalization of $\mathsf{M}_{\to \land \lor}$ follows from our proof for its completeness.

This is a joint work with Ryo Takemura. The author is supported by KAKENHI (Grant-in-Aid for JSPS Fellows) 16J04925.

ABSTRACT. We say that a formula $\tau(v)$ is a numeration of a theory $T$ if $\{n \in \omega : {\sf PA} \vdash \tau(\overline{n})\}$ is exactly the set of all G\"odel numbers of the axioms of $T$. For each numeration $\tau(v)$ of $T$, the provability predicate ${\sf Pr}_\tau(x)$ of $T$ is naturally constructed. An arithmetical interpretation $f$ is a mapping from the set of all propositional variables to the set of sentences of arithmetic. Each arithmetical interpretation $f$ is uniquely extended to the mapping $f_\tau$ from the set of all modal formulas to the set of sentences of arithmetic so that $f_\tau$ commutes with every propositional connective, and $f_\tau(\Box A)$ is ${\sf Pr}_\tau(\ulcorner f_\tau(A) \urcorner)$. The provability logic ${\sf PL}_\tau(U)$ of $\tau(v)$ relative to a theory $U$ is the set $\{A : U \vdash f_\tau(A)$ for all arithmetical interpretations $f\}$ of modal formulas (see \cite{AB,BE}).

We proved the following two theorems.

Theorem 1 Let $U$ be any recursively axiomatized consistent extension of ${\sf PA}$. If ${\sf L}$ is one of the logics ${\sf GL}_\alpha$, ${\sf D}_\beta$, ${\sf S}_\beta$ and ${\sf GL}_\beta^-$ where $\alpha \subseteq \omega$ is recursively enumerable and $\beta \subseteq \omega$ is cofinite, then there exists a $\Sigma_1$ numeration $\tau(v)$ of some extension of $I\Sigma_1$ such that ${\sf PL}_\tau(U)$ is exactly ${\sf L}$.

Theorem 2 Let $T$ be any recursively axiomatized consistent extension of ${\sf PA}$. If ${\sf L}$ is one of the logics ${\sf K}$ and ${\sf K} + \Box(\Box^n p \to p) \to \Box p$ ($n \geq 1$), then there exists a $\Sigma_2$ numeration $\tau(v)$ of $T$ such that ${\sf PL}_\tau(T)$ is exactly ${\sf L}$.

The logics ${\sf K} + \Box(\Box^n p \to p) \to \Box p$ ($n \geq 1$) were introduced by Sacchetti \cite{SA}.

ABSTRACT. Proof mining is a research program introduced by U. Kohlenbach in the 1990s, which aims to obtain explicit quantitative information (witnesses and bounds) from proofs of an apparently ineffective nature. This offshoot of interpretative proof theory 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.

For the first time, this paradigm is applied to the field of convex optimization. We focus our efforts on one of its central results, the proximal point algorithm. This algorithm, or more properly said this class of algorithms, consists, roughly, of an iterative procedure that converges (weakly or strongly) to a fixed point of a mapping, a zero of a maximally monotone operator or a minimizer of a convex function. Similarly to other cases previously considered in nonlinear analysis, we may obtain rates of metastability or rates of asymptotic regularity. What is interesting here, however, is that for a relevant subclass of inputs to the algorithm -- ``uniform'' ones, like uniformly convex functions or uniformly monotone operators -- we may obtain an effective rate of convergence. The notion of convergence, being represented by a Pi_3-sentence, has been usually excluded from the prospect of being quantitatively tractable, unless its proof exhibits a significant isolation of the use of reductio ad absurdum. Here, however, a peculiarity of the input, namely its uniformity, translates into a logical form that makes possible this sort of extraction.

These results are joint work with Laurentiu Leustean and Adriana Nicolae.

ABSTRACT. Local operators (also known as Lawvere-Tierney topologies in the context of topos theory, or modal operators in other categorial contexts) have been useful in proving independence results in categorial set theory and more recently in providing categorial interpretations for quantum predicates. Our aim here is to use local operators and their duals to highlight a neglected feature of the usual logical connectives, namely their modal character. Disjunction and conditional have already been recognized as species of possibility; our contribution is the use of dual local operators to show that conjunction and subtraction are species of necessity. More exactly, disjunction is a possibility connective, conditional is a contingency connective, conjunction is a necessity connective and subtraction is an impossibility connective. The modal characters of unary and zero-ary connectives are also discussed.

ABSTRACT. \documentclass[bsl,meeting]{asl} \AbstractsOn \pagestyle{plain} \def\urladdr#1{\endgraf\noindent{\it URL Address}: {\tt #1}.} \newcommand{\NP}{} %\usepackage{verbatim} \begin{document} \thispagestyle{empty} \NP \absauth{Dariusz Surowik} \meettitle{Intuitionistic tense logic. Some remarks} \affil{Department of Logic, Informatics and Philosophy of Science, University of Bia{\l}ystok, Plac Uniwersytecki 1, 15-403, Bia{\l}ystok, Poland} \meetemail{surowik@uwb.edu.pl}

\par In the talk we would like to consider some system of intuitionistic tense logic. We will propose an axiomatization and Kripke-style semantics for this system. The crucial difference between Kripke’s models for intuitionistic tense logic and Kripke models for tense logic constructed over classical propositional logic is in the fact that in the case of tense logic constructed over classical propositional logic the relation R is used only to interpret tense operators; for intuitionistic logic, this relation is used not only to interpret tense operators but also to interpret intuitionistic connectives: negation and implication. We will show the basic properties and compare it to other intuitionistic tense logic systems.

\end{document}

ABSTRACT. \documentclass[bsl,meeting]{asl}
\AbstractsOn
\pagestyle{plain}
\def\urladdr#1{\endgraf\noindent{\it URL Address}: {\tt #1}.}
\newcommand{\NP}{}
%\usepackage{verbatim}
\begin{document}
\thispagestyle{empty}
\NP  
\absauth{Joachim Mueller-Theys}
\meettitle{On the Provability of Consistency}
\affil{Kurpfalzstr. 53, 69\,226 Nu{\ss}loch bei Heidelberg, Germany}
\meetemail{mueller-theys@gmx.de}
\smallskip

\noindent
A {\it consistency sentence}
${\rm Con} _\Sigma ^\sigma$
$:=$
$\neg {\rm Prov} _\Sigma ( \ulcorner \sigma \urcorner )$
states
in the standard model that
the decidable system
$\Sigma$
is consistent,
viz.
$\mathcal N \models {\rm Con} _\Sigma ^\sigma$
iff
$\Sigma \not\vdash \bot$.
We showed at
\cite{1}
that this is the case
if
$\Sigma \vdash \neg \sigma$
or
$\Sigma \not\vdash \sigma$.
So G\"odel's
${\rm Con} _\Sigma$
is a consistency sentence indeed.
By L\"ob's Theorem,
$\Sigma
\not\vdash
{\rm Con} _\Sigma ^\bot$
if
$\Sigma \vdash {\rm PA}$
is consistent.

We have recently found
an alternative consistency sentence,
the unprovability of which
can be shown much more easily
and
already for consistent
$\Sigma \vdash {\rm Q}$.
The proof exploits
that
the provability predicate
does {\it not} negatively represent
$\Sigma$
in itself,
viz. there are
$\sigma _{\rm B}$
such that
$\Sigma \not\vdash \sigma _{\rm B}$,
but  
$non
\
\Sigma \vdash
\neg {\rm Prov} _\Sigma
( \ulcorner \sigma _{\rm B} \urcorner )$,
whence
${\rm Con} _\Sigma '$
$:=$
${\rm Con} _\Sigma ^{\sigma _{\rm B}}$
already does the job.
\cite{1}

Specifying a remark of Evgeny I. Gordon during LC '15,
such {\it negative} consistency sentences
do not show
the unprovability of consistency {\it in general};
they only show
the unprovability of consistency {\it by them.}
Accordingly,
there might be {\it positive} consistency sentences,
which would---by the analogous argument---prove the consistency of
$\Sigma$
in
$\Sigma$.  
If
$\Sigma \not\vdash \sigma$
and
$\Sigma
\vdash
\neg  
{\rm Prov} _\Sigma
( \ulcorner \sigma \urcorner )$,
${\rm Con} _\Sigma ^\sigma$
is a positive consistency sentence;
and
{\it total} negative self-irrepresentability
seems to be unnatural and unlikely.

In search for suchlike sentences,
we realised that
$\Sigma \not\vdash {\rm Con} _\Sigma ^\sigma$
for all
$\Sigma \vdash \neg \sigma$,
and,
subsequently,
that the required
$\Sigma \not\vdash {\rm Con} _\Sigma ^\bot$
implies
$\Sigma \not\vdash {\rm Con} _\Sigma ^\sigma$
can be proven without any precondition on
$\sigma$.
This has the incredible consequence that
$\Sigma \not\vdash
\neg {\rm Prov} _\Sigma ( \ulcorner \sigma \urcorner ) $
{\it for all}
$\sigma$.
In particular,
all consistency sentences are negative.
It follows either that
there is {\it no}
${\rm Con} _\Sigma ^\sigma$
stating
in the theory of
$\Sigma$
that
$\Sigma$
is consistent.

Note.
We obtained the theorem
first
in a more complicated and less general way by
$\neg \Box p \not\in {\bf GL}$
(which we had gained from a lemma for \cite{2})
and
Solovay's Theorem.

\begin{thebibliography}{10}

\bibitem{1}
{\scshape Mueller-Theys, J.},
{\itshape Defining \& simplifying
G\"odel's 2$^{\it nd}$ Incompleteness Theorem},
{\bfseries\itshape ASL 2017 Spring Meeting} (Seattle).

\bibitem{2}
\bysame ,
{\itshape On Uniform Substitution},
{\bfseries\itshape The Bulletin of Symbolic Logic},
vol.~20 (2014), pp.~264--5.

\end{thebibliography}
\vspace*{-0.5\baselineskip}

\end{document}

ABSTRACT. Semantic formalizations of epistemic situations as Kripke models produce complete descriptions: for each sentence F, they specify which of F or ~F holds. This renders semantic formalizations inadequate for incomplete scenarios. To represent all epistemic situations, complete and incomplete, we need epistemic theories, i.e., sets of epistemic formulas ([1]), analogous to mathematical theories, many/most of which are incomplete (group theory, Peano Arithmetic, etc.).

We consider epistemic theories of card dealing and establish their completeness. One should not expect epistemic completeness to be maintained throughout the game: players could use private communications to learn facts which do not follow from the game description. For such situations, epistemic theories become essential.

Assume a deck of cards dealt to n players. Consider epistemic logic S5_n with atomic propositions `player i is dealt card j’. For a given property P, let <P> denote its representation by a formula. Let H be set of formulas 
   H = S5_n + <rules of dealing> + <each player knows her hand and deems possible any dealing consistent with it>. 
For each combination d of cards dealt, define theory
   H_d = <common knowledge of H> + <d>.  
The standard model of card dealing (cf. [2]) has all possible dealings as worlds, indistinguishability as accessibility relations, and the natural evaluation of atomic propositions.
   Completeness Theorem: H_d proves F iff  F is true at world d in the standard model. 
   Corollary: Theory H_d of card dealing is complete for each combination of cards dealt.

Bibliography

[1] S.Artemov, Syntactic Epistemic Logic,  Book of abstracts. 15th Congress of Logic, Methodology and Philosophy of Science, University of Helsinki, 2015, pp. 109-110.

[2] R.Fagin, J.Halpern, Reasoning about knowledge, MIT Press, 1995.

ABSTRACT. In my talk I will define limitwise monotonic reducibility between sequences of sets via of Sigma-reducibility on the families of initial segments. Also I will consider the description of the limitwise monotonic reducibility between sequences of sets on the language of Sigma-definability of abelian groups.

ABSTRACT. There is well-known result, that for any natural $m>n+1$ nontrivial Rogers semilattices from level $\Sigma^0_{m}$ are nonisomorphic to Rogers semilattices from level $\Sigma^0_{n}$. It is still an open question, whether it is possible to remove this gap between levels. Here we concentrate our interest in similar properties for analytical hierarchy.

ABSTRACT. In order to prove his famous incompleteness theorems Gödel have developed a formalization of the notions of formal language and provability in arithmetical terms. Latter it were established that instead of using Gödel’s explicit formalization of the notion of provability one could use any “reasonable formalization” (predicates that satisfy Hilbert-Bernays-Löb derivability conditions). Essentially, we propose similar “axiomatic” replacement for Gödel numbering. For a given theory T, its first-order language is usually given by an inductive definition, we introduce a theory Syn(T) that gives a “natural” formalization of the language that reflects its inductive definition. We prove Diagonal Lemma for any T that interprets Syn(T). And thus we establish Gödel’s second incompleteness theorem for this T with respect to any predicate that satisfy Hilbert-Bernays-Löb derivability conditions. Our approach is applicable to some theories that are less expressive than the usual arithmetical theories that could represent all computable functions. In particular, our version of Diagonal Lemma holds for the complete and decidable elementary theory Th(N, C) of natural numbers with Cantor pairing function, C(n, m) = (n + m)(n + m + 1)/2 + m. This work is supported by the Russian Science Foundation under grant 16-11-10252.

ABSTRACT. Backwards proof search and theorem proving with a standard cut-free calculus for the propositional fragment of minimal logic is insufficient because of three problems. Firstly, the proof search is not in general terminating caused by the possibility of looping. Secondly, it might generate proofs which are permutations of each other and represent the same natural deduction. Finally, during the proof some choice should be made to decide which rules to apply and where to use them. Several proof systems of I.Johansson's minimal logic of predicates were introduced in [1]. Looping is the main issue in the propositional fragment of the system GM^- developed in [1]. Looping may easily be removed by checking if a sequent has already occurred in the branch. Though this is insufficient as it requires much information to be stored. Some looping mechanisms have been considered earlier in [2,3]. One way to detect loops is adding history to each sequent. We introduce two systems for propositional fragment of minimal logic (SwMin and ScMin) which are slightly different. Both systems are based on the idea of adding context to the sequents. In one system, SwMin, the history is kept smaller, but ScMin detects loops more quickly. The heart of the difference between the two systems is that in the SwMin loop checking is done when a formula leaves the goal, whereas in the ScMin it is done when it becomes the goal. 

Theorems

1. The systems GM^- and SwMin are equivalent. 

2. The systems GM^- and ScMin are equivalent

ABSTRACT. The goal of my paper is to present a formal semantics that deals with some peculiar phenomena that have been rather neglected in logical literature. In particular, these phenomena concern the surprising fact that on the level of natural language, logical connectives seem to be sensitive to the syntactic structure of the sentences they connect. One consequence of this fact is the failure of two basic principles that are respected by most logical theories: Uniform Substitution and Replacement of Equivalents. For an illustration, let us consider a counterexample to the second principle. We regard the following two sentences as equivalent in the sense that they are mutually inferable (even though they might differ in pragmatic implicatures):

(1) If A is not the murderer, then B is. (2) A or B is the murderer.

However, the first from the following two arguments seems to be valid but the second, which is obtained by replacement of equivalents, not:

(1) It is not the case that A or B is the murderer. Therefore, neither A nor B is the murderer. (2) It is not the case that if A is not the murderer then B is. Therefore, neither A nor B is the murderer.

To see that (2) is not valid, consider the situation in which A is among the suspects but B is not.

In the talk, we will provide a precise formal semantics and a corresponding deductive calculus that deals with these kinds of phenomena.

ABSTRACT. In this work, our purpose is to analyze the Peterson's Intermediate Syllogisms by means of Caroll's diagrammatic method. For this aim, we firstly construct a formal system PISLCD (Peterson's Intermediate Syllogistic Logic with Caroll Diagrams), which gives us a formal approach to logical reasoning with diagrams, for representations of the fundamental Intermediate propositions and show that they are closed under the intermediate 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 specic knowledge or exclusive ability is needed in order to understand it and use it. In other respects, we examine algebraic properties of Peterson's intermediate syllogisms in PISLCD. 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 Peterson's intermediate syllogistic system consists of 4000 syllogistic moods. 105 of them are valid forms. Finally, we show that any intermediate syllogism is valid if and only if it is provable in PISLCD. This means that PISLCD is sound and complete.

ABSTRACT. Reasoning about autonomous agents' informational attitudes, such as knowledge and belief, has been a long-standing area in the research of AI and intelligent agents~\cite{fag,mey1}. The typical perception-action cycle for intelligent agents assumes that an agent forms her beliefs about the environment and acts or makes decisions in accordance with such belief and her preference. Hence, reasoning about belief and knowledge plays a central role in the operational process of agent systems. In the multi-agent environment, an agent generally forms her beliefs by receiving information from different sources. Therefore, it is crucially important to keep track of the information sources and the derivation process that can be regarded as justifications of the agent's belief. However, belief formation from perceptions is actually a dynamic process. In recent years, modeling the dynamic change of belief has been extensively studied in the dynamic epistemic logic (DEL) paradigm with a lot of applications to AI, computer science, multi-agent systems, philosophy, and cognitive science ~\cite{Benthem2,del}. In this paper, we present a logic for reasoning about evidence and belief. Our framework not only takes advantage of the source-tracking capability of justification logic~\cite{art08}, but also allows the distinction between the actual observation and simply potential admissibility of evidence. We present the axiomatization for the basic logic and its dynamic extension, and investigate its properties and applications.

ABSTRACT. One of the virtues of Voevodsky's celebrated univalence axiom is that it offers a formal justification for the common practice among mathematicians of identifying objects just in case they are isomorphic. Since in general there may be different isomorphisms between any two objects, it follows that a thing can be recognized as the same again in more than one way. Equipped with this axiom and other powerful features, homotopy type theory (The Univalent Foundations Program 2013) provides a novel notion of equality with a subtle structure that takes account of the different reasons a thing can be the same.

Over one hundred years ago, Frege (1982) drew attention to a puzzle concerning the slippery and multifaceted nature of equality. In a sense, he also arrived at the conclusion that there should be different ways for two objects to be identified --- and he explained this by saying that two objects expressing a different sense denote the same referent. Now, a natural question is ``can the homotopy-type theoretic notion of equality shed new light on Frege's puzzle?"

In this work-in-progress talk, I shall propose a constructive solution for Frege's puzzle based on elementary insights from homotopy type theory. I claim that, from the viewpoint of constructive semantics, Frege's solution is unable to explain adequately the informative content of identity statements, since, as I shall argue, not only identity statements of the form "a=b", but also "a=a" may contribute to extensions of our knowledge. More precisely, I hold that my approach can be seen as an extension of Frege's ideas to account for constructive reasoning.

ABSTRACT. It is commonly accepted that G. Frege announced his logicist project in Begriffsschrift. Disregarding what he achieved in this work, almost all historical studies agree that Frege formulated his goal of justifying that arithmetic is not an autonomous theory, but it is based on logic alone. The formal system developed in Begriffsschrift, the concept-script, is thus seen as the first step to realise Frege's logicist program.

I put forward a new interpretation of Frege's use of Begriffsschrift concept-script and argue that, according to this use, it is incorrect to claim that he outlined a logicist program in 1879. Two main argumental lines support this claim. First, I show that in 1880-1882 Frege presented the concept-script of Begriffsschrift as a tool for arithmetic, and not as a logical theory from which to deduce arithmetical theorems. Arithmetic was presented as an independent theory, with a specific domain of entities. In fact, Frege meant to apply the formal resources of this formal system - in particular, its theory of quantification - to express the logical relations that bind the atomic formulas of arithmetic together. He thus did not want either to replace the proper symbols of arithmetic with logical ones or to modify the interpretation of the letters used in arithmetical expressions; arithmetic provided the semantic content which was related by means of the concept-script. Second, I consider Frege's results in Begriffsschrift and conclude that they are incompatible with his later logicist program.

Frege might have had intuitions concerning the logical nature of arithmetical truths in 1879. However, he did not articulate them. Besides, I conclude that he could not defend them as a programmatic goal without contradicting key features of his factual use of the concept-script.

ABSTRACT. We introduce several versions of game-theoretic semantics (GTS) for the Alternating-Time Temporal Logic (ATL) and for its extension ATL+. In GTS, truth is defined in terms of existence of a winning strategy in a semantic evaluation game, and thus the game-theoretic perspective appears in the framework of ATL on two semantic levels: on the object level, in the standard semantics of the strategic operators, and on the meta-level, where game-theoretic logical semantics can be applied to ATL. We unify these two perspectives into semantic evaluation games specially designed for ATL. That game-theoretic perspective enables us to identify new variants of the semantics of ATL, based on limiting the time resources available to the verifier and falsifier in the semantic evaluation game; we introduce and analyse an unbounded GTS and prove it to be equivalent to the standard (Tarski-style) compositional semantics. We also introduce a non-equivalent finitely bounded semantics and argue that it is quite natural from both logical and game-theoretic perspectives. We also apply the GTS for ATL+ to identify a hierarchy of extensions of ATL with tractable model checking.

ABSTRACT. I want to find an account of plurality of logics which exploits both the monist and the pluralist intuitions. I present logical dynamism, which, based on Brandomian inferentialism and logical expressivism asserts that there is one common logic, which nevertheless can develop in many ways indicated by the many logical systems which have been devised.

ABSTRACT. Two “Styles” of axiomatization: Rules versus Axioms. A Modern Perspective.

In a Hilbert-style non-logical axiomatic theory the semantics of logical symbols is rigidly fixed, while the semantics of non-logical symbols vary giving rise to different models of a given theory. All non-logical content of such a theory is comprised in its non-logical axioms (e.g. axioms of ZF) while rules, which generate from these axioms new theorems, belong to the logical part of the theory (aka “underlying logic”).

An alternative approach to axiomatization due to Gentzen amounts to a presentation of formal calculi in the form of systems of rules without axioms. Gentzen did not try to extend his approach to non-logical theories by considering specific non-logical rules as a replacement for non-logical axioms. However the more recent work in Univalent Foundations of Mathematics suggests that the Gentzen-style rule-based approach to formal presentation of theories may have important applications also outside the pure logic.

A reason why one may prefer a rule-based formal representation is that it is more computer-friendly. This, in particular, motivates the recent work on the “constructive justification” of the Univalence Axiom via the introduction of new operations on types and contexts ?? . However this pragmatic argument does not meet the related epistemological worries. What kind of knowledge may represent a theory having the form of a bare system of rules ? Is such a form of a theory appropriate for representing a knowledge of objective human-independent reality? How exactly truth features in rule-based non-logical theories?

Using HoTT as a motivating example I provide some answers to these questions and show that the Gentzen-style rule-based approach provides a viable alternative to the standard axiomatic approach not only in logic but also in science more generally.

ABSTRACT. See PDF

ABSTRACT. %% FIRST RENAME THIS FILE .tex. %% BEFORE COMPLETING THIS TEMPLATE, SEE THE "READ ME" SECTION %% BELOW FOR INSTRUCTIONS. %% TO PROCESS THIS FILE YOU WILL NEED TO DOWNLOAD asl.cls from %% http://aslonline.org/abstractresources.html.

\documentclass[bsl,meeting]{asl}

\AbstractsOn

\pagestyle{plain}

\def\urladdr#1{\endgraf\noindent{\it URL Address}: {\tt #1}.}

\newcommand{\NP}{} %\usepackage{verbatim}

\begin{document} \thispagestyle{empty}

%% BEGIN INSERTING YOUR ABSTRACT DIRECTLY BELOW; %% SEE INSTRUCTIONS (1), (2), (3), and (4) FOR PROPER FORMATS

\NP \absauth{Juan Carlos Mart\'{\i}nez} \meettitle{On pcf spaces which are not Fr\'echet-Urysohn} \affil{Faculty of Mathematics, University of Barcelona, 08007 Barcelona, Spain} \meetemail{jcmartinez@ub.edu}

%% INSERT TEXT OF ABSTRACT DIRECTLY BELOW

An {\em admissible poset} is a triple $\langle T, \prec, i\rangle$ such that $T$ is a non-empty set, $\prec$ is a well-founded ordering on $T$ and $i : [T]^2 \rightarrow [T]^{<\omega }$ satisfying the following two properties:

(1) For all $u,s,t\in T$, $u \preceq s$ and $u \preceq t$ iff $u \preceq v$ for some $v\in i\{s,t\}$.

(2) For all $t\in T$ and all $\alpha$ less than the $\prec$-rank of $t$, $\{s \in T : s\prec t \} \cap \{s\in T : \mbox{rank}(s) = \alpha \}$ is infinite.

An admissible poset $\langle T, \prec, i \rangle$ has associated with it a locally compact, Hausdorff and scattered space $X$ of underlying set $T$ whose basic open sets are of the form $b_t \setminus (b_{u_0}\cup\dots \cup b_{u_n})$, where $b_t = \{s\in T : s \preceq t \}$ for each $t\in T$. If $Y$ is a subset of $T$, $\overline{Y}$ denotes the closure of $Y$ in $X$.

A {\em pcf structure} is an admissible poset $\langle \theta + 1,\prec, i \rangle$ where $\theta$ is an infinite ordinal such that the following conditions are satisfied:

\vspace{2mm} (PCF1) \hspace{3.7mm} If $\nu \prec \mu$ then $\nu \in \mu$.

\vspace{2mm} (PCF2) \hspace{3.7mm} $\overline{\omega} = \theta + 1$.

\vspace{2mm} (PCF3)\hspace{3.7mm} If $I \subseteq \theta + 1$ is an interval, then $\overline{I}$ is also an interval.

\vspace{2mm} (PCF4) \hspace{3.7mm} $\xi \prec \theta$ for every $\xi \in \theta$.

\vspace{2mm} (PCF5) \hspace{3.7mm} For each $\nu \in \theta$ of uncountable cofinality there is a club $C_{\nu}$ of $\nu$ such that \hspace*{19.5mm} $\overline{C_{\nu}}\subseteq \nu + 1$.

The compact, Hausdorff, scattered space $X$ associated with a pcf structure is called a {\em pcf space}, whose {\em height} is defined as the least ordinal $\alpha$ such that the $\alpha$th Cantor-Bendixson level of $X$ is empty. In \cite{pe}, it was shown by means of a forcing argument that if CH holds then there is a pcf space of height $\omega_1 + 1$ which is not Fr\'echet-Urysohn, answering in a partial way a question posed by Todorcevic. Then, we will give here a simpler proof of Pereira's theorem by means of a forcing-free argument and we will extend his result to pcf spaces of any height $\delta + 1$ where $\delta < \omega_2$ with $\mbox{cf}(\delta) = \omega_1$.

\begin{thebibliography}{10}

\bibitem{pe} {\scshape L. Pereira}, {\itshape Applications of the topological representation of the pcf-structure}, {\bfseries\itshape Archive for Mathematical Logic}, vol.~47 (2008), no.~5, pp.~517--527.

%% INSERT YOUR BIBLIOGRAPHIC ENTRIES HERE; %% SEE (4) BELOW FOR PROPER FORMAT. %% EACH ENTRY MUST BEGIN WITH \bibitem{citation key} %% %% IF THERE ARE NO ENTRIES %% DELETE THE LINE ABOVE (\begin{thebibliography}{20}) %% AND THE LINE BELOW (\end{thebibliography})

\end{thebibliography}

\vspace*{-0.5\baselineskip} % this space adjustment is usually necessary after a bibliography

\end{document}

%% READ ME %% READ ME %% READ ME

INSTRUCTIONS FOR SUPPLYING INFORMATION IN THE CORRECT FORMAT:

1. Author names are listed as First Last, First Last, and First Last.

\absauth{FirstName1 LastName1, FirstName2 LastName2, and FirstName3 LastName3}

2. Titles of abstracts have ONLY the first letter capitalized, except for Proper Nouns.

\meettitle{Title of abstract with initial capital letter only, except for Proper Nouns}

3. Affiliations and email addresses for authors of abstracts are listed separately.

% First author's affiliation \affil{Department, University, Street Address, Country} \meetemail{First author's email} %%% NOTE: email required for at least one author \urladdr{OPTIONAL} % % Second author's affiliation \affil{Department, University, Street Address, Country} \meetemail{Second author's email} \urladdr{OPTIONAL} % % Third author's affiliation \affil{Department, University, Street Address, Country} % Second author's email \meetemail{Third author's email} \urladdr{OPTIONAL}

4. Bibliographic Entries

%%%% IF references are submitted with abstract, %%%% please use the following formats

%%% For a Journal article \bibitem{cite1} {\scshape Author's Name}, {\itshape Title of article}, {\bfseries\itshape Journal name spelled out, no abbreviations}, vol.~XX (XXXX), no.~X, pp.~XXX--XXX.

%%% For a Journal article by the same authors as above, %%% i.e., authors in cite1 are the same for cite2 \bibitem{cite2} \bysame {\itshape Title of article}, {\bfseries\itshape Journal}, vol.~XX (XXXX), no.~X, pp.~XX--XXX.

%%% For a book \bibitem{cite3} {\scshape Author's Name}, {\bfseries\itshape Title of book}, Name of series, Publisher, Year.

%%% For an article in proceedings \bibitem{cite4} {\scshape Author's Name}, {\itshape Title of article}, {\bfseries\itshape Name of proceedings} (Address of meeting), (First Last and First2 Last2, editors), vol.~X, Publisher, Year, pp.~X--XX.

%%% For an article in a collection \bibitem{cite5} {\scshape Author's Name}, {\itshape Title of article}, {\bfseries\itshape Book title} (First Last and First2 Last2, editors), Publisher, Publisher's address, Year, pp.~X--XX.

%%% An edited book \bibitem{cite6} Author's name, editor. % No special font used here {\bfseries\itshape Title of book}, Publisher, Publisher's address, Year.

ABSTRACT. In 2015, T\"ornquist answered an old question of Mathias by showing that there are no infinite mad families in the Solovay model. Mathias's original paper explores a connection between mad families and the $H$-Ramsey property for $H$ a happy family, but T\"ornquist's proof is purely combinatorial and does not exploit this connection. We prove the following theorem: in the Solovay model, every $X\subseteq[\omega]^\omega$ is $H$-Ramsey for every happy family $H$ that also belongs to the Solovay model. This gives a new proof of T\"ornquist's theorem.

T\"ornquist also asked whether the Axiom of Determinacy ($\mathsf{AD}$) implies that there are no infinite mad families. Using a new generic absoluteness result that builds on the absoluteness results of Neeman–Zapletal, we show how to give a positive answer under $\mathsf{AD}^+$, a well-studied strengthening of $\mathsf{AD}$. (It is open whether $\mathsf{AD}$ and $\mathsf{AD}^+$ are equivalent.) In fact, we show that under $\mathsf{AD}^+$ every $X\subseteq [\omega]^\omega$ is $H$-Ramsey for every happy family $H$.

ABSTRACT. Maximal independent families are combinatorial objects that have applications in various areas of mathematics. A maximal independent family can be constructed using the Axiom of Choice, and an old result of Arnold Miller shows that there are no analytic maximal independent families. We strengthen this result by showing that in the Cohen model, there are no projective maximal independent families. We also introduce a new cardinal invariant related to maximal independent families and provide some partial results about it. This is joint work with Jörg Brendle (U Kobe, Japan).

ABSTRACT. %% TO PROCESS THIS FILE YOU WILL NEED TO DOWNLOAD asl.cls from %% http://aslonline.org/abstractresources.html.

\documentclass[bsl,meeting]{asl} \AbstractsOn \pagestyle{plain}

\def\urladdr#1{\endgraf\noindent{\it URL Address}: {\tt #1}.}

\newcommand{\NP}{} %\usepackage{verbatim}

\begin{document} \thispagestyle{empty}

\NP \absauth{Yechiel M. Kimchi} \meettitle{Partition relations equiconsistent with $o(o(\ldots o(\kappa)\ldots)) = 2$} \affil{CS Faculty, The Technion, Haifa 32000, Israel} \meetemail{yechiel@cs.technion.ac.il}

%% INSERT TEXT OF ABSTRACT DIRECTLY BELOW

{\bf Preamble}: We try to associate the consistency strength of statements like $o(\kappa) = \alpha$ (for $\kappa$ measurable) with various partition relations of the form $\kappa \rightarrow{}(\mu)^{\alpha}_{\lambda}$. Here, we restrict ourselves to partitions of the form $\aleph_1 \rightarrow (\omega^\alpha)^{\omega^\alpha}_{\aleph_0}$. Since we work under $ZFC$, the partition properties are limited to definable functions.

In \cite{78}, M. Spector proved that for $\alpha = 1$ \begin{center} $CON(\exists \kappa(o(\kappa) = \alpha)) \iff CON(\aleph_1 \rightarrow (\omega^\alpha)^{\omega^\alpha}_{\aleph_0})$ \end{center} In \cite{87} we have shown that it can be generalized to $\alpha = 2$ only (which serves as the basis for the current presentation). In order to resurrect the nice equiconsistency we defined the notion of {\em weak-homogeneity}, and recently, in \cite{15}, we extended the result to \begin{center} $CON(\exists \kappa(o(\kappa) = \kappa^+)) \iff CON(\aleph_1 \xrightarrow{\text{\fontsize{1.5}{4}\selectfont WH}}(\aleph_1)^{\aleph_1}_{\aleph_0})$ \end{center}

The failure of the original equiconsistency for $\alpha = 3$, lead us in the past to prove \begin{center} $CON(\aleph_1 \rightarrow (\omega^3)^{\omega^3}_{\aleph_0}) \iff CON(\exists \kappa(o(o(\kappa)) = 2))$ \end{center} % In this presentation we extend the latter for all $\alpha < \omega$, and for that we need two simple definitions. The first one is just notational: $\kappa \xrightarrow{\text{\fontsize{1.5}{4}\selectfont Cl}}(\mu)^{\alpha}_{\lambda}$ means that both the homogeneous sequence of o.t. $\mu$ and the sequences of o.t. $\alpha$ in the domain of the functions, are restricted to closed sequences. The second iterates the $o(\kappa)$ function: \\ {\bf Definition}: $o^n(\mu)$ is defined by induction on $n \in \omega$ for any ordinal $\mu$: \\ \hspace*{18mm} (i) $o^0(\mu) = \mu$ \hspace{5mm} (ii) $o^{n+1}(\mu) = o(o^n(\mu))$

\vspace{1mm} We are now able to state the following two related theorems: \\ \vspace{1mm} \hspace*{-1.5mm}{\bf Theorem 1}: For any $n \in \omega (n \ge 2)$, % $CON(\aleph_1 \xrightarrow{\text{\fontsize{2.5}{4}\selectfont Cl}}(\omega^n)^{\omega^n}_{\aleph_0}) \iff CON(\exists \kappa(o^n(\kappa) = 2))$\\ %\vspace{2mm} \hspace*{-0.4mm}{\bf Theorem 2}: For $n \in \omega (n \ge 1)$, $CON(\aleph_1 \rightarrow (\omega^{n+1})^{\omega^{n+1}}_{\aleph_0}) \iff CON(\exists \kappa(o^n(\kappa) = 2))$

\vspace{2mm} {\bf Note 1}: The new result is the forward direction (from left to right). % while the other direction has been proved in the past.\\

{\bf Note 2}: The exact consistency strength of the statement $\aleph_1 \rightarrow (\omega^\omega)^{\omega^\omega}_{\aleph_0}$, % using the language of large cardinals, is still not known. All we know (cf. \cite{87}) is that it implies the consistency of the statement $\exists \kappa(o(\kappa) > \kappa)$ -- witnessing yet another jump in the relationship between partition properties and measurable cardinals.

\begin{thebibliography}{10}

\bibitem{78} {\scshape M. Spector}, {\itshape Natural Sentences of Mathematics which are independent of $V = L$, $V = L^\mu$ etc.}, Preprint, 1978

\bibitem{87} {\scshape Y.M. Kimchi}, {\itshape Dissertation, Hebrew Univ. of Jerusalem, Israel}, 1987

\bibitem{15} \bysame %%{\scshape Y.M. Kimchi}, {\itshape Partition Relation Equiconsistent with $\exists \kappa(o(\kappa) = \kappa^+)$}, The 5th European Set Theory Conference, Newton Inst., Cambridge UK, August 2015 \urladdr{https://www.newton.ac.uk/seminar/20150826140014302}

\end{thebibliography}

\vspace*{-0.5\baselineskip} % this space adjustment is usually necessary after a bibliography

\end{document}

ABSTRACT. \documentclass[a4paper,12pt,titlepage,leqno]{article}

\begin{document}

\begin{center} {\bf The tree property at the double successor of a singular cardinal \par}

R.~Honzik: Charles University, Department of Logic,\\ Celetn{\' a} 20, Praha 1, 116 42, Czech Republic\\ radek.honzik@ff.cuni.cz\\ web page: logika.ff.cuni.cz/radek

\end{center}

\textbf{Abstract.} We compare several methods for obtaining the tree property at the double successor of a singular strong limit cardinal $\kappa$ with countable cofinality. We will focus on the case when $\kappa$ is equal to $\aleph_\omega$, and discuss large cardinal assumptions used for these results. We will also discuss possible values of the continuum function at $\kappa$. Some of the results are joint with Sy D.\ Friedman and {\v S}.\ Stejskalov{\'a}. \end{document}

ABSTRACT. In this paper we consider prefix realizability problems of infinite words over an finite alphabet for some classes of languages such as the class of context-free languages, the class of regular languages, the class of languages accepted by finite deterministic pushdown automata by final states, the class of languages accepted by finite deterministic pushdown automata by empty stack.

ABSTRACT. It is well-known that every set of reals with positive measure contains a perfect subset. In a joint project of Chong, Li, Yang and Wei Wang, we study the computability of such perfect subsets. We show that every effectively closed set $C$ with positive measure contains a low perfect subset. Moreover, the Turing degrees of perfect subsets of $C$ contain all degrees above the halting problem. We also prove that every set with positive measure contains a perfect subset not computing any given non-computable set.

ABSTRACT. Let $\mathcal F$ be a family of total functions which is computable by an oracle $A$, where $A$ is an arbitrary set. A numbering $\alpha:\omega\mapsto \mathcal F$ is called $A$-computable if the binary function $\alpha(n)(x)$ is $A$-computable, \cite{BG}.

\begin{lemma} Let $\mathcal F$ be an infinite $A$-computable family of total functions, where $A$ is an arbitrary set. Then $\mathcal F$ has an $A$-computable Friedberg numbering. \end{lemma}

A degree $a$ is hyperimmune if $a$ contains a hyperimmune set, and $a$ is hyperimmune free otherwise. Every nonzero degree comparable with $0'$ is hyperimmune. Dekker showed that for every non-recursive c.e. set $A$ there is a hyperimmune set $B$ such that $B\equiv_T A$, which means that every non-recursive c.e. degree contains a hyperimmune set.

\begin{lemma} For every hyperimmune set $A$ there exists a non-recursive $A$-computable set $B$. \end{lemma}

It is known \cite{BI}, that if $A$ is an arbitrary set, $\mathcal F$ is an infinite $A$-computable family of total functions and $\mathcal F$ has at least two nonequivalent $A$-computable Friedberg numberings, then $\mathcal F$ has infinitely many pairwise nonequivalent $A$-computable Friedberg numberings. And also \cite{Iss1}, if $\mathcal F$ is an infinite $A$-computable family of total functions, where $\emptyset' \leq_{T} A$, then $\mathcal F$ has infinitely many pairwise nonequivalent $A$-computable Friedberg numberings.

We extend these results,

\begin{theorem} Let $\mathcal F$ be an infinite $A$-computable family of total functions, where $A$ is a hyperimmune set. Then $\mathcal F$ has infinitely many pairwise nonequivalent $A$-computable Friedberg numberings. \end{theorem}

Note that, \cite{Iss2}, if an $A$-computable family $\mathcal F$ of total functions contains at least two elements, where $A$ is a hyperimmune set, then $\mathcal F$ has no $A$-computable principal numbering.

\begin{theorem} (Issakhov) Let $\mathcal F$ be a finite $A$-computable family of total functions, where Turing degree of the set $A$ is hyperimmune free. Then $\mathcal F$ has an $A$-computable principal numbering. \end{theorem}

QUESTION. Is it true the formulation of previous theorem for infinite family?

The main talk will be around this question.

ABSTRACT. Roman Kossak formulated in \cite{Peano} the following 'Converse to Tarski' problem: Let $FS(X)$ be a formula of the language of $PA$ with a additional predicate symbol $X$ expressing that $X$ is a full satisfaction class. $FS(X)$ is an example of a formula $\Phi(X)$ such that: \begin{enumerate} \item $Con(PA(X)+\Phi(X))$ and: \item if $(\mathcal{M}, X) \models \Phi(X)$, then $X$ is not definable in $\mathcal{M}$. \end{enumerate} Problem: Assume $\Phi(X)$ satisfies 1. and 2. Is it true that for every nonstandard $\mathcal{M} \models PA$ and every $X \subseteq |\mathcal{M}|$, if $(\mathcal{M}, X) \models \Phi(X)$, then there is a nonstandard satisfaction class definable in $(\mathcal{M}, X)$?

We answer the question in the negative, using the seminal result of Harrington, formulated and proved (in the version useful for tackling the 'Converse to Tarski' problem) in unpublished notes In our talk, we present the proof of Harrington's unpublished result and demonstrate how the solution of the 'Converse to Tarski' follows. The interpretation of the result is that, roughly speaking, it is not the case that undefinability of a given set $X$ in a nonstandard model of arithmetic does not always 'come from' Tarski's theorem on undefinability of truth by (arithmetic) reducibility of a satisfaction class to $X$.

ABSTRACT. In this abstract we consider the properties of central types for the existentially prime strongly convex Jonsson theories in some enrichment by Jonsson set. This class of such theories is a subclass of a broad class of Jonsson theories. In particular, the Jonsson theories include the class of all fields of a fixed characteristic. In the given abstract, problems related to the classical problems of the general Model Theory concerning the topics under enrichment were considered. First of all, we note the values of enrichment. Using the one-place predicate, the Jonsson subset is singled out and the concepts of Jonsson stability and various kinds of similarities are considered for the Jonsson completion. The following results were obtained:Coincidence of Jonsson stability for a prototype of the central type and stability in classical meaning of its center. Equivalence of the categoricity of companions of fragments for Jonsson set and their centers also considered. The above notion of stability has an applied value for studying the properties of the central types in this enrichment. In the second place, it is necessary to note the significance of the concept of the central type in this enrichment. The very idea of a central type presupposes an additional description of the properties of incomplete Jonsson theories by means of central completion. The Jonsson subsets of the semantic model of the existentially prime convex Jonsson theory have good theoretic-model properties. This new point of view on Jonsson sets concerns the Morley rank and it is preserved in the syntactic and semantic similarity of the above theories.

ABSTRACT. We show that there is an effectively closed maximal eventually different family of functions in spaces of the form $\prod_n F(n)$ for $F\colon \mathbb N \to \mathbb N\cup\{\mathbb N\}$ and give an exact criterion for when there exists an effectively compact such family. The proof generalizes and simplifies the argument due to Horowitz and Shelah that there is a Borel maximal eventually different family.