ABSTRACT. In this talk I will discuss about the reflection and non-reflection of the property ``of coloring number bigger than a cardinal kappa'' of graphs and the connection of them to some other reflection statements.

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. Schreier families on countable index sets have been used in Banach space theory to study asymptotic objects and ranks of compacity. We will present a generalization of these objects to the uncountable setting and some applications to nonseparable Banach spaces, which can be found in a joint work with Jordi Lopez-Abad and Stevo Todorcevic. Our methods to built such families in all cardinals below the first Mahlo cardinal involve Ramsey theory and a deep combinatorial analysis of families on trees.

ABSTRACT. In Kripke Platek Set Theory (KP), every monotone, set-bounded Sigma_1-operator has a Sigma_1-definable least fixed point. Hence Sigma_1-separation is strong enough to prove that the least fixed point is actually a set. To the aim of understanding the relation between these two principles, we perform an analysis of some distinct fixed-points-statements over KP.

ABSTRACT. aa

ABSTRACT. A well-ordering principle of type one consists of a construction which transforms linear orders into linear orders, together with the assertion that well-foundedness is preserved. It is known that many second order axioms of complexity Pi^1_2 (e.g. arithmetical comprehension, arithmetical transfinite recursion) are equivalent to natural well-ordering principles of type one. Montalbán and Rathjen have conjectured that Pi^1_1-comprehension, which is a Pi^1_3-statement, corresponds to a well-ordering principle of type two: one that transforms each well-ordering principle of type one into a well-order. I will present recent progress towards this conjecture.

ABSTRACT. We reason in different ways on different occasions. Sometimes it is suitable to reason classically, sometimes constructively and sometimes paraconsistently. We might insist on, prefer, be trained in, or find familiar, some forms of reasoning. Each form will enjoy its own suite of formal representations. Some formal representations are clearly extensions of others, for example, we can add modal operators to classical propositional logic. But sometimes we are called upon to reason in a way that is to-our-lights: incorrect, unfamiliar, disagreeable or perverse; call these ‘abhorrent’ for short. At such times, to allay the threat of incorrectness, triviality, or absurdity, we reason hypothetically, or “in quotation marks”. We compartmentalise the reasoning in some way. The tractable technical question is how to formally represent how we do this in such a way as to ultimately fend from whatever we find abhorrent. The deeper, philosophical question is how to understand what it is that we are doing when in the process of orchestrating such reasoning. After all, it is only later that we model such reasoning using a formal or semi-formal representation that re-constructs the reasoning to show that it was legitimate.

ABSTRACT. Ever since the sophisticated analysis provided by David Lewis, counterfactuals have been a challenge to logicians, because they were shown to escape both the traditional truth-valued semantics and the standard possible worlds semantics. Lewis' semantics will be here generalized and shown capable of covering, in a modular way, all the systems for counterfactuals presented in Lewis (1973). On its basis, and along the methodology of Negri (2017), proof systems are developed that feature a transparent justification of their rules Negri (2017a), good structural properties, analyticity, direct completeness and decidability proofs (Negri and Sbardolini, 2016, Negri and Olivetti, 2015, Girlando et al., 2017).

References

Girlando, M., S. Negri, N. Olivetti (2017) Labelled sequent calculi based on neighbourhood semantics for PCL and its extensions, ms.

Lewis (1973) Counterfactuals. Routledge.

Negri, S. (2017) Proof theory for non-normal modal logics: The neighbourhood formalism and basic results. IfCoLog Journal of Logics and their Applications, vol. 4, pp. 1241-1286.

Negri, S. (2017a) Non-normal modal logics: a challenge to proof theory. In P. Arazim and T. Lávička (eds) The Logica Yearbook 2016, College Publications.
 

Negri, S. and N. Olivetti (2015) A sequent calculus for preferential conditional logic based on neighbourhood semantics. In H. De Nivelle (ed) Automated Reasoning with Analytic Tableaux and Related Methods, Lecture Notes in Computer Science, vol. 9323, Springer, pp. 115-134.

Negri, S. and G. Sbardolini (2016) Proof analysis for Lewis counterfactuals. The Review of Symbolic Logic, vol. 9, pp.44-75.

ABSTRACT. Penelope Maddy's naturalistic approach to philosophy of mathematics aims to explain why the research community embraces some candidates for axiomatic foundations of mathematics and rejects others. In \cite{maddy}, she argued that since set theory aims to be a foundation for mathematics, it should conform to the methodological maxim \textsc{maximize} and therefore, axiomatic set theories that are \emph{restrictive} ought to be rejected. She then went on to define a formal notion of restrictiveness, based on a fixed class of interpretations. In \cite{first,second,Joel}, this notion was discussed and a number of technical and substantial issues were raised. Following \cite{IL}, this talk will present the general framework for interpretations and their derived notions of restrictiveness and then go on to discuss a \emph{symmetrised} version of Maddy's original notion that takes both inner model and outer model constructions into account and can deal with the substantial issues raised in \cite{second}.

ABSTRACT. Work on proving consistency of the intensional Martin-Lof type theory with a sequence of univalent universes (“MLTT+UA”) led to the understanding that in type theory we do not know how to construct an interpretation of syntax from a model of inference rules. That is, we now have the concept of a model of inference rules and the concept of an interpretation of the syntax and a conjecture that implies that the former always defines the latter. This conjecture, stated as the statement that the syntactic model is an initial object in the category of all models of a given kind, is called the Initiallity Conjecture. In my talk I will outline the various parts of this new vision of the theory of syntax and semantics of dependent type theories.

ABSTRACT. We present the so called generalized connectives of multiplicative linear logic (MLL). These general connectives were formerly introduced by J.-Y. Girard [2] but most of the results known after then are due to V. Danos and L. Regnier [1]. This talk elaborates on these seminal works and brings several innovations.

A multiplicative generalized (or n-ary) connective can be defined by two pointwise orthogonal sets of partitions, P and Q, over the same domain {1, ..., n}. Actually, we can use partitions according two different points of view (i.e., two syntaxes), sequential and parallel, preserving the same notion of orthogonality (P ⊥ Q). Anyway, general connectives are more expressive in the parallel syntax since this allows to represent correct proofs, namely proof-nets, containing generalized connectives (n-ary links) that cannot be defined (decomposed) by means of the basic (binary) multiplicative ones, Par and Tensor. Dislike the standard proof-nets, these ”more liberal“ proof-nets do not correspond (sequentialize) to any sequential proof (if we exclude the trivial axioms).

In this talk, we characterize an ”elementary“ class of non-decomposable connectives: the class of entangled connectives. Actually, entangled connectives are the “smallest” generalized multiplicative connectives (w.r.t. the number of partitions or, equivalently, w.r.t. the number of rules or switchings), if we exclude, of course, the basic ones. Surprisingly, non-decomposable generalized connectives witness an asymmetry between proof-nets and sequent proofs since the former ones allow to express a kind of parallelism (concurrency) that the latter ones cannot do.

ABSTRACT. Benchmarking automated theorem proving (ATP) systems using standardised problem sets is a well-established method for measuring their performance, especially in the case of classical logical systems. However, the availability of such libraries for \textit{non-classical} logics is very limited. For intuitionistic logic several small collections of formulas have been published and used for testing ATP systems and Raths, Otten and Kreitz~\cite{raths2007iltp} consolidated and extended these small sets to provide the ILTP Library \url{http://www.cs.uni-potsdam.de/ti/iltp/}. For quantified modal systems we have both Wisniewski, Steen and Benzm\"uller's as well as the Raths and Otten libraries of problems.

In this work we seek to provide a similar benchmark for Girard's Linear Logic~\cite{girardLL} and some of its variants. For quick bootstrapping of the collection of problems we use Girard's translation of the collection of intuitionistic theorems discussed in the ILTP library. Eventually we hope to compare different Linear Logic provers over an augmented collection of problems.

ABSTRACT. This work is joint with Raine Rönnholm.

In the context of classical game theory, multiplayer games with a common goal are trivial. In practice, however, finding a strategy is a computational or logical problem.

We work with the following framework:

a) The players share a common goal. b) The players assume no distinct roles. c) The players are allowed to communicate before the rules of the game are revealed, but not after that.

Continuing with simplifying conditions: 1) The possible outcomes are reduced to win or loss. 2) Following the standard normalization, each player has only one move in the play. These moves are done simultaneously. 3) Every player has the same set of moves.

We show how to formalize this in the logical setting, and prove some results that show that first order logic is asymptotically almost surely too weak to provide a winning strategy, on one hand, but first order logic with the Rescher quantifier suffices a.a.s, on the other hand.

ABSTRACT. Let C be a class of models in a fixed signature and R a relation on C; e.g. A R B may mean "B is a submodel of A", "B is a homomorphic image of A", "B is an extension (for models of arithmetic or set theory: an end-extension, a generic extension) of A", "B is an existential completion of A", etc. We interpret modal formulas by sentences of a model-theoretic language L such that \Diamond\varphi is true at a model A ("\varphi is possible at A'') iff \varphi is true at some model B with A R B. A few recent instances of a similar approach deal with models of PA (Henk, Visser) and ZF (Hamkins, Lowe, Block). In these cases, the first-order languages are powerful enough to put the interpretation inside them. This is not true for arbitrary models: \Diamond\varphi may be not first-order expressible. However, once L is chosen strong enough to overcome this, truth and validity of modal formulas can be defined in terms of general frame semantics, and the modal theory of (C,R) defined as the set of all valid modal formulas turns out to be a~normal modal logic. This provides a general framework for defining and studying modal logics of model theoretic relations.

We apply this approach to the case where A R B means "B is a submodel of A". In general, even infinitary first-order languages are not powerful enough to express the satisfiability in submodels. However, for any signature with <\kappa functional symbols (and arbitrarily many predicate symbols), the monadic fragment of the second-order language L^{2}_{\kappa,\omega} expresses the satisfiability of its own sentences in submodels. We prove that whenever the signature contains at least one functional symbol of arity >1 and C is the class of all models in this signature, then the modal theory of (C,R) is S4 if the signature does not have constant symbols, and S4.1.2 otherwise.

ABSTRACT. We study computably enumerable equivalence relations (ceers). We construct weakly precomplete dark ceer over any dark ceer. Our result implies that there is an infinite chain of non-equivalent weakly precomplete dark ceers over ant dark ceer.

ABSTRACT. A preorder is a reflexive and transitive binary relation. We are interested in computably enumerable (c.e.) preorders, in particular, in weakly pre-complete c.e. preorders. Let P and Q be c.e. preorders. We say that P is computably reducible to Q if there is a computable function f such that xPy iff f(x)Qf(y) for every x, y. A c.e. preorder P is light if there exists a c.e. preorder Q in which all classes are singletones such that Q\leq_cP, and c.e. preorder P is called dark if $P$ is not light and has no computable classes, \cite{S2}. A c.e. preorder $P$ is finite if $P$ has a finite number of classes. We say that c.e. preorder $P$ is weakly pre-complete if for every total function $\varphi_e$ there exist $x_e$ such that $\varphi_e(x_e)\sim_P x_e$.

\begin{theorem} Let $P$ be a non-universal c.e.preorder. Then there exists a weakly pre-complete, non-universal c.e. preorder $Q$, such that $P\leq_c Q$ \end{theorem}

\begin{theorem} For every finite c.e. preorder $P$ there are infinitely many minimal dark c.e. preorders $P_d$ such that $P\leq_c P_d$ \end{theorem}

ABSTRACT. One of the widely known ways to extend computability theory on the objects of mathematical analysis is computable analysis [1]. On the other hand, to describe computability in an uncountable structure we can use an approach via definability by sigma-formulas in hereditarily finite superstructure over that structure, which was introduced by Yu.L. Ershov in [2].

In this talk we will compare expressive powers of sigma-definability in hereditarily finite superstructures and computable analysis. In particular, we show that there exists a computable real function, which is not sigma-definable in hereditarily finite superstructure over the real exponential field.

[1] Weihrauch, K., Computable analysis. Texts in Theoretical Computer Science. An EATCS Series. Springer-Verlag, Berlin, 2000. [2] Ershov, Yu.L., Definability and Computability, Consultants Bureau, New York-London-Moscow, 1996.

ABSTRACT. This is joint work with Uri Andrews, Hristo Ganchev, Rutger Kuyper, Steffen Lempp, Joseph Miller and Mariya Soskova. The talk will be an overview on the structural properties of the cototal enumeration degrees which form a proper substructure of the enumeration degrees. The cototal enumeration degrees properly extend the substruc- ture of the total enumeration degrees. The skip is a monotone operator on enumeration degrees. We study cototality, using the skip operator and give some examples of classes of enumeration degrees that either guarantee or prohibit cototality. The skip has many of the nice properties of the Turing jump, but not every e-degree is reducible to its skip. The e-degrees reducible to their skip are exactly the cototal degrees. The cototal enu- meration degrees are characterized [1] as the enumeration degrees of complements of maximal independent sets for infinite computable graphs on the natural numbers. The image of the continuous degrees, introduced by Joseph Miller [5], is contained in the co- total enumeration degrees [1]. Further characterizations are given by Ethan McCarthy [4], Takayuki Kihara, Arno Pauly [2] and Takayuki Kihara by private conversation. Recently Joseph Miller and Mariya Soskova [6] prove that the cototal enumeration degrees form a dense substructure of the enumeration degrees. Moreover they show that these are exactly the enumeration degrees which contain sets with good approximations in the sense of Alistair Lachlan and Richard Shore [3].

[1] Uri Andrews, Hristo Ganchev, Rutger Kuyper, Steffen Lempp, Joseph Miller, Alexandra Soskova and Mariya Soskova, On cototality and the skip operator in the enumeration degrees, submitted.

[2] Takayuki Kihara and Arno Pauly, Point degree spectra of represented spaces, submitted.

[3] Alistair Lachlan and Richard Shore, The n-rea enumeration degrees are dense, Archive for Mathematical Logic, vol. 31 (1992), no. 4, pp. 277–285.

[4] Ethan McCarthy, Cototal enumeration degrees and the Turing degree spectra of minimal subshifts, to appear in the Proceedings of the American Mathematical Society.

[5] Joseph Miller, Degrees of unsolvability of continuous functions, Journal of Symbolic Logic, vol. 69 (2004), no. 2, pp. 555–584.

[6] Joseph Miller and Mariya Soskova, Density of the cototal enumeration degrees, submitted.

ABSTRACT. We propose a new kind of formula size game for modal logic. We illustrate the use of our game by proving FO is non-elementarily more succinct than ML. We are also working on an adaptation of our game for the modal mu-calculus.

ABSTRACT. We formulate multirole logic as a new form of logic and naturally generalize Gentzen's celebrated result of cut-elimination between two sequents into one between multiple sequents.

While the first and foremost inspiration for multirole logic came to us during a study on multiparty session types in distributed programming, it seems natural in retrospective to introduce multirole logic by exploring the well-known duality between conjunction and disjunction in classical logic. Let R0 be a (possibly infinite) underlying set of integers, where each integer is referred to as a role. In multirole logic, each formula A can be annotated with a set R of roles to form the i-formula [A]_R. For each ultrafilter U on the power set of R0, there is a (binary) logical connective \land_U such that [A_1\land_U A_2]_R is interpreted as the conjunction (disjunction) of [A_1]_R and [A_2]_R if R is in U (R is not in U). Furthermore, the notion of negation is generalized to endomorphisms on R0. We formulate both multirole logic (MRL) and linear multirole logic (LMRL) as natural generalizations of classical logic (CL) and classical linear logic (CLL), respectively. Among various meta-properties established for MRL and LMRL, we obtain one named multiparty cut-elimination stating that every cut involving one or more sequents can be eliminated.

ABSTRACT. This paper studies logical relations among plural categorical statements(e.g., ‘Any unicorns are animals’, ‘Any of the unicorns are animals').

ABSTRACT. Modal mu-calculus is the extension of propositional modal logic by constructors for fixed points of inductive and co-inductive definitions. Kozen [1] proposed an axiomatisation for the logic which was proved to be complete by Walukiewicz [2]. Kozen's system contains cut and Walukiewicz' proof makes essential use of this rule. We present a cut-free sequent calculus for the logic that features a strengthening of the standard induction rule for greatest fixed point. The system is readily seen to be sound and its completeness is established by utilising a novel calculus of circular proofs. As a corollary we obtain a new, constructive, proof of completeness for Kozen's axiomatisation which avoids the usual detour through automata and games.

[1] Dexter Kozen, Results on the propositional mu-calculus, Theoretical Computer Science, vol. 27 (1983), pp. 333–354.

[2] Igor Walukiewicz, Completeness of Kozen’s axiomatisation of the propositional mu-calculus, Information and Computation, vol. 157 (2000), pp. 142–182.

ABSTRACT. The investigation concerns display calculi --- a generalization of sequent calculi due to Nuel Belnap. The generalization is obtained by replacing comma in sequents with a number of formal structural connectives. Sequents are then pairs of structures, which are built from formulas using structural connectives. Display framework provides several advantages over traditional sequent calculi, including a general cut-elimination result, which holds for all display calculi satisfying a number of conditions. Another advantage is that display calculi can be applied to study classes of logics by making the notion of extension more precise.

A display calculus is built around some structural rules called display equivalences, which postulate basic relations between structural connectives. It is assumed that display equivalences should satisfy the display property, which says that any structure in a sequent can be displayed by providing an equivalent sequent, in which this structure is the entire antecedent or the entire consequent. Display property has an important philosophical value related to the proof-theoretic semantics.

In this work we investigate some technical aspects of display property, using Rajeev Gore's display calculus for intuitionistic logic to illustrate our ideas. We show that while display property allows us to characterize naturally the class of logics given by extensions of a display calculus, weakening it can give us more expressive power. The investigation also raises questions, on the way structural connectives are involved in formulating introduction rules.

This work was supported by the Grants Council (under RF President) for State Aid of Leading Scientific Schools (grant NSh-6848.2016.1) and by Alexander von Humboldt Foundation.

ABSTRACT. Several natural deduction calculi are known for relevant logics, see Anderson and Belnap \cite{AB1}, Dunn \cite{Dunn02}, Brady \cite{Brady-n}, and Meyer and McRobbie \cite{Meyer}. Some of them are with the explicit distribution rule, such as Anderson--Belnap's and Meyer--McRobbie's, some of them have normalization theorems, such as Brady's, however, all of them, use a kind of relevance numerals in order to keep track of the use of hypotheses.

On the other hand, relevant numerals are not needed in sequent calculi of relevant logics, see e.g. Dunn \cite{Dunn73}, \cite{Dunn02}, Minc \cite{Minc}, Bimbo \cite{Bimbo07}. We formulate a natural deduction calculus, of a particular relevant logic, by defining the translation from its sequent calculus formulation into natural deduction. We consider the contraction--less relevant logic $RW_+^\circ$ and we take its sequent calculus $GRW_+^\circ$, admitting cut--elimination, presented in \cite{mlq}. The resulting natural deduction calculus is a normalizing natural deduction system, without explicit distribution rule and free from relevant numerals. Our translations from sequent to natural deduction calculus and vice versa are similar to Negri's translations between those calculi for intintuitionistic linear logic \cite{Negri}, however, due to the presence of two types of multisets of formulae, intensional and extensional ones, needed for the proof of the distribution of conjunction over disjunction in relevant logics, see Dunn \cite{Dunn73} and Minc \cite{Minc}, our translations are significantly different from Negri's translations.

\begin{thebibliography}{10}

\bibitem{AB1} \sc A. Anderson, N. Belnap Jr., \it Entailment: the logic of relevance and necessity, \rm vol. 1, Princeton University Press, Princeton, New Jersey, 1975.

\bibitem{Bimbo07}\sc K. Bimbo, \it $LE_\rightarrow^t$, $LR^\circ_{\land\sim}$, $LK$ and cutfree proofs, \rm Journal of Philosophical Logic, 36, pp. 557--570. 2007

\bibitem{Brady-n} \sc R. T. Brady, \it Normalized natural deduction system for some relevant logics I: The logic DW, \rm Journal of Symbolic Logic, Vol. 7, Number 1, 35--66, 2006.

\bibitem{Dunn73} \sc J. M. Dunn, \it A 'Gentzen system' for positive relevant implication, \rm The Journal of Symbolic Logic 38, pp. 356-357, 1973.

\bibitem{Dunn02} \sc J. M. Dunn, G. Restall, \it Relevance logic, \rm Handbook of Philosophical Logic, vol. 6, , D. Gabbay and F. Guenthner (eds.), Kluwer Academic Publlishers, 1-128, 2002.

\bibitem{Gen} G. Gentzen, \rm Collected Papers, \rm (ed. M. E. Szabo), North--Holland, Amsterdam, 1969.

\bibitem{mlq} M. Ili\'c, \it An alternative Gentzenization of $RW_+^\circ$, \rm Mathematical Logic Quarterly 62, No. 6, pp. 465--480, 2016.

\bibitem{Meyer} \sc R. K. Meyer, M. A. McRobbie, \it Multisets and relevant implication I and II, \rm Australian Journal of Philosophy, Vol. 60, No. 2, pp 107--139 and Vol. 3 pp. 265--281, 1982.

\bibitem{Minc}\sc G. Minc, \it Cut elimination theorem for relevant logics, \rm Journal of Soviet Mathematics 6, pp. 422-428, 1976.

\bibitem{Negri} \sc S. Negri, \it A normalizing system of natural deduction for intuitionistic linear logic, \rm Archive for Mathematical Logic 41, pp. 789--810, 2002.

\end{thebibliography}

ABSTRACT. In [2], Kohlenbach did an analysis of the proof of Browder's theorem (in [1]) via the monotone functional interpretation. I will be following the same outline but guided by the bounded functional interpretation ([3], [4]). Although the bounds obtained are the same, this example provides a first look at how the bounded functional interpretation works in practice.

ABSTRACT. Intuitionistic Zermelo-Fraenkel set theory with Collection, ZFI2C, is a two-sorted variant of a standard reference theory that relates to set-theoretic explicit mathematics as usual ZF relates to classical set-theoretic mathematics.

The paper is concerned with some effectivity properties of ZFI2C plus an additional intuitionistic principles, such that DCS (Double Complement of Sets), and some another principles: M (Markov Principle),UP (Uniformization Principle), etc. Specifically, let T be an extension of ZFI2C by addition of each combinations of principles DCS, M, ECT, UP, UZ. In the paper we prove that the theory T has the following properties: 1. Disjuntive property (DP, effectively by proof of antecedent), 2. Numerical existence property (NEP, effectively by proof of antecedent), 3. Markov rule (MR, effectively by proofs of antecedents of the rule). 4. Church rule (CR, by proofs of antecedent of the rule), 5. Uniformization rule (UR, effectively by proofs of antecedents of the rule).

In each of these axioms and rules each formula can contain only set parameters, but not number parameter.

ABSTRACT. Prawitz conjectured that intuitionistic first-order logic is complete with respect to a notion of proof-theoretic validity [1, 2, 3]. We show that this conjecture is false. The notion of validity obeys the following standard conditions, where S refers to atomic bases (systems of production rules):

1. |=_S A ∧ B ⇐⇒ S A and |=_S B. 2. |=_S A ∨ B ⇐⇒ |=_S A or |=_S B. 3. |=_S A → B ⇐⇒ A |=_S B. 4. Γ |=_S A ⇐⇒ For all S: (|=_S Γ ⇒ |=_S A). 5. If Γ |=_S A and Γ, A |=_S B, then Γ |=_S B.

Any semantics obeying these conditions satisfies the generalized disjunction property

For every S: if Γ |=_S A ∨ B, where ∨ does not occur positively in Γ, then either Γ |=_S A or Γ |=_S B.

This implies the validity (|=_S) of Harrop’s rule ¬A → (B ∨ C)/(¬A → B) ∨ (¬A → C), which is admissible but not derivable in intuitionistic logic.

[1] Dag Prawitz, Towards a foundation of a general proof theory, Logic, Method- ology and Philosophy of Science IV (P. Suppes et al., editors), North-Holland, 1973, pp. 225–250.

[2] Dag Prawitz, An approach to general proof theory and a conjecture of a kind of completeness of intuitionistic logic revisited, Advances in Natural Deduction (L. C. Pereira, E. H. Haeusler and V. de Paiva, editors), Springer, Berlin, 2014, pp. 269–279.

[3] Peter Schroeder-Heister, Validity concepts in proof-theoretic semantics, Synthese, vol. 148 (2006), pp. 525–571.

ABSTRACT. Gödel’s Dialectica interpretation is a proof interpretation of Heyting arithmetic into a system of computable functionals of finite type. De Paiva [1], Hyland [2] and others have worked on the idea of a semantic version of Dialectica: starting with a category of types and a fibration of predicates over it, a new structured category is built whose morphisms correspond to the Dialectica interpretation of logical implication. Recently, von Glehn [3] has adapted this idea for the original Dialectica interpretation to categorical models of dependent type theory. I will discuss how we can build models of dependent type theory based on other variants of Dialectica, including the Diller-Nahm variant. [1] V.C.V. de Paiva, The Dialectica categories, Categories in Computer Science and Logic (John W. Gray and Andre Scedrov, editors), American Mathematical Society, Providence, RI, 1989, pp. 47–62. [2] J.M.E. Hyland, Proof theory in the abstract, Annals of Pure and Applied Logic, vol. 114 (2002), pp. 43–78. [3] T.L. von Glehn, Polynomials and Models of Type Theory, PhD thesis, University of Cambridge, 2014.

ABSTRACT. The revival of Kreisel's program of \textit{unwinding of proofs} by Kohlenbach as \textit{proof mining} has been very fruitful for applications in many mathematical disciplines, especially within analysis. The scope of the program is the extraction of constructive information (e.g. computable bounds) from nonconstructive mathematical proofs. This can be a priori guaranteed by certain logical metatheorems. The quantitative content emerges through the discovery of quantifiers that were implicit in the original proof. The bounds obtained are explicit, highly uniform and of low complexity. We present here: (i) Bounds extracted for the computation of approximate common fixed points of one-parameter nonexpansive semigroups on a subset of a Banach space, obtained via proof mining on a proof by Suzuki. The bounds differ from those that had been obtained in \cite{kohkousuz} via proof mining on a completely different proof by Suzuki of a generalised version of the studied statement. (ii) Computable rates for the convergence of the resolvents of set-valued operators on a real Banach space that fulfill certain accretivity conditions to the zero of each operator, that were extracted via proof mining on a proof by Garc\'{i}a-Falset. The above results are, among others, included in \cite{mythesis} and can be of interest for optimization theory.

\begin{thebibliography}{10}\bibitem{kohkousuz} {\scshape Ulrich Kohlenbach and Angeliki Koutsoukou-Argyraki}, {\itshape Effective asymptotic regularity for one-parameter nonexpansive semigroups}, {\bfseries\itshape Journal of Mathematical Analysis and Applications}, vol.~433 (2016), no.~2, pp.~1883--1903.

\bibitem{mythesis} {\scshape Angeliki Koutsoukou-Argyraki}, {\bfseries\itshape Proof Mining for Nonlinear Operator Theory: Four Case Studies on Accretive Operators, the Cauchy Problem and Nonexpansive Semigroups}, PhD thesis, Technische Universit\"{a}t Darmstadt, URN: urn:nbn:de:tuda-tuprints-61015, 2017 \end{thebibliography}

ABSTRACT. Our purpose is to obtain the sense or the meaning of some text. This goal is quite opposite to the Melchuk’s approach which goes from the meaning to the text. Obviously, the former is more important for solving most NLP problems. Lambda-expressions can easily be encoded in Prolog Consider the sentence Every boy loves some girl. Prolog: det(lbd(q, lbd(p, exists(x, (q@x & p@x))))) --> [some]. det(lbd(q,lbd(p, forall(x,(q@x -> p@x))))) --> [every]. v(lbd(s,lbd(x,s@lbd(y, (loves(x,y)))))) --> [loves]. English loves takes a GQ object but interprets it as quantified in, with a metalanguage version of loves in the translation that takes an e-type object. This is similar to what Montague did. n(lbd(x,boy(x)))--> [boy]. n(lbd(x,girl(x)))--> [girl]. If we ask: ?- s(SSem,[every,boy,loves,some,girl],[]), pp(SSem). We’ll obtain the result of the Prolog program executed: (x11)(boy(x11) => (Ex2)(girl(x2) & loves(x11, x2))) which, when we change the fonts a bit, becomes ∀ x11(boy(x11) → ∃x2(girl(x2) ∧ loves(x11, x2))) Similarly: ?- s(SSem, [some, girl, loves, some, girl],[]), pp(SSem). Result: (Ex41)(girl(x41) & (Ex5)(girl(x5) & loves(x41, x5))) Which becomes ∃x 41(girl(x41) ∧ ∃x5(girl(x5) ∧ loves(x41, x5))) The syntax could be farcified using X-bar theory. ip(SSem) --> np(NPSem), ibar(IbarSem), {var replace(NPSem, NPSem1), beta(NPSem1@IbarSem, SSem)}. ibar(VPSem)--> i(MvdVbL), vp(VPSem, MvdVbL). i([])--> [Aux],{isAux(Aux)}. i([Verb])--> [InflVerb], {pastInfl(Verb, InflVerb),isVerb(Verb)}…

Examples in Russian: ?- ip([какой-то, мальчик, целовал, каждый, девочка]). Result: (Ex451)(мальчик(x451) & (x46)(девочка(x46) -> целовать(x451,x46))) ?- ip([один, студент, подарил, все, цветы]). Result: (Ex141)(студент(x141) & (x15)(цветы(x15) -> подарить(x141,x15))) ?- ip(['Иван', застрелил, один, бунтовщик]). Result: (Ex20)(бунтовщик(x20) & застрелить(Иван,x20)) ?- ip([он, застрелил, один, бунтовщик]). Result: (Ex20)(бунтовщик(x20) & застрелить(он,x20)) ?- ip([один, студент, выучил, все, правила]). Result: (Ex441)(студент(x441) & (x45)(правило(x45) -> выучить(x441,x45))) ?- ip([все, правила, выучил, один, студент]). Result: (x411)(правило(x411) -> (Ex42)(студент(x42) & выучить(x411,x42)))

ABSTRACT. The three Written English expressions ‘statement’, ‘proposition’, and ‘sentence’ used in logic and philosophy of logic are ambiguous (multisense, polysemic): people use each with multiple normal meanings (senses, definitions). Several of their meanings are vague (imprecise, indefinite): they admit borderline (marginal, fringe) cases. This paper juxtaposes, distinguishes, and analyses several senses of these words focusing on a constellation of recommended senses. As recommended, a statement is a unique event, a speech-act performed by a unique person at a unique time and place. In contrast, propositions and sentences are timeless and placeless abstractions. A proposition is an intensional object, a sense composed of senses (concepts). A sentence is a linguistic entity (string-type) composed of character-types. Sentences in themselves are meaningless. It is only a proposition that is properly said to be true or to be false, although—with suitable qualification—statements, or even sentences, may be said to be true or false in appropriate derivative senses. Persons use sentences to express the propositions they state in the statements they make. As examples make clear, one and the same sentence is routinely used on different occasions to express different propositions. Likewise clarified by examples is the fact that different sentences express one and the same proposition. Persons make statements; they don’t make sentences or propositions. This paper clarifies, qualifies, and, in a few cases, retracts various views previously expressed by the author. It is intended as a philosophical sequel to [1], [2] and [3] [1] JOHN CORCORAN, Meanings of implication, Diálogos, vol. 9 (1973), pp. 59-76. [2] JOHN CORCORAN, Argumentations and logic, Argumentation, vol. 3 (1989), pp. 17-43. [3] JOHN CORCORAN, Sentence, proposition, judgment, statement, and fact: speaking about the Written English used in logic, The Many Sides of Logic, (Walter Carnielli et al., editors), College Publications, 2009, pp. 71–103.

ABSTRACT. Sometimes when trying to prove a fact by induction, one gets "stuck" at the induction step. The solution is often to use a "stronger" induction hypothesis. We provide a precise characterization of this phenomenon and show that this characterization applies to a number of natural examples. By reflecting on mathematical practice, we argue that our definition does capture the notion of "proof by strengthened induction hypothesis". The general problem of when one must, in order to prove a fact X, first prove another fact Y, seems very hard. Interestingly, the special case of proof by strengthened induction hypothesis turns out to be more manageable.

ABSTRACT. Eclecticism is not a position available to an intuitionist mathematician/logician of faith. The classical mathematician/logician may even consider the intuitionist position quite interesting, since constructive proofs, although usually longer, are more informative than indirect classical proofs, since they have an algorithmic nature and satisfy interesting informative properties such as the disjunction property and the property of the existential quantifier. To the intuitionist mathematician/logician however, there seems to be no alternative but to revise and revoke the universal validity of certain classical principles of reasoning; for the intuitionist, mathematics must be constructed exclusively on constructively valid forms of argument. From the point of view of the classical mathematician, the intuitionist proposition, if taken seriously, would imply a mutilation of the mathematical corpus; for the intuitionist it is simply the only correct way of doing mathematics. In 2015 Dag Prawitz (see [2]) proposed the idea of an ecumenical system, a codification where the classical and the intuitionist could coexist in peace. The main idea behind this codification is that the classical and the intuitionist share the constants for conjunction and negation, but each have their own disjunction and implication. Similar ideas were present in Dowek [1] and Krauss [3], but without Prawitz philosophical motivations. The aims of the present paper are: [1] to investigate the proof theory for Prawitz’ Ecumenical system, [2] to propose a truth-theoretical semantics for which Prawitz’ system is sound and complete, [3] to compare Prawitz system with other ecumenical approaches, and [4] to propose a generalization of the ecumenical idea.

[1] Dowek, Gilles, On the definitions of the classical connective and quantifiers, Why is this a proof (Eward Haeusler, Wagner Sanz and Bruno Lopes, editors), College Books, UK, 2015, pp. 228 - 238. [2] Prawitz, Dag, Classical versus intuitionistic logic, Why is this a proof (Eward Haeusler, Wagner Sanz and Bruno LOpes, editors), College Books, UK, 2015, pp.15 32. [3] Peter H. Krauss, A constructive interpretation of classical mathematics, Mathematische Schriften Kassel, preprint No. 5/92 (1992)

ABSTRACT. As Terence Tao has recalled several times, mathematics can benefit not only from correct proofs, or proofs that require some changes to be correct, but also from outlines of strategies for a proof, whether for opening lines of research or closing them definitely. Here, we discuss how a certain kind of logician could argue for P = NP following a translation between logics approach. As P = NP amounts to FOL(LFPO) = SOL, one could argue for the latter by providing a suitable translation between those logics. Though we do not provide any such a translation, we show that such an approach regarding those logics is not a priori ruled out. Thus, the broad strategy is: 1. Follow the identities provided by descriptive complexity theory (see Immerman 1998). 2. Compare the expressive powers of FOL(LFPO) and SOL via logical translations (see Manzano 1996). 3. Give reassurance of three kinds: a) Conceptual: the corresponding translations do not distort the studied phenomena. b) Mathematical: the translations do not imply any obvious contradiction with well-established mathematical results. c) Philosophical: the translations do not imply any gratuitous counterintuitive claim regarding logic, mathematics or human nature (cf. Aaronson 2016).

ABSTRACT. \documentclass[a4paper,12pt,fleqn]{article} \usepackage{amsmath, amssymb} %\usepackage[T1]{fontenc} \pagestyle{empty} \begin{document} \bibliographystyle{plain} \begin{tabular}{c} Euclidean Geometry in Renaissance \\ Ryszard Mirek\\ Institute of Logic, Pedagogical University of Krakow, Poland\\ e-mail: mirek.r@poczta.fm\\\end{tabular} \vspace{0.3in}\newline\indent In Euclidean Elements in Book IV, Proposition 16, one can find how to inscribe an equilateral and equiangular fifteen-angled figure in a given circle. This construction was used both in theoretical and practical terms by Piero della Francesca. For instance in the setting of his painting \emph {Baptism of Christ} one can find the first part of the construction. In the top side of the rectangle we construct an equilateral triangle, and we find that its apex falls at the point where the central vertical axis passes through the tip of Christ’s right foot. Then we locate the center of the triangle and find it to be precisely at the fingertips of Christ’s hands in prayer. In this way it is possible to set the center point of the painting. The result can be combined with Proposition 1.13 of his \emph{De Prospectiva Pingendi}. In the second part of the treatise one can find more geometrical problems and theorems that have obvious relevance to Piero's work as a painter. There are problems of drawing a combination of prisms (Proposition 2.6), a beam of octogonal cross-section, lying on the ground plane (2.8), of drawing a cross-vaulted structure with a square ground plane (2.11). \newline\indent My goal here is to describe the advanced geometrical exercises presented in the form of propositions. The treatise of Piero della Francesca is manifestation of a union of the fine arts and the mathematical sciences of arithmetic and geometry. The proofs of propositions are presented both in geometrical and mathematical form but from a logical point of view it is proposed by me a method of natural deduction that takes into account the importance of diagrams within formal proofs.

\end{document}

ABSTRACT. Curry's paradox represents a problem for uniform approaches to self-referential paradoxes, as seemingly no negation is involved in it and triviality is reached without the explosion principle, unlike most of the other paradoxes. In particular, purely paraconsistent approaches will not serve to block or solve the paradox. Using some ideas from abstract algebra and Abelian logic, in this paper we argue that the strategy of blocking Curry's paradox by rejecting Detachment can be seen as a generalization of the rejection of the explosion principle, and thus of the paraconsistent strategy. This would imply that a uniform approach to all the self-referential paradoxes, at least those where object-language connectives are involved, is possible.

ABSTRACT. The study of decomposing Borel functions originated by a question asked by Luzin: is every Borel function decomposable into countably many continuous functions? This question was answered negatively. So we turn to focus on: what kind of Borel functions is decomposable into countably many continuous functions?

Jayne-Rogers' theorem shows that, a function of Baire class $1$ is decomposable into countably many continuous functions with closed domains iff the preimage of any $F_{\sigma}$ set is still $F_{\sigma}$. The generalization of Jayne-Rogers' theorem is named The Decomposability Conjecture.

In this talk, we will introduce the recent developments on the decomposability conjecture.

ABSTRACT. Alberto Marcone
Strongly surjective linear orders

A linear order L is strongly surjective if there exists an order preserving surjection from L onto each of its suborders. For example, an ordinal is strongly surjective if and only if it is of the form omega^alpha m, for some alpha<omega₁ and m>0.

Our main result is that the set StS of countable strongly surjective linear orders is a check D₂(Pi¹₁)-complete set. This means that StS is the union of an analytic and a coanalytic set, and is complete for the class of sets that can be written in this way. More in detail, we show that the countable strongly surjective linear orders which are scattered form a Pi¹₁-complete set, while the countable strongly surjective linear orders which are not scattered form a Sigma¹₁-complete set. Our proof of the upper bound for scattered strongly surjective orders makes an essential use of both effective descriptive set theory and the fact that order preserving surjections well quasi-order the countable linear orders ([L,CCM1]).

Even if the study of the first two levels of the projective hierarchy is a long-standing topic, examples of sets that are true Delta¹₂ are very rare. In fact, as far as we know, StS is the first concrete example of a "natural" check D₂(Pi¹₁)-complete set.

If time permits, I'll also discuss uncountable strongly surjective linear orders. We can prove their existence under either PFA or Diamond⁺, while the provability in ZFC of the existence of these orders is an interesting open problem.

This is joint work with Riccardo Camerlo and Raphaël Carroy [CCM2].

[CCM1] Riccardo Camerlo, Raphaël Carroy, Alberto Marcone, Epimorphisms between linear orders, Order 32 (2015), 387--400, arXiv:1403.2158.

[CCM2] Riccardo Camerlo, Raphaël Carroy, Alberto Marcone, Linear orders: when embeddability and epimorphism agree, arXiv:1701.02020.

[L] Charles Landraitis, A combinatorial property of the homomorphism relation between countable order types, The Journal of Symbolic Logic 44 (1979), 403--411.

ABSTRACT. Let C be a class of countable structures, closed under isomorphism. The collection of all members of C with domain omega forms a subspace of Cantor space: the atomic diagram of each space becomes a subset of omega, using a Godel coding of the atomic formulas in the language of C with extra constants from omega. We give this space the subspace topology, and then endow the quotient space I(C), under the relation of isomorphism, with the quotient topology. The result is that we view the isomorphism types of elements of C as elements of this topological space I(C).

The isomorphism relation on C often resembles various of the well-known Borel equivalence relations on either Cantor space or Baire space. Determining which Borel equivalence relations yield spaces homeomorphic to I(C) requires the use of techniques from computable structure theory, along with reductions of the sort used in Borel reducibility, only stronger. These reductions may be regarded as type-2 computable functions. Often the main goal is to determine which definable relations on the members of C, if added to the language, turn I(C) into a recognizable space: when this happens, we may say that the elements of C are classified up to isomorphism by the members of the recognizable space.

The talk will consist largely of examples of these phenomena, mostly using classes in which isomorphism is an arithmetic relation, such as algebraic fields, finite-valence graphs, torsion-free abelian groups, and equivalence structures.

ABSTRACT. A first-order structure equipped with a dense linear ordering without endpoints is said to be weakly o-minimal if all its subsets definable in dimension one are finite unions of convex sets. Unlike o-minimality, weak o-minimality is not preserved under elementary equivalences. The strong cell decomposition property is a feature of certain weakly o-minimal structures (ex. weakly o-minimal expansions of real closed fields without non-trivial definable valuations) guaranteeing the existence of a certain canonical o-minimal extension. The latter is constructed using completions of so called strong cells, the building blocks of definable sets.

It is well known that for models of weakly o-minimal theories, a weaker version of cell decomposition theorem holds. For sets definable in models of weakly o-minimal theories, I am proposing a notion of completion together with variants of definable connectedness and definable compactness, and discuss some of their fundamental properties. This generalizes similar concepts recently developed by S. Tari in the setting of weakly o-minimal structures admitting the strong cell decomposition property.

ABSTRACT. Our talk concerns satisfaction classes in models of Peano Arithmetic. A \emph{full satisfaction class} in a model $M$ of PA is a subset $S \subset M$ such that the expanded structure $(M,S)$ satisfies a certain version of Tarski's compositional clauses for the satisfaction predicate for (the codes of) arithmetical formulae. It is not at all trivial for a model of PA to admit a full satisfaction class. A surpising theorem by Lachlan states that any model $M$ of PA which admits a full satisfactions class $S$ is recursively saturated. However, Lachlan's argument, although very clever, seemed to be based on a rather \textit{ad hoc} trick. We would like to show a modification of the proof which makes the presentation substantially more principled, although it doesn't change the essence of Lachlan's argument. If time allows, we will show how this modified proof allows to show a stronger result after slight adjustments. The result states that every model $M$ of PA which has a partial satisfaction class also has a partial inductive satisfaction class. A \emph{partial satisfaction class} is a subset $S \subset M$ such that in the expanded structure $(M,S)$, the compositional clauses are satisfied for all (codes of) formulae with complexity at most $\Sigma_c$ for some nonstandard $c$. A partial satisfaction class is \emph{inductive} if the expanded structure satisfies all induction axioms in the language extended with a new predicate for $S$. So any model that has a partial satisfaction class also has one which satisfies induction. This result actually implies Lachlan's Theorem and an earlier result by Stuart Smith that any model which has a full satisfaction class also has a nondefinable class piecewise coded in the model. The discussed theorem on partial satisfaction classes has already appeared in a joint paper by Mateusz Łełyk and the author but with a more complicated proof.

ABSTRACT. A type $p\in S(T)$ is called special, if there are $a,b\models p$ such that ${\rm tp}(b/a)$ is isolated and non-algebraic, and ${\rm tp}(a/b)$ is non-isolated. The Lachlan conjecture says that if a theory is Ehrenfeucht then it is unstable. It can be seen that if there is a counterexample of the Lachlan conjecture then the theory has a special type. In this talk, I will introduce some result on a relation between generic structures and theories with a special type and generic structures.

ABSTRACT. We define generalized Goodstein sequences with respect to the Schwichtenberg-Wainer hierarchy of fast growing functions. The resulting Goodstein principles will then not be provable in the usual theory for non iterated inductive definitions. The results are partly in joint work with T. Arai and S. Wainer.

ABSTRACT. The principle of definition by recursion on a wellfounded relation [1], can be stated as follows: Let A be any set and let P be the set of all partial functions from A to some set B. Let G : A × P → B be any function and let R be any binary relation.

Fact 1: If R is wellfounded on A then there exists a unique function $f : A → B such that 

(1) for all x in A (f(x) = G(x; f restricted to x^R));

where x^R = {y in A | y  R  x }.

If R is not wellfounded on the entire domain A, an obvious way of extending this method of definition is to identify a proper subset W of A on which R is wellfounded and to apply the principle to this set. The usual choice for W is the wellfounded part of A (w.r.to R), defined as the set of all R-wellfounded points of A.

In my talk, after examining several different strategies to prove Fact 1, I will present a new approach to extend this method of definition to all kinds of binary relations. We look at subsets X of A on which R is not necessarily wellfounded, yet there exists a unique function g : X → B which satisfies (1) for all x in X. Let’s call such subsets determined. Then we can prove: 

Theorem 2: There exists unique a subset U of A such that

 a) U is R-closed, i.e., for all x in U, x^R is a subset of U;

 b) U is determined and all R-closed subsets of U are determined;

 c) U is the largest subset of A satisfying (a) and (b).

Theorem 2 ensures, for any relation R, the existence and uniqueness of a function g : U → B which satisfies (1) on its domain and is defined on a domain U which extends the wellfounded part W of R.

[1] R. Montague, Well-founded relations: generalizations of principles of induction and recursion, Bulletin American Mathematical Society, vol. 61, p. 442

ABSTRACT. Hindman's Theorem states that for every colouring of the natural numbers using finitely many colours, there is an infinite set H of such that all finite sums of distinct elements of H have the same colour. Hindman's Theorem is known to follow from ACA₀⁺ and to imply ACA₀; determining its exact logical strength is a significant open problem in reverse mathematics. A related open problem, originally formulated by combinatorialists, is whether there is a proof of the restriction of Hindman's Theorem to sums of length at most 2 that does not establish the full theorem.

Recently, Dzhafarov et al. proved that the restriction of Hindman's Theorem to sums of length at most 3, and 3 colours, already implies ACA₀. By modifying their methods, we show that also the restriction to sums of length at most 2, and 4 colours, implies ACA₀. Thus, the best currently known upper and lower bounds on Hindman's Theorem for sums of length at most 2 are the same as for the full theorem. On the other hand, Carlucci has formulated some versions of Hindman's Theorem which are provably equivalent to ACA₀. We obtain two new simple examples of this kind, as well as some implications between restrictions of Hindman's Theorem and restrictions of Ramsey's Theorem for pairs. Some of our implications can be witnessed by strong computable reductions.

Joint work with Lorenzo Carlucci, Francesco Lepore, and Konrad Zdanowski.

ABSTRACT. We study the uncountable version of a natural variant of the Open Coloring Axiom. More concretely, suppose that $\kappa$ is an uncountable regular cardinal and $X$ is a subset of the generalized Baire space ${}^\kappa\kappa$ (the space of functions $\kappa\to\kappa$ equipped with the bounded topology). Then $OCA*_\kappa(X)$ denotes the following statement: for every partition $[X]^2=R_0\cup R_1$ such that $R_0$ is an open subset of $[X]^2$, either $X$ is a union of $\kappa$ many $R_1$-homogeneous sets, or there exists a $\kappa$-perfect $R_0$-homogeneous set. We show that after L\'evy-collapsing an inaccessible $\lambda>\kappa$ to $\kappa^+$, $OCA*_\kappa(X)$ holds for all $\kappa$-analytic subsets $X$ of ${}^\kappa\kappa$. Furthermore, the Silver dichotomy for $\Sigma^0_2(\kappa)$-equivalence relations on $\kappa$-analytic subsets also holds in this model. Thus, both of the above statements are equiconsistent with the existence of an inaccessible $\lambda>\kappa$. We also examine games characterizing the above partition property.

ABSTRACT. We prove various extensions of the Tennenbaum phenomenon to the case of computable quotient presentations of models of arithmetic and set theory. Specifically, no nonstandard model of arithmetic has a computable quotient presentation by a c.e.~equivalence relation. No $\Sigma_1$-sound nonstandard model of arithmetic has a computable quotient presentation by a co-c.e.~equivalence relation. No nonstandard model of arithmetic in the language $\{+,\cdot,\leq\}$ has a computably enumerable quotient presentation by any equivalence relation of any complexity. No model of \ZFC\ or even much weaker set theories has a computable quotient presentation by any equivalence relation of any complexity. And similarly no nonstandard model of finite set theory has a computable quotient presentation.

ABSTRACT. It is a well known empirical phenomenon that natural axiomatic theories are well-ordered by their consistency strength. One expression of this phenomenon comes from ordinal analysis, a research program whereby recursive ordinals are assigned to theories as a measurement of their consistency strength. One method for calculating the proof-theoretic ordinal of a theory T involves demonstrating that T can be approximated over a weak base theory by reflection principles, such as consistency statements and their generalizations. Why are natural theories amenable to such analysis? Fixing a base theory T that interprets elementary arithmetic, we study recursive monotonic functions on the Lindenbaum algebra of T. In this talk we discuss some results that demonstrate that consistency and other reflection principles are canonical among such functions. We also discuss how these results address our motivating questions.