Sequent Calculi for the Propositional Logic of HYPE

In this paper we discuss sequent calculi for the propositional fragment of the logic of HYPE. The logic of HYPE was recently suggested by Leitgeb (Journal of Philosophical Logic 48:305–405, 2019) as a logic for hyperintensional contexts. On the one hand we introduce a simple $$\mathbf{G1}$$ G 1 -system employing rules of contraposition. On the other hand we present a $$\mathbf{G3}$$ G 3 -system with an admissible rule of contraposition. Both systems are equivalent as well as sound and complete proof-system of HYPE. In order to provide a cut-elimination procedure, we expand the calculus by connections as introduced in Kashima and Shimura (Mathematical Logic Quarterly 40:153–172, 1994).

Sequent Calculi for Orthologic with Strict Implication

In this study, new sequent calculi for a minimal quantum logic (\(\bf MQL\)) are discussed that involve an implication. The sequent calculus \(\bf GO\) for \(\bf MQL\) was established by Nishimura, and it is complete with respect to ortho-models (O-models). As \(\bf GO\) does not contain implications, this study adopts the strict implication and constructs two new sequent calculi \(\mathbf{GOI}_1\) and \(\mathbf{GOI}_2\) as the expansions of \(\bf GO\). Both \(\mathbf{GOI}_1\) and \(\mathbf{GOI}_2\) are complete with respect to the O-models. In this study, the completeness and decidability theorems for these new systems are proven. Furthermore, some details pertaining to new rules and the strict implication are discussed.

Consistent disjunctive sequent calculi and Scott domains

Based on the framework of disjunctive propositional logic, we first provide a syntactic representation for Scott domains. Precisely, we establish a category of consistent disjunctive sequent calculi with consequence relations, and show it is equivalent to that of Scott domains with Scott-continuous functions. Furthermore, we illustrate the approach to solving recursive domain equations by introducing some standard domain constructions, such as lifting and sums. The subsystems relation on consistent finitary disjunctive sequent calculi makes these domain constructions continuous. Solutions to recursive domain equations are given by constructing the least fixed point of a continuous function.

Residuated Algebraic Structures in the Vicinity of Pre-rough Algebra and Decidability

Varieties of topological quasi-Boolean algebras in the vicinity of pre-rough algebras [28, 29] are expanded to residuated algebraic structures by introducing a new implication operation and its residual in these structures. Sequent calculi for some classes of residuated algebraic structures are established. These sequent calculi have the strong finite model property which yields the decidability of the word problem for corresponding classes of algebraic structures.

De Finettian Logics of Indicative Conditionals Part II: Proof Theory and Algebraic Semantics

In Part I of this paper, we identified and compared various schemes for trivalent truth conditions for indicative conditionals, most notably the proposals by de Finetti (1936) and Reichenbach (1935, 1944) on the one hand, and by Cooper (Inquiry, 11, 295–320, 1968) and Cantwell (Notre Dame Journal of Formal Logic, 49, 245–260, 2008) on the other. Here we provide the proof theory for the resulting logics and , using tableau calculi and sequent calculi, and proving soundness and completeness results. Then we turn to the algebraic semantics, where both logics have substantive limitations: allows for algebraic completeness, but not for the construction of a canonical model, while fails the construction of a Lindenbaum-Tarski algebra. With these results in mind, we draw up the balance and sketch future research projects.

Free Logics are Cut-Free

The paper presents a uniform proof-theoretic treatment of several kinds of free logic, including the logics of existence and definedness applied in constructive mathematics and computer science, and called here quasi-free logics. All free and quasi-free logics considered are formalised in the framework of sequent calculus, the latter for the first time. It is shown that in all cases remarkable simplifications of the starting systems are possible due to the special rule dealing with identity and existence predicate. Cut elimination is proved in a constructive way for sequent calculi adequate for all logics under consideration.