ABSTRACT. Covertly computational insights have influenced the Theory of Evolution from the very start. I shall discuss recent work on some central problems in Evolution that was inspired and informed by computational ideas. Considerations about the performance of genetic algorithms led to a novel theory of the role of sex in Evolution based on the concept of mixability, the population genetic equations describing the evolution of a species can be reinterpreted as a repeated game between genes played through the multiplicative update algorithm, while a theorem on satisfiability can shed light on the emergence of complex adaptations.

ABSTRACT. Admissible computability is an extension of traditional computability theory to ordinals beyond the finite ones. I will discuss two manifestations of admissible computability in the study of effective randomness and in the study of effective properties of uncountable structures.

ABSTRACT. Logic and games are entangled in delicate ways. Logics {\bf of} games are used to analyze how players reason and act in a game. I will discuss dynamic-epistemic logics that analyze various phases of play in this mode. But one can also study logic {\bf as} games, casting major logical notions as game-theoretic concepts. The two perspectives create a circle, or double helix if you will, of contacts all around. I will address this entanglement, and the issues to which it gives rise (\cite{vB}).

ABSTRACT. I will give an overview of dependence logic, the goal of which is to establish a basic logical theory of dependence and independence underlying seemingly unrelated subjects such as game theory, causality, random variables, database theory, experimental science, the theory of social choice, Mendelian genetics, etc. There is an abundance of new results in this field demonstrating a remarkable convergence. The concepts of (in)dependence in the different fields of humanities and sciences have surprisingly much in common and a common logic is starting to emerge.

ABSTRACT. We will describe a program for analyzing groups and sets definable in certain pairs (R, P). Examples include:

(1) R is an o-minimal ordered group and P is a real closed field with bounded domain (joint work with Peterzil) (2) R is an o-minimal structure and P is a dense elementary substructure of R (work in progress with Hieronymi)

In each of these cases, a relevant notion of a pregeometry and genericity is used.

ABSTRACT. A structure $M$ is quasiminimal if every definable subset of $M$ is either countable or co-countable. The field of complex numbers is a strongly minimal structure and hence quasiminimal, but if we add the natural exponential function, the quasiminimality of the structure becomes an open problem. Boris Zilber defined the non-elementary framework of \textit{quasiminimal excellent classes} in 2005 in order to show that his class of \textit{pseudoexponential fields} is uncountably categorical. He conjectured that the unique pseudoexponential field of cardinality $2^{\aleph_0}$ fitting into this framework is isomorphic to the complex numbers with exponentiation. A key property for the categoricity of quasiminimal excellent classes was the technical axiom of excellence, which was adopted from Shelah’s work for excellent sentences in $L_{\omega_1\omega}$. However, the original proof of the categoricity of pseudoexponential fields turned out to have a gap and the problem lay in sh! owing that the excellence axiom holds.

In the paper \textit{Quasiminimal structures and excellence}\cite{cite1} we fill the gap in the proof with a surprising result: the excellence axiom is actually redundant in the framework of quasiminimal excellent classes. This result elegantly combines methods from classification theory that were generalized to different non-elementary frameworks by a group of people. These methods have a combinatorial core idea that is independent of the compactness of first order logic. We also study whether other quasiminimal structures fit into this uncountably categorical framework.

The paper strengthens the belief that non-elementary methods can provide effective tools to analyse structures that are out of reach for traditional model-theoretic methods. Different frameworks have been suggested and the methods refined and there are many interesting paths in the ongoing research. The paper is joint work of Martin Bays, Bradd Hart, Tapani Hyttinen, MK and Jonathan Kirby.

ABSTRACT. The talk will be devoted to various versions of algorithmic reducibility notion between algebraic structures. In particular, the reducibilities under Turing operetors, enumeration operators, and under $\Sigma$-formulas will be considered. Several constructions of jump inversion where these reducibilities do not coincide. Furthermore, the $\Sigma$-reducibility between the direct sums of cyclic p-groups will be studied in detail.

ABSTRACT. .

ABSTRACT.  

Proofs by mathematical induction seem to require certain interdependencies between the instances of the generalizations they prove. The character and significance of these interdependencies will be the main subject of this talk.

ABSTRACT. Datalog is a language based on function-free Horn clauses used to inductively define new relations from finite relational structures. Datalog has many nice computational and logical properties. For example, Datalog captures PTIME on ordered structures, which means that evaluating fixed Datalog programs (i.e. rule sets) over finite structures is in PTIME and, moreover, every PTIME-property on ordered structures can be expressed as a Datalog program (see [1] for a survey). After giving a short overview of Datalog we argue that this formalism has certain shortcomings and is not ideal for knowledge representation, in particular, for inductive ontological knowledge representation and reasoning. We consequently introduce Datalog+/- which is a new framework for tractable ontology querying, and for a variety of other applications. Datalog+/- extends plain Datalog by features such as existentially quantified rule heads, negative constraints, and equalities in rule heads, and, at the same time, restricts the rule syntax so as to achieve decidability and tractability. In particular, we discuss three paradigms ensuring decidability: chase termination, guardedness, and stickiness, which were introduced and studied in [2, 3, 4, 5].

[1] Dantsin, E.; Eiter, T.; Georg, G.; and Voronkov, A. 2001. Complexity and expressive power of logic programming. ACM Computing Surveys 33(3):374-425. [2] Cali, A.; Gottlob, G.; and Kifer, M. 2013. Taming the innite chase: Query answering under expressive relational constraints. Journal of Articial Intelligence Research 48:115-174. [3] Cali, A.; Gottlob, G.; and Lukasiewicz, T. 2012. A general Datalog-based frame- work for tractable query answering over ontologies. Journal of Web Semantics 14:57-83. [4] Cali, A.; Gottlob, G.; and Pieris, A. 2012. Towards more expressive ontology languages: The query answering problem. Artificial Intelligence 193:87-128. [5] Gottlob, G.; Manna, M.; and Pieris, A. 2013. Combining decidability paradigms for existential rules. Theory and Practice of Logic Programming 13(4-5):877-892.

ABSTRACT. Recent investigations in denotational semantics led Ehrhard to define a new model of lambda-calculus and linear logic called finiteness spaces. In finiteness spaces, types are interpreted as topological vector spaces, lambda-terms and (via the Curry-Howard correspondence) intuitionistic proofs are interpreted as analytic functions in topological vector spaces.

However, analytic functions are infinitely differentiable, thus the question arise whether differentiation can be defined as a meaningful syntactic operation. A positive answer from a computational perspective is given by differential lambda$-calculus, an extension of lambda-calculus in which the operations of differentiation and Taylor expansion of a lambda-term are definable. One of the interests of differential lambda-calculus lies in the analogy that can be drawn between the usual notion of differentiation (i.e. linearity in mathematical sense) and its computational meaning (i.e. linearity in computational sense).

It turns out that differentiation and the actual infinite operation involved in Taylor expansion makes sense also in a purely logical setting. The right syntax is provided by differential linear logic (DiLL) and analyzed in terms of differential interaction nets by T. Ehrhard and L. Regnier (2006). DiLL is an extension of LL characterized by three new rules dealing with the ! modality: cocontraction, codereliction, and coweakening. The latter rules are called "co-structural" and, in a one-sided sequent calculus setting, can be considered as symmetric duals of the ?-rules. Co-structural rules give a logical status to differentiation.

In this paper, we introduce a natural deduction system for intuitionistic DiLL. We show normalization and, as corollaries, subformula, separability and introduction form properties for this system. Its relationships with the natural deduction systems for intuitionistic logic are discussed.

ABSTRACT. We outline an intuitionistic view of knowledge which maintains the Brouwer-Heyting-Kolmogorov semantics and is consistent with Williamson's suggestion that intuitionistic knowledge is the result of verification and that verifications do not necessarily yield strict proofs. On this view, A --> KA is valid and KA --> A is not. The former expresses the constructivity of truth, while the latter demands that verifications yield strict proofs. Unlike in the classical case where

Classical Knowledge ==> Classical Truth

intuitionistically

Intuitionistic Truth ==> Intuitionistic Knowledge.

Consequently we show that KA --> A is a distinctly classical principle, too strong as the intuitionistic truth condition for knowledge, ``false is not known,''which can be more adequately expressed by e.g., ~(KA & ~A) or, equivalently, ~(K⊥).

We construct a system of intuitionistic epistemic logic:

IEL = intuitionistic logic IPC + K(A-->B)-->(KA-->KB) + (A-->KA) + ~(K⊥)

provide a Kripke semantics for it and prove IEL soundness, completeness and the disjunction property.

IEL can be embedded into an extension of S4, S4V, via the Godel embedding ``box every subformula.'' S4V is a bi-modal classical logic consisting of the rules and axioms of S4 for [] and D for K, with the connecting axiom []A --> KA. The soundess of the embedding is proved.

Within the framework of IEL, the knowability paradox is resolved in a constructive manner. Namely, the standard Church-Fitch proof reduces the intuitionistic knowability principle A --> <>KA to A --> ~~KA, which is an IEL-theorem. Hence the knowability paradox in the domain of IEL disappears since neither of these principles are intuitionistically controversial. We argue that previous attempts to analyze the paradox were insufficiently intuitionistic.

ABSTRACT. We discuss relationships between the existence property (EP) and its weak variants in intermediate predicate logics.

In [2], we provided a negative answer to Ono's problem P52 in intermediate predicate logics (Does EP imply the disjunction property? [1]), and presented some related results.

To solve the problem, we considered two variants of EP in super-intuitionistic predicate logics, and used them to construct counterexamples in intermediate logics. One variant is an extreme EP; namely, for every \exists xA(x), L |- \exists xA(x) implies that there exists a fresh individual variable v such that L |- A(v). This property is so extreme that none of intermediate predicate logics has it. However, if we restrict \exists xA(x) to a sentence, EP implies this property, which we call the sentential existence property (sEP). Another one is a weak variant of EP; an intermediate predicate logic L is said to have the weak existence property (wEP), if for every \exists xA(x) that contains no free variables other than v_1, ..., v_n, L |- \exists xA(x) implies L |- A(v_1)\vee...\vee A(v_n). Then, it is easy to see that EP implies wEP, and wEP implies sEP.

In the present talk, we show that the converses of these implications do not hold in intermediate predicate logics.

[1] H. Ono, Some problems in intermediate predicate logics, Reports on Mathematical Logic, vol. 21 (1987), pp.55--67.

[2] N.-Y. Suzuki, A negative solution to Ono's problem P52: Existence and disjunction properties in intermediate predicate logics, submitted.

ABSTRACT. For several normal modal logics we construct countable many their normal extensions, which are Hallden complete, as well as uncountable many, which are not. Our approach to this task is purely semantic.

ABSTRACT. In 1906, Russell [5] showed that all the known set-theoretic paradoxes (till then) had a common form. In 1969, Lawvere [3] used the language of category theory to achieve a deeper unication, embracing not only the set-theoretic paradoxes but incompleteness phenomena as well. To be precise, Lawvere gave a common form to Cantor's theorem about power sets, Russell's paradox, Tarski's theorem on the undefinability of truth, and Godel's first incompleteness theorem. In 2003, Yanofsky [7] extended Lawvere's ideas using straightforward set-theoretic language and proposed a universal schema for diagonalization based on Cantor's theorem. In this universal schema for diagonalization, the existence of a certain (diagonalized-out and contradictory) object implies the existence of a fixed-point for a certain function. He showed how self-referential paradoxes, incompleteness, and fixed-point theorems all emerge from the single generalized form of Cantor's theorem. Yanofsky extended Lawvere's analysis to include the Liar paradox, the paradoxes of Grelling and Richard, Turing's halting problem, an oracle version of the P=?NP problem, time travel paradoxes, Parikh sentences, Lob's Paradox and Rice's theorem. In this talk, we fit more theorems in the universal schema of diagonalization, such as Euclid's theorem on the infinitude of the primes, and new proofs of Boolos [1] for Cantor's theorem on the non-equinumerosity of a set with its powerset. We also show the existence of Ackermann-like functions (which dominate a given set of functions such as primitive recursive functions) using the schema. Furthermore, we formalize a reading of Yablo's paradox [6], the most challenging paradox in the recent years, in the framework of Linear Temporal Logic (LTL [2]) and the diagonal schema, and show how Yablo's paradox involves circularity by presenting it in the framework of LTL. All in all, we turn Yablo's paradox into a genuine mathematico logical theorem. This is the first time that Yablo's paradox becomes a (new) theorem in mathematics and logic. We also show that Priest's [4] inclosure schema can fit in our universal diagonal/fixed-point schema. The inclosure schema was used by Priest for arguing for the self-referentiality of Yablo's sequence of sentences, in which no sentence directly refers to itself but the whole sequence does so.

[1] George Boolos, Constructing Cantorian Counterexamples, Journal of Philosophical Logic, vol. 26 (1997), no. 3, pp. 237-239.

[2] Fred Kroger & Stephan Merz, Temporal Logic and State Systems, EATCS Texts in Theoretical Computer Science, Springer, 2008.

[3] F. William Lawvere, Diagonal arguments and cartesian closed categories, Category theory, homology theory and their applications II (Seattle Research Center of the Battelle Memorial Institute), LNM 92, Springer, Berlin, 1969, pp. 134-145.

[4] Graham Priest, Yablo’s Paradox, Analysis, vol. 57 (1997), no. 4, pp. 236-242.

[5] Bertrand Russell, On some difficulties in the theory of transfinite numbers and order types, Proceedings of the London Mathematical Society, vol. s2-4 (1907), no. 1, pp. 29-53.

[6] Stephen Yablo, Paradox without Self-Reference, Analysis, vol. 53 (1993), no. 4, pp. 251-252.

[7] Noson S. Yanofsky, A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points, Bulletin of Symbolic Logic, vol. 9 (2003), no. 3, pp. 362-386.

ABSTRACT. The algebraic models of substructural logics are residuated ordered algebras [2]. Embedding a residuated ordered algebra into a complete algebra of the same class has many applications in logic, e.g., the canonical extension is used to obtain relational semantics for non-classical logics [1].

The underlying sets of the algebraic structures of interest are often partially ordered. The canonical extensions of posets have been studied in [1, 2]. Upon closer inspection it can be seen that the completions in [1] and [2] are generally different. Both use a construction, first appearing in [3], based on a Galois connection between sets of filters and ideals, however, the choice of filters differs.

We investigate the construction from [3] for various choices of filters and ideals, consider the extension of operations defined on the posets and focus on some specific properties of completions obtained via this construction. Next we present a construction for completions of posets that makes use of the prime filters of the posets. We show that the completion obtained via this second construction is isomorphic to the former for a particular choice of filters.

ABSTRACT. Nowadays many-valued logics occupy new areas of computer science. Being extensively used in various areas, theoretical investigations of different properties in such logics is a challenging area of research [1]. Firstly it worths mentioning that axiomatic systems for many valued logics are not well developed. Secondly many notions are not naturally extended in many valued logics from already existing analogues of classical or other "well-developed" non classical logics. One of the key properties to characterize first order logic is compactness. We formulate an analogue of classical compactness theorem for arbitrary N-valued logic. To prove it overloading operators are constructed.

ABSTRACT. Descriptions and statements about the physical world often involve vague predicates, e.g., "x is red". It has become a common procedure to assign vague predicates intermediate truth values that are real numbers between 0 and 1. However, there is no satisfactory account what it means to be true to a given degree, which leaves doxastic degrees as the only option. Furthermore, real numbers provide an almost absurd accuracy as well as a natural metric, where in fact we want to state no more than, say, that x is rather red than not, perhaps redder or less red than some y. That suggests considering vagueness as a relational notion.

A thereby established vagueness relation is a partial order. Advantages of a relational account of vagueness are that vague predicates form a comparatively weak structure without metric and that the well-known problem of higher-order vagueness vanishes.

There is no reason not to implement doxastic degrees on the object language level. Furthermore, with the practice of evaluating vague predicates, relational vagueness should be allowed to depend on perception and epistemic as well as pragmatic context and hence be non-extensional. To set up a requisite formal language, we enclose vagueness predicates in quotation marks and perform their assessment with a background in mind which provides epistemic and pragmatic context. Thus a ternary predicate is introduced, B'Ax''Ay'b, read "I believe, with background b, Ax to at least as high a degree as Ay". Given background b, believing Ax with absolute confidence is formalized as B'Ax''0=0'b.

Such a formalization may be applied to conferring values to physical magnitudes which uses approximations and error bars. "The value of a is v" would then be vague as much as "x is red", acknowledging a fuzzy nature of experimental, particularly, macroscopic physics.

ABSTRACT. This report concerns to the problem of constructing tableau-based proof procedure for a logic of generalized truth values. We propose two different tableau-style formalisation for a logic which captures a syntactical analogue of semantic logical consequence relation. One of them is more or less 'traditional' and resembles tableau systems for relevant logic FDE. Another one is appropriate for designing a proof search procedure and based on well known KE formalism.

ABSTRACT. The admissible rules of a logic are those rules under which the set of its theorems are closed. Many non-classical logics have interesting admissible rules, and these admissible rules carry quite a bit of information. In fact, some logics can even be completely characterised by way of their admissible rules. Consider the lattice of intermediate logics, that is, the lattice of consistent extensions of propositional intuitionistic logic. The disjunction property is an example of an admissible rule. It is well-known that there are continuum many logics among that lattice that enjoy the disjunction property, Medvedev’s logic and Kreisel–Putnam logic to name but two. It was shown by Maksimova that Medvedev’s logic can be characterised as the maximal intermediate logic above Kreisel–Putnam logic with the disjunction property. The intuitionistic propositional logic itself can also be characterised as the maximal intermediate logic that admits a particular set of rules, as has been independently confirmed by Skura and Iemhoff. The rules they employed arose independently in the work of Citkin and Visser. These rules can be stratified in natural way with respect to admissibility in the logics of bounded branching, also known as the Gabbay–de Jongh logics. We will present a characterisation of each of these logics as being the maximal intermediate logic admitting a particular strata of the aforementioned rules.

ABSTRACT. The usual approach to treating the probability of a sentence leads to a kind of polymodal logic with iterated (or not iterated) probability operators over formulae (see [3]). On the other hand, there were some papers dealing with probabilistic form of inference rules (see [1], [2] and [4]). The sequent calculi present a particular mode of deduction relation analysis. The combination of these concepts, the sentence probability and the deduction relation formalized in a sequent calculus, makes it possible to build up sequent calculus probabilized --- the system {\bf LKprob}. Sequents in {\bf LKprob} are of the form $\Gamma\vdash_a^b\Delta$, meaning that 'the probability of provability of $\Gamma\vdash\Delta$ is in interval $[a,b] \cap I$', where $I$ is a finite subset of reals $[0,1]$.

Let $\text{\rm Seq}$ be the set of all sequents of the form $\Gamma\vdash\Delta$. A model for {\bf LKprob} is any mapping $p: \text{\rm Seq} \to [0,1]$ satisfying: \it (i) \rm $p(A\vdash A)=1$, for any formula $A$; \it (ii) \rm if $p(AB\vdash )=1$, then $p( \vdash AB)=p( \vdash A)+p( \vdash B)$, for any formulas $A$ and $B$; \it (iii) \rm if sequents $\Gamma\vdash\Delta$ and $\Pi\vdash\Lambda$ are equivalent in $\text{\bf LK}$, in sense that there are proofs for both sequents $\bigwedge \Gamma \rightarrow \bigvee \Delta \vdash \bigwedge \Pi \rightarrow \bigvee \Lambda$ and $\bigwedge \Pi \rightarrow \bigvee \Lambda\vdash \bigwedge \Gamma \rightarrow \bigvee \Delta $ in $\mathbf{LK}$, then $p(\Gamma\vdash\Delta)=p(\Pi\vdash\Lambda)$.

We prove that our probabilistic sequent calculus {\bf LKprob} is sound and complete with respect to the models just described.

\begin{thebibliography}{10}

\bibitem{cite1} {\scshape A. M. Frisch, P. Haddawy}, {\itshape Anytime deduction for probabilistic logic}, {\bfseries\itshape Artificial Intelligence}, vol.~69 (1993), pp.~93--122.

\bibitem{cite2} {\scshape T. Hailperin}, {\itshape Probability logic}, {\bfseries\itshape Notre Dame Journal of Formal Logic}, vol.~25 (1984), pp.~198--212.

\bibitem{cite3} {\scshape Z. Ognjanovi\'c, M. Ra\v skovi\'c, Z. Markovi\'c}, {\itshape Probability logics}, {\bfseries\itshape Logic in Computer Science}, Zbornik radova 12 (20), Z. Ognjanovi\'c (ed.), Mathematical Institute SANU, Belgrade, 2009, pp. ~35--111.

\bibitem{cite4} {\scshape C. G. Wagner}, {\itshape Modus tollens probabilized}, {\bfseries\itshape British Journal for the Philosophy of Science}, vol.~54(4) (2004), pp.~747–-753.

\end{thebibliography}

ABSTRACT. The proposed talk gives a general outline of a line of research aimed at providing a wide array of logics (spanning from dynamic logics to monotone modal logic through substructural logics) with display type proof systems which in particular enjoy a uniform strategy for cut elimination. We generalize display calculi in two directions: by explicitly allowing different types, and by dropping the full display property. The generalisation to a multi-type environment makes it possible to introduce specific tools enhancing expressivity, which have proved useful e.g. for a smooth proof-theoretic treatment of multi-modal and dynamic logics. The generalisation to a setting in which the full display property is not required makes it possible to account for logics, such as monotone modal logic, which admit connectives which are neither adjoints nor residuals.

ABSTRACT. We investigate the complexity of systems of Multi-agent Justification Logic with interacting justifications (see [1]). The system we study has n agents, each based on some (single-agent) justification logic (we consider J, J4, JD, JD4, JT, LP) and a transitive, irreflexive binary relation, C. Each agent i has its own set of axioms, depending on the logic it is based on. If iCj, then we include axiom t:i φ -> t:j φ (we do not include V-Verification as in [1]). Finally, it has a sufficient amount of propositional axioms and an axiomatically appropriate constant specification, which is in P. Traditionally, to establish upper complexity bounds for satisfiability for Justification Logic, we use a set of tableau rules to generate a branch and then we run the ∗-calculus on it. A similar system for (diamond-free) modal logic was studied in [2]. We adjust appropriately the tableau for the corresponding system in [2] and the ∗-calculus can be run locally for every prefix, so we can use the same methods as in [2] to establish upper bounds. On the other hand, we can see that if we replace [i] by x:i in a diamond-free modal formula (for all i), then the new formula is satisfiable iff the old one was. Thus, we can prove the same complexity bounds as in [2] - with the exception that where satisfiability for a modal logic is in NP, the corresponding justification logic has its satisfiability in the second level of the polynomial hierarchy. [1] Antonis Achilleos, Complexity jumps in Multi-agent Justification Logic with interacting justifications, Under submission [2] ____ Modal logics with hard diamond-free fragments, Under submission

ABSTRACT. We describe two sufficient properties of graphs Gn on n vertices such that the formulas based on them have exponential Resolution proof steps. The network style graphs of Tseitins formulas and graphs of Urquhart are examples of graphs with mentioned properties. If at least one of these properties is not valid for any graph, then the corresponding formula has polynomial bounded resolution refutation.

ABSTRACT. We consider the decomposability problem for finite theories, i.e. the problem to decide whether a theory can be represented as a union of two (or several) theories sharing a given set of signature symbols. The algorithmic complexity of this problem has been studied in various calculi, ranging from first-order logic to classical propositional and Description Logics. The results suggested that the complexity of decomposability coincides with the complexity of entailment in the underlying logic. Although this observation was not too surprising, a general method for proving this claim was missing. We describe a method of proving that the complexity of deciding decomposability coincides with the complexity of entailment in fragments of first-order logic. We illustrate this method by showing the complexity of decomposability in signature fragments of first-order logic, i.e. those which are obtained by putting restrictions on signature.

ABSTRACT. The aim of this talk is to propose a constructive understanding of second order logic: it is argued that a better grasp of the functional content of the comprehension rule comes from the consideration of inference rules independently of logical correctness; the situation is analogous to that of computation, whose proper functional description imposes to consider non terminating (i.e. “wrong”) algorithms. The Curry-Howard correspondence allows indeed a shift from the question of provability (within a formal system) to that of typability for pure lambda terms, representing for instance recursive functions. By relying on well-known results on type inference, an equational description, independent of type systems, of the predicates required to build proofs of totality is presented: one no more focuses on what one can prove by means of a certain package of rules, but rather on what the rules needed to prove a certain formula must be like, at the level of their functional description. This might look a bit weird at first glance: by applying this technique it is possible, in principle, to construct second order proofs of totality for all partial recursive functions! The assumption that every system of type equations defines a set of types is indeed equivalent to a naive comprehension axiom. The focus on typability conditions exposes a different point of view on the phenomenon of incompleteness: the lack of the relevant “diagonal” or “limit ” proof is indeed explained by the lack of the relevant “diagonal” or “limit” predicates. On the other hand, on the basis of a characterization of the solvability of type equations by means of recursive techniques, it is conjectured that such a “naıve” approach to second order proofs is “complete” in the following sense: all total recursive functions are provably total in some consistent subsystem of the whole (violently inconsistent) system of equational types.

ABSTRACT. This work describes an intuitive semantics in the style of Girard's well-known cigarette vending machine for Full Intuitionistic Linear Logic. Full Intuitionistic Linear Logic (FILL) was introduced by Hyland and de Paiva [1] as arising from its categorical semantics, while hinting at its independent interest as a framework for forms of parallelism in Functional Programming. The systems FILL and its intuitionistic counterpart FIL[2] show that the constructive character of logical systems is not given by syntactic size restrictions on sequent calculus, but comes about by explaining connectives in terms of intensional constructions/operations/transformations on derivations of the system. This seems to us the central message of the Brouwer-Heyting-Kolmogorov (BHK) interpretation and also of the Curry-Howard isomorphism, which we take as guiding criteria for our mathematical logic investigations. This work also aims to explain to the mythical man-on-the street what Full Intuitionistic Linear Logic is about. We were pressed on the point that, elegance of categorical constructions and esthetic criteria on proof systems notwithstanding, one should always be able to say what our logical operations mean in common words, when describing a new logical system like FILL. Initially we had no intuitive explanation for the multiplicative disjunction 'par', which now seems more understandable in terms of interactions with a 'stock-keeping' system.

ABSTRACT. Born out of the need to formalize common sense in Articial Intelligence (AI), Ar- gumentation Logic (AL) brings together the syllogistic roots of logic with recent argumentation theory from AI to propose a new logic based on argumentation.

Argumentation Logic is purely proof theoretic dened via a criterium of acceptabil- ity of arguments. Arguments in AL are sets of propositional formulae with the acceptability of an argument ensuring that the argument can defend against any other argument that is inconsistent with it, under a given propositional theory. AL can be linked to Natural Deduction allowing us to reformulate Propositional Logic (PL) in terms of argumentation and to show that, under certain conditions, AL and PL are equivalent. AL separates proofs into direct and indirect ones, the latter being through the use of a restricted form of Reductio ad Absurdum (RAA) where the (direct) derivation of the inconsistency must depend on the hypothesis posed when we apply the RAA rule.

As such AL is able to isolate inconsistencies in the given theory and to behave agnostically to them. This gives AL as a conservative paraconsistent extension of PL that does not trivialize in the presence of inconsistency. The logic then captures in a single framework defeasible reasoning and its synthesis with the strict form of reasoning in classical logic. The interpretation of implication in AL is dierent from that of material implication, closer to that of default rules but where proof by contradiction can be applied with them. AL has recently formed the basis to formalize psychological theories of story comprehension.

ABSTRACT. We study the $\exists$--interpretability of constructive structures of finite predicate signatures. This definition is motivated by a kind of effective interpretability of abstract databases and leads to a good natural translation of $\exists$--queries.

The following definition is a restricted variant of the standard well--known definition of interpretability of structures:

\smallskip \noindent{\bf Definition. } {\it Let $\mathfrak{A}_0$ and $\mathfrak{A}_1$ be two structures of finite predicate signatures and let $\langle P_1,\ldots, P_k\rangle$ be the signature of $\mathfrak{A}_0$. We say that $\mathfrak{A}_0$ has a $\exists$--interpretation in $\mathfrak{A}_1$ if there exist \begin{itemize} \item $n\in\omega$ and a finite tuple of parameters $\bar p\in\mathfrak{A}_1$, \item $\exists$--formula $U(\bar x,\bar y)$, $|\bar x|=n$, \item $\exists$--formulas $E^+(\bar x_0,\bar x_1,\bar y)$ and $E^-(\bar x_0,\bar x_1,\bar y)$ such that $|\bar x_0|=|\bar x_1|=n$, \item $\exists$--formulas $P^+(\bar x_1,\ldots,\bar x_m,\bar y)$ and $P^-(\bar x_1,\ldots,\bar x_m,\bar y)$, for each predicate symbol $P$ of the signature of $\mathfrak{A}_0$, where $m$ is the arity of $P$ with the property $|\bar x_1|=\cdots=|\bar x_m|=n$, \end{itemize} such that \begin{enumerate} \item The set $(U^{\mathfrak{A}_1}(\bar x))^2$ is a disjunct union of the sets $\{\langle\bar x_0,\bar x_1\rangle\mid \mathfrak{A}_1\models E^\varepsilon(\bar x_0,\bar x_1,\bar p)\}$, $\varepsilon\in\{+,-\}$. \item For any $m$--ary predicate symbol $P$ of the signature of $\mathfrak{A}_0$, the set $(U^{\mathfrak{A}_1}(\bar x))^m$ is a disjunct union of the sets $\{\langle\bar x_0,\ldots,\bar x_m\rangle\mid \mathfrak{A}_1\models P^\varepsilon(\bar x_0,\ldots,\bar x_m,\bar p)\}, \ \varepsilon\in\{+,-\}$. \item Let $\widehat{P_i}=\{\langle\bar x_1,\ldots,\bar x_m\rangle\mid\mathfrak{A}_1\models P^+(x_1,\ldots,\bar x_m,\bar p)\}, \mbox{ äëÿ }i=1,\ldots,k$. Then the relation $E=\{\langle \bar x_0,\bar x_1\rangle\mid\mathfrak{A}_1\models E^+(\bar x_0,\bar x_1,\bar p)\}$ is a congruence on $\mathfrak{B}=\langle U^{\mathfrak{A}_1}(\bar x),\widehat{P}_1,\ldots,\widehat{P}_k\rangle$ and the quotient algebra $\mathfrak{B}/\!E$ is isomorphic to $\mathfrak{A}_0$. \end{enumerate} }

\noindent{\bf Theorem. } {\it \begin{enumerate} \item The $\exists$--interpretability generates an upper semilattice ${\mathcal L}_\exists$ in which computable structures form a principal ideal ${\mathcal L}^0_\exists$; in particular, there exists a universal computable structure, i.e., a computable structure that $\exists$-interprets any computable structure. \item Any finite partial order is embeddable into ${\mathcal L}^0_\exists$. \end{enumerate} }

ABSTRACT. Computable presentations for projective planes are studied. We prove that the isomorphism problem is $\Sigma^1_1$-complete for the following classes of projective planes: pappian projective planes, desarguesian projective planes, arbitrary projective planes.

ABSTRACT. It is well established that the class of countable symmetric irreflexive graphs is complete in computable model theory: every countable structure in a finite language can be coded into a graph in such a way that the graph has the same spectrum, the same computable dimension, and the same categoricity spectrum as the original structure, and shares most other known computable-model-theoretic properties of the original structure as well. In 2002, Hirschfeldt, Khoussainov, Shore, and Slinko collected related results and proved more, showing that many other classes of countable structures are complete in the same sense. On the other hand, classes such as linear orders, Boolean algebras, trees, and abelian groups are all known not to be complete in this way. We address the most obvious class for which this question was still open, by giving a coding of graphs into countable fields in such a way as to preserve all of these properties.

ABSTRACT. This work is concerned with the generalized computability theory, as well as properties of the real exponential field. To describe computability we use an approach via definability by Sigma-formulas in hereditarily finite superstructures, which was introduced in [1]. In particular, we establish the uniformization property for Sigma-predicates in the hereditarily finite list superstructure over the real exponential field. (See [2] for the structure's definition) We shall outline the proof of the following theorem.

Theorem 1. For any Sigma-predicate P in the hereditarily finite list superstructure over the real exponential field exists a Sigma-function f such that its domain dom(f)={x: exists y P(x,y)} and its graph G(f) is a subset of P.

As a corollary we obtain existence of an universal Sigma-function in the same structure.

1. Ershov, Yu. L. (1996). Definability and Computability, Consultants Bureau, New York-London-Moscow. 2. Goncharov, S. S. and Sviridenko, D. I. (1985). Sigma-programming (Russian), Vychisl. Sist. 107, pp. 3-29.

ABSTRACT. We present recent results on a version of dynamic logic suitable to describe properties of approximation spaces, with the set of finite elements considered as a structure (typical example is the set of rational numbers within the set of real numbers). We consider the case when this structure generates on a whole approximation space an induced structure in a way definable in dynamic logic. We apply this general technique to approximation spaces from effective model theory and HF-computability.

ABSTRACT. One of the directions of research in modern computability theory focus on studying properties of limitwise monotonic functions and limitwise monotonic sets. We prove the existence of incomparable Σ^0_2-sets relative to limitwise monotonic reducibility and there is no maximal element in the class of all lm-degrees of Σ^0_2-sets. Moreover, we prove that every countable partial order can be embedded into the class of all lm-degrees of Σ^0_2-sets.

ABSTRACT. We study the greatest under reduction computable numberings of families of sets which are uniformly computably enumerable relative to an arbitrary oracle.

ABSTRACT. It is well known many infinite families of c.e. sets whose Rogers semilattice contains an ideal without minimal elements, for instance, the family of all c.e. sets, \cite{Ers}. Moreover, there exists a computable family of c.e. sets whose Rogers semilattice has no minimal elements at all, \cite{Bad2}. In opposite to the case of the families of c.e. sets, for every computable numbering $\alpha$ of an infinite family $\mathfrak F$ of computable functions, there is a Friedberg numbering of $\mathfrak F$ which is reducible to $\alpha$, \cite{Ers}. This means that the Rogers semilattice of any computable family of total functions from level 1 of the arithmetical hierarchy contains no ideal without minimal elements.

We study computable families of total functions of any level of the Kleene-Mostowski hierarchy above level 1 and try to find elementary properties of Rogers semilattices that are different from the properties of Rogers semilattices for the families of computable functions.

\begin{theorem}\label{th1} For every n, there exists a $\Sigma^0_{n+2}$-computable family of total functions whose Rogers semilattice contains an ideal without minimal elements. \end{theorem}

Note that every Rogers semilattice of a $\Sigma^0_{n+2}$-computable family $\mathfrak F$ contains the least element if $\mathfrak F$ is finite, \cite{Ers}, and infinitely many minimal elements, otherwise, \cite{BG}.

Theorem \ref{th1} is based on the following criterion that extends the criterion for minimal numbering from \cite{Bad2}.

\begin{theorem} Let $\alpha$ be a numbering of an arbitrary set $\mathcal S$. Then there is no minimal numbering of $\mathcal S$ that is reducible to $\alpha$ if and only if, for every c.e. set $W$, if $\alpha (W)=S$ then there exists a c.e. set $V$ such that $\alpha (V)=\mathcal S$ and, for every positive equivalence $\varepsilon$, either $\varepsilon\upharpoonright W\nsubseteq \theta_{\alpha}$ or $W\nsubseteq [V]_{\varepsilon}$. \end{theorem}

\begin{thebibliography}{100}

\bibitem{Ers} {\scshape Yu. L. Ershov}, {\bfseries\itshape Theory of numberings}, Nauka, Moscow, 1977 (in Russian).

\bibitem{Bad2} {\scshape S. A. Badaev}, {\itshape On minimal enumerations}, {\bfseries\itshape Siberian Adv. Math.}, vol. 2 (1992), no. 1, pp. 1--30.

\bibitem{BG} {\scshape S. A. Badaev and S. S. Goncharov}, {\itshape Rogers semilattices of families of arithmetic sets}, {\bfseries\itshape Algebra and Logic}, vol. 40 (2001), no. 5, pp. 283--291.

\end{thebibliography}

ABSTRACT. We investigate minimal enumerations in analytical hierarchy. One of the most important minimal numberings is Friedbergs numbering. Owings showed that there is no Pi^1_1-computable Friedberg enumeration of all Pi^1_1-sets using metarecursion theory. This result is obtained in classic computability theory for higher levels of analytical hierarchy.

ABSTRACT. In this paper we find a first order formula which defines the first jump of the least element in the structure of the $\omega$-enumeration degrees.

ABSTRACT. For an infinite sequence of sets $\mathscr{R} = \{R_n\}_{n\in\omega}$ and a set $X$, we write $\mathscr{R}\leq_{c.e.} X$ if for every $n$, $R_n$ is computably enumerable in $X^{(n)}$, uniformly in $n$. Soskov \cite{omega-degrees} considered the following redicibility between sequences of sets \[\mathscr{R} \leq_\omega \mathscr{P}\mbox{ iff }(\forall X \subseteq \mathbb{N})[\mathscr{P} \leq_{c.e.} X\ \Rightarrow\ \mathscr{R}\leq_{c.e.} X].\] This reducibility naturally induces an equivalence relation, whose equivalence classes are called $\omega$-enumeration degrees. They form an upper semi-lattice, which have been extensively studied by a number of researchers in Sofia University over the past decade.

In this talk we discuss how to encode an infinite sequence of sets $\mathscr{R}$ into a single countable structure $\mathcal{N}_{\mathscr{R}}$, preferably in a finite language, such that the Turing degree spectrum of $\mathcal{N}_{\mathscr{R}}$ is the set \[Sp(\mathcal{N}_{\mathscr{R}}) = \{d_T(X) \mid \mathscr{R} \mbox{ is c.e. in }X\}.\] We present two such methods. The first one was studied by Soskov \cite{soskov} and is based on the so-called Marker's extensions \cite{marker}. The other approach is based on the idea of coding each set $R_n$ by a sequence of pairs of computable structures \cite{pairs-rec-str}. We conclude that for any two infinite sequences of sets $\mathscr{R}$ and $\mathscr{P}$ we can build countable structures $\mathcal{N}_{\mathscr{R}}$ and $\mathcal{N}_{\mathscr{P}}$ such that \[\mathscr{R} \leq_\omega \mathscr{P}\ \iff\ Sp(\mathcal{N}_{\mathscr{P}}) \subseteq Sp(\mathcal{N}_{\mathscr{R}}).\] In other words, the $\omega$-enumeration degrees are embeddable into the Muchnik degrees generated by spectra of structures.

ABSTRACT. We extend the limitwise monotonicity notion to the case of arbitrary computable linear ordering to get a set which is limitwise monotonic precisely in the non-computable degrees. Also we get a series of connected non-uniformity results to obtain new examples of non-uniformly equivalent families of computable sets with the same enumeration degree spectrum.

ABSTRACT. A connection between the classical and the Heyting's logic is given by the Glivenko's Theorem: for every propositional formula $A$, $A$ is classically provable iff $\neg\neg A$ is provable intuitionistically. \rm This theorem can be understood as a possible way of intuitionistic interpretation of the classical reasoning. Embedding of the implicative fragment of classical logic into the implicative fragment of the Heyting's logic was considered by J. P. Seldin [3] and L. C. Pereira, E. H. Haeusler, V. G. Costa, W. Sanz [2]. Seldin's interpretation essentially depends on the presence of conjunction, but the second one is obtained in the pure language of implication. Here we define, in spirit of Kolmogorov's interpretation, a mapping of the pure implicational propositional language enabling to prove the corresponding result. Let $p_1,\dots,p_n$ be a list of all propositional letters occurring in formula $A\to B$ and $q$ any propositional letter not occurring in $A\to B$. Then the image $b(A\to B)$ of $A\to B$ is defined inductively as follows: $b(p)=(p\to q)\to q$, for each $p\in\{p_1,\dots,p_n\}$, and $b(A\to B)=b(A)\to b(B)$. Namely, $b(A\to B)$ is obtained by replacing each occurrence of a propositional letter $p$ in $A\to B$ by $(p\to q)\to q$, where $q$ is a new letter.

{\bf Embedding Lemma.} \emph{For every propositional implicational formula $A$, $A$ is provable in classical logic iff $b(A)$ is provable in Heyting logic.}

This is a part of our paper [1] dealing with an alternative approach to normalization of the implicative fragment of classical logic.

\begin{thebibliography}{10}

\bibitem{cite1} {\scshape B. Bori\v ci\'c, M. Ili\'c}, {\itshape An Alternative Normalization of the Implicative Fragment of Classical Logic}, \rm (to appear).

\bibitem{cite2} {\scshape L. C. Pereira, E. H. Haeusler, V. G. Costa, W. Sanz}, {\itshape A new normalization strategy for the implicational fragment of classical propositional logic}, {\bfseries\itshape Studia Logica}, vol. 96 (2010), no. 1, pp. 95--108.

\bibitem{cite3} {\scshape J. P. Seldin}, {\itshape Normalization and excluded middle I}, {\bfseries\itshape Studia Logica}, vol. 48 (1989), no. 2, pp. 193--217.

\end{thebibliography}

ABSTRACT. In [1], the second author has developed a proof-theoretic approach to Glivenko theorems for substructural propositional logics. In the present talk, by using the same techniques, we will extend them for substructural predicate logics. It will be pointed out that in this extension, the following double negation shift scheme (DNS) plays an essential role. (DNS): \forall x \neg \neg \varphi(x) \rightarrow \neg \neg \forall x \varphi(x)$ Among others, the following is shown, where QFLe and QFLe$^{\dagger}$ are predicate extensions of FLe and FLe$^{\dagger}$, respectively (see [1]). The Glivenko theorem holds for QFLe$^{\dagger}$ +(DNS) relative to classical predicate logic. Moreover, this logic is the weakest one among predicate logics over QFLe for which the Glivenko theorem holds relative to classical predicate logic. Then we will study negative translations of substructural predicate logics by using the same approach. We introduce a negative translation, called extended Kuroda translation and over QFLe it will be shown that standard negative translations like Kolmogorov translation and G\"odel-Gentzen translation are equivalent to our extended Kuroda translation. Thus, we will give a clearer unified understanding of these negative translations by substructural point of view.

ABSTRACT. I address the lack of expressiveness of Kripke's theory of truth (over arithmetic) along the lines suggested by H. Field, namely equipping it with a primitive, non-trivial conditional. However, I focus my attention on computationally simple methods to interpret a primitive conditional. I provide an inductive construction and define a corresponding monotone operator that improves on Kripke's construction and show some nice features.

ABSTRACT. We present a unifying, categorical approach to several constructive completeness theorems for intuitionistic (and classical) first-order theories, as well for theories in certain fragments of first-order logic, based on a theorem by A. Joyal [Thm 6.3.5, Makkai and Reyes, 1977]. We show that the notion of exploding (Tarski-) model introduced by W. Veldman [Veldman 1976] is adequate for certain fragments of first-order logic (as well as for classical first-order logic) and that Veldman's modified Kripke semantics arises, as a consequence, as semantics in a suitable sheaf topos. In the process we give an alternative proof of Veldman's completeness theorem, and note the equivalence of this theorem with the Fan Theorem. Finally, we show that the disjunction-free fragment is constructively complete with respect to modified Kripke semantics without appeal to the Fan Theorem, as well as without appeal to decidable axiomatizability and size restrictions on the language. This is joint work with Christian Espindola.

ABSTRACT. The correspondence and completeness of logics with fixed point operators has been the subject of recent research (see~\cite{BezHod:TCS},~\cite{muALBA}). These works aim to develop a Sahlqvist-like theory for their respective fixed point settings. That is, they identify classes of formulas which are preserved under canonical extensions and have first-order frame correspondents.

We prove that the members of a certain class of intuitionistic mu-formulas are \emph{canonical}, in the sense of~\cite{BezHod:TCS}. When projected onto the classical case, our class of canonical mu-formulas subsumes the class described in~\cite{BezHod:TCS}. Our methods use a variation of the algorithm ALBA (Ackermann Lemma Based Algorithm) developed in~\cite{DistMLALBA}. We show that all mu-inequalities that can be successfully processed by our algorithm, $\mu^*$-ALBA, are canonical.

Formulas are interpreted on a bounded distributive lattice $\A$ with additional operations. The canonical extension of $\A$, denoted $\A^\delta$, is a complete lattice in which the completely join-irreducible elements ($\jty(\A^\delta)$) are join-dense, and the completely meet-irreducible elements ($\mty(\A^\delta)$) are meet-dense. An \emph{admissible valuation} takes all propositional variables to elements of $\A$. The algorithm aims to ``purify'' an inequality $\alpha \leq \beta$ by rewriting it as a (set of) pure (quasi-)inequalities. A pure quasi-inequality has no occurrences of propositional variables; only special variables whose interpretations range over $\jty(\A^\delta) \cup \mty(\A^\delta)$ are present. The fact that admissible and ordinary validity coincide for pure inequalities is the lynchpin for proving canonicity.

The proof of the soundness of the rules of the algorithm $\mu^*$-ALBA rests on the order-topological properties of formulas (term functions) of the $\mu$-calculus.

ABSTRACT. ¥begin{document} ¥thispagestyle{empty}

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

¥NP ¥absauth{Ryota Akiyoshi} ¥meettitle{Proof-Theoretic Analysis of Brouwer's Argument of the Bar Induction} ¥affil{Faculty of Letters, Kyoto University, Yoshidahonmachi, Sakyo Ward, Kyoto Prefecture 606-8501, Japan} ¥meetemail{georg.logic@gmail.com}

In a series of papers, Brouwer had developed intuitionistic analysis, in particular the theory of choice sequences. An important theorem called the ``fan theorem" plays an essential role in the development of it. The fan theorem was derived from another stronger theorem called the ``bar induction", which is an induction principle on a well-founded tree. We refer to [4,5] as standard references of Brouwer's intuitionistic analysis.

Brouwer's argument in [1] contains a controversial assumption on canonical proofs of some formula. In many cases, constructive mathematicians have assumed the bar induction as axiom, hence the assumption has not been examined by them.

In this talk, we sketch an approach of Brouwer's argument via infinitary proof theory. We point out that there is a close similarity between Brouwer's argument and Buchholz' method of the $¥Omega$-rule ([2,3]). In particular, Brouwer's argument in [1] seems very close to Buchholz' embedding theorem of the (transfinite) induction axiom of $ID_{1}$ in [2], which is a theory of non-iterated inductive definition. By comparing these two arguments, we give a natural explanation of why Brouwer needed the assumption. Our conclusion is that Brouwer supposed the assumption in order to avoid the impredicativity or a vicious circle which is essentially the same as one in the $¥Omega$-rule for $ID_{1}$. In other words, the impredicativity can be explained in a very clear way from the view point of the $¥Omega$-rule. Moreover, Brouwer's argument can be formulated in a mathematically precise way by the $¥Omega$-rule. Therefore, we conclude that his introduction of the assumption is mathematically well-motivated. If time is permitting, we suggest how to carry out this idea in a mathematical way.

¥begin{thebibliography}{10}

¥bibitem{B1} {¥scshape Luitzen Egbertus Jan Brouwer}, {¥itshape ¥"{U}ber Definitionsbereiche von Funktionen}, {¥bfseries¥itshape Mathematische Annalen}, vol.~97, 1927, pp.~60--75.

¥bibitem{B2} {¥scshape Wilfried Buchholz}, {¥itshape The $¥Omega_{¥mu +1}$-Rule}, in {¥bfseries¥itshape Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies}, LNM 897, 1981, pp.~188--233.

¥bibitem{B3} {¥scshape Wilfried Buchholz}, {¥itshape Explaining the {G}entzen-{T}akeuti reduction steps}, {¥bfseries¥itshape Archive for Mathematical Logic}, vol.~40, pp.~255--272.

¥bibitem{D1} {¥scshape Michael A. E. Dummett}, {¥bfseries¥itshape Elements of Intuitionism}, 2nd edition, OUP, 2000.

¥bibitem{TvD} {¥scshape A. S. Troelstra and D. van Dalen}, {¥bfseries¥itshape Constructivism in Mathematics}, Vol.1, North-Holland, 1988.

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

¥end{thebibliography}

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

¥end{document}

ABSTRACT. Reflection principles based on provability predicates were introduced in the 1930s by Rosser and Turing, and later were explored by Feferman, Kreisel & Levi, Schmerl, Artёmov, Beklemishev and others. We study reflection principles of Peano Arithmetic based on both proof and provability predicates. We find a classification of these principles and establish their linear ordering with respect to their deductive strength in Peano Arithmetic. The proof essentially relies on the Gödel-Löb-Artёmov logic GLA.

ABSTRACT. The Caucal hierarchy of infinite graphs with colored edges is a wide class of graphs with decidable monadic theories[1]. Graphs from this hierarchy can be considered as structures with finite number of binary relations. It is known that the exact upper bound for order types of the well-orderings that lie in this class is ε0 [2]. Actually, any well-ordering from Caucal hierarchy can be used as a constructive ordinal notation system. We investigate systems of fundamental sequences for that well-orderings and the corresponding fast-growing hierarchies of computable functions. For a well-ordering (A,<) we can determine a system of fundamental sequences λ[n] by a relation Cs(x,y) such that Cs(α, β) <=> α is a limit point of < A and β = α[n], for some n. Our principal result is that for a well-ordering with a pair of Schmidt-coherent fundamental sequences (A,<,Cs1,Cs2) from Caucal hierarchy the corresponding fast-growing hierarchies fα1(x) and fα2(x) are equivalent in the following sense: for all α < β we have fβ1(n) > fα2(n) and fβ1(n) > fα2(n), for all large enough n (Schmidt-coherence is a classical condition that implies that functions from fast-growing hierarchy are strictly increasing [3]). We show that any two well-orderings with Schmidt-coherent systems of fundamental sequences from Caucal hierarchy of the same order type < ω^ω give rise to the equivalent fast-growing hierarchies. We also prove that it is possible to extend a graph with a well-ordering from Caucal hierarchy by a Schmidt-coheren system of fundamental sequences for the well-ordering in such a way that the resulting graph will lie in Caucal hierarchy. [1] Didier Caucal, On Infinite Terms Having a Decidable Monadic Theory, Mathematical Foundations of Computer Science 2002 (Diks, Krzysztof and Rytter, Wojciech), vol. 2420, Springer Berlin Heidelberg, 2002, pp. 165–176. [2] Braud Laurent, Arnaud Carayol, Linear Orders in the Pushdown Hierarchy, Lecture Notes in Computer Science (Samson Abramsky, et.al. eds.), vol. 6199, Springer Berlin Heidelberg, 2010, pp. 88–99. [3] Diana Schmidt, Built-up Systems of Fundamental Sequences and Hierarchies of Number-Theoretic Functions, Archive for Mathematical Logic, vol. 18 (1976), pp. 47–53.

ABSTRACT. In 1985, Harvey Friedman introduced a new kind of embeddability relation between finite labeled rooted trees, namely the gap-embeddability relation. Under this embeddability relation, the set of finite rooted trees with labels bounded by a fixed natural number n is a well-partial-ordering. The well-partial-orderedness of these trees (if we put a universal quantifier in front) gives rise to a statement not provable in Pi11-CA_0. There are still some open questions left about these famous well-partial-orderings. For example, what is the maximal order type of these sets of trees with the gap-embeddability relation? The maximal order type of a well-partial-ordering is an important characteristic of that well-partial-ordering and it captures in some sense its strength. In this talk, I will discuss some new recent developments concerning this topic.

ABSTRACT. Reverse mathematics studies which natural subsystems of second order arithmetic are equivalent to key theorems of ordinary or non-set-theoretic mathematics. The main philosophical application of reverse mathematics proposed thus far is foundational analysis, which explores the limits of various weak foundations for mathematics in a formally precise manner. Richard Shore [1, 2] proposes an alternative framework in which to conduct reverse mathematics, called computational reverse mathematics. The formal content of his proposal amounts to restricting our attention to omega-models of RCA0 when we prove implications and equivalences in reverse mathematics.

Despite some attractive features, computational reverse mathematics is inappropriate for foundational analysis, for two major reasons. Firstly, the computable entailment relation employed in computational reverse mathematics does not preserve justification for all of the relevant foundational theories, particularly a partial realisation of Hilbert’s programme due to Simpson [3].

Secondly, computable entailment is a Pi^1_1-complete relation, and hence employing it commits one to theoretical resources which outstrip those acceptable to the stronger foundational programmes such as predicativism and predicative reductionism. This argument can be formalised within second order arithmetic, making it accessible to partisans of foundational frameworks such as predicativism. In doing so we show that the existence of the set of sentences which are computably entailed is equivalent over ACA0 to Pi^1_1 comprehension.

[1] Shore, R. A., Reverse Mathematics: The Playground of Logic, The Bulletin of Symbolic Logic, vol. 16 (2010), no. 3, pp. 378–402. [2] Shore, R. A., Reverse mathematics, countable and uncountable: a computational approach, Effective Mathematics of the Uncountable, Lecture Notes in Logic, (D. Hirschfeldt, N. Greenberg, J. D. Hamkins, and R. Miller, editors), ASL and Cambridge University Press, Cambridge, 2013, pp. 150–163. [3] Simpson, S G., Partial realizations of Hilbert’s program, The Journal of Symbolic Logic, vol. 53 (1988), pp. 349–363.

ABSTRACT. We introduce a general notion of semantic structure for first-order theories, covering a variety of constructions such as Tarski and Kripke semantics, and prove that, over Zermelo Fraenkel set theory (ZF), the completeness of such semantics is equivalent to the Boolean Prime Ideal theorem (BPI). In particular, we deduce that the completeness of that type of semantics for non-classical theories is unprovable in intuitionistic Zermelo Fraenkel set theory IZF. Using results of Joyal and McCarty, we conclude also that the completeness of Kripke semantics is equivalent, over IZF, to the Law of Excluded Middle plus BPI. By results from Banaschewski and Bhutani, none of these two principles imply each other, and so this gives the exact strength of Kripke completeness theorem in the sense of constructive reverse mathematics.

ABSTRACT.  

ABSTRACT. We analyze the computable part of three hierarchies from analysis and set theory. The hierarchies are those induced by the Cantor-Bendixson rank, the differentiability rank of Kechris and Woodin, and the Denjoy rank. Our goal is to identify the descriptive complexity of the initial segments of these hierarchies. For example, we show that for each recursive ordinal alpha>0, the set of Turing indices of computable C[0,1] functions that are differentiable with rank at most alpha is Pi_{2alpha+1}-complete. Similar results hold for the other hierarchies. Underlying of all the results is a combinatorial theorem about trees. We will present the theorem and its connection to the results.

ABSTRACT. A Sigma-construction of Solovay is extended to the case of intermediate sets which are not necessarily subsets of the ground model, with a more transparent description of the resulting forcing notion than in a classical paper of Grigorieff. As an application, we prove that, for a given name t (not necessarily a name of a subset of the ground model), the set of all sets of the form t[G] (the G-interpretation of t), G being generic over the ground model, is Borel. This result was first established by Zapletal by a descriptive set theoretic argument.

ABSTRACT. A norm is a surjective function from the Baire space R onto an ordinal. Given two norms φ, ψ we write φ ≤_N ψ if φ continuously reduces to ψ. Then ≤_N is a preordering and so passing to the set of corresponding equivalence classes yields a partial order, the hierarchy of norms.

Assuming the axiom of determinacy (AD) the hierarchy of norms is a wellorder. The length Σ of the hierarchy of norms was investigated by Löwe in [1]; he determined that Σ ≥ Θ^2 (where Θ := {α | There is a surjection from R onto α}). In his talk "Multiplication in the hierarchy of norms", given at the ASL 2011 North American Meeting in Berkeley, Löwe presented a binary operation × on the hierarchy of norms such that for wellchosen norms φ, ψ the ordinal rank of φ×ψ in the hierarchy of norms is at least as big as the product of the ordinal ranks of φ and ψ, which implies that Σ is closed under ordinal multiplication and so Σ ≥ Θ^ω.

In this talk I will note that in fact for wellchosen norms φ, ψ the ordinal rank of φ×ψ is exactly the product of the ranks of φ and ψ with an intermediate factor of ω_1. Furthermore using a stratification of the hierarchy of norms into initial segments closed under the ×-operation I will show that Σ ≥ Θ^(Θ^Θ).

[1] BENEDIKT LÖWE, The length of the full hierarchy of norms, Rendiconti del Seminario Matematico dell'Università e del Politecnico di Torino, vol. 63 (2005), no. 2, pp. 161-168.

ABSTRACT. In parallel with the Borel hierarchy, one can define the levels $\Sigma^0_{\alpha}(\Pi^1_1)$ ($\alpha <\omega_1$) of the Borel-on-coanalytic hierarchy by starting with $\Pi^1_1$ in place of the class $\Delta^0_1$ of clopen sets. In this talk, we consider the consistency strength of determinacy for infinite perfect-information games with payoff in $\Sigma^0_\alpha(\Pi^1_1)$. This has been computed exactly for $\alpha = 0, 1$, by Martin, Harrington, and J. Simms. For $\alpha > 1$, dual results of Steel~\cite{Steel} and Neeman~\cite{Neeman} have shown the strength to reside within a very narrow range in the region of a measurable cardinal $\kappa$ of largest possible Mitchell order $o(\kappa)$. However, an exact equiconsistency had yet to be isolated.

We have recently completed work pinpointing the determinacy strength of levels of the Borel hierarchy of the form $\Sigma^0_{1+\alpha+3}$, showing a level-by-level correspondence between these and a family of natural $\Pi_1$ reflection principles. Combining our techniques with those of \cite{Neeman} and \cite{Steel}, we can characterize the strength of $\Sigma^0_{1+\alpha+3}(\Pi^1_1)$-DET in terms of inner models with measurable cardinals. In particular, $\Sigma^0_4(\Pi^1_1)$-DET is equivalent to the existence of a mouse satisfying $(\exists \kappa) o(\kappa)=\kappa^{++}$ plus the schema that each true $\Pi_1$ statement with parameters in $P^2(\kappa)$ reflects to an admissible set containing $P(\kappa)$.

We will also discuss progress on calculating the strength of $\Sigma^0_2(\Pi^1_1)$-DET, relating this to Mitchell's hierarchy of weak repeat point measures.

ABSTRACT. It is quite well-known result of Martin that the existence of a measurable cardinal is enough to prove the determinacy of all boldface Pi^1_1 sets. The argument nicely modifies to get the determinacy of all lightface Pi^1_1 sets from the existence of O^sharp. With this argument in mind, I will discuss how the technique has been pushed since then to get more determinacy in the difference hierarchy of Pi^1_1 sets, including a family of new determinacy results following from sharp-like hypotheses. To achieve this I will also demonstrate a generalised notion of computability suitable for defining the lightface Borel hierarchy in uncountable spaces.

ABSTRACT. By analogy with the notions of determinative conjuncts in CPL, we introduce the same notion for modal tautologies. On the base of introduced modal determinative conjuncts we introduce the notion of strong equality for modal tautologies and compare different measures of proof complexity (size, steps, space and width) for them in some proof systems of MPL. We prove that 1) in some proof systems the strong equal modal tautologies have the same proof complexities and 2) there are such proof systems, in which some measures of proof complexities for strong equal modal tautologies are the same, the other measures differ from each other only by the sizes of tautologies.

ABSTRACT. Fraisse-Hrushovski constructions were first introduced by Hrushovski as a method for constructing strongly minimal sets that do not fit within Zilber's trichotomy conjecture. The construction can be seen as a two-step process where first a rank $\omega$ structure is constructed from a countable amalgamation class, using a variation of a Fraisse limit construction, and then the structure is ``collapsed'' to a strongly minimal substructure.

In this talk we acquaint ourselves with the rank $\omega$, non-collapsed version of the construction and its associated combinatorial geometry, and provide a general method of showing that one simple Fraisse-Hrushovski construction is a (proper) reduct of another Fraisse-Hrushovski construction.

ABSTRACT. Our interest is to obtain a new information on the model-theoretic properties of the Jonsson theories and the structure of their classes of models. To date, the best studied of the perfect Jonsson theory and their classes of existentially closed models. In this thesis, we consider a new approach to the study of Jonsson theories. We will work with special subsets of the semantic model of fixed Jonsson theory or of some Jonsson fragment of an arbitrary complete theory. We introduce the notion of Jonsson set as the corresponding closure of some existential formula in the semantic model. Using of the Jonsson sets we consider such properties as a stability, a categoricity and a similarity of relevant models and theories related to these sets.

ABSTRACT. This paper applies model theory to macroeconomic theory. In mathematical models of macroeconomic theory, the hypothesis of a "representative agent" is ubiquitous, but the search for a rigorous justification has so far been unsuccessful and was ultimately abandoned until very recently. Herzberg (2010) constructed a representative utility function for finite-dimensional social decision problems, based on an bounded ultrapower construction over the reals, with respect to the ultrafilter induced by the underlying social choice function (via the Kirman-Sondermann (1972) correspondence). However, since the decision problems of macroeconomic theory are typically infinite-dimensional, Herzberg's original result is insufficient for many applications. We therefore generalise his result by allowing the social alternatives to belong to a general reflexive Banach space W; in addition to known results from convex analysis, our proof uses a nonstandard enlargement of the superstructure over the union of W with the reals, obtained by a bounded ultrapower construction with respect to the Kirman-Sondermann ultrafilter.

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

\documentclass[bsl,meeting]{asl} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %TCIDATA{OutputFilter=Latex.dll} %TCIDATA{Version=5.50.0.2890} %TCIDATA{} %TCIDATA{BibliographyScheme=Manual} %TCIDATA{LastRevised=Monday, April 07, 2014 19:30:57} %TCIDATA{}

%\documentclass[10pt,a4paper]{asl} \usepackage[latin1]{inputenc} \usepackage{amsmath} \usepackage{amsfonts} \usepackage{amssymb} \begin{document}

\end{document}\AbstractsOn \pagestyle{plain} \def\urladdr#1{\endgraf\noindent{\it URL Address}: {\tt #1}.} \newcommand{\NP}{} \input{tcilatex} \begin{document}

\thispagestyle{empty}

%% BEGIN INSERTING YOUR ABSTRACT DIRECTLY BELOW;

%% SEE INSTRUCTIONS (1), (2), (3), and (4) FOR PROPER FORMATS \NP \absauth{Bruno Dinis, Imme van den Berg}

\meettitle{An axiomatic approach to modelling of orders of magnitude} % First author's affiliation \affil{CMAF, University of Lisbon,Faculdade de Ciências Universidade de Lisboa Campo Grande, Edifício C6, Gabinete 6.2.18 P-1749-016 Lisboa , Portugal} \meetemail{bruno.salsa@gmail.com} % % Second author's affiliation \affil{Mathematics Department, University of Évora, Colégio Luís António Verney Rua Romão Ramalho, 59 7000-671 Évora, Portugal} \meetemail{ivdb@uevora.pt}

%% INSERT TEXT OF ABSTRACT DIRECTLY BELOW Many arguments deal informally with orders of magnitude of numbers. If one tries to maintain the intrinsic vagueness of orders of magnitude - they should be bounded, but stable under at least some additions -, they cannot be formalized with ordinary real numbers, due to the Archimedean property and Dedekind completion. Still there is the functional approach through Oh's and oh's and more generally Van der Corput's neutrices\cite{vdcorput-60}, both have some operational shortcomings.

Nonstandard Analysis disposes of a natural example of order of magnitude: the (external) set of infinitesimals is bounded and closed under addition% \cite{koudjetithese}\cite{koudjetivandenberg}. Adopting the terminology of Van der Corput, we call a \emph{neutrix} an additive convex subgroup of the nonstandard reals. An \emph{external number} is the set-theoretic sum of a nonstandard real and a neutrix. The external numbers capture the imprecise boundaries of informal orders of magnitude and permit algebraic operations which go beyond the calculus of the Oh's and oh's\cite{dinisberg}. This external calculus is based more on semigroup operations than group operations, but happens to be fairly operational in concrete cases and allows for total order with a generalized form of Dedekind completion\cite% {dinisberg2}.

Based on joint work with Imme van den Berg, we discuss an axiomatics for the calculus of neutrices and external numbers, trying to do justice to the vagueness of orders of magnitude. In particular we consider foundational problems which appear due to the fact that some axioms are necessarily of second order, and the fact that the external calculus exceeds existing foundations for external sets\cite{kanoveireeken1}.

\begin{thebibliography}{9} %% INSERT YOUR BIBLIOGRAPHIC ENTRIES HERE; %% SEE (4) BELOW FOR PROPER FORMAT. %% EACH ENTRY MUST BEGIN WITH \bibitem{citation key} %%

\bibitem{vdcorput-60} J.G. van der Corput, \textit{Neutrix calculus, neutrices and distributions}, MRC Tecnical Summary Report. University of Wisconsin, 1960.

\bibitem{dinisberg} B. Dinis, I. P. van den Berg,\textit{\ Algebraic properties of external numbers}, J. Logic and Analysis 3:9 (2011) 1--30.

\bibitem{dinisberg2} B. Dinis, I. P. van den Berg, \textit{On structures with two semigroup operations }(to appear)

\bibitem{kanoveireeken1} V. Kanovei, M. Reeken, Nonstandard Analysis, axiomatically, Springer Monographs in Mathematics (2004).

\bibitem{koudjetithese} F. Koudjeti, Elements of External Calculus with an aplication to Mathematical Finance, PhD thesis, Labyrinth publications, Capelle a/d IJssel, The Netherlands (1995).

\bibitem{koudjetivandenberg} F. Koudjeti and I.P. van den Berg. Neutrices, external numbers and external calculus, in Nonstandard Analysis in Practice, p. 145-170. F. and M. Diener eds., Springer Universitext, 1995. %% IF THERE ARE NO ENTRIES %% DELETE THE LINE ABOVE (\begin{thebibliography}{20}) %% AND THE LINE BELOW (\end{thebibliography}) \end{thebibliography}

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

\end{document}

ABSTRACT. Generalizing the notion of numerosity, introduced in [1], we say that a function n from the powerset of a given set Ω is an elementary numerosity if it satisfies the properties 1. the range of n is the non-negative part of a non-archimedean field F that extends R; 2. n({x}) = 1 for every x ∈ Ω ; 3. n(A ∪ B) = n(A) + n(B) whenever A and B are disjoint. We have shown that every non-atomic finitely additive or sigma-additive measure is obtained from an elementary numerosity by taking its ratio to a unit. The proof of this theorem relies in showing that, given a non-atomic finitely additive or sigma- additive measure over Ω, there exists a suitable ultrafilter on Ω such that the elementary numerosity of a set can be defined as the equivalence class of a particular real Ω- sequence. A proof can also be obtained from Theorem 1 of [2], by an argument of saturation. This result allowed to improve nonstandard models of probability, first studied in [3], that overcome some limitations of the conditional probability; further research aims towards models that avoid the Borel-Kolmogorov paradox. For this reasons, we do believe that this topic could be of particular interest not only to mathematicians but also to philosophers. [1] V. Benci, M. Di Nasso, Numerosities of labelled sets: a new way of counting, Advances in Mathematics, vol. 173 (2003), pp. 50–67. [2] C.W. Henson, On the nonstandard representation of measures, Transactions of the American Mathematical Society, vol. 172 (1972), pp. 437–446. [3] V. Benci, L. Horsten, S. Wenmackers, Non-Archimedean probability, Milan Journal of Mathematics (to appear), arXiv:1106.1524.

ABSTRACT. Inside the class of formally real fields, we study strongly normal extensions as defined in chap. VI, [Kol]. Fix L/K a strongly normal extension of formally real differential fields such that the subfield C_K of constant elements of K is real closed.

Let U be a saturated model of the theory of closed ordered differential fields containing L (see [Sin]), U is real closed and for i^2=-1, U(i) is a model of DCF_0.

We denote gal(L/K) the group of differential K-automorphisms of L and Gal(L/K):=gal(<L, C_U> / <K, C_U>).

Theorem 1. The group Gal(L/K), respectively gal(L/K), is isomorphic to a definable group G in the real closed field C_U, respectively C_K.

Under the hypothesis that K is relatively algebraically closed in L, we prove that given any u\in L\setminus K, there exists \sigma\in Gal(L/K) such that \sigma(u)\neq u.

Let K\subseteq E\subseteq L be an intermediate differential field extension. As the elements of Gal(E/K) are not supposed to respect the order induced on <E,C_U> by the one of U, they do not need to have an extension in Gal(L/K). Therefore, we do not get a 1-1 Galois correspondence like in the classical case where C_K is algebraically closed (see [Pil]).

Let Aut(L/K) denote the subgroup of elements of Gal(L/K) that are increasing, let \eta:G\rightarrow Gal(L/K) denote a group isomorphism given by Theorem 1 and < L,C_U>^r be the real closure of <L,C_U> in U.

Proposition 2. Let G_0 be a definable subgroup of G. There is a finite tuple \bar d\in <L,C_\U>^r such that \eta(G_0)\cap Aut(L/K) is isomorphic (as a group) to Aut(L(\bar d)/K(\bar d)).

Bibliography

[Kol] E. R. Kolchin, Differential algebra and algebraic groups, Pure and Applied Mathematics, Vol. 54. Academic Press, New York-London, 1973. xviii+446 pp.

[Pil] A. Pillay, Differential Galois Theory I, Illinois Journal of Mathematics, vol.42 (1998), no.4, pp.978--699.

[Sin] M. Singer, The model theory of ordered differential fields, Journal of Symbolic Logic, 43 (1978), no.1, pp.82--91.

ABSTRACT. The notion of n-dependent theories introduced by Shelah is a natural generalization of dependent or more frequently called NIP theories. They form a proper hierarchy of first order theories in which the case n equals to 1 coincides which NIP theories. In my talk, I give an overview about algebraic extensions of fields defined in structures with certain properties (superstable, stable, NIP, etc.). For instance, infinite NIP fields of positive characteristic are known to be Artin-Schreier closed. I extend this result to the wider class of infinite n-dependent fields for any natural number n and present some applications to valued fields defined in this setting. Secondly, I show that non-separable closed pseudo-algebraically closed (PAC) fields have the n-independence property for all natural numbers n which is already known for the independence property (n equal to 1) due to Duret. Hence, non-separable closed PAC fields lie outside of the hierarchy of n-dependent fields.

ABSTRACT. \documentclass[bsl,meeting]{asl}\AbstractsOn \pagestyle{plain}\def\urladdr#1{\endgraf\noindent{\it URL Address}: {\tt #1}.}\newcommand{\NP}{}% \usepackage{verbatim}\begin{document}\thispagestyle{empty}% % BEGIN INSERTING YOUR ABSTRACT DIRECTLY BELOW; % % SEE INSTRUCTIONS (1), (2), (3), and (4) FOR PROPER FORMATS\NP \absauth{Beibut Kulpeshov} \meettitle{Some remarks on $\aleph_0$-categorical weakly circularly minimal structures} \affil{Department of Information Systems and Mathematical Modelling, International Information Technology University, 34 A Manas str./8 A Zhandosov str., 050040, Almaty, Kazakhstan} \meetemail{b.kulpeshov@iitu.kz}

The notion of {\it circular minimality} has been introduced and originally studied by D.~Macpherson and C.~Steinhorn in \cite{mac}. Here we continue studying the notion of {\it weak circular minimality} being its generalisation.

A {\it circular} order relation is described by a ternary relation $K$ satisfying the following conditions:\\ (co1) $\forall x\forall y \forall z (K(x,y,z)\to K(y,z,x));$\\ (co2) $\forall x\forall y \forall z (K(x,y,z)\land K(y,x,z) \Leftrightarrow x=y \lor y=z \lor z=x);$\\ (co3) $\forall x\forall y \forall z(K(x,y,z)\to \forall t[K(x,y,t) \lor K(t,y,z)]);$\\ (co4) $\forall x\forall y \forall z (K(x,y,z)\lor K(y,x,z))$.

A set $A$ of a circularly ordered structure $M$ is said to be {\it convex} if for any $a, b\in A$ the following holds: for any $c\in M$ with $K(a,c,b)$ we have $c\in A$ or for any $c\in M$ with $K(b,c,a)$ we have $c\in A$. A circularly ordered structure $M=\langle M, K, \ldots \rangle$ is {\it weakly circularly minimal} if any definable (with parameters) subset of $M$ is a finite union of convex sets \cite{km}. Any weakly o-minimal structure is weakly circularly minimal, but the inverse is not true in general. Some of interesting examples of weakly circularly minimal structures that are not weakly o-minimal were studied in \cite{km, kb30, ksm}.

In \cite{km}--\cite{ksm} $\aleph_0$--categorical 1-transitive weakly circularly minimal structures have been studied, and was obtained their description up to binarity. Here we discuss some properties of $\aleph_0$--categorical weakly circularly minimal structures that are not 1-transitive. In particular, we study a behaviour of 2-formulas in such structures.

\begin{thebibliography}{10} \bibitem{mac} H.D.~Macpherson, Ch.~Steinhorn, {\it On variants of o-minimality}, {\bf Annals of Pure and Applied Logic}, 79 (1996), pp. 165--209. \bibitem{km} B.Sh.~Kulpeshov, H.D.~Macpherson, {\it Minimality conditions on circularly ordered structures}, {\bf Mathematical Logic Quarterly}, 51 (2005), pp. 377--399. \bibitem{kb30} B.Sh.~Kulpeshov, {\it On $\aleph_0$-categorical weakly circularly minimal structures}, {\bf Mathematical Logic Quarterly}, 52 (2006), pp. 555--574. \bibitem{ksm} B.Sh.~Kulpeshov, {\it Definable functions in the $\aleph_0$-categorical weakly circularly minimal structures}, {\bf Siberian Mathematical Journal}, 50 (2009), pp. 282--301.

%% INSERT YOUR BIBLIOGRAPHIC ENTRIES HERE; %% SEE (4) BELOW FOR PROPER FORMAT. %% EACH ENTRY MUST BEGIN WITH \bibitem{citation key}%%%% IF THERE ARE NO ENTRIES %% DELETE THE LINE ABOVE (\begin{thebibliography}{20}) %% AND THE LINE BELOW (\end{thebibliography}) \end{thebibliography}\vspace*{-0.5\baselineskip} % this space adjustment is usually necessary after a bibliography \end{document}

ABSTRACT. Abstract Elementary Classes (AECs) corresponds to an abstract framework for studying non first order axiomatizable classes of structures. Grossberg, VanDieren and Villaveces studied uniqueness of limit models as a weak notion of superstability in AECs.

Hirvonen and Hyttinen gave an abstract setting similar to AECs to study classes of metric structures which are not axiomatizable in continuous logic, called Metric Abstract Elementary Classes (MAECs).

In this work, we will talk about a study of a metric version of limit models as a weak version of superstability in categorical MAECs, and some consequences of uniqueness of limit models in domination, orthogonality and parallelism of Galois types.

ABSTRACT. We introduce the concept of a locally finite Abstract Elementary Class and develop the theory of excellence for such classes. From this we find a family of complete $L_{\omega_1,\omega}$ sentences $\phi^r$ such that $\phi^r$ is $r$-excellent and $\phi^r$ homogeneously characterizes $\aleph_r$, improving results of Hjorth and Laskowski-Shelah and answering a question of Souldatos. This provides the first example of an Abstract Elementary Class where the spectrum of cardinals on which amalgamation holds contains more than one interval.

ABSTRACT. We show that the number of types of sequences of tuples of a fixed length can be calculated from the number of 1-types and the length of the sequences. Specifically, if $\kappa \leq \lambda$, then

$$\sup_{\|M\| = \lambda} |S^\kappa(M)| = \left( \sup_{\|M\| = \lambda} |S^1(M)| \right)^\kappa$$

We show that this holds for any abstract elementary class with $\lambda$ amalgamation%, but it is new for first order theories when $\kappa$ is infinite . No such calculation is possible for nonalgebraic types. We introduce a generalization of nonalgebraic types for which the same upper bound holds. We use this to answer a question of Shelah from [Sh:c].