ABM 2014, Arbeitstagung Bern-München
18.12.2014-19.12.2014
Place
Mathematics Institute LMU, Room B 349.
Welcome dinner
Alter Simpl19:00, Türkenstrasse 57
Thursday Talks
- 09:00-09:45, Stanley Wainer: "A miniaturized predicativity"
- 09:45-10:15, Coffee Break
- 10:15-11:00, Florian Ranzi: "A flexible type system for the small Veblen ordinal"
- 11:00-11:45, Timotej Rosebrock: "Semi-Decidability in Explicit Mathematics"
- 11:45-12:30, Sam Sanders: "On a hitherto unexploited nonstandard extension of the finitary standpoint"
- 12:30-15:00, Lunch break
- 15:00-15:45, Peter Schuster: "Transfinite Methods as Admissible Rules"
- 15:45-16:30, Ioannis Kokkinis: "First Steps towards Probabilistic Justification Logic"
- 16:30-17:15, Michel Marti: "Towards Deduction Trees for Intuitionistic Modal Logic"
Thursday dinner
Los Faroles18:00, Nordendstrasse 26
Friday Talks
- 09:00-09:45, Anton Freund: "Slow consistency, slow reflection, and a hierarchy between PA and PA+Con(PA)"
- 10:00-10:45, Dieter Probst: "Defining truth classes in conservative extensions of PA"
Abstracts
- Stanley Wainer: "A miniaturized predicativity"
The basis of this work is Leivant's (1995) theory of ramified
induction over N, which has elementary recursive strength. It
has been redeveloped and extended in various ways by many people;
for example, Spoors and W. (2012) built a hierarchy of ramified theories
whose strengths correspond to the levels of the Grzegorczyk hierarchy.
Here, a further extension of this hierarchy is developed, in terms of
a predicatively generated infinitary calculus with stratifications of
numerical inputs up to and including level ω. The autonomous
ordinals are those below Γ, but they are generated
according to a weak (though quite natural) notion of transfinite induction
whose computational strength is "slow" rather than "fast" growing.
It turns out that the provably computable functions are now those
elementary recursive in the Ackermann function (i.e. Grzegorczyk's
ω-th level). All this is closely analogous to recent works of
Jaeger and Probst (2013) and Ranzi and Strahm (2013) on iterated stratified
inductive definitions, but their theories have full, complete induction as basis,
whereas ours have only a weak, ramified form of numerical induction at bottom.
- Florian Ranzi: "A flexible type system for the small Veblen ordinal"
The small Veblen ordinal θΩω0 is a well-known
ordinal in proof theory; it can be described by making use of Veblen functions
of arbitrary finite arity and it is the ordinal that measures the strength of
Kruskal's theorem. A natural subsystem of second order arithmetic for the
small Veblen ordinal is obtained by augmenting ACA0 by
Π12 bar induction, as shown by Rathjen and Weiermann (1993). We
propose a natural and flexible type system FIT whose strength is measured by
θΩω0. The acronym FIT stands
for Function(al)s, Inductive definitions, and Types. FIT
is patterned in a variant of Feferman's explicit mathematics: it contains
partial combinatory logic as its operational core and builds types on top by
using positive comprehension and accessibility inductive definitions. Induction
on the natural numbers as well as accessible parts is given in natural type 1
level functional form.
The formulation of FIT bears some similarities with the flexible type system
QL(F0-IR) introduced by Feferman (1992). Whereas our system FIT
accounts for infinitary inductive definitions, QL(F0-IR) only allows
finitary inductive types. Feferman (1992) showed that QL(F0-IR) is a
conservative extension of primitive recursive arithmetic PRA.
This talk will introduce the system FIT and provide an insight into the methods
used to obtain the small Veblen number as the lower and upper bound of the
proof-theoretic ordinal of FIT.
- Timotej Rosebrock: "Semi-Decidability in Explicit Mathematics"
Explicit mathematics have been introduced by Solomon Feferman as a
framework for Bishop style constructive mathematics. The first sort of
objects are operations. Operations may in addition be names of types, the
objects of the second sort. Types are collections of objects of the first
sort (but not all collections form a type). Explicit mathematics have the
so-called applicative axioms. Furthermore the existence of some types can be
proved via some axioms about operations for constructing names of types.
In this talk, we formalise the concept of decidability and several classically
equivalent concepts of semi-decidability in explicit mathematics and check if
they are provably equivalent in this framework. In particular, we construct a
countermodel, which is the restriction of the so-called Kleene's second model
to recursive functions.
- Sam Sanders: "On a hitherto unexploited nonstandard extension of the finitary standpoint"
The primitive recursive functions are the class of number-theoretic functions obtained by dropping 'unbounded search' from the definition of recursion.
This class forms a strict subclass of the recursive functions definable in Peano Arithmetic, the usual axiomatization of arithmetic. Goedel famously
proved that primitive recursion in all finite types exactly captures the recursive functions definable in Peano Arithmetic, i.e. extending primitive recursion
to a larger class of objects yields a much larger class of recursive functions. Now, the bar recursive functionals form a strict extension of the primitive
recursive functionals in all finite types, and it is a natural question if one can capture bar recursion by extending primitive recursion to a larger class of objects.
In this talk, we show that primitive recursion in all finite types with nonstandard number parameters captures bar recursion.
- Peter Schuster: "Transfinite Methods as Admissible Rules" (j.w.w. Davide Rinaldi)
Let ⊢ be a mono-conclusion entailment relation on a semigroup (S, ∗) such that if U, a⊢ c and U, b ⊢ c, then U, a ∗ b ⊢ c,
for all finite subsets U and elements a,b,c of S.
Let ⊢ be the multi-conclusion entailment relation on S that is generated by ⊢ and the axioms a∗b⊢∗ a,b and d⊢∗
where a,b ∈ S are arbitrary but d is a distinguished
element of S. Then every proof of U⊢∗ v can be converted into a proof of U⊢v whenever U is a finite subset and v an element of S. As a by-product,
the cut rule is eliminated. As an application, we can prove that the theory of integral domains is conservative for definite Horn clauses over the
theory of reduced rings; other applications to algebra are about local rings, valuation rings and ordered fields. The conversion also allows to eliminate,
from indirect proofs of statements of elementary wording, instances of the appropriate incarnation of Zorn's Lemma: the Krull-Lindenbaum Lemma in universal form.
- Ioannis Kokkinis: "First Steps towards Probabilistic Justification Logic"
Justification logic includes formulas of the form t:α meaning "the
agent believes α for reason t". Of course not all justifications for
belief are equal. Trying to describe our uncertainty for different sources of
justification we enrich the language of justification logic with operators of
the form P≥st, with the indented meaning "the justification formula
t holds with probability s".
In our talk we will introduce the probabilistic justification logic PJ, a
logic in which we can reason about the probability of justification
statements. We will present its syntax and semantics, prove a strong
completeness theorem and establish its decidability.
The axiomatization of PJ relies on an infitary rule, in order to avoid the
non-compactness difficulties and achieve strong completeness. The semantics for
PJ consists of a set of possible worlds, each a model of justification logic
and a probability measure on sets of possible worlds. Strong completeness is
proved via a standard countermodel construction. Decidability is achieved by
reducing the satisfiability problem for PJ in to a system of linear equalities
and inequalities.
- Michel Marti: "Towards Deduction Trees for Intuitionistic Modal Logic"
Based on a proof system for intuitionistic modal logics using nested sequents
which was developed by Strassburger, we try to give an alternative and more
constructive completeness proof for the intuitionistic modal logic IK. Our
approach uses deduction trees, which are closely related to the method of
deduction chains.
- Anton Freund: "Slow consistency, slow reflection, and a hierarchy between PA and PA+Con(PA)"
We present the notion of slow consistency of a theory as introduced by M. Rathjen, S.-D. Friedman and A. Weiermann (2013). These authors have
shown that the slow consistency of Peano arithmetic (PA) is a Π1-formula which extends PA to a theory strictly between PA and PA+Con(PA).
Furthermore they have built a hierarchy of height omega between PA and PA+Con(PA) by iterating slow consistency statements. In this talk we
discuss ways of extending this hierarchy transfinitely. For the most natural extension we will see that the limit step is related to a principle which
can be described as "uniform slow Σ1-reflection".
While we know that parameter-free slow reflection is Π1-conservative over PA+Con(PA) the status of
uniform slow reflection is still open.
- Dieter Probst: "Defining truth classes in conservative extensions of PA"
Following the terminology of Eyanant and Visser [1], truth classes are satisfaction classes with additional
properties. We present extensions of PA whose conservativity can be shown by cut-elimination techniques and that allow to define various truth classes.
[1] Ali Eyanant and Albert Visser. New constructions of satisfaction classes, in: Unifying the philosophy of truth
(Achourioti, T., Galinon, H., Fujimoto, K. and Martínez-Fernández, J. eds.), Springer, to appear.
Accommodation
Organizers
Last change
17. December 2014
