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 ACA0 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 SR,I is well-founded on JR,I ; where we write SR,I and JR,I to highlight that their definitions depend on 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 [( ∀xI (∀yI (yRxP(y))) → P(x)) → ∀xI (P(x))].
The goal of this work is to express and prove the theorems above by using intuitionistic logic and first order reasoning. Hence given a SR,I -inductive predicate P on JR,I we will prove that for every xJR,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 aG b = 1 if ab 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.