The Schedule

Graded models are one of the more radical departures from the classical notion of model which stem from (at least) three distinct origins: Boolean-valued models, continuous model theory, and semantics of predicate many-valued logics.

The predicate symbols in such models are interpreted as functions that assign, to each tuple of elements of the domain, values from a certain set of grades (which is usually endowed with some additional structure).

In this talk I focus on the last of these three origins. In its first part I present recent results in extending the class of logics for which graded models provide sound and complete semantics and in the second part I analyze various forms of Skolem and Herbrand theorems valid in these logics.

One of the foundational results of (classical) finite model theory, due to Ronald Fagin, shows that every formula of a finite relational language is either almost surely true or almost surely false over finite structures. This has been called a 0-1 law. This talk intends to contribute to the finite model theory of many-valued logics by generalizing this 0-1 law to first-order finite models valued over finite MTL-chains. We will prove that for any first-order (or infinitary with finitely many variables) formula Phi, there is a truth-value that Phi takes almost surely in every finite many-valued model and such that every other truth-value is almost surely not taken. This result also generalizes a theorem for Lukasiewicz logic due to Robert Kosik and Christian G. Fermüller. (This talk is based on joint work with Guillermo Badia.)

In the the present contribution, we prove an Omitting Types Theorem (OTT) for an

arbitrary fragment of hybrid- dynamic first-order logic with rigid symbols (i.e. symbols

with fixed interpretations across worlds) closed under negation and retrieve. The

logical framework can be regarded as a parameter and it is instantiated by some well-known

hybrid and/or dynamic logics from the literature. We develop a forcing technique

and then we study a forcing property based on local satisfiability, which lead to a

refined proof of the OTT. For uncountable signatures, the result requires compactness,

while for countable signatures, compactness is not necessary. We apply the OTT to

obtain upwards and downwards Lowenheim-Skolem theorems for our logic, as well as

a completeness theorem for its constructor-based variant. The main result of this paper

can easily be recast in the institutional model theory framework, giving it a higher level

of generality. This is joint work with Daniel Gaina and Tomasz Kowalski.

In this talk we argue that a symmetric picture of the relationship between equality and apartness can be attained by considering these notions on the background of bi-intuitionistic logic instead of the usual intuitionistic logic. As the intuitionistic negation of a relation of apartness is an equality, the dual-intuitionistic co-negation of an equality is a relation of apartness. At the same time, as the intuitionistic negation of equality is not an apartness, the co-negation of an apartness is not an equality.

(This is joint work with Paolo Maffezioli)

Using labeled sequent calculi, I show that Lewis' logic of counterfactuals can be translated in a bimodal logic with two modalities over worlds and sets of worlds. Importantly, each modality is normal, in the sense it validates the necessitation rule and axiom K. Consequently, the resulting calculus, except being labeled, is entirely standard and the proof of cut-elimination theorem goes through with only minor adjustments

We consider extensions of Infinite-valued Łukasiewicz predicate logic with identity by many-valued analogues of classical cardinality quantifiers, looking for compactness properties matching those of their classical counterparts. It is well known, for example, that first order logic enriched with the quantifier "there are uncountably many ...", or the quantifier "there are more than continuum many...", is countably compact. But each classical cardinality quantifier splits in several possible versions in the many-valued setting, and compactness is sensible to this diversity. More important, compactness is sensible to the type of identity allowed: there are Łukasiewicz versions of the above

mentioned classical quantifiers that yield countably compact extensions under crisp identity, but to obtain countable compactness under many-valued identity we have to go up to the first strong limit cardinal of uncountable cofinality. We explain the notions and methods utilized to obtain these results.

Van Benthem's celebrated modal characterization theorem states that

modal logic is precisely the bisimulation-invariant fragment of

first-order logic. We discuss an analogous result for (Zadeh) fuzzy

modal logic within fuzzy first-order logic. The appropriate notion

that replaces bisimilarity in this context is behavioural distance,

and we call a formula bisimulation-invariant if it is non-expansive

w.r.t. behavioural distance. The modal characterization result then

takes the form of an approximation theorem: Every

bisimulation-invariant formula in fuzzy first-order logic can be

approximated by fuzzy modal formulae of bounded rank. Time permitting,

we will give an outlook on generalizations.

(joint work with Sergei Odintsov and Heinrich Wansing)

This talk is devoted to modal logics by Grigore Moisil, one of pioniers of computer science and of algebraic logic.

In 1942, G. Moisil developed a series of modal logics motivated by—at the time—quite novel considerations. As it turns out these logics are closely connected to some now well-known non-classical logics. The aim of our work is to shed some light on Moisil's work, outline these connections and to supplement formal proofs to some facts Moisil seems to have envisioned. The novelty of Moisil's approach was to associate a logic not with a single matrix but with a class of algebraic systems,

namely, the class of bi-residuated lattices, which contain residual operations with respect to both the join (represented by the implication connective) and the meet (represented by the difference connective)

operations. This system, which we denote here BiM, turns out to be equivalent to C. Rauszer's logic HB, which, in turn, is a conservative extension of intuitionistic propositional logic with the difference

connective. In this way Moisil has anticipated by more than thirty years

the development of bi-intuitionistic logic. This logic is also related to Dummett's linear logic and to Gödel-Smetanich (here-and-there) logic via its special and three-valued extensions, respectively. Finally,

Moisil has shown that three-valued Łukasewicz logic can be defined

within the three-valued BiM-extension.

The modal aspect of Moisil's paper comes in the form of the general modal logic GML, which conservatively extends BiM with operators of impossibility, contingency, possibility, and necessity definable via

implication and difference connectives. This logic makes clear how different Moisil's view of modalities was compared to the modern one. Motivated by this fact we compare Mosil's approach to modal logic with the one by J. Łukasiewicz and K. Došen.

The final logic from Moisil's paper we are interested in is the general symmetric modal logic GSML, which is obtained by adding to GML an involutive and contrapositive negation motivated by the properties of Łukasiewicz's negation. As Moisil himself pointed out, the difference

connective becomes definable via negation and implication in GSML,

illuminating the connection of GSML to both Heyting-Ockham logic N* and

the logic HYPE suggested recently by Leitgeb as a basic logic of

hyperintensional contexts.

We will show that bi-intuitionistic propositional logic is the maximal logic that is compact, has Tarski Union Property, and is preserved under bi-asimulations.

The compactness in this result is assumed relative to theories understood as pairs of sentence sets of the form (truth assumptions, falsity assumptions); bi-asimulations, in their turn, are a modification of bisimulation that is known to semantically characterize bi-intuitionistic propositional logic in the style of van Benthem Modal Characterization Theorem.

The result continues a long line of similar results for other related logics (intuitionistic propositional and first-order logics, basic modal first-order logic, the logic of the universal modality, etc), however, the machinery of the proof is relatively novel and deserves a somewhat detailed sketch.

The talk is based on a joint work with Guillermo Badia.