Aim

This workshop is held to discuss on recent studies of proof theory of non-classical logic, especially hybrid logic.

Date & Time

7th March 2024, 10:00-16:40

Abstracts

Andrzej Indrzejczak (University of Łódź): 

Hybrid Logic Extended with Lambda and Iota Operators

Complex names conveying information about their intended designates are of common use in natural languages. Definite descriptions, usually formalised by means of iota operator, are of special interest, and as such they were intensely investigated by philosophers of language. Particularly interesting and difficult problems are generated by their behaviour in intensional contexts. We focus on the development of well-behaved proof-theoretic tools for dealing with iota operator in hybrid logic which offers the most subtle framework for this aim. Additionally, the introduction of lambda operator for making complex predicates facilitates things greatly. Two proof systems for hybrid logic with lambda and iota operator will be presented. The first is based on the approach of Hintikka to definite descriptions, and was developed first by Fitting in the setting of standard modal logic, and then by Indrzejczak in the setting of hybrid logic. The second is based on the Russellian approach to definite descriptions and was developed recently by Indrzejczak and Zawidzki.

Nils Kürbis (Ruhr-Universität Bochum):

A Theory Definite Descriptions Formalised by Binary Quantification for Modal Logic

Definite Descriptions can be fruitfully formalised by a binary quantifier. Complete sentences of the form 'The F is G' are formalised by Ix(F, G). This takes on Russell's point that definite descriptions have meaning only in the context of complete sentences in which they occur. It also has the advantage of incorporating scope distinctions directly into the notation. It sometimes said that scope distinctions are unnecessary in the non-modal case (although I'm sceptical, essentially for Russellian reasons). It is, however, almost universally agreed that scope distinctions are unavoidable when definite descriptions are formalised in modal logic. I shall present the proof theory of a system of modal logic with the binary quantifier for definite descriptions. The background logic for this is a positive free logic. 'The F is G' can be true in a world even if there exists no F in that world, but not if there is more than one. The modal logics are the usual suspects of normal modal logics. I'll also consider how to reconstruct the important concept of rigidity in this framework. This will also illustrate how difference in scope are treated.  

Ren-June Wang (National Chung Cheng University):

Path Models and Their Corresponding Sequent Calculi for Modal Logics

Compared with the standard possible world semantics, a path in a path model is a finite sequence of possible worlds in which each world, except the first, is accessible from the one it follows. So, roughly speaking, path models are a semantic framework adjusted from the standard possible world semantics such that the structure of frames is categorized by the set of paths rather than the relation between worlds. To further utilize the mechanism, truth values are then directly assigned to sequences of sequents of modal formulas, not to formulas, as normally done. Consequently, some style of Gentzen-type sequent calculi with sequences of sequents as the objects in a proof can be straightforwardly interpreted in accordance with path models. In this paper, we will demonstrate path models and their corresponding calculi of sequences of sequents for the normal modal logics extended from K by axioms D, T, 4, B, and 5, and prove the completeness theorem with respect to these models and calculi. Furthermore, for the logics extended from K by D, T and 4, we will discuss their cut-free versions of calculi.

Dazhu Li (University of Chinese Academy of Sciences):

Tableau Calculi for The Hybrid Logic of The Hide and Seek Game and Further Extensions

As suggested by the name, the logic of the hide and seek game is a framework to capture the interaction of players in the hide and seek game, which can be broadly conceived as a pursuit-evasion environment. So far, many properties of the logic have been explored, and it turns out that a hybrid extension of the logic has many advantages. In this talk, we proceed to present tableau calculi for a crucial decidable fragment of the hybrid logic of the hide and seek game and its further extensions, and show that the resulting calculi are complete. Also, we analyze the features of the logical frameworks that can force the tableau calculi to be unterminated. This is an ongoing project joint with Fenrong Liu and Katsuhiko Sano.

Yuichiro Hosokawa (Gunma Prefectural Women's University)

From Counterfactual Conditionals to Temporal Conditionals

In this presentation, I introduce some of the results in "From Counterfactual Conditionals to Temporal Conditionals" (Hosokawa, 2023). More specifically, I present some of the prooftheoretical results rather than the model-theoretical results in it. Hosokawa (2023) considers the following counterfactual transitive inference referred to as (CT): if it were the case that φ, then it would be the case that ψ, and if it were the case that ψ, then it would be the case that χ; therefore, if it were the case that φ, then it would be the case that χ. Whereas (CT) can be formalized in David Lewis's most basic counterfactual logic V so that (CT) becomes valid in his sphere model (Lewis, 1973), (CT) can also be formalized in a special case of Braüner's natural deduction system for Hybrid Logic (Braüner, 2011), which Hosokawa (2023) referred to as hybrid tense logic for temporal conditionals (HTL_TC). I then review some proof-theoretical (or rather inferentialistic) merits that Hosokawa (2023)'s formalization has but David Lewis’s formalization does not. Also, if time allows, I would like to present new related results, namely, interpretation of hybrid counterfactual logic with downarrow binder (a straightforward extension of V_HC(@) in Sano (2009)) into HTL_TC and comparison of their expressive power.

Patrick Blackburn (Roskilde University):

Proof Theory for Prior's Ideal Language

This talk is a technical follow-up to my AWPL keynote address: I will discuss the proof theory of Prior's Ideal Language (PIL) with respect to general models. I will begin with some remarks on axiomatics, and then present a (sound and complete) tableau system for PIL. I may also make some brief remarks about natural deduction.