ABSTRACT. I will discuss reasoning about strategic abilities of rational agents and groups (coalitions) of agents to guarantee achievement of their goals, while acting and interacting within a society of agents. That strategic interaction can be quite complex, as it usually involves various patterns combining cooperation and competition. 

In this talk I will show how formal logic can be useful in capturing such reasoning. I will first present as a background the basic “Coalition Logic” and then I will give a brief overview of some recently introduced andstudied more expressive and versatile logical systems, including:    

1. the Socially Friendly Coalition Logic (SFCL), enabling formal reasoning about strategic abilities of individuals and groups to ensure achievement of their private goals while allowing for cooperation with the entire society;   
2. the Logic of Coalitional Goal Assignments  (LCGA), capturing reasoning about strategic abilities of the entire society to cooperate in order to ensure achievement of the societal goals, while protecting the abilities of individuals and groups within the society to achieve their individual and group goals. 
3. the Logic for Conditional Strategic Reasoning (ConStR), formalising reasoning about agents’ strategic abilities conditional on the goals of the other agents and on the actions that they are expected to take in pursuit of these goals. 

In conclusion, I will take a more general perspective on a unifying logic-based framework for strategic reasoning in social context. 

ABSTRACT. The present article examines a system of four-valued logic recently introduced by Oleg Grigoriev and Dmitry Zaitsev. In particular, besides other interesting results, we will clarify the connection of this system to related systems developed by Paul Ruet and Norihiro Kamide. By doing so, we discuss two philosophical problems that arise from making such connections quite explicit: first, there is an issue with how to make intelligible the meaning of the connectives and the nature of the truth values involved in the many-valued setting employed --- what we have called `the Haackian theme'. We argue that this can be done in a satisfactory way, when seen according to the classicist's light. Second, and related to the first problem, there is a complication arising from the fact that the proof system advanced may be made sense of by advancing at least four such different and incompatible readings --- a sharpening of the so-called `Carnap problem'. We make explicit how the problems connect with each other precisely and argue that what results is a kind of underdetermination by the deductive apparatus for the system.

ABSTRACT. In this paper, we elaborate on the ordered-pair semantics originally presented by Matthew Clemens for LP (Priest's \textit{Logic of Paradox}). For this purpose, we build on a generalization of Clemens semantics to the case of n-tuple semantics, for every n. More concretely, i) we deal with the case of a language with quantifiers, and ii) we consider philosophical implications of the semantics. The latter includes, first, a reading of the semantics in epistemic terms, involving multiple agents. Furthermore, we discuss the proper understanding of many-valued logics, namely LP and K3 (Kleene strong 3-valued logic), from the perspective of classical logic, along the lines suggested by Susan Haack. We will also discuss some applications of the semantics to issues related to the mixed consequence relations, promoted by Pablo Cobreros, Paul Egre, David Ripley and Robert van Rooij.

ABSTRACT. Formal reasoning with `non-denoting terms', esp. non-referring descriptions such as ``the King of France'', is still an under-investigated area. The recent exception being a series of papers e.g. by Indrzejczak and Zawidzki. The present paper offers an alternative to their approach: instead of free logic and sequent calculus, it's framed in partial type theory with natural deduction in sequent style and utilizes a Tich\'{y}an theory of descriptions. It successfully handles deduction with intensional transitives whose complements are non-referring descriptions and Strawsonian rules for them.

ABSTRACT. According to Russell, strict uses of the definite article ‘the’ in a definite description ‘the F’ involve uniqueness; in case there is more than one F, ‘the F’ is used somewhat loosely, and an indefinite description ‘an F’ should be preferred. We give an account of constructions of the form ‘the F is G’ in which the definite article is used loosely (and in which ‘the F’ is, therefore, incomplete), essentially by replacing the usual notion of identity in Russell’s uniqueness clause with the notion of qualified identity proposed by Więckowski, i.e., ‘a is the same as b in all Q-respects’, where Q is a subset of the set of predicates P. This modification gives us qualified notions of uniqueness and definiteness. A qualified definiteness statement ‘the Q-unique F is G’ is strict in case Q = P and loose in case Q ⊂ P. The account is made formally precise in terms of proof theory and proof-theoretic semantics.

ABSTRACT. Logics of content relationship defined by Richard Epstein, i.e., relatedness logics and dependence logics, are special cases of relating logic. Such systems are extensions of classical logic obtained by introducing implications whose truth requires that 1) the antecedent is false or the consequent is true, 2) the antecedent is related to the consequent with respect to content. Epstein’s systems differ due to various understandings of the content relationship.

In the paper, we would like to present Epstein’s logics proof theory, focusing on approaches that have not been discussed so far. Thus, we will focus on natural deduction systems and comment on sequent systems.

ABSTRACT. Non-Fregean logics were proposed by Roman Suszko as the opposition to the idea, attributed to Frege, that sentences denote their own truth values. A critique of this view has been raised in Wittgenstein's \textit{Tractatus}, which became a philosophical base for developing new logical systems by Suszko. Following Wittgenstein and Wolniewicz \cite{suszko-recenzja}, he disagreed with the Fregean view on denotation arguing that identity of the logical value of two sentences does not entail identity of their denotations \cite{Suszko:1968a,suszko1975}.

Suszko provided syntactic and algebraic characterization of several non-Fregean systems; the weakest non-Fregean logic introduced by him, \textsf{SCI} (\textit{Sentential Calculus with Identity}), was obtained from Classical Propositional Calculus (hereafter, \textsf{CPC}) by extending the language with the identity connective `$\equiv$', and by adding, as axioms, formulas of the following forms:\smallskip

\begin{tabular}{lllll} ($\equiv_{1}$) & $\phi\equiv \phi $ && ($\equiv_{3}$) & $(\phi\equiv \chi)\to (\phi\leftrightarrow \chi )$ \\[2pt] ($\equiv_{2}$) & $(\phi\equiv\chi)\to (\neg \phi \equiv \neg\chi )$ && ($\equiv_{4}$) & $((\phi\equiv \psi)\land(\chi\equiv \omega ))\to((\phi\otimes \chi) \equiv (\psi\otimes \omega))$ \end{tabular}

\smallskip \noindent where $\otimes \in \{ \land, \lor, \to, \leftrightarrow, \equiv\}$. Modus ponens (MP) is the only rule of inference. Identity characterized by $\mathsf{SCI}$ is very strong; every thesis of this logic with `$\equiv$' as the main connective follows under the first axiom scheme. Formulas of this form are called \textit{trivial equations}.

The distinction between a truth value and a denotation of a sentence allows for a much more refined analysis of its content. However, the fact that only trivial equations are theorems of \textsf{SCI} makes the analysis drastically limited. Suszko himself found three theories, extending $\mathsf{SCI}$, philosophically important. In this paper we focus on one of them, \textsf{WB} (\textsf{W} stands for `Wittgenstein' and \textsf{B} -- for `Boolean'). In \textsf{WB}, the axiomatic basis of \textsf{SCI} is enriched with \textit{Boolean axioms}, that is, formulas of the forms:\smallskip

\begin{tabular}{lllll} $(\equiv_{5})$ & $(( \phi\land \chi) \lor \psi) \equiv ((\chi \lor \psi) \land (\phi \lor \psi))$ && $(\equiv_{8})$ & $(\phi\land \top) \equiv \phi$ \\[2pt] $(\equiv_{6})$ & $(( \phi\lor \chi ) \land \psi) \equiv ((\chi \land \psi) \lor (\phi \land \psi))$ && $(\equiv_{9})$ & $(\phi\to \chi ) \equiv (\neg \phi \lor \chi )$ \\[2pt] $(\equiv_{7})$ & $(\phi\lor \bot) \equiv \phi$ && $(\equiv_{10}$) & $(\phi\leftrightarrow \chi ) \equiv ((\phi\to \chi )\land(\chi\to \phi ))$ \end{tabular}

\smallskip \noindent Semantically, \textsf{WB} is interpreted in Boolean algebras.

Decidability of \textsf{SCI} was settled in \cite{bloom-suszko1972}, and sequent calculi were proposed already in the seventies \cite{michaels1974,Rogava:1975,Rogava:1979}; later on a large number of proof systems and proof procedures for \textsf{SCI} has been developed \cite{Wasilewska1976,wasilewska1984,golinskapilarek2007RS-SCI,orlowska-golinskapilarek2011DT,chlebowski2018,golinskapilarek2019DSCI,GolinskaPilarek2021,JGP:inJP,AI:SCI22}. In the case of \textsf{WB}, for a long time the axiomatic account was the only available proof-theoretic description of the logic. Although \textsf{WB} seems relatively simple, its decidability has not been proved so far.

In \cite{ATphd} sequent calculi for three extensions of \textsf{SCI}, called \textsf{WB}, \textsf{WT} and \textsf{WH}, were developed. To the best of our knowledge, \cite{ATphd} introduced the first sequent systems for these logics. However, the author of \cite{ATphd} presented arguments that in the sequent calculus for \textsf{WB} the rule of cut is not eliminable. In our talk we will present a new variant of sequent calculus for \textsf{WB}, $\mathsf{SC_{WB}}$, and we will demonstrate the proof of cut elimination in $\mathsf{SC_{WB}}$. Using derived rules of $\mathsf{SC_{WB}}$ we will define a decision procedure for \textsf{WB}.

The rules of $\mathsf{SC_{WB}}$ are sound in the original algebraic semantics, but we also define an extension of a truth-valuation semantics for \textsf{WB} and use it in the proof of correctness of the procedure. Finally, we use $\mathsf{SC_{WB}}$ as a point of departure for a definition of Kripke-style semantics for \textsf{WB}. It is well-known that the stronger extensions of \textsf{SCI}---\textsf{WT} and \textsf{WH}---correspond to modal logics \textsf{S4} and \textsf{S5}, it is not settled, however, what is the modal content of \textsf{WB}. Our Kripke semantics opens up a possibility to adress this issue.

ABSTRACT. Temporal logic is used, int.al., to model purely logical aspects of reasoning about events in time, whereas erotetic logic is used, int.al., to model purely logical aspects of reasoning with questions involved. Many great logicians worked in both these branches of philosophical logic (some being considered as the founding fathers or at least pioneers in both of them---like Arthur Prior or Nuel Belnap), which makes at least one good reason to have the two---the temporal and the erotetic---in one framework.

The method of Socratic proofs is a proof method grounded in the logic of questions called Inferential Erotetic Logic \cite{AW:1995,AW:2013,DLJ:2024}. The method has been adjusted to a number of various logics \cite{AW:2004,AW:2006SPQ,WVL:2005,DLJ:2007,DLJ:2008,SzChDLJ:LFI} and it can be viewed as a formal tool of analysis of cognitive processes which we would describe as inquiring into a problem, problem-solving, problem reformulating, dividing problems into subproblems or even answering questions by pure questioning \cite{AW:2013,DLJ:2024}.

The aims of our presentation are twofold. First, we will describe the erotetic calculus for Propositional Linear-Time Temporal Logic (\textsf{PLTL}) from purely proof-theoretical perspective. Technically, the calculus is a variant of sequent-calculus formulation of analytic tableaux, using ideas coming from natural deduction \cite{Bolotov2006, Bolotov2007} and resolution systems \cite{temporalresolutionFisher} to deal with some specific problems of \textsf{PLTL} (like loops). We will present a decision procedure for \textsf{PLTL} and discuss its implementation in Python.

In the second part of the presentation we shall focus on the erotetic aspect of the method; we will discuss its potential in the modelling of reasoning involving questions.

ABSTRACT. We will present a calculus of Socratic transformations for Propositional Linear-Time Temporal Logic (PLTL). Socratic transformations simulate reasoning aimed at solving a given logical problem by pure questioning [2, 3]. This is the method that transforms the initial question into consecutive questions without making any use of answers to the questions just transformed. Informally, a successful transformation, called a Socratic proof, ends with a question of a specified final form, which can be answered from a semantic point of view in only one rational way.

We aim to tackle temporal problems requiring specific — temporal — reasoning for their solution. That is why we developed our Socratic calculus based on Propositional Linear-Time Logic [1, 4], where formulae are interpreted over linear, discrete sequences of states that are finite in the past and infinite in the future.

References [1] Emerson, E.A. (1990). Temporal and Modal Logic. J. van Leeuwen (Ed.), Handbook of theoretical computer science: Volume b, formal models and semantics. (pp. 996–1072.). Cambridge, MA, USA: MIT Press. [2] Leszczyńska-Jasion, D., Urbański, M., Wiśniewski, A. (2013). Socratic trees. Studia Logica, 101, 959-986. [3] Wiśniewski, A. (2004). Socratic Proofs. Journal of Philosophical Logic, 33(2), 299–326. [4] Wolper, P. (1985). The tableau method for temporal logic: An overview. Logique et Analyse, 28, 119–136.

ABSTRACT. Propositional Linear-Time Temporal Logic (PLTL) has been considered in a number of proof systems, ranging from tableaux methods [8, 5] and natural deduction [3, 4] to sequent calculi [1, 6]. The sequent calculi and tableaux methods approaches are based on the similar reasoning: usually involving state-prestate rules and facing similar problems around loop-generating formulas. However, the labelled natural deduction approach employs a different rationale that involves relational judgements and, thus, faces different obstacles revolving around (the principle of) induction.

We will present a labelled hypersequent calculi [7, 2] for PLTL that follows that relational reasoning and yet avoids the problem of induction.

References [1] R. Alonderis and R. Pliuskevicius. Sequent systems for PLTL. Lietuvos matematikos rinkinys, 54:1–5, 2013. [2]  A. Avron. A constructive analysis of RM. Journal of Symbolic Logic, 52, 1987. [3]  A. Bolotov, A. Basukoski, O. Grigoriev, and V. Shangin. Natural deduction calculus for linear-time temporal logic. In Lecture Notes in Computer Science, volume 4160 LNAI, 2006. [4]  A. Bolotov, O. Grigoriev, and V. Shangin. Automated natural deduction for propositional linear-time temporal logic. In Proceedings of the International Workshop on Temporal Representation and Reasoning, 2007. [5]  J. Gaintzarain, M. Hermo, P. Lucio, and M. Navarro. Systematic Semantic Tableaux for PLTL. Electronic Notes in Theoretical Computer Science, 206, 2008. [6]  J. Gaintzarain, M. Hermo, P. Lucio, M. Navarro, and F. Orejas. A cut-free and invariant- free sequent calculus for PLTL. In Lecture Notes in Computer Science, volume 4646 LNCS, 2007. [7]  A. Indrzejczak. Sequents and Trees. Springer Nature Switzerland, 2021. [8]  P. Wolper. The tableau method for temporal logic: An overview. Logique et Analyse, 28:119–136, 1985.

ABSTRACT. attached as a file

ABSTRACT. Solving logic puzzles by modelling them in first order logic (FOL) is old hat in computer science [3]. For instance, Prover9 theorem prover and Mace4 model finder [4] have been applied to logical puzzles [2]. We show here how Mace4 can be used to solve probabilistic tasks. The proposed approach is to formalise the probabilistic puzzle in equational FOL.

ABSTRACT. The substructural Strict/Tolerant logic based on a strong Kleene valuation ($sST$) was motivated by its ability to express a fully transparent truth predicate and the tolerance principle without falling into the traps of semantic and soritical paradoxes. Even though $sST$ rejects the meta-inferential rule of Cut, it has been shown that many instances of Cut are recoverable. Thus, not only theories of truth and vagueness based on $sST$ can avoid the semantic and soritical paradoxes, these theories stay very close to classical theories which is counted as a virtue of $sST$. In a recent paper by Murzi and Rossi, the authors argue that the notion of (un)paradoxicality plays a major role in recapturing the ``safe'' instances of Cut. However, the theory of truth based on $sST$ cannot be extended to express the notion (un)paradoxicality on pain of revenge paradox. Similarly, in a recent paper by Bruni and Rossi, the authors argue that the theory of vagueness based on $sST$ cannot be extended to express the notion of determinateness on pain of revenge paradox, even though ``determinateness'' plays a major role in the theory.

In this paper, we argue that given the analysis of these revenge paradoxes, the Strict/Tolerant logician should prefer a weak Kleene variation of the Strict/Tolerant logic ($wST$). We argue that $wST$ can express a fully transparent truth predicate and the tolerance principle as well as the notions of (un)paradoxicality and determinateness (though we prefer to use the notion of groundedness to encompass both of these notions), while still being immune to revenge. We conclude that the logic $wST$ is more appealing than $sST$, for it has the same virtues as $sST$ while it has an unmatched expressive power.

ABSTRACT. This paper introduces a unified Gentzen-style framework for until-free propositional linear-time temporal logic. The proposed framework can handle both Gentzen-style single-succedent sequent calculus and Gentzen-style natural deduction system uniformly. Furthermore, the paper establishes an equivalence, alongside providing proofs for cut-elimination and normalization theorems.A theorem for equivalence between them and cut-elimination and normalization theorems for them are proved.

ABSTRACT. Gentzen-style sequent calculi and Gentzen-style natural deduction systems are introduced for a family (C-family) of connexive logics over Wansing's basic connexive logic C. The C-family is derived from C by incorporating the Peirce law, the law of excluded middle, and the generalized law of excluded middle. Theorems establishing equivalence between the proposed sequent calculi and natural deduction systems are demonstrated. Cut-elimination and normalization theorems are established for the proposed sequent calculi and natural deduction systems, respectively.

ABSTRACT. In this paper, we prove the semantic incompleteness of the Hilbert-style system for the minimal normal term-modal logic with equality and non-rigid terms that was proposed in Liberman et al. (2020) "Dynamic Term-modal Logics for First-order Epistemic Planning." Term-modal logic is a family of first-order modal logics having term-modal operators indexed with terms in the first-order language. While a first-order formula is valid over the class of all frames in the Kripke semantics for the term-modal logic proposed there, Liberman et al. (2020)'s Hilbert-style system cannot derive it. We show this fact by introducing a non-standard Kripke semantics which makes the meanings of constants and function symbols relative to the meanings of relation symbols combined with them.

ABSTRACT. Quantum logic (QL) is a non-classical logic for analyzing the propositions of quantum physics. Modal logic MB, which is a logic for directly handling the value of the inner product that appears in quantum mechanics, was constructed With the development of QL. Although the basic properties of this logic have already been analyzed in a previous study, there are still some parts that are incomplete. They are concerned with the completeness theorem and the decidability of the validity problem. In this study, those problems are solved by constructing a tree sequent calculus of this logic.