ABSTRACT. The enumeration degrees are an upper semi-lattice with a least element and jump operation. They are based on a positive reducibility between sets of natural numbers, enumeration reducibility, introduced by Friedberg and Rogers in 1959. The Turing degrees have a natural isomorphic copy in the structure of the enumeration degrees, namely the substructure of the total enumeration degrees. A long-standing question of Rogers is whether the substructure of the total enumeration degrees has a natural first order definition. The first advancement towards an answer to this question was made by Kalimullin. He discovered the existence of a special class of pairs of enumeration degrees, K-pairs, and showed that this class has a natural first order definition. Building on this result, he proved the first order definability of the enumeration jump operator and consequently obtained a first order definition of the total enumeration degrees above 0'. Ganchev and Soskova showed that when we restrict ourselves to the local structure of the enumeration degrees bounded by 0', the class of K-pairs is still first order definable. They investigated maximal K-pairs and showed that within the local structure the total enumeration degrees are first order definable as the least upper bounds of maximal K-pairs.

The question of the global definability of the total enumeration degrees is finally solved by Cai, Ganchev, Lempp, Miller and Soskova. They show that Ganchev and Soskova's local definition of total enumeration degrees is valid globally. Then using this fact, they show that the relation ``c.e. in'', restricted to total enumeration degrees is also first order definable. We will discuss these results and certain consequences, regarding the automorphism problem in both degree structures.

This research was supported by a BNSF grant No. DMU 03/07/12.12.2011, by a Sofia University SF grant and by a Marie Curie international outgoing fellowship STRIDE (298471) within the 7th European Community Framework Programme.

ABSTRACT. There are (at least) two ways in which knowledge can enter into elections.

1. When a voter strategizes, i.e. votes for someone who is not her first preference then she needs to know something about how the others are voting. In the absence of knowledge, the only safe vote is an honest vote.   But in the presence of knowledge, a  "dishonest" vote may be better than an honest one.  Also, perhaps they too want to know how she is voting.  We discuss how knowledge affects strategizing and when cycles will form.

2. When a politician campaigns, he wants to influence the voters’ beliefs. What should he say in order to appeal to them in the best way?   If the politician knows the preferences of various groups of voters then he will choose the right thing to say so as to make a favorable impression on most voters and antagonize the fewest voters. 

We also consider the temperament of the voters - voters may be pessimistic, optimistic, or use some form of expected value to evaluate the candidate and his utterances.

We will make use of joint work with Samir Chopra, Walter Dean and Eric Pacuit, as well as suggest some new ideas.

ABSTRACT. Henkin (1961) enriched first-order logic with so-called branching or Henkin quantifiers such as $\left(\begin{array}{c} \forall x\\ \exists y \end{array}\right)$ and $\left(\begin{array}{cc} \forall x & \exists y\\ \forall z & \exists w \end{array}\right).$ The former is intended to express the fact that the existential qua ntifier $\exists y$ is independent of the universal quantifier $\forall x$. The latter is more easily introduced in terms of the idea of dependence: the existential quantifier $\exists y$ depends only on the universal quantifier $\forall x$, and the existential quantifier $\exists w$ depends only on the universal quantifier $\forall z$. The notions of independence and dependence are codified in terms of the existence of certain (Skolem) functions. It turns out that prefixing first-order formulas with branching quantifiers results in a logic which is strictly stronger than ordinary first-order logic.

In the first part of my presentation I will quickly review various formalisms which develop Henkin's ideas. One of them is Independence-Friendly logic introduced by Hintikka and Sandu (1989). The first branching quantifier is expressed in IF logic by $\forall x(\exists y/\left\{ x\right\} $) (``for all $x$ there is a $y$ which is independent of $x$''). Similarly, the second branching quantifier is expressed by $\forall x\exists y\forall z( \exists w/\left\{ x,y\right\} )$ (``for all $x$ there is a $y$ and for all $z$ there is a $w$ which is independent from both $x$ and $y$''). The notion of independence is spelled out in game-theoretical terms. With each IF formula $\varphi$, model $\mathbb{M}$, and partial assignment $s$ whose domain is restricted to the free variables of $\varphi$, we associate an extensive win-lose game of imperfect information $G(\mathbb{M},\varphi,s)$. When $\varphi$ is the sentence $\forall x(\exists y/\left\{ x\right\} )x=y$, and $s$ is the empty assignment, in a play of the game $G(\mathbb{M},\varphi,s)$ $\forall$ chooses an individual $a\in M$ to be the value of $x$ after which $\exists$ chooses an individual $b\in M$ to be the value of $y$ without knowing the choice made earlier by $\forall$. Player $\exists$ wins the play if $a$ is the same individual as $b$. Otherwise player $\forall$ wins. We stipulate that $\varphi$ is true (false) in $\mathbb{M}$ if there is a winning strategy for player $\exists$ ($\forall$). The notion of strategy is the standard notion of choice function in classical game theory. In games of imperfect information such a function is required to be uniform. A comprehensive presentation of the model-theoretical properties of IF logic may be found in Mann, Sandu, and Sevenster (2011). Hintikka (1996) explores the significance of IF logic for the foundations of mathematics.

As expected, games of imperfect information may be indeterminate. For instance, on models with at least two elements, the IF sentence $\forall x(\exists y/\left\{ x\right\} )x=y$ is neither true nor false. Blass and Gurevich (1986) follow a suggestion by Aitaj and resolve the indeterminacy of this sentence by applying von Neumann's Minimax theorem: $\forall x(\exists y/\left\{ x\right\} )x=y$ gets the probabilistic value $\frac{1}{n}$ on any finite model with $n$ elements. This value is the expected utility returned to the existential player by any mixed strategy equilibrium in the underlying game. This idea has been explored systematically for the first time in Sevenster (2006), and then further developed in Sevenster and Sandu (2010), and in Mann, Sandu and Sevenster (2011). In the second part of my talk I will review some of the recent results on probabilistic IF logic.

Finally I will address the question: What kind of probabilistic logic is probabilistic IF logic? Here I shall draw some comparisons to other probabilistic semantics (Leblanc's probabilistic semantics, Bacchus' and Halpern's probabilistic interpretations of first-order logic.)

\begin{thebibliography}{10}

%% 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})

\bibitem{BG} {\scshape A. Blass and Y. Gurevich}, {\itshape Henkin quantifiers and complete problems}, {\bfseries\itshape Annals of pure and Applied Logic}, vol.~32 (1986), no.~1, pp.~1--16.

\bibitem{He} {\scshape L. Henkin}, {\itshape Some remarks on infinitely long formulas}, {\bfseries\itshape Intuitionistic Methods: Proceedings of the Symposium on Foundations of Mathematics} (P. Bernays, editor), Pergamon Press, Oxford, 1959, pp.~169--183.

\bibitem{HS} {\scshape J. Hintikka and G. Sandu}, {\itshape Informational Independence as a Semantic Phenomenon}, {\bfseries\itshape Logic, Methodology and Philosophy of Science} (J.~E.~Fenstead et al, editors), Elsevier, Amsterdam, 1989, pp.~571--589.

\bibitem{MSS} {\scshape A. I. Mann, G. Sandu and M. Sevenster}, {\bfseries\itshape Independence-Friendly Logic: A Game-Theoretic Approach}, Cambridge University Press, 2011.

\bibitem{S} {\scshape M. Sevenster}, {\bfseries\itshape Branches of Imperfect Information: Logic, Games, and Computation}, PhD Thesis, University of Amsterdam, 2006.

\bibitem{SS} {\scshape M. Sevenster and G. Sandu}, {\itshape Equilibrium Semantics of Languages of Imperfect Information}, {\bfseries\itshape Annals of Pure and Applied Logic}, vol.~161 (2010), pp.~618--631.

\end{thebibliography}

ABSTRACT. The roots of UD-randomness are firmly analytic: Avigad defined it in 2013 using concepts from a 1916 theorem of Weyl concerning uniform distribution. Avigad showed in his original paper that UD-randomness is very weak. While every Schnorr random real is UD-random, the class of UD-random reals is incomparable with the class of the Kurtz random reals. In this talk, I will present some subsequent work on the Turing degrees of the UD-random reals and the relationships between UD-randomness and other randomness notions.

This work is joint with Wesley Calvert.

ABSTRACT. Using matrix iterations of ccc posets we prove the consistency, with ZFC, of some constellations of Cichoń's diagram where the cardinals on the right hand side assume three different values. We also discuss the influence of the constructed models on other classical cardinal invariants of the continuum.

ABSTRACT. When working with measurable flows, it is sometimes convenient to choose a countable cross-section and to reduce a problem of interest to a similar question for the action induced by the flow on this cross-section. In some cases, one wants to impose additional restrictions on the cross-section, usually by restricting possible distances between points within each orbit.

Historically, cross-sections of flows were studied mainly in the context of ergodic theory. One of the most important results here is a theorem of D. Rudolph, which states that any free measure preserving flow, when restricted to an invariant subset of full measure, admits a cross-section with only two possible distances between adjacent points.

Borel dynamics deals with actions of groups on standard Borel spaces, when the latter is not equipped with any measure. In this more abstract context, one needs to construct cross-sections that are regular on all orbits without exceptions, and methods of ergodic theory, which tend to produce cross-sections only almost everywhere, are therefore frequently insufficient. In this regard, M. G. Nadkarni posed a question whether the analog of Rudolph's Theorem holds true in the Borel setting: Does every free Borel flow admit a cross-section with only two different distances between adjacent points?

The talk will provide an overview of these and other results concerning the existence of regular cross-sections, and a positive answer to Nadkarni's question will be given. As an application of our methods, we give a classification of free Borel flows up to Lebesgue Orbit Equivalence, by which we understand orbit equivalence preserving Lebesgue measure on each orbit. This classification is an analog of the classification of hyperfinite equivalence relations obtained by R. Daugherty, S. Jackson, and A. S. Kechris.

ABSTRACT. Logic has been called the "calculus of computer science" - and yet, while any physics student is required to take several semesters of calculus, the same cannot be said about logic and students of computer science. Despite the great and burgeoning activity in logic-related topics in computer science, there has been very little interest, in North America at least, in developing a strong logic component in the undergraduate curriculum. Meanwhile, in other parts of the world, departments have set up specialized degree programs on logical methods and CS. This special session, organized under the auspices of the ASL's Committee on Logic Education, aims to explore the role of logic in the computer science curriculum. How are computer scientists trained in logic, if at all? What regional differences are there, and why? Is a greater emphasis on logic in the computer science undergraduate curriculum warranted, both from the point of view of training for research in CS and from the point of view of training for industry jobs? What should an ideal "Logic for Computer Science" course look like?

Byron Cook believes that, in the rush to create engineers and scientists, we have lost sight of the fact that an education should be broad and place emphasis on principles rather than specific skills such as Javascript. Logic is the perfect topic in this setting, as it has application in both humanities and science, and fosters a discussion about mechanics while not requiring a significant amount of technical overhead.

The Association for Computing Machinery has just chartered a new Special Interest Group on Logic and Computation (SIGLOG). Education is one of the prime concerns of this new SIG and one of the activities on the SIG's education committee will be to advocate for a greater presence of logic in the curriculum. Prakash Panangaden discusses the aims of the new SIG with particular emphasis on its educational mission.

Nicole Schweikardt will report on experiences with designing an undergraduate introductory course on logic in computer science at Goethe-University Frankfurt.

The University of Technology Vienna participates in a European Masters program in computational logic and has just started a doctoral program in Logical Methods in Computer Science. Alexander Leitsch describes these initiatives and considers lessons other departments can draw from the Vienna experience.

Presentations will be followed by a panel discussion. Materials will be available on the Committee on Logic Education website at http://ucalgary.ca/aslcle/.

ABSTRACT. Goldblatt proved that the modal logic S4.2 characterizes Minkowski spacetimes; the possible worlds represent events, and the intended interpretation of the modal operator is ``it is now or it will be the case in the causal future that''. Unfortunately, the expressive power of this logic is very limited; the fundamental relativistic effects such as the twin paradox, time dilatation, etc. are inexpressible.

In our talk, we will modalize the first-order theory of reals to answer this challenge. The worlds, again, will represent events, while the modal operator will represent ``It is visible that'' or ``it was the case in the lightlike separated past that''. We use only functions and relations of reals; the solely modal novelty is the presence of non-rigid designators to deal with the clocks of observers. This theory, beyond its expressive power could be a first step towards a connection of the axiomatic operational foundations of spacetime and the research inspired by Prior and Belnap such as theories of branching spacetimes.

ABSTRACT. I want to present a three-valued paracomplete logic, based on the work of Hartry Field, that captures, in a reasonably intuitive way, how we reason under the phenomenon of vagueness in languages with a truth predicate. I claim that this is a first step towards a satisfactory logic for the Vagueness and Liar-like paradoxes where the naive theory of truth can be implemented; that is, where we can have the Intersubstitutivity Principle (IP): If two sentences A and B are alike except that one has a sentence C where the other has Tr^⌈C^⌉, then A |= B and B |= A. I will use a language L suitable to express canonical names for its own sentences and I will extend it to a new language, L⁺, with a truth predicate, Tr. I will use models with a set W of ordered three valued points and create a process of revision for the conditional where each point is enlarged to a Kripke fixed point.

ABSTRACT. We introduce a graphical approach to modalities. We employ formal systems where graphs are expressions that can be manipulated so as to mirror reasoning at the semantical level. This visual approach is exible and modular providing decision procedures for several normal logics. Promising cases are the application of this approach to PDL for structured data [1] and to memory logics [2]. [1] Veloso, P., Veloso, S. Benevides, M.: PDL for Structured Data: a Graph-Calculus Approach. Journal of the IGPL, to appear (2014) [2] Areces, C., Figueira, S. Mera, S. : Completeness Results for Memory Logics. LNCS 5407, pp. 16{30, Springer (2009)

ABSTRACT. The language of Graded Modal Logic (GML, Kit Fine, 1972) is an extension of the classical propositional modal language with counting (or \emph{grading}) modal operators $\lozenge_n$, for $n\geq 0$, which have purely quantitative meaning. S. Tobies proves (Tobies, 2000) that the satisfiability problem for the graded modal language is PSPACE-complete.

The language of Majority Logic (MJL, Pacuit and Salame, 2004) augments the graded modal language with some qualitative capabilities. Two extra unary modal operators, $M$ and $W$, are added. In Kripke models $M\varphi$ says that more than half of all accessible worlds satisfy $\varphi$, what represents the simplest case of \emph{rational grading}.

The language of Presburger Modal Logic (PML, Demri and Lugiez, 2006) is a many-relational modal language with independent relations, having the so-called \emph{presburger constraints}, which can express both integer and rational grading. Demri and Lugiez show that the satisfiability for the PML language is PSPACE-complete, what strengthens the main result of Tobies, and answers the open question about MJL.

At that time a generalization of modal operators for rational grading in the spirit of the majority operators is given (Tinchev and Y., 2006), and it is used in the language of Generalized Graded Modal Logic (GGML, Tinchev and Y., 2010). New unary grading operators are considered, $M^r$ and $W^r$, where $r$ is a rational number in (0,1). These operators distinguish the part of accessible worlds having some property.

The generalized rational grading operators are expressible by presburger constraints, so the PSPACE completeness of the satisfiability for the generalized graded modal language is a consequence of that for PML. On the other hand an independent proof using a specific technique for exploring the complexity of rational grading is given (Y., 2011). The presence of separate integer and rational grading operators, and the use of the technique developed for the latter allow following a common way for obtaining complexity results as in less, so in more expressive languages with rational grading. In particular, complexity results---from polynomial to PSPACE---for a range of description logics, syntactic analogs of fragments of GGML, are obtained (Y., 2012, 2013).

In this talk we consider many-relational generalized graded modal language adopting \emph{inverse relations} and \emph{intersection of relations}. Rational grading operators are $\upharpoonright\!\!\sigma\!\!\upharpoonleft^r$ and $\downharpoonright\!\!\sigma\!\!\downharpoonleft^r$, where $\sigma$ is an intersection of (possibly inverse) relations. We show that the satisfiability problem for this expressive modal language with generalized grading keeps the PSPACE complexity.

ABSTRACT. We define the notion of fuzzy bisimulation for the standard Godel modal logic and prove the corresponding Hennessy-Milner style theorem.

ABSTRACT. In R.A. Bull characterized a class of axiomatic extensions of the modal logic S4 (the logic of the class of transitive and symmetric frames) with the finite model property. This result takes the form of a syntactic characterization of a class of formulas that may be added as axioms to S4, somewhat in the spirit of Sahlqvist's famous result in modal correspondence theory. Hybrid logics expand the syntax of modal logic by adding special variables, know as nominals, which are always interpreted as singletons in models and thus act as names for the states at which they hold. Additional syntactic machinery which capitalizes on the naming power of the nominals, like the satisfaction operator or the universal modality, is often added. This makes hybrid languages significantly more expressive than their modal cousins, while retaining their good computational behaviour. In this talk we show how to extend Bull's result to three hybrid languages. The proof we offer is algebraic and serves to illustrate the usefulness of the new algebraic semantics for hybrid logics recently introduced by the authors. Bull's proof makes essential use of the algebraic property of `well-connectedness' which is equivalent, in the dual relational semantics, to the ability to take generated submodels. Since the truth of hybrid languages is not invariant under generated submodels, the generalization to hybrid logic is not straight-forward.

ABSTRACT. We prove that a modal consequence operation extending S4.3 is almost structurally complete (with respect to infinitary rules) if and only it is finitely approximable. We also provide an uniform basis, consisting of infinitary rules, for all admissible rules there.

ABSTRACT. On the basis of dynamic model of self-reference statements the variant of multiple-valued logic describing external operations of such statements is considered. It is noted that for formulations and self-reference statements descriptions is enough the language with negation (~) and biconditional (<->) . The truth table for biconditional for type formulae of True, Liar, TruthTeller and (TruthTeller <-> Liar), is Cayley table for the Klein four-group V . It suggests that the truth space for values of self-reference statements is described by quaternion algebra H.

ABSTRACT. G\"{o}del 3-valued logic G3 is the strongest of the G\"{o}del many-valued logics introduced in [1]. Although the Routley-Meyer semantics (RM-semantics) was defined for interpreting relevant logics in the early seventies of the last century (cf. [4]), it was soon found out to be suitable for characterizing a wide family of logics regardless of their being relevant or not, due to its malleability. Still, a necessary condition for a logic S to be characterized by the RM-semantics is that Routley and Meyer's basic positive logic B$_{+}$ is included in S (cf. [4]). The aim of this paper is to provide an RM-semantics for G3 once this logic has been axiomatized as an extension of B$_{+}$ (cf. [2], [3]).

ABSTRACT. The depth relevance condition (drc) is a strengthening of the variable-sharing property. A logic S has the drc if $A$ and $B$ share at least a propositional variable at the same depth in all theorems of the form $A\rightarrow B$ (cf. [1]). Logics with the drc have been used for defining non-trivial strong na\"{\i}ve set theories. In [3], \textquotedblleft the class of implication formulas known to trivialize NC\textquotedblright\ is recorded. (NC abbreviates \textquotedblleft na\"{\i}ve comprehension\textquotedblright ; cf. [3], p. 435.) The aim of this paper is to show how to invalidate any member in this class by using \textquotedblleft weak relevant model structures\textquotedblright\ (cf. [2]). Weak relevant model structures only verify logics with the drc.

ABSTRACT. This work builds on the well-known 0-1 law for the asymptotic probabilities of first-order definable properties of finite graphs (in general, relational structures). Fagin's proof of this result is based on a transfer between almost sure properties in finite graphs and true properties of the countable random graph (aka, Rado graph).

Both the transfer theorem and the 0-1 law hold in some non-trivial extensions of first-order logic (e.g., with fixed point operators) but fail in others, notably in most natural fragments of monadic second-order (MSO) and even for modal logic formulae, in terms of frame validity. The question we study here is how to characterise -- axiomatically or model-theoretically -- the set of almost surely valid in the finite formulae of MSO, i.e. those with asymptotic probability 1. This question applies likewise to every logical language where truth on finite structures is well-defined. The set of almost sure validities in the finite of a given logical language is a well-defined logical theory, containing all validities of that language and closed under all sound finitary rules of inference. Beyond that, very little is known about these theories in cases where the transfer theorem fails.

In this work we initiate a study of the theories of almost sure validity in modal logic and in the universal and existential fragments of MSO on binary relational structures, aiming at obtaining explicit logical characterisations of these theories. We provide such partial characterisations in terms of characteristic formulae stating almost sure existence (for the existential fragment) or non-existence (for the universal fragment) of bounded morphisms to special target finite graphs. Identifying explicitly the set of such finite graphs that generate almost surely valid characteristic formulae seems a quite difficult problem, to which we so far only provide some partial answers and conjectures.

ABSTRACT. This paper extends Reynolds' separation logical system for pointer while program verification to second-order logic. This extension enables us, for example, to capture a set of integer values, in order to capture the set of reachable nodes in a heap predicate. This paper proves its completeness theorem that states that every true asserted program is provable in the logical system. In order to prove the completeness, this paper also shows the expressiveness theorem that states the weakest precondition of every program and every assertion can be expressed in the assertion language.

ABSTRACT. We prove that the determinacy of Gale-Stewart games whose winning sets are infinitary rational relations accepted by 2-tape Büchi automata is equivalent to the determinacy of (effective) analytic Gale-Stewart games which is known to be a large cardinal assumption. Then we prove that winning strategies, when they exist, can be very complex, i.e. highly non-effective, in these games. We prove the same results for Gale-Stewart games with winning sets accepted by real-time 1-counter Büchi automata, then extending previous results obtained about these games.

(1) There exists a 2-tape Büchi automaton (respectively, a real-time 1-counter Büchi automaton) A such that: (a) there is a model of ZFC in which Player 1 has a winning strategy $\sigma$ in the game $G(L(A))$ but $\sigma$ cannot be recursive and not even in the class $(\Sigma_2^1 \cup \Pi_2^1)$; (b) there is a model of ZFC in which the game $G(L(A))$ is not determined.

(2) There exists a 2-tape Büchi automaton (respectively, a real-time 1-counter Büchi automaton) A such that $L(A)$ is an arithmetical $\Delta_3^0$-set and Player 2 has a winning strategy in the game $G(L(A))$ but has no hyperarithmetical winning strategies in this game.

(3) There exists a recursive sequence of 2-tape Büchi automata (respectively, of real-time 1-counter Büchi automata) $A_n$, $n\geq 1$, such that all games $G(L(A_n))$ are determined, but for which it is $\Pi_2^1$-complete hence highly undecidable to determine whether Player 1 has a winning strategy in the game $G(L(A_n))$.

ABSTRACT. We prove that $T_{NC^1}$, the true universal first-order theory in the language containing names for all uniform $NC^1$ algorithms, cannot prove that for sufficiently large $n$, SAT is not computable by circuits of size $n^{2kc}$ where $k\geq 1, c\geq 4$ unless each function $f\in SIZE(n^k)$ can be approximated by formulas $\{F_n\}^{\infty}_{n=1}$ of subexponential size $2^{O(n^{2/c})}$ with subexponential advantage: $P_{x\in \{0,1\}^n}[F_n(x)=f(x)]\geq 1/2+1/2^{O(n^{2/c})}$. Unconditionally, $V^0$ cannot prove that for sufficiently large $n$, SAT does not have circuits of size $n^{\log n}$. The proof is based on an interpretation of Kraj\'{i}\v{c}ek's proof \cite{cite1} that certain NW-generators are hard for $T_{PV}$, the true universal theory in the language containing names for all p-time algorithms.

\begin{thebibliography}{10}

\bibitem{cite1} {\scshape Jan Kraj\'{i}\v{c}ek}, {\itshape On the proof complexity of the Nisan-Wigderson generator based on a hard NP$\cap$coNP function}, {\bfseries\itshape Journal of Mathematical Logic}, vol.~11 (1), 2011, pp.~11--27.

\end{thebibliography}

ABSTRACT. It is well known that some problems in complexity theory can be cast as problems of constructions of expanded extensions of models of bounded arithmetic. These models are usually required to satisfy some form of bounded induction but at the same time not introduce any new lengths of strings. We shall discuss some general facts and one specific construction of this kind.

ABSTRACT. Artemov established an arithmetical interpretation for the Logics of Proofs LP(CS), which yields a classical provability semantics for the modal logic S4. These Logics of Proofs are parameterized by so-called constant specifications CS that state which axioms can be used in the reasoning process, and the arithmetical interpretation relies on the constant specifications being finite. In our paper, we remove this restriction by introducing weak arithmetical interpretations that are sound and complete for a wide class of constant specifications, including infinite ones. In particular, they interpret the full Logic of Proofs LP.

ABSTRACT. Let $\mathbf{d}$ be a Turing degree. A computable structure $\mathfrak{A}$ is {\itshape $\mathbf{d}$-autostable} if, for every computable structure $\mathfrak{B}$ isomorphic to $\mathfrak{A}$, there exists a $\mathbf{d}$-computable isomorphism from $\mathfrak{A}$ onto $\mathfrak{B}$. A decidable structure $\mathfrak{A}$ is {\itshape $\mathbf{d}$-autostable relative to strong constructivizations} if every decidable copy $\mathfrak{B}$ of $\mathfrak{A}$ is $\mathbf{d}$-computably isomorphic to $\mathfrak{A}$.

Let $\mathfrak{A}$ be a computable structure. A Turing degree $\mathbf{d}$ is called the {\itshape degree of autostability} of $\mathfrak{A}$ if $\mathbf{d}$ is the least degree such that $\mathfrak{A}$ is $\mathbf{d}$-austostable. A degree $\mathbf{d}$ is the {\itshape degree of autostability relative to strong constructivizations} ({\itshape degree of $SC$-autostability}) of a decidable structure $\mathfrak{A}$ if $\mathbf{d}$ is the least degree such that $\mathfrak{A}$ is $\mathbf{d}$-autostable relative to strong constructivizations. Note that here we follow~\cite{Goncharov11} and use the term {\itshape degree of autostability} in place of {\itshape degree of categoricity}. A great number of works (see, e.g.,~\cite{FKM10,CFS13,Bazhenov13}) uses the term {\itshape degree of categoricity}.

\begin{theorem} Let $\alpha$ be a computable ordinal.

(1)\ $\mathbf{0}^{(\alpha)}$ is the degree of autostability of some computable Boolean algebra;

(2)\ $\mathbf{0}^{(\alpha)}$ is the degree of $SC$-autostability of some decidable Boolean algebra. \end{theorem}

Using the results of~\cite{CFS13}, we obtain the following corollaries.

\begin{corollary} There exists a decidable Boolean algebra without degree of $SC$-au\-to\-sta\-bi\-li\-ty. \end{corollary}

\begin{corollary} The index set of decidable Boolean algebras with degrees of $SC$-autostability is $\Pi^1_1$-complete. \end{corollary}

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-860.2014.1).

\begin{thebibliography}{10}

\bibitem{Goncharov11} {\scshape S. S. Goncharov}, {\itshape Degrees of Austostability Relative to Strong Constructivizations}, {\bfseries\itshape Proceedings of the Steklov Institute of Mathematics}, vol.~274 (2011), no.~1, pp.~105--115.

\bibitem{FKM10} {\scshape E. B. Fokina, I. Kalimullin, R. Miller}, {\itshape Degrees of Categoricity of Computable Structures}, {\bfseries\itshape Archive for Mathematical Logic}, vol.~49 (2010), no.~1, pp.~51--67.

\bibitem{CFS13} {\scshape B. F. Csima, J. N. Y. Franklin, R. A. Shore}, {\itshape Degrees of Categoricity and the Hyperarithmetic Hierarchy}, {\bfseries\itshape Notre Dame Journal of Formal Logic}, vol.~54 (2013), no.~2, pp.~215--231.

\bibitem{Bazhenov13} {\scshape N. A. Bazhenov}, {\itshape Degrees of Categoricity for Superatomic Boolean Algebras}, {\bfseries\itshape Algebra and Logic}, vol.~52 (2013), no.~3, pp.~179--187.

\end{thebibliography}

ABSTRACT. Let $ \alpha \geqslant 1 $ be a computable ordinal and $ {\mathfrak A} $ be a computable structure. The $ \Delta^{0}_{\alpha} $-dimension of $ {\mathfrak A} $ is maximal $ n \leqslant \omega $ such that there exist $ n $ computable presentations of $ {\mathfrak A} $ without any $ \Delta^{0}_{\alpha} $ isomorphism between them. $ {\mathfrak A} $ is $ \Delta^{0}_{\alpha} $-categorical if this dimension is 1.

In \cite {Ash87}, it was noted that if $ {\mathfrak A} $ has a $ \Sigma^{0}_{\alpha} $ Scott family then it is $ \Delta^{0}_{\alpha} $-categorical. Moreover, a set of conditions $ \Phi ({\mathfrak A}) $ was found, under which this sufficient condition becomes necessary: if $ \Phi ({\mathfrak A}) $ holds then $ {\mathfrak A} $ has a $ \Sigma^{0}_{\alpha} $ Scott family iff it is $ \Delta^{0}_{\alpha} $-categorical.

We prove that under a similar set of conditions $ \Phi' ({\mathfrak A}) $, this equivalence also holds, and, in addition, the $ \Delta^{0}_{\alpha} $-dimension of $ {\mathfrak A} $ is $ 1 $ or $ \omega $. The main part of this result is the theorem below. In addition, we fix a small error in the original formulation of $ \Phi ({\mathfrak A}) $.

If $ \bar {a}, \bar {b} $ are tuples in $ {\mathfrak A} $ of the same length, then $ \bar {a} \leqslant_{\alpha} \bar {b} $ means that every infinite $ \Pi_{\alpha} $ formula true on $ \bar {a} $ is true on $ \bar {b} $. $ {\mathfrak A} $ is $ \alpha $-friendly if the relations $ \leqslant_{\beta} $ are c.e.\ uniformly in $ \beta < \alpha $. Let $ \Rightarrow $ be a binary relation on finite tuples in $ {\mathfrak A} $. We define a relation $ \text {{\rm Free}}^{\Rightarrow}_{\alpha} (\bar {a}, \bar {c}) $ on tuples in $ {\mathfrak A} $ as follows: $$ \forall \beta \,{<}\, \alpha \,\, \forall \bar {a}_{1} \,\, \exists \bar {a}' \,\, \exists \bar {a}'_{1} \,\, \bigl[\: |\bar {a}| = |\bar {a}'| \text {, }\,\, \bar {c}, \bar {a}, \bar {a}_{1} \leqslant_{\beta} \bar {c}, \bar {a}', \bar {a}'_{1} \text {, } \, \text {and} \,\, \bar {c}, \bar {a} \not\Rightarrow \bar {c}, \bar {a}' \: \bigl] \text {.} $$ If $ \Rightarrow $ is $ \geqslant_{\alpha} $ then this definition coincides with the one in \cite {Ash87}.

{\bf Theorem}. Let $ {\mathfrak A} $ be a computable $ \alpha $-friendly structure. Suppose that $ \Rightarrow $ is a relation on finite tuples in $ {\mathfrak A} $ such that \\ {\rm a)} $ \Rightarrow $ is transitive, i.e., $ \bar {a} \Rightarrow \bar {b} $ and $ \bar {b} \Rightarrow \bar {c} $ imply $ \bar {a} \Rightarrow \bar {c} $; \\ {\rm b)} if $ g : {\mathfrak A} \to {\mathfrak A} $ is an automorphism then $ \bar {a} \Rightarrow g (\bar {a}) $ for every $ \bar {a} $ in $ {\mathfrak A} $. \\ If the relation $ \not\Rightarrow $ is c.e.\ and for every $ \bar {c} $ in $ {\mathfrak A} $, we can effectively find $ \bar {a} $ s.t.\ $ \text {{\rm Free}}^{\Rightarrow}_{\alpha} (\bar {a}, \bar {c}) $, then there exists a computable sequence $ \{ {\mathfrak B}_{i} \}_{i \in \omega} $ of computable presentations of $ {\mathfrak A} $ s.t.\ there is no $ \Delta^{0}_{\alpha} $ isomorphism between $ {\mathfrak B}_{i} $ and $ {\mathfrak B}_{j} $ for $ i \neq j $.

\begin{thebibliography}{10}

\bibitem {Ash87} {\scshape C.J.\ Ash}, {\itshape Categoricity in hyperarithmetical degrees}, {\bfseries\itshape Annals of Pure and Applied Logic}, vol.~34 (1987), no.~1, pp.~1--14.

\end{thebibliography}

ABSTRACT. We consider the categoricity of countable scattered linear orders. Recall that linear order is \emph{scattered} if it has no dense suborder. A computable linear order $L$ is \emph{computably ($\Delta^0_n$-, resp.) categorical} if for every computable copy $L'$ of $L$ there is a computable ($\Delta^0_n$-, resp.) isomorphism between $L'$ and $L$. J.~Remmel, S. Goncharov, V. Dzgoev obtained the description of computably categorical linear orders. Namely, they proved that a computable linear order is computably categorical if and only if it contains finitely many pairs of successors. Ch. McCoy} obtained the description of $\Delta^0_2$-categorical computable linear order with additional conditions. We proved that if $L$ is a computable scattered linear order such that $L$ is a finite sum of scattered orders of rank $n$ then $L$ is $\Delta^0_{2n}$-categorical.

ABSTRACT. In Diagonally Non-Computable Functions and Bi-Immunity, Carl Jockusch and Andrew Lewis-Pye proved that every DNC function computes a bi-immune set. They asked whether every DNC function computes an effectively bi-immune set. Several attempts have been made to solve this problem in the last few years. We construct a DNC function that computes no effectively bi-immune set, thereby answering their question in the negative. We obtain a few corollaries that illustrate how our technique can be applied more broadly.

ABSTRACT. Analysing betting strategies where only integer values are allowed, perhaps for a given set F, gives an interesting variant on algorithmic randomness where category and measure intersect. We build on earlier work of Bienvenu, Stephan, and Teutsch, and study reals random in this sense, and their intricate relationship with the c.e. degrees. This is joint work with George Barmpalias and Rod Downey.

ABSTRACT. Recently, connections between differentiability and various notions of effective randomness have been studied. These results are typically of the form ``x in [0,1] is random if and only if every function f in C is differentiable at x,'' where C is some subclass of the computable functions; for example, Brattka, Miller and Nies gave such characterisations for computable and Martin-Löf randomness.

In this talk we will present a complementary result for effective genericity. More precisely, our result says that x in [0,1] is 1-generic if and only if every differentiable computable function has continuous derivative at x. This result can be seen as an effectivisation of a result by Bruckner and Leonard.

This talk is based on joint work with Sebastiaan Terwijn.

ABSTRACT. We consider the complexity of initial segments of computable linear orders. We prove that $\Sigma^0_2$-initial segments of computable linear orders contain in total all computable linear orders without the greatest elements and all $\Sigma^0_2$-degrees.

ABSTRACT. We show that for every degree u REA in 0', there is a pair a_0,a_1 of distinct r.e. degrees such that (a_0)' = u = (a_1)', and such that the set {x' : x <= a_0}, which consists of all jumps of sets Turing-below a_0, is equal to the corresponding set {x' : x <= a_1}. This defeats certain approaches to proving the rigidity of the r.e. degrees.

ABSTRACT. If a < b are elements of a lattice, then we say that a cups to b if there is a c < b such that a + c = b. Kristiansen proves that if a < b in the lattice of honest elementary degrees and a is significantly above 0 (that is, there is a function elementary in a that majorizes every elementary function), then a cups to b. We improve this result by relaxing the restriction that a is significantly above 0 to simply that a is non-zero: if a and b are honest elementary degrees with 0 < a < b, then a cups to b. This answers a question of Kristiansen.

ABSTRACT. We consider structures $\mathcal{A}$ with an additional relation $R$. We say that two relations $R$ and $S$ on structures $\mathcal{A}$ and $\mathcal{B}$ respectively have the same (relativised) degree spectrum if, for sets $C$ on a cone above \textbf{d}, \[ \{R^{\tilde{\mathcal{A}}} \oplus C : \tilde{\mathcal{A}} \cong \mathcal{A} \text{ and } \tilde{\mathcal{A}} \leq_T C \} = \{S^{\tilde{\mathcal{B}}} \oplus C : \tilde{\mathcal{B}} \cong \mathcal{B} \text{ and } \tilde{\mathcal{B}} \leq_T C \}. \] Using determinacy, these degree spectra are partially ordered. Many classes of degrees which relativise, such as the $\Sigma^0_\alpha$ degrees or $\alpha$-CEA degrees, are degree spectra. This is a notion which captures solely the model-theoretic properties of the relation $R$. We will advocate for the naturality of this viewpoint by recasting existing results in this new language, giving new results, and putting forward new questions. Existing results of Harizanov in show that there are two minimal degree spectra, the computable sets and the c.e.\ sets. Ash and Knight considered whether Harizanov's results could be generalised. We give a partial positive answer by showing that any degree spectrum which contains a non-$\Delta^0_2$ degree contains all of the 2-CEA degrees. We also give an example of two incomparable degree spectra.

ABSTRACT. In \cite{nonlown}, for any $n\ge 2$, it was constructed a linear ordering $L$ such that the spectrum $Sp(L)$ contains exactly all non-low$_n$ degrees. Recall, the {\it spectrum} of a linear ordering $L$ is the class $Sp(L) = \{\deg_T(R) \mid R \cong L\}$.

R. Miller \cite{Miller} constructed a linear ordering whose $\Delta_2^0$-spectrum contains exactly all nonlow$_0$ $\Delta_2^0$-degrees, i.e., all nonzero $\Delta_2^0$-degrees. The {\it $\Delta_2^0$-spectrum} of linear ordering $L$ is the class $Sp(L)^{\Delta_2^0} = \{\deg_T(R) \in \Delta_2^0 \mid R \cong L\} = Sp(L) \cap \Delta_2^0$.

The author \cite{Fr1} constructed a linear ordering whose $\Delta_2^0$-spectrum contains exactly all nonlow$_1$ $\Delta_2^0$-degrees.

In \cite{nonlown}, for any $n\ge 2$, it was constructed a linear ordering $L$ such that $Sp(L)$ contains exactly all high$_n$ degrees. Also in \cite{nonlown} it was remarked that there does not exist a linear orderings $L$ such that $Sp(L)$ is exactly all high$_n$ degrees for $n \in \{0, 1\}$.

\begin{theorem} There exists a linear ordering $L$ such that $Sp^{\Delta_2^0}(L) = \{\mathbf{0}'\}$. In other words, $\Delta_2^0$-spectrum of $L$ contains exactly all high$_0$ $\Delta_2^0$-degrees. \end{theorem}

\begin{theorem} There exists a linear ordering whose $\Delta_2^0$-spectrum contains exactly all high$_1$ $\Delta_2^0$-degrees. \end{theorem}

\begin{thebibliography}{9} \bibitem{Fr1} {\scshape A.~Frolov}, {\itshape $\Delta_2^0$-copies of linear orderings}, {\bfseries\itshape Algebra and Logic}, vol.~45 (2006), no.~3, pp.~201--209 (in english), pp.~69--75 (in russian).

\bibitem{nonlown} {\scshape A.~Frolov, V.~Harizanov, I.~Kalimullin, O.~Kudinov, R.~Miller}, {\itshape Spectra of high$_n$ and nonlow$_n$ degrees}, {\bfseries\itshape Journal of Logic and Computation}, vol.~22 (2012), no.~4, pp.~745--754.

\bibitem{Miller} R.~Miller, {\scshape R.~Miller}, {\itshape The $\Delta_2^0$ spectrum of a linear ordering}, {\bfseries\itshape Journal of Symbolic Logic}, vol.~66 (2001), no.~2, pp.~470--486. \end{thebibliography}

ABSTRACT. The properties of degree spectra of countable structures have been studied extensively in computable model theory. Recently Andrews and Miller [1] introduced and studied a notion of the degree spectra of a theory which is defined as DegSp(T) = {Deg(M) | M is a model of T}. In particular, they constructed a theory whose spectrum is equal to a non-degenerate union of two cones, which is known to be impossible for a degree spectrum of a structure.

In our work we consider an analogous question for $\Sigma_n$-spectrum of a structure. We say two structures A and B are $\Sigma_n$-equivalent, if they satisfy the same $\Sigma_n$-sentences. Let A be a countable structure. The $\Sigma_n$-spectrum of A is defined as the set {Deg(B) | B is $\Sigma_n$-equivalent to A}$. The construction from [1] actually implies that there is a structure $A$ such that $\Sigma_2$-spectrum of A is equal to a non-degenerate union of two cones. We show that this result does not hold anymore if we replace $\Sigma_2$-equivalence by $\Sigma_1$-equivalence.

Theorem. Let A be a countable structure. Then $\Sigma_1$-spectrum of A cannot be equal to a non-degenerate union of two cones.

We also discuss other properties of $\Sigma_n$-spectra and related open question.

[1] Uri Andrews, Joseph S. Miller, Spectra of theories and structures, to appear in the Proceedings of the American Mathematical Society.

ABSTRACT. This talk reports on an application of proof mining to the asymptotic behavior of Ishikawa iterations for nonexpansive mappings \cite{Leu14,Leu10}. {\em Proof mining} is a paradigm of research concerned with the extraction, using proof-theoretic methods, of finitary content from mathematical proofs. This research direction can be related to Terence Tao's proposal \cite{Tao07} of {\em hard analysis}, based on finitary arguments, instead of the infinitary ones from {\em soft analysis}.

We present uniform effective rates of asymptotic regularity for the Ishikawa iteration associated to nonexpansive self-mappings of convex subsets of uniformly convex Busemann geodesic space. We show that these results are obtained by a logical analysis of an asymptotic regularity proof due to Tan and Xu \cite{TanXu93}, consisting of two main steps: the first one with a classical proof, analyzed using the combination of monotone functional interpretation and negative translation, while the second one has a constructive proof, analyzed more directly using monotone modified realizability. As a consequence, our results are guaranteed by a combination of logical metatheorems for classical and semi-intuitionistic systems, proved by Gerhardy and Kohlenbach \cite{GerKoh06,GerKoh08} for different classes of spaces and adapted to uniformly convex Busemann spaces in \cite{Leu14}.

\begin{thebibliography}{10}

\bibitem{GerKoh06} {\scshape P. Gerhardy, U. Kohlenbach}, {\itshape Strongly uniform bounds from semi-constructive proofs}, {\bfseries\itshape Annals of Pure and Applied Logic}, vol.~141 (2006), pp.~89--107.

\bibitem{GerKoh08} {\scshape P. Gerhardy, U. Kohlenbach}, {\itshape General logical metatheorems for functional analysis}, {\bfseries\itshape Transactions of the American Mathematical Society}, vol.~360 (2008), pp.~2615--2660.

\bibitem{Leu10} {\scshape L. Leu\c{s}tean}, {\itshape Nonexpansive iterations in uniformly convex $W$-hyperbolic spaces}, {\bfseries\itshape Nonlinear Analysis and Optimization I: Nonlinear Analysis} (A. Leizarowitz, B. S. Mordukhovich, I. Shafrir, A. Zaslavski, editors), Amer. Math. Soc., Providence, RI, 2010, pp.~193--209.

\bibitem{Leu14} {\scshape L. Leu\c{s}tean}, {\itshape An application of proof mining to nonlinear iterations}, {\bfseries\itshape arXiv:1203.1432v1 [math.FA]}, 2012; accepted for publication in Annals of Pure and Applied Logic.

\bibitem{TanXu93} {\scshape K.-K. Tan, H.-K. Xu}, {\itshape Approximating fixed points of nonexpansive mappings by the Ishikawa iteration process}, {\bfseries\itshape J. Math. Anal. Appl.}, vol.~178 (1993), pp.~301--308.

\bibitem{Tao07} {\scshape T. Tao}, {\itshape Soft analysis, hard analysis, and the finite convergence principle}, 2007, available on terrytao.wordpress.com/2007/05/23/soft-//analysis-hard-analysis-and-the-finite-convergence-principle/.

\end{thebibliography}

ABSTRACT. This work in progress is joint with Emanuele Frittaion, Matthew Hendtlass, Paul Shafer, and Jeroen Van der Meeren.

If $(Q,{\leq_Q})$ is a quasi-order we can equip $Q$ with several topologies. We are interested in the Alexandroff topology $A(Q)$ (the closed sets are exactly the downward closed subsets of $Q$) and the upper topology $u(Q)$ (the downward closures of finite subsets of $Q$ are a basis for the closed sets). $A(Q)$ and $u(Q)$ are (except in trivial situations) not $T_1$, yet they reflect several features of the quasi-order. For example, $(Q,{\leq_Q})$ is a well quasi-order (WQO: well-founded and with no infinite antichains) if and only if $A(Q)$ is Noetherian (all open sets are compact or, equivalently, there is no strictly descending chain of closed sets). Moreover, if $(Q,{\leq_Q})$ is WQO then $u(Q)$ is Noetherian.

Given the quasi-order $(Q,{\leq_Q})$, we consider two natural quasi-orders on the powerset $\mathcal{P}(Q)$:

\begin{align*}

A \leq^\flat B \iff & \forall a \in A\, \exists b \in B\, a \leq_Q b; \\

A \leq^\sharp B \iff & \forall b \in B\, \exists a \in A\, a \leq_Q b.

\end{align*}

We write $\mathcal{P}^\flat(Q)$ and $\mathcal{P}^\sharp(Q)$ for the resulting quasi-orders, and $\mathcal{P}_f^\flat(Q)$ and $\mathcal{P}_f^\sharp(Q)$ for their restrictions to the collection of finite subsets of $Q$.

Goubault-Larrecq proved that if $(Q,{\leq_Q})$ is WQO then $u(\mathcal{P}^\flat(Q))$ and $u(\mathcal{P}_f^\sharp (Q))$ are Noetherian, even though $\mathcal{P}^\flat(Q)$ and $\mathcal{P}_f^\sharp (Q)$ are not always WQOs.

We study these theorems and some of their consequences from the viewpoint of reverse mathematics, proving for example: \begin{itemize}

\item over $\mathsf{RCA}_0$, $\mathsf{ACA}_0$ is equivalent to each of \lq\lq if $(Q,{\leq_Q})$ is WQO then $u(\mathcal{P}^\flat(Q))$ is Noetherian\rq\rq, and \lq\lq if $(Q,{\leq_Q})$ is WQO then $A(\mathcal{P}_f^\flat(Q))$ is Noetherian\rq\rq;

\item $\mathsf{ACA}_0$ proves \lq\lq if $(Q,{\leq_Q})$ is WQO then $u(\mathcal{P}_f^\sharp(Q))$ is Noetherian\rq\rq, yet $\mathsf{WKL}_0$ does not.

\end{itemize}

ABSTRACT. Cantor's Diagonal Argument came out of his third proof for the uncountability of the set of real numbers (see e.g. \cite{franks}). Unlike the first and second proofs, the diagonal argument can also show the non-equinumerosity of a set with its powerset. In modern terms the proof is as follows: for a function $F\!:\!A\!\rightarrow\!\mathscr{P}(A)$, where $\mathscr{P}(A)\!=\!\{B\mid B\subseteq A\}$ is the powerset of $A$, the anti-diagonal set $D_F=\{a\!\in\!A\mid a\not\in F(a)\}$ is not in the range of $F$ because if it were, say $D_F=F(\alpha)$, then $\alpha\!\in\!D_F\leftrightarrow \alpha\not\in F(\alpha)\leftrightarrow\alpha\not\in D_F$ contradiction. This argument shows up also in Russell's Paradox, the set of sets which do not contain themselves, $R=\{x\mid x\not\in x\}$, and in Turing's non-recursively-enumerable set $\overline{K}=\{n\in \mathbb{N}\mid n\not\in W_n\}$ where $W_n$ is the domain of the $n^{\rm th}$ recursive function $\varphi_n$ (i.e., $W_n=\{x\!\in\!\mathbb{N}\mid \exists y: \varphi_n(x)=y\}$) by which one can show the algorithmic unsolvability of the halting problem (of a given algorithm on a given input). There are, in fact, many other instances of the diagonal arguments in wide areas of mathematics from logic and set theory to computability theory and theory of computational complexity.

In this talk, we examine this argument in more detail and discuss some other proofs (e.g. \cite{raja1,raja2}) of Cantor's theorem (on the non-equinumerosity of a set with its powerset). By introducing a generalized diagonal argument, we show that all other proofs should fit in this generalized form, which is roughly as follows: for a function $g:A\rightarrow A$ the generalized anti-diagonal set $D_F^g=\{g(a)\mid g(a)\not\in F(a) \}$ is not in the range of $F$ because if it were, say $D_F^g=F(\alpha)$, then $g(\alpha)\in D_F^g\leftrightarrow g(\alpha)\not\in F(\alpha) \leftrightarrow g(\alpha)\not\in D_F^g$ contradiction. For the argument to go through, the function $g$ should satisfy some conditions; and we will prove that every subset of $A$ (say $B\subseteq A$) that is not in the range of $F$ (for all $a\in A$, $B\not=F(a)$ holds) should somehow be in this generalized anti-diagonal form ($B\cap g[A]=D_F^g$) for some suitable function $g$ which satisfies those conditions; cf. \cite{dekker,horowitz}. We will argue that this provides a characterization for diagonal proofs and indeed characterizes the objects whose existence are proved by a kind of diagonal(izing out) argument.

\bibitem{dekker}{\scshape Jacob C. E. Dekker}, {\itshape Productive Sets}, {\bfseries\itshape Transactions of the American Mathematical Society}, vol.~78 (1955), no.~1, pp.~129--149.

\bibitem{franks}{\scshape John Franks}, {\itshape Cantor's Other Proofs that $\mathbb{R}$ is Uncountable}, {\bfseries\itshape Mathematics Magazine}, vol.~83 (2010), no.~4, pp.~283--289.

\bibitem{horowitz}{\scshape Bruce M. Horowitz}, {\itshape Sets Completely Creative via Recursive Permutations}, {\bfseries\itshape Zeitschrift f\"{u}r Mathematische Logik und Grundlagen der Mathematik}, vol.~24 (1978), no.~25--30, pp.~445--452.

\bibitem{raja1}{\scshape Natarajan Raja}, {\itshape A Negation-Free Proof of Cantor's Theorem}, {\bfseries\itshape Notre Dame Journal of Formal Logic}, vol.~46 (2005), no.~2, pp.~231--233.

\bibitem{raja2}{\scshape Natarajan Raja}, {\itshape Yet Another Proof of Cantor's Theorem}, {\bfseries\itshape Dimensions of Logical Concepts} (Jean-Yves B\'{a}ziau and Alexandre Costa-Leite, editors), Cole\c{c}\~{a}o CLE: Volume 54, Campinas, Brazil, 2009, pp.~209--217.

ABSTRACT. Goedel's Completeness Theorem is one of the most fundamental results in mathematical logic. When formalized in arithmetic, it is often referred to as the Arithmetized Completeness Theorem (ACT). The ACT is a surprisingly powerful machinery for constructing nonstandard models of arithmetic. For instance, it has been known [1, 2] that "all possible kinds" of extensions of a model of Peano arithmetic can, in a sense, be realized using the ACT. We find new applications of the ACT in the context of second-order arithmetic. These include an alternative proof of Harrington's theorem [3] that WKL0 is Pi11-conservative over RCA0.

[1] Kenneth Mc Aloon, Completeness theorems, incompleteness theorems and models of arithmetic, Transactions of the American Mathematical Society, vol. 239 (1978), pp. 253-277.

[2] James H. Schmerl, End extensions of models of arithmetic, Notre Dame Journal of Formal Logic, vol. 33 (1992), no. 2, pp. 216-219.

[3] Stephen G. Simpson, Subsystems of Second Order Arithmetic, Perspectives in Logic, Cambridge University Press, 2009.

ABSTRACT. Some properties of Intuitionistic Set Theory with the principle UP.

Let ZFI2C be usual intuitionistic Zermelo-Fraenkel set theory in two-sorted language (where sort 0 is for natural numbers, and sort 1 is for sets).

Axioms and rules of the system are: all usual axioms and rules of intuitionistic predicate logic,intuitionistic system of arithmetic,and all usual proper axioms and schemes of Zermelo-Fraenkel set theory for variables of sort 1,namely, axioms of Extensionality, Infinity, Pair, Union, Power set, Infinity, and schemes: Separation, Transfinite Induction as Regularity, and Collection as Substitution.

It is well-known that both ZFI2C and ZFI2C+DCS(where DCS is a well-known principle Double Complements of Sets) have some important effectivity properties: disjunction property, numerical existence property (but not full existence property!) and also that the Markov Rule,the Church Rule,and the Uniformization Rule are admissible in it. Such reach collection of properties shows that these theories are sufficiently constructive theories.

On the other hand, ZFI2C+ DCS contains the classical theory ZFI2C = ZFI2C+LEM) in the sense of Godel negative translation. Moreover, a lot of important mathematical reasons may be formalized in ZFI2C+DCS, so,we can formalize and decide in it a lot of informal problems about transformation of a classical reason into intuitionistical proof and extraction of some exact description of a mathematical object from some proof of it`s existence.

So, the theory ZFI2C+DCS can be considered as a basic system of Intuitionistic Set Theory. We can extend it by a some well-known intuitionistic principles, such that Markov Principle M, Extended Church Principle ECT, and the Principle UP.

It is well-known that both theories ZFI2C+DCS+M+ECT, and ZFI2C+DCS+M has the same effectivity properties as ZFI2C+DCS. It is known also that ZFI2C+DCS+M+ECT is conservative over the theory ZFI2C+DCS+M w.r.t. the class A.E.N. of all AE-formulae over arithmetical negative (in the usual sense). We also prove that ZFI2C+M+ ECT is conservative over the theory ZFI2C+M.

The Principle UP is a well-known specifical intuitionistic principle. It claims that we cannot define effectivly non-trivialfunction from sets to natural numbers.It has been studed in intuitionistic type theory very closely.

In the article we prove that ZFI2C+ DCS+ M+ CT+UP is conservative over the theory ZFI2C+DCS+M w.r.t. the same class A.E.N.

Of course, we also prove that ZFI2C+M+ECT is conservative over the theory ZFI2C+M w.r.t. of the same class A.E.N.

We also prove that theories ZFI2C+DCS+M+CT+UP, ZFI2C+DCS+M+UP, ZFI2C+ DCS+ UP, and ZFI2C+UP have the same effectivity properties as ZFI2C and ZFI2C+DCS.

ABSTRACT. In recent literature, the theory of computably enumerable equivalence relations (ceers) has been widely investigated (see, for instance, [1], [2]). One of the most fruitful approaches is to study them considering the degree structure generated by the following reducibility: Given two ceers R and S, we say that R is reducible to S (R<S) if there is a computable function f s.t., for every x,y, xRy iff f(x)Sf(y). In this talk, we propose to make use of this reducibility within a more general context than that of ceers, namely in the study of (simply undirected) c.e. graphs. Our presentation is divided in two parts. Firstly, we focus on computable graphs. While the theory of computable equivalence relations is quite trivial [1], in this context the situation is more complicate. We provide a partial characterization for the computable case. Secondly, we move to universal graphs. We offer a natural, yet not trivial, example of an universal graph U. More generally, recall that there is a unique random graph RG s.t. every countable graph G can be embedded as an induced subgraph of RG ([3]). This fact depends on a specific property (*) of RG (see [3]) for the definition of (*). Hence, it is natural to ask for some analogue of (*) in our context -- specially after noticing that (*) fails for U. We discuss several candidates for this role.

[1] U. Andrews, S. Lempp, J. S. Miller, K. M. Ng, L. San Mauro, A. Sorbi, Universal computably enumerable equivalence relations, Journal of Symbolic Logic, to appear

[2] S. Gao, P. Gerdes, Computably Enumerable Equivalence Relations, Studia Logica, February 2001, Volume 67, Issue 1, pp 27-59 vol.~67 (2001), no.~1, pp.27--59.

[3] P. Cameron, The random graph, The Mathematics of Paul Erd\"os, II (2nd ed.)} (R. L. Graham, J. Nešetřil and S. Butler, ed.), Springer, Publisher's address, 2013, pp.353--378.

ABSTRACT. We investigate the order dimensions of several degree structures such as Turing degree structure. It may be nice if we can decompose a given degree structure into "simpler" partial orders naturally defined for the structure. Indeed, it is known that every partial order is embeddable into the product order of a family of linear orders. The order dimension of a given partial order is defined as the least cardinality of such a family. Thus, the order dimension of a degree structure tells us how many linear orders at least we should have so that the degree structure is embeddable into the product order of those linear orders. The concept "order dimension" was introduced by Dushnik and Miller in 1941, and it is also called Dushnik-Miller dimension. As our main results on the order dimensions of degree structures, this talk includes the following results: the order dimension of Turing degree structure is uncountable and at most the cardinality of the continuum; the order dimension of Muchnik degree structure is the cardinality of the continuum; and the order dimension of Medvedev degree structure is lying between the cardinality of the continuum and the cardinality of the power set of the continuum.

ABSTRACT. The talk will cover some recent results about computable numberings in Ershov hierarchy

ABSTRACT. Davies-trees are special sequences of countable elementary submodels which played important roles in generalizing arguments using the Continuum Hypothesis to pure ZFC proofs. The most notable application of this technique is probably Jackson and Mauldin's solution to the Steinhaus tiling problem.

The aim of this talk is to introduce Davies-trees and to point out several new applications in infinite combinatorics. Such include simple proofs to the following results: the plane is the union of n+2 "clouds" provided that the continuum is at most aleph_n; every uncountably chromatic graph contains k-connected uncountably chromatic subgraphs for each finite k (both results are due to Komjath).

Our belief is that Davies-trees did not get their well deserved attention despite the fact that they provide an easily applicable tool for logicians and set theorists.

ABSTRACT. We investigate a series of axioms, which capture the combinatorial core of the Mathias model. These axioms are formulated in terms of games with Borel sets and functions, without explicitly refering to forcing. In this way we derive a descriptive set theoretical axiomatization of the Mathias model. We consider some properties of this model, in particular values of cardinal coefficients. We derive them directly from our axioms. Although we concentrate on the Mathias model, our methods are more general. One can produce an analogous axiomatization of other models obtained by the iteration of suitably definable proper forcing.

ABSTRACT. We introduce a variant of Martin's axiom, called the grounded Martin's axiom or grMA. This principle asserts that the universe is a ccc forcing extension and that MA holds for posets from the ground model. The new axiom, which emerges naturally from the analysis of the Solovay-Tennenbaum proof of the consistency of MA, is shown to have many of the desirable properties of the weaker fragments of MA. In particular, we show that grMA is consistent with a singular continuum and also that it is consistent with the left side of Cichoń's diagram collapsing to omega_1. We also show that grMA is better behaved than MA when adding generic reals. Specifically, grMA is preserved under adding a Cohen real and holds after adding a random real to a model of MA.

ABSTRACT. An elementary epimorphism $f : M \rightarrow N$ (between model-theoretic structures in some language) is a homomorphism such that, for every formula $\phi$ in the language with parameters $n_1, \ldots , n_k$ from $N$ true in $N$, there are $f$-pre-images $m_1, \ldots , m_k$ of the $n_i$'s such that $\phi(m_1, \ldots , m_k)$ holds in $M$. Here we investigate elementary epimorphisms between models of set theory. We show that the only $\Pi_1$-elementary epimorphisms between models of ZF are isomorphisms. In contrast, there are non-trivial $\Sigma_1$-elementary epimorphisms, and non-trivial (full) elementary epimorphisms between models of ZFC$^-$ (ZFC without Power Set). Furthermore, we study the inverse system induced by the last example, and its inverse limit. Inverse limits do not always exist, and even when they do they might not be the entire thread class, but in this case it is.

ABSTRACT. The generic ultrafilter $\mathcal{G}_2$ forced by the partial ordering $\mathcal{P}(\omega\times\omega)/(\mathrm{Fin}\times\mathrm{Fin})$ is a non-p-point which is also not a Fubini product of p-points, but is a Rudin-Keisler immediate successor of its projected Ramsey ultrafilter. In \cite{BDR}, it was shown that $\mathcal{G}_2\not\ge_T[\omega_1]^{<\omega}$, and hence is below the maximum Tukey type for ultrafilters, yet it is not basically generated. In \cite{D}, we show that, in fact, $\mathcal{G}_2$ is a Tukey immediate successor of its projected Ramsey ultrafilter, and moreover, the projected Ramsey ultrafilter is the only nonprincipal ultrafilter with Tukey type strictly below that of $\mathcal{G}_2$. This is done by showing that $\mathcal{P}(\omega\times\omega)/(\mathrm{Fin}\times\mathrm{Fin})$ contains a dense subset which in fact forms a topological Ramsey space and then proving a Ramsey-classification theorem for equivalence relations on fronts. Moreover, we generalize this to show that for all $2\le k<\omega$, $\mathcal{P}(\omega^k)/\mathrm{Fin}^{\otimes k}$ is forcing equivalent to a new topological Ramsey space $\mathcal{E}_k$ which is a generalization of the Ellentuck space. The generic ultrafilters $\mathcal{G}_k$ are non-p-points which have exactly $k$ Tukey predecessors, as well as exactly $k$ Rudin-Keisler predecessors.

 [BDR] Andreas Blass, Natasha Dobrinen, Dilip Raghavan, The next best thing to a p-pint, Submitted.

[D] Natasha Dobrinen, High dimensional Ellentuck spaces and initial chains in the Tukey structure of non-p-points, Submitted.

ABSTRACT. We consider a variant of the Rudin-Keisler order for ideals on $\omega$ and prove the existence of a complete co-analytic ideal with respect this order. The key tool is a parameterization of all co-analytic ideals. We obtain this parameterization via a method which yields a simple proof of Hjorth's 1996 theorem on the existence of a complete co-analytic equivalence relation. Unlike Hjorth's proof, ours does not rely on the use of the effective theory specific to $\Pi^1_1$ sets and thus generalizes under PD to other projective classes.

ABSTRACT. We define budding trees, show that they form a topological Ramsey space, and discuss applications.

ABSTRACT. Consider a first-order language L. For any L-formula alpha, let #alpha stand for the Gödel number of alpha. An L-theory T is finitely inseparable if and only if there is a recursive function f such that for any two disjoint recursively enumerable sets A and B such that {#alpha: alpha is a valid sentence in L} is included in A and {#alpha: alpha is an L-sentence refuted by some finite model of T} is included in B, f(a, b)does not belong to A union B, where a and b are indices of A and B respectively. It is easy to see that finite inseparability implies undecidability and the former is strictly stronger than the latter. Let C be a binary predicate and I will show the finite inseparability of the theory axiomatized by the following three axioms: (1) For all x (Cxx); (2) For all x, for all y(if Cxy, then Cyx); (3) For all x, for all y(if(Cxy and not x=y), then for some z(Cxz and not Cyz)). Making use of the said result, I will also show the finite inseparability of the theory axiomatized by (1), (2), (4) For all x, for all y (if for all z(Cxz iff Cyz), then x=y) and (5) For any formula alpha, if there is some x such that alpha, then there is some y such that for all z(Cyz iff there is some u such that alpha and Cuz). The foregoing theory contains exactly the mereological part and the quasi-Boolean part of Clarke’s system. There is still one more part of Clarke’s system, that is, the quasi-topological part. It is still unknown whether the full Clarke’s system is finitely inseparable or not. However, such a system does have finite models and some of them are of a peculiar kind. Based on this observation, I conjecture that the full Clarke’s system is also finitely inseparable.

ABSTRACT. We say a structure M in a first order language L is indivisible if for every colouring of its universe M in two colours, there is a monochromatic substructure M′ ⊆ M such that M′ ≅ M. Additionally, we say that M is symmetrically indivisible if M′ can be chosen to be symmetrically embedded in M (That is, every automorphism of M′ can be can be extended to an automorphism of M), and that M is elementarily indivisible if M′ can be chosen to be an elementary substructure.

The notion of indivisibility is a long-studied subject. We will present these strengthenings of the notion, examples and some basic properties. We will define a new "product" of structures which preserves these notions along with other nice properties, and use it to answer some questions presented in [HKO11] regarding the properties and interaction between these notions. In particular: Does elementary indivisibility imply symmetric indivisibility? Is an elementarily indivisible structure neccesarily homogeneous? If M is symmetrically indivisible and L₀⊆L, is M reduced to L₀ symmetrically indivisible?

[HKO11] Assaf Hasson, Menachem Kojman and Alf Onshuus, On symmetric indivisibility of countable structures, Model Theoretic Methods in Finite Combinatorics, AMS, 2011, pp.417–452.

ABSTRACT. This talk will present a necessary and sufficient condition for Cantor's Forth construction to yield an onto mapping in terms of a new ordinal rank. We will emphasise that the rank is derived from a combination of a smallest and a greatest fixpoint (of monotone operators). We will also highlight the existence of homogeneous structures for all possible countable ordinal ranks, with a construction using unions of wreath powers.

ABSTRACT. A group $G$ is called {\bf amenable} if every $G$-flow (i.e. a compact Hausdorff space along with a continuous G-action) supports an invariant Borel probability measure. If every $G$-flow has a fixed point then we say that $G$ is {\bf extremely amenable}. Let $M$ be a relational countably categorical structure which is a Fra\"{i}ss\'{e} limit of a Fra\"{i}ss\'{e} class $\mathcal{K}$. To see whether $Aut(M)$ is amenable one usually looks for an expansion $M^*$ of $M$ so that $M^*$ is a Fra\"{i}ss\'{e} structure with extremely amenable $Aut(M^* )$. Moreover it is usually assumed that $M^*$ is a {\bf precompact} expansion of $M$, i.e. every member of $\mathcal{K}$ has finitely many expansions in $Age(M^* )$. Some theorems of O.Angel, A.Kechris, R.Lyone and A.Zucker describe amenability of $Aut(M)$ in this situation. It is a basic question in the subject if there is a countably categorical structure $M$ with amenable automorphism group which does not have expansions as above.

We connect this material with the property of existence of nice enumerations, introduced by G.Ahlbrandt and M.Ziegler in 1986. We also give some interesting examples of countably categorical structures $M$ so that $Aut(M)$ is amenable, but $M$ does not have order expansions with extremely amenable automorphism groups.

ABSTRACT. Theorem. Let n > 2. The n-variable fragment of first-order logic does not have the weak Beth definability property (wBDP). Moreover, there are a theory and a strong implicit definition of a unary relation D for this theory such that there is no explicit definition for D even in the n-variable fragment with infinite conjunctions and disjunctions, not even if we restrict the models to the finite ones. Neither the theory nor the implicit definition use substitution of variables.

Failure of wBDP for n = 4 was not known, failure for n greater than 4 was proved by Ian Hodkinson, and for n = 3 by Andras Simon. The present proof is considerably simpler than theirs. Beth definability property fails for the 2-variable fragment L2, and it holds for the n-variable fragment if we restrict the sizes of the models to < n + 2 (for all n greater than 1). We conjecture that wBDP holds for L2. If so, L2 is a natural logic distinguishing Beth definability property from wBDP.

ABSTRACT. A clone on a set $A$ is a set of finitary functions on $A$ that includes the projection functions and is closed for composition. It is called a clone with constants when it contains all the constant functions on $A$. Every truth-functional propositional language determines the clone generated by the interpretation of its operator symbols. If we consider propositional languages interpreted with a three-valued truth-functional scheme, the clones generated by the weak and strong Kleene operators are specially interesting, because Kleene logics have been applied to the study of several fields, like partial predicates, semantical paradoxes, vagueness, the semantics of programming languages, etc.

The clone with constants generated by the weak Kleene propositional operators and the constant functions will be called the weak Kleene clone and analogously for the strong Kleene clone. It is well known that the strong Kleene clone coincides with the clone of three-valued functions monotonic on the order of information (i.e., the partial order on ${0,1,2}$ determined by $2\leq 0$, $2\leq 1$). The aim of this paper is to determine all the clones that are extensions of the weak Kleene clone but are not included in the strong Kleene clone. Equivalently, this amounts to the characterization of all the clones that can be obtained when we add to the weak Kleene clone a set of functions that include some function non-monotonic on the order of information. Using Jablonskij's theorem that determines all three-valued maximal clones and Lau's theorem that characterizes all the three-valued submaximal clones (see \cite{Lau}, II5 and II14), it is easy to check that only two maximal clones ($C_{2}$ and $U_{2}$) and three submaximal clones (one of them being the strong Kleene clone) contain the weak Kleene clone. The paper will determine completely all the clones in the interval between the weak Kleene clone and $U_{2}$ and all the clones between the weak Kleene clone and $C_{2}$ that are not contained in the strong Kleene clone.

ABSTRACT. In this talk I will present some properties of the universe of sets from the perspective of a particular sheaf topos, which I call the random topos. This is a boolean topos, hence a model of classical set theory, whose properties make it a natural home for developing a version of probability theory based on random elements.

An important feature of the topos is a fundamental notion of independence. This gives rise to a canonical definition of random element: an element (e.g., from the interval [0,1]) is defined to be random if it is contained in all measure 1 subsets that are indpendent of it. This definition can be used to support the development of theories of probability and measure, in which all sets are measurable (though not necessarily Lebesgue measurable), and measures are kappa-additive for any aleph, kappa. (Of course the Axiom of Choice fails, though Dependent Choice holds.)

The above results closely mirror work of van Lambalgen from 1992. However, our approach differs from his in two main respects. The first is that our model is a sheaf topos built over a site of probability spaces. Because of this, statements about randomness get translated, by Kripke-Joyal semantics in the topos, into statements in standard (Kolmogorov-style) probability theory. Second, the notion of independence that we use can be understood prior to and separately from the definition of randomness. Independence in our sense corresponds roughly to "no information in common''. In contrast, van Lambalgen's notion of independence has a definition of randomness built into it.

ABSTRACT. In our ordinary life it is inevitable for everyone has to adjust one's own belief state in light of new information when the new information is inconsistent with his belief state. Some philosophers such as Quine and AGM (Alchourrόn et al.) suggested that the loss of information value should be minimized as possible whenever one confronts the inconsistency and the principle in belief revision theory is usually so-called information economy principle (IEP for short). Furthermore, Gärdenfors has constructed a model who recommended the idea of epistemic entrenchment to this model to explain why IEP works. But Rott casted some doubts on IEP due to the postulates of epitemic entrenchment proposed by Gärdenfors sometimes failed to realize the features of nonmonotonic reasoning, i.e. it is possible that one might keep the less entrenched beliefs rather than the more ones in the process of belief change. In this paper, I want to present a game-theoretic framework to reconstruct the notion of epistemic entrenchment to avoid the challenges from Rott and prove that IEP is still available to be the norm to estimate the process of belief change.

ABSTRACT. We examine the prospects for a na\"ive theory of classes, in which full ``na\"ive'' comprehension and an extensionality rule are maintained by weakening the background logic. Without extensionality, proving na\"ive comprehension consistent is formally analogous to proving na\"ive truth consistent, and in recent years much progress has been made on the latter question. But there is no natural analog for extensionality in the case of truth, so the question arises whether these logics for reasoning about truth can also be shown consistent with a form of extensionality. In a series of papers, and in his 2006 book (\cite{brady2006}), Ross Brady has presented various theories of na\"ive classes. We begin by providing a simpler, more accessible version of Brady's proof of the consistency of these theories. Our new presentation of Brady then makes it easy to see how Brady's result can be generalized to apply to certain logics which have a modal-like semantics given using four-valued, as opposed to three-valued worlds. (These include some logics from \cite{bacon2013}.) These ``new'' logics have a significant advantage over Brady's original: they validate a weakening rule (indeed, a weakening axiom) for a non-contraposable conditional. Since these laws are crucial if the conditional is to be used for restricted quantification, this is a substantial improvement.

Still, we do not think even these logics are satisfactory. The non-contraposable conditional which validates weakening in these logics is not the conditional of the extensionality rule. But there's strong intuitive motivation for the conditional in the extensionality rule to validate weakening. Otherwise, there will be ``sets'' which contain everything, but which are not extensionally equivalent. While Brady's logics (and the four-valued generalizations) deliver a form of extensionality, in the absence of weakening the formal rule does not capture the intuitive notion of extensionality.

ABSTRACT. Some positive applications of the counterexamples of Robinson property on the characterization of Interpolation and Compactness properties

ABSTRACT. Methods of topological dynamics have been introduced to model theory by Newelski and since then saw further development in that field by other authors. Given a model $M$ with all types over $M$ definable and a definable group $G$, we consider the category of definable flows. This category has a universal object $S_G(M)$, the space of types in $G$ over $M$. It is shown that the Ellis semigroup of this flow is isomorphic to $S_G(M)$ itself. It can be considered as a model-theoretic equivalent to $\beta G$, the large compactification of $G$.

In the talk I will describe the results from my paper that give a description of definable topological dynamics of a large class of groups interpretable in an $o$-minimal expansion of the field of reals along with their universal covers interpreted in a certain two-sorted structure. The results provide a wide range of counterexamples to a question by Newelski whether the Ellis group of the universal definable $G$-flow is isomorphic to $G/G^{00}$ and generalize methods from used by Gismatullin, Penazzi and Pillay that provided a particular counterexample.

ABSTRACT. A Polish structure  is a pair $(X,G)$, where $G$ is a Polish group acting faithfully on a set $X$ so that the stabilizers of all singletons are closed subgroups of $G$ (this definition comes from K. Krupiński).

Notice that, in the above definition, it is not required that $X$ is a topological space. I will discuss some issues concerning existence of topologies on $X$ satysfying some natural conditions. Special attention will be given to the case in which $X$ carries a structure of a group (i. e., $(X,G)$ is a Polish group structure).

ABSTRACT. In this talk we present that the general concept of formal inconsistencies can be well-developed for any given semantics $\models$ (no matter it is truth functional or not). Note that the concept negation is not a necessary part in our treatment. In this theory of formal inconsistencies, there are two important concepts, model existence property (i.e., w.r.t.~the given inconsistency, every consistent set has a model with respect to $\models$) and explosiveness property (i.e., w.r.t.~the given inconsistency, every inconsistent set is also absolutely inconsistent). Now given a semantics $\models$, it will generate a set of inconsistencies, say, $Ins_{\models} =\{I_i,\dots\}$. If a $\models$-sound proof system $L$ has both model existence property and explosiveness for some inconsistency $I\in Ins_{\models}$, then all inconsistencies in $Ins_{\models}$ are provably equivalent in $L$. \par Then it is natural to ask, for the classical semantics, whether there are incompactible paraconsistencies in the following sense, i.e., are there two inconsistencies $I_1, I_2$ (generated from classical semantics) such that there are classically sound proof systems $L_1, L_2$ such that in $L_1$ it has $I_1$ model existence and $I_2$ explosiveness but not $I_1$ explosiveness and not $I_2$ model existence. And in $L_2$ it has $I_2$ model existence and $I_1$ explosiveness but not $I_2$ explosiveness and not $I_1$ model existence. We will prove that the answer is positive, which shows that there are incompatible paraconsistencies.