Quine and Slater on Paraconsistency and Deviance

In a famous and controversial paper, B. H. Slater has argued against the possibility of paraconsistent logics. Our reply is centred on the distinction between two aspects of the meaning of a logical constant ^*c^* in a given logic: its operational meaning, given by the operational rules for ^*c^* in a cut-free sequent calculus for the logic at issue, and its global meaning, specified by the sequents containing ^*c^* which can be proved in the same calculus. Subsequently, we use the same strategy to counter Quine's meaning variance argument against deviant logics. In a nutshell, we claim that genuine rivalry between (similar) logics ^*L^* and ^*L^* is possible whenever each constant in ^*L^* has the same operational meaning as its counterpart in ^*L^* although differences in global meaning arise in at least one case.     

A Sound and Complete Tableau Calculus for Reasoning about only Knowing and Knowing at Most

We define a tableau calculus for the logic of only knowing and knowing at most ON, which is an extension of Levesque's logic of only knowing O. The method is based on the possible-world semantics of the logic ON, and can be considered as an extension of known tableau calculi for modal logic K45. From the technical viewpoint, the main features of such an extension are the explicit representation of "unreachable" worlds in the tableau, and an additional branch closure condition implementing the property that each world must be either reachable or unreachable. The calculus allows for establishing the computational complexity of reasoning about only knowing and knowing at most. Moreover, we prove that the method matches the worst-case complexity lower bound of the satisfiability problem for both ON and O. With respect to [22], in which the tableau calculus was originally presented, in this paper we both provide a formal proof of soundness and completeness of the calculus, and prove the complexity results for the logic ON.     

Tableau reductions: Towards an optimal decision procedure for the modal necessity

We present a new prefixed tableau system $\mathsf{TK}$ for verification of validity in modal logic $\mathsf{K}$. The system $\mathsf{TK}$ is deterministic, it uniquely generates exactly one proof tree for each clausal representation of formulas, and, moreover, it uses some syntactic reductions of prefixes. $\mathsf{TK}$ is defined in the original methodology of tableau systems, without any external technique such as backtracking, backjumping, etc. Since all the necessary bookkeeping is built into the rules, the system is not only a basis for a validity algorithm, but is itself a decision procedure. We present also a deterministic tableau decision procedure which is an extension of $\mathsf{TK}$ and can be used for the global assumptions problem.     

A Duality for the Algebras of a Łukasiewicz <Emphasis Type="Italic">n</Emphasis> + 1-valued Modal System

In this paper, we develop a duality for the varieties of a Łukasiewicz n + 1-valued modal system. This duality is an extension of Stone duality for modal algebras. Some logical consequences (such as completeness results, correspondence theory...) are then derived and we propose some ideas for future research. Presented by Daniele Mundici     

The Tense Logic for Master Argument in Prior’s Reconstruction

In this paper we examine Prior’s reconstruction of Master Argument [4] in some modal-tense logic. This logic consists of a purely tense part and Diodorean definitions of modal alethic operators. Next we study this tense logic in the pure tense language. It is the logic K _t 4 plus a new axiom (P): ‘p Λ G p ⊃ P G p’. This formula was used by Prior in his original analysis of Master Argument. (P) is usually added as an extra axiom to an axiomatization of the logic of linear time. In that case the set of moments is a total order and must be left-discrete without the least moment. However, the logic of Master Argument does not require linear time. We show what properties of the set of moments are exactly forced by (P) in the reconstruction of Prior. We make also some philosophical remarks on the analyzed reconstruction. Presented by Jacek Malinowski     

Constraints for Input/Output Logics

In a previous paper we developed a general theory of input/output logics. These are operations resembling inference, but where inputs need not be included among outputs, and outputs need not be reusable as inputs. In the present paper we study what happens when they are constrained to render output consistent with input. This is of interest for deontic logic, where it provides a manner of handling contrary-to-duty obligations. Our procedure is to constrain the set of generators of the input/output system, considering only the maximal subsets that do not yield output conflicting with a given input. When inputs are authorised to reappear as outputs, both maxichoice revision in the sense of Alchourrón/Makinson and the default logic of Poole emerge as special cases, and there is a close relation with Reiter default logic. However, our focus is on the general case where inputs need not be outputs. We show in what contexts the consistency of input with output may be reduced to its consistency with a truth-functional combination of components of generators, and under what conditions constrained output may be obtained by a derivation that is constrained at every step.     

A Calculus of Substitutions for DPL

We consider substitutions in order sensitive situations, having in the back of our minds the case of dynamic predicate logic (DPL) with a stack semantics. We start from the semantic intuition that substitutions are move instructions on stacks: the syntactic operation [y/x] is matched by the instruction to move the value of the y-stack to the x-stack. We can describe these actions in the positive fragment of DPLE. Hence this fragment counts as a logic for DPL-substitutions. We give a calculus for the fragment and prove soundness and completeness.