ABSTRACT. We say that a first-order monadic logic of order (FOMLO) sentence is satisfiable over the reals if there is some valuation for the monadic predicates which makes the formula true. Burgess and Gurevich showed that satisfiability for this logic is decidable. They built on pioneering work by Lauchli and Leonard who, in showing a similar result for linear orders in general, had presented some basic operations for the compositional building of monadic linear structures.

We look at some recent work in using these basic operations to give a synthesis result. That is, we present an algorithm which given a FOMLO sentence which is satisfiable over the reals, outputs a specific finite description of a model.

ABSTRACT. First--order Peano arithmetic $PA$ is axiomatized over a finite algebraic base theory by the full induction scheme $$\varphi(0,v) \land \forall x \, (\varphi(x,v) \rightarrow \varphi(x+1,v)) \rightarrow \forall x \, \varphi(x,v),$$ where $\varphi(x,v)$ ranges over all formulas in the language of arithmetic $\{0,1,+,\cdot,<\}$. Fragments of arithmetic are obtained by restricting, in one way or another, the induction scheme axiomatizing $PA$. Classical examples include the theories of $\Sigma_n$ and $\Pi_n$ induction and their parameter free counterparts.

In this talk we present a new kind of restriction on the induction scheme, giving rise to new subsystems of arithmetic that we collectively call \emph{local induction} theories. Roughly speaking, local indiction axioms have the form $$\varphi(0,v) \land \forall x \, (\varphi(x,v) \rightarrow \varphi(x+1,v)) \rightarrow \forall x \in \mathcal{D} \, \varphi(x,v).$$ That is to say, we restrict the $x$'s for which the axiom claims $\varphi(x,v)$ to hold to the elements of a prescribed subclass $\mathcal{D}$ of the universe. Natural choices for $\mathcal{D}$ are the sets of the $\Sigma_n$--definable elements of the universe as well as other related substructures of definable elements.

We will study the basic properties of the local induction theories obtained in this way and derive a number of applications to the study of 'classical' fragments of $PA$. Remarkably, we show that the hierarchy of local reflection principles can be reexpressed in terms of our local induction theories, thus filling a gap in our understanding of the equivalence between reflection and induction in arithmetic.

ABSTRACT. Progress in mathematics has often involved a good deal of conceptual clarification, including increasingly precise characterizations of concepts (e.g. those of infinity, of continuity, perhaps of ‘set,’ etc.) that were less clearly understood by earlier theorists. But the sometimes-vast difference between the earlier and later concepts that go by the same name raises the possibility that such conceptual refinement really brings with it a whole new subject-matter for the branch of mathematics in question, rather than a clarified understanding of the concepts used by earlier generations. This talk investigates Gottlob Frege’s approach to understanding this kind of conceptual progress, and assesses the plausibility of his view that a given subject-matter can survive essentially unscathed despite fairly radical changes in the surrounding theory.

ABSTRACT. Cantor's theorem that no one-one function maps a set a onto the power set of a follows from the statement that no function maps a set a onto the power set of a. Paul Bernays showed how to encode assignments of subclasses of a given A to members of A by means of a class of ordered pairs, and he deployed a familiar diagonal argument to show that no assignment of subclasses of A to members of A is onto. It much less clear how to make sense of an assignment of members of A to subclasses of A, but when we do, we are in a position to show that no such assignment is one-one. Unfortunately, familiar arguments for this claim fail to provide an explicit characterization of two different subclasses of A which are assigned one and the same member of A by a given assignment. George Boolos later showed how to specify explicit counterexamples to the claim that a function from the power set of a set a into the set a is one-one. Similar constructions turn out to be available in the case of classes, but they are sensitive to the presence of impredicative class comprehension. We explore some ramifications of this observation for traditional philosophical puzzles raised by the likes of Russell's paradox of propositions in Appendix B of "The Principles of Mathematics" and Kaplan's paradox.

ABSTRACT. The goal of this research is to rule out "natural" independence phenomena in Set Theory by maximizing your theory in terms of large cardinals and forcing axioms. Using large cardinals in ZFC, by the results of Woodin, we have a clear understanding of the theory of the second-order structure (\omega, P(\omega), \in)) and what it should be.

In this talk, we try to extend this understanding to the theory of the structure (\omega_1, P(\omega_1), \in) by using large cardinals, forcing axioms, and some hypothesis from inner model theory in ZFC. This is joint work with Matteo Viale.

ABSTRACT. A classical theorem of Mansfield shows that there exists a well-ordering of the set \omega^\omega of all functions from \omega to \omega$that is definable over the collection H(\omega_1) of all hereditarily countable sets by a \Pi_1-formula without parameters if and only if every such function is contained in Gödel's constructible universe L. In particular, the existence of such a well-ordering implies that the continuum hypothesis holds. We consider the question whether this implication generalizes to higher cardinalities: does the existence of a well-ordering of the set \omega_1^{\omega_1} of all functions from \omega_1 to \omega_1 that is definable over H(\omega_2) by a \Pi_1-formula without parameters imply that the GCH holds at \omega_1? This is joint work with Peter Holy (Bristol).

ABSTRACT. It is an interesting program to investigate the relationship between the proof theory of second order arithmetic and more general second order systems (e.g. theories of sets and classes such as von Neumann-Bernays-Goedel set theory and Morse-Kelley set theory). Which proof-theoretic results can be lifted from second order arithmetic to theories of sets and classes, for which is this not the case, and what are the reasons? What is specific of second order number theory and what additional insights can we gain?

One of the crucial questions is how to distinguish between "small" and "large" in the various contexts. In second order arithmetic, the small objects are the natural numbers whereas the large objects are the infinite sets of natural numbers. Hence it seems natural to identify the small objects in sets and classes with sets and the large objects with proper classes.

As long as only comparatively weak systems are concerned, the moving up from second order arithmetic to sets and classes seems to be a matter of routine. However, as soon as well orderings enter the picture, the situation becomes interesting. In second order arithmetic, every $\Pi^1_1$ statement is equivalent to the question whether a specific arithmetic relation is well ordered; on the other hand, in set theory a simple elementary formulas expresses the well foundedness of a given relation.

We propose studying the (new) notion of weak well order in sets and classes as the proof-theoretically adequate analogue of well order in second order arithmetic. To support this claim several results about inductions and recursions in connection with weak well orders will be presented. This is joint work with D. Flumini.

ABSTRACT. We discuss the automation of inductive proof.

ABSTRACT. In [4], Maddy gives a semi-formal account of restrictiveness by defining a corresponding formal notion based on a class of interpretations. In [2] and [3], Maddy's notion of restrictiveness was discussed and the theory ZF + `Every uncountable cardinal is singular' was presented as a potential witness to the restrictiveness of ZFC. More recently, Hamkins has given more examples and pointed out some structural issues with Maddy's definition [1]. We look at Maddy's definitions from the point of view of an abstract interpretation relation. We consider various candidates for this interpretation relation, including one that is close to Maddy's original notion, but fixes the issues raised in [1]. Our work brings to light additional structural issues that we also discuss.

ABSTRACT. It has been argued by Feferman and others that when we accept a mathematical theory, we implicitly commit ourselves to reflection principles for this theory. When we reflect on this implicit commitment, we come to explicitly believe certain reflection principles. In my talk I will discuss our epistemic warrant for this resulting explicit belief in reflection principles.

ABSTRACT. We introduce several first-order axiom systems for general relativity and show that they are complete with respect to the standard models of general relativity, i.e., to Lorentzian manifolds having the corresponding smoothness properties.

This is only a sample of our approach (see the references in [2]) to the logical analysis of special and general relativity theory in the axiomatic framework of modern mathematical logic. The aim of our research is to build a flexible hierarchy of axiom systems (instead of one axiom system only), analyzing the logical connections between the different axioms and axiomatizations. We try to formulate simple, logically transparent and intuitively convincing axioms. The questions we study include: What is believed and why? - Which axioms are responsible for certain predictions? - What happens if we discard some axioms? - Can we change the axioms, and at what price?

[1] H. Andréka, J.X. Madarász, I. Németi, and G. Székely, An axiom system for general relativity complete with respect to Lorentzian manifolds, arXiv:1310.1475, 2013.

[2] H. Andréka, J.X. Madarász, I. Németi, and G. Székely, A logic road from special relativity to general relativity, Synthese, vol. 186 (2012), no. 3, pp. 633–649, arXiv:1005.0960.

ABSTRACT. In [1] a new framework for predicative mathematics was developed. The main new features of this framework are that it is type-free, based on a subsystem of ZF, and the language it employs includes nothing that is not used in ordinary mathematical texts. In particular: it reflects real mathematical practice in making an extensive use of statically defined abstract set terms of the form {x|φ}.

In this work we show how large portions of classical analysis can be developed within that framework in a natural, predicatively acceptable way. Among other things, this includes the introduction of the natural numbers, the real line and continuous real functions, as well as formulating and proving the main classical results concerning these notions.

[1] Arnon Avron, A New Approach to Predicative Set Theory, Ways of Proof Theory (R. Schindler, editor), Onto Series in Mathematical Logic, onto verlag, 2010, pp. 31 - 63.

ABSTRACT. Moritz Cantor was so impressed by the achievements of Piero della Francesca in mathematics and geometry that devoted him in his Vorlesungen uber Geschichte der Mathematik far more attention than to any other contem- porary algebraicist. In Francesca's treatise De prospectiva pingendi we find the advanced geometrical exercises presented in the form of propositions. For instance, in Book 1, Proposition 8, he shows that the perspective images of orthogonals converge to a point. Proposition 12 shows how to draw in per- spective a surface of undefined shape, which is located in profile as a straight line. The task is to find the image of a line perpendicular to the picture plane. But the most interesting is Proposition 13 that shows how to degrade a square and, more precisely the sides of the square. It is obvious that most of these propositions are used in the paintings of Francesca. The purpose of the study is to describe these results in the form of logi- cal system EF. Generally, the logical language is six sorted, with sorts for points, lines, circles, segments, angles, and areas. As proofs it is possible to employ the method of natural deduction. The aim is to demonstrate that such a method is the most useful for the presentation of the geometric proofs of Francesca, taking into account also the importance of diagrams within them.

ABSTRACT. The history of modern mathematical proof theory begins with Beweistheorie or Hilbert’s proof theory. The mathematical theories such as logicism (Frege, Russell), intuitionism (Brouwer, Heyting), set theory (Cantor, Dedekind) influenced directly the conception of proof and generally modern proof theory. The modern proof theory is based not only on mathematical theories, but also on the philosophical and logical proof theories, such as Aristotle’s conception of demonstration. According to Aristotle a demonstration is a “scientific syllogism”, in which the premises are true, first, immediate, more known than the conclusion, prior to the conclusion and causes of the conclusion. Aristotle’s theory of demonstration impacted on the development of logic and, in particular, on the philosophical and logical conception of proof. Can we say that Aristotle’s conception of demonstration is modern? Is the actual conception of proof really based on Aristotle’s conception? The purpose of my talk is to analyze Aristotle’s definition of demonstration and compare it with the modern approach to demonstration. [1]Barnes, J. Aristotle. Posterior Analytics. Oxford University Press, 1976. [2]Hendricks, V. et al., eds, Proof Theory: History and Philosophical Significance, Kluwer. 2000.

ABSTRACT. As it is widely-known, fiction became a serious problem for several classical conceptions closed related to philosophy of logic (J. Woods, 2006). This was mainly due to some of the leading features of reasoning in fiction. Firstly, inference in fiction involves reasoning with incomplete information. Stories describe their characters, places, and events only in an incomplete way. Due to the fact that stories are composed by a finite set of sentences, a large amount of information about them remains unknown. Secondly, inference in fiction also involves reasoning with inconsistent information. Inconsistencies can emerge from two sources. On the one hand, information belonging to a fiction contradicts reality in many aspects. On the other hand, some stories are based on a contradiction or contain inconsistent information. This is the case of stories in which contradictions are an essential part of their plots. In order to cope with the abovementioned features of reasoning in fiction, we propose a semantic approach of fiction based on an intuitionistic modal system. The semantic model is an adaptation of the multiple-expert semantics developed by Melvin Fitting in 1992. Firstly, we consider a propositional language to represent fictional information formally. That propositional language is interpreted in an intuitionistic modal semantics that involves two different perspectives and a partial valuation. On the one hand, these two perspectives make it possible to distinguish two sources of information involved in reasoning in fiction, i.e., fiction and reality. On the other hand, the partial valuation makes it possible to deal with incomplete information. A relation of logical consequence is defined in order to distinguish between valid and invalid inferences within the fictional context. Finally, we explore different proof-theoretical alternatives in order to characterize a deductive system for this semantic approach.

ABSTRACT. Metalogical extensions incorporate metalogics by means of new logical symbols. Among many other things, they thereby yield a soundness criterion for immanent attempts, which try to reflect provability or truth by means of unary formulae in stock. However, this benchmark cannot be met within sufficiently strong consistent theories—a further consequence of the Diagonal Lemma. Thus it is particularly questionable whether Prov(x) really expresses provability and Con (derived therefrom) really states consistency: the 2nd Incompleteness Theorem may be doubted.