### Abstracts

**Michael Bärtschi — "Uniform fixpoints and relatives in second order
arithmetic"**

We will introduce an extension of the usual language of second order arithmetic in order to
introduce a uniform version of the fixpoint axiom (FP). With ACA_{0} as our base
theory, we will discuss connections to uniform versions of (ATR), i.e., the axiom scheme
of arithmetic transfinite recursion, and embed the uniform theory (UFP)_{0} into a
subsystem of Kripke Platek set theory. Finally, we will touch upon the impact of adding
additional rules and axiom schemas.

**Lukas Jaun — "An In Depth Look at the Exact Completion Construction in the Category of Sets"**

Vitale gave a self-contained description how to construct the Exact Completion which works for any weakly cartesian closed category.

We will apply this construction to the category of Sets where we can more directly observe how it works.

**Eveline Lehmann — "Subset models for justification logic"**

Inspired by the topological semantics in evidence logic we established new semantics for justification logic. Instead of using Kripke structures and basic evaluations, our evidence function maps to each world and each justification term some set of worlds. If such an evidence set E(w,t) is a subset of some truthset [F], we say „t justifies F“. Beside presenting our models I will explain, why and how we use so called impossible worlds in this framework.

**Nenad Savić — "Relevant Justification Logic"**

We introduce a relevant justification logic, RJ4, which is a combination of the relevant logic R and the justification logic J4. We describe the corresponding class of models, provide the axiomatization and prove that our logic is sound and complete.

**Silvia Steila — "Proving well-foundedness results using first order reasoning"**

(On-going work with Stefano Berardi and Makoto Tatsuta)

Classically a binary relation *R* is well-founded on a set *I* if there are no
infinite *R*-decreasing sequences of elements of *I*. Many relevant theorems about well-founded
relations are of the form: assume that a binary relation *R* is well-founded on *I*, then the
binary relation *S _{R,I}* is well-founded on

*J*; where we write

_{R,I}*S*and

_{R,I}*J*to highlight that their definitions depend on

_{R,I}*R*and

*I*. Among others: Kleene Brower's theorem, Enriques' theorem, Nested Fan Theorem, Homogeneous Closure Theorem, Podelski-Rybalchenko Termination Theorem and the Almost Full Theorem. Their original proofs use classical logic and second order reasoning.

There are different definitions of well-foundedness which are not equivalent over second order
intuitionistic arithmetic and it is well know that well-foundedness can be reformulated in such a way that
all the theorems above are provable using intuitionistic logic and second order reasoning.
The definition used to this aim is: a relation is intuitionistically well-founded on
*I* if *I* is a superset of all *R*-inductive predicates: i.e.,

- ∀
*P*[( ∀*x*∈*I*(∀*y*∈*I*(*yRx*→*P*(*y*))) →*P*(*x*)) → ∀*x*∈*I*(*P*(*x*))].

*S*-inductive predicate

_{R,I}*P*on

*J*we will prove that for every

_{R,I}*x*∈

*J*

_{R,I}*P(x)*holds, by involving only a finite number of

*R*-inductive predicates, which of course depend on the given

*P*.

**Olim Tuyt — "Decidability for S5 modal Gödel logics"**

In this talk we will prove a decidability result for an S5 modal Gödel
logic. Propositional Gödel logic **LC**, as introduced by Dummet (1959), is
the infinite-valued logic with truth values in the [0,1]-interval and 1 as the
designated truth value. Its truth functions are minimum and maximum for
conjunction and disjunction respectively together with Gödel implication
→_{G}, where *a* →_{G} *b* = 1 if *a* ≤ *b* and = *b* otherwise. This logic **LC** is
axiomatized by extending intuitionistic logic with the axiom of prelinearity
(ϕ → ψ) ∨ (ψ → ϕ).

From results by Bull (1966), Mints (1968) and Ono (1977), it is known
that the one-variable fragment of first-order intuitionistic logic, **MIPC**, is
decidable. In this talk we consider the Gödel analogue of **MIPC** by extending it with
(ϕ → ψ) ∨ (ψ → ϕ). As its standard Kripke semantics does not
possess the finite model property, we introduce an alternative semantics.
Approaching the new semantics algebraically, we prove decidability of this
logic and determine the complexity of S5(**G**)-validity.