Abstract Artemov (2019, The provability of consistency) offered the notion of constructive truth and falsity of arithmetical sentences in the spirit of Brouwer–Heyting–Kolmogorov semantics and its formalization, the logic of proofs. In this paper, we provide a complete description of constructive truth and falsity for Friedman’s constant fragment of Peano arithmetic. For this purpose, we generalize the constructive falsity to $n$-constructive falsity in Peano arithmetic where $n$ is any positive natural number. Based on this generalization, we also analyse the logical status of well-known Gödelean sentences: consistency assertions for extensions of PA, the local reflection principles, the ‘constructive’ liar sentences and Rosser sentences. Finally, we discuss ‘extremely’ independent sentences in the sense that they are classically true but neither constructively true nor $n$-constructively false for any $n$.

Abstract In this paper, we introduce a new logic that we call ‘resource sharing linear logic (RSLL)’. In linear logic (LL), formulas without modality express some resource-conscious situation (a formula can be used only once); formulas with modality express a situation with unlimited resources. We introduce the logic RSLL in which we have a strengthened modality (S5-modality) that can be understood as expressing not only unlimited resources but also resources shared by different agents. Observing that merely strengthening the modality allows weakening axiom to be derivable in a Hilbert-style formulation of this logic, we reformulate RSLL as a logic similar to affine logic by a hypersequent calculus that has weakening as a primitive rule. We prove the completeness of the hypersequent calculus with respect to phase semantics and the cut-elimination theorem for the system by a syntactical method. We also prove the decidability of RSLL via a computational interpretation of RSLL, which is a parallel version of Kopylov’s computational model for LL. We then introduce an explicit counterpart of RSLL in the style of Artemov’s justication logic (JRSLL). We prove a realization theorem for RSLL via its explicit counterpart.

Abstract It is well known that the modal logic S5 can be embedded in the classical predicate logic by interpreting the modal operator in terms of a quantifier. Wajsberg [10] proved this fact in a syntactic way. Mints [7] extended this result to the quantified version of S5; using a purely proof-theoretic method he showed that the quantified S5 corresponds to the classical predicate logic with one-sorted variable. In this paper we extend Mints' result to the basic modal logic S4; we investigate the correspondence between the quantified versions of S4 (with and without the Barcan formula) and the classical predicate logic (with one-sorted variable). We present a purely proof-theoretic proof-transformation method, reducing an LK-proof of an interpreted formula to a modal proof.