ABSTRACT. Gödel logics are [0,1]-valued logics intermediate between intuitionistic and classical logic. In this tutorial, we cover their definitions and basics.

ABSTRACT. Link to abstract

ABSTRACT. In this paper, we present an algorithm for establishing decidability and finite model property of intuitionistic modal logic IK. These two results have been previously established independently by proof theoretic and model theoretic techniques respectively. Our algorithm, by contrast, enables us to establish both properties at the same time and simplifies previous approaches. It implements root-first proof search in a labelled sequent calculus that employs two binary relations: one corresponding to the modal accessibility relation and the other to the preorder relation of intuitionistic models. As a result, all the rules become invertible, hence semantic completeness could be established directly by extracting a (possibly infinite) countermodel from a failed proof attempt. To obtain the finite model property, we rather introduce a simple loopcheck ensuring that root-first proof search always terminates. The resulting finite countermodel displays a layered structure akin to that of intuitionistic first-order models.

ABSTRACT. We present a polymorphic linear lambda-calculus as a proof language for second-order intuitionistic linear logic. The calculus includes addition and scalar multiplication, enabling the proof of a linearity result at the syntactic level.

ABSTRACT. This paper presents a formal theory of Krivine’s classical realisability interpretation for the first-order Peano arithmetic (PA). To formulate the theory as an extension of PA, we first modify Krivine’s original definition to the form of number realisability, similar to Kleene’s intuitionistic realisability for Heyting arithmetic. By axiomatising our realisability with additional predicate symbols, we obtain a first-order theory CR (compositional realisability) that can formally realise every theorem of PA. Although CR itself is conservative over PA, adding a type of reflection principle that roughly states that “realisability implies truth” results in CR being essentially equivalent to the Tarskian theory CT (compositional truth), which is known to be proof-theoretically stronger than PA. Thus, CT can be considered a formal theory of classical realisability. In addition, we prove that a weaker reflection principle that preserves the difference between realisability and truth is sufficient for CR to achieve the same strength as CT.

ABSTRACT. Inspired by McGee's semantics for conditionals, we define a language with contexts explicitly encoded in formulas to evaluate propositions under assumptions. We give a three-valued semantics for the language and define a ternary notion of validity, unifying two kinds of validity in the literature. By the new notion of validity, an inference is not just valid or invalid, but valid or invalid under a set of assumptions. Based on the three-valued semantics and ternary notion of validity, we give a unified solution to some typical puzzles concerning indicatives and epistemic modals.