This paper is a step toward showing what is achievable using non-classical metatheory—particularly, a substructural paraconsistent framework. What standard results, or analogues thereof, from the classical metatheory of first order logic can be obtained? We reconstruct some of the originals proofs for Completeness, Löwenheim-Skolem and Compactness theorems in the context of a substructural logic with the naive comprehension schema. The main result is that paraconsistent metatheory can ‘re-capture’ versions of standard theorems, given suitable restrictions and background assumptions; but the shift (...) to non-classical logic may recast the meanings of these apparently ‘absolute’ theorems. (shrink)

The work is concerned with the so called display property of display logic. The motivation behind it is discussed and challenged. It is shown using one display calculus for intuitionistic logic as an example that the display property can be abandoned without losing subformula, cut elimination and completeness properties in such a way that results in additional expressive power of the system. This is done by disentangling structural connectives so that they are no longer context-sensitive. A recipe for characterizing structural (...) extensions of display calculi is provided. (shrink)

Proof-theoretic semantics is an alternative to model-theoretic semantics. It aims at explaining the meaning of the logical constants in terms of the inference rules that govern their behaviour in proofs. We argue that this must be construed as the task of explaining these meanings relative to a logic, i.e., to a consequence relation. Alas, there is no agreed set of properties that a relation must have in order to qualify as a consequence relation. Moreover, the association of a consequence relation (...) to a logical calculus is not as straightforward as it may seem. We show that these facts are problematic for the proof-theoretic project but the problems can be solved. Our thesis is that the consequence relation relevant for proof-theoretic semantics is the one given by the sequent-to-sequent derivability relation in Gentzen systems. (shrink)

Arguments, the story goes, have one or more premises and only one conclusion. A contentious generalisation allows arguments with several disjunctively connected conclusions. Contentious as this generalisation may be, I will argue nevertheless that it is justified. My main claim is that multiple conclusions are epiphenomena of the logical connectives: some connectives determine, in a certain sense, multiple-conclusion derivations. Therefore, such derivations are completely natural and can safely be used in proof-theoretic semantics.

Proof-theoretic semantics is an alternative to model-theoretic semantics. It aims at explaining the meaning of the logical constants in terms of the inference rules that govern their behaviour in proofs. We argue that this must be construed as the task of explaining these meanings relative to a logic, i.e., to a consequence relation. Alas, there is no agreed set of properties that a relation must have in order to qualify as a consequence relation. Moreover, the association of a consequence relation (...) to a logical calculus is not as straightforward as it may seem. We show that these facts are problematic for the proof-theoretic project but the problems can be solved. Our thesis is that the consequence relation relevant for proof-theoretic semantics is the one given by the sequent-to-sequent derivability relation in Gentzen systems. (shrink)

One of the most fruitful applications of substructural logics stems from their capacity to deal with self-referential paradoxes, especially truth-theoretic paradoxes. Both the structural rules of contraction and the rule of cut play a crucial role in typical paradoxical arguments. In this paper I address a number of difficulties affecting noncontractive approaches to paradox that have been discussed in the recent literature. The situation was roughly this: if you decide to go substructural, the nontransitive approach to truth offers a lot (...) of benefits that are not available in the noncontractive account. I sketch a noncontractive theory of truth that has these benefits. In particular, it has both a proof- and a model-theoretic presentation, it can be extended to a first-order language, and it retains every classically valid inference. (shrink)

Standard reasoning about Kripke semantics for modal logic is almost always based on a background framework of classical logic. Can proofs for familiar definability theorems be carried out using a nonclassical substructural logic as the metatheory? This article presents a semantics for positive substructural modal logic and studies the connection between frame conditions and formulas, via definability theorems. The novelty is that all the proofs are carried out with a noncontractive logic in the background. This sheds light on which modal (...) principles are invariant under changes of metalogic, and provides evidence for the general viability of nonclassical mathematics. (shrink)