We prove that all extensions of Heyting Arithmetic with a logic that has the finite frame property possess the de Jongh property.

The idea of rejection originated by Aristotle. The notion of rejection was introduced into formal logic by Łukasiewicz [20]. He applied it to complete syntactic characterization of deductive systems using an axiomatic method of rejection of propositions [22, 23]. The paper gives not only genesis, but also development and generalization of the notion of rejection. It also emphasizes the methodological approach to biaspectual axiomatic method of characterization of deductive systems as acceptance (asserted) systems and rejection (refutation) systems, introduced by Łukasiewicz (...) and developed by his student Słupecki, the pioneers of the method, which becomes relevant in modern approaches to logic. (shrink)

This volume is the first ever collection devoted to the field of proof-theoretic semantics. Contributions address topics including the systematics of introduction and elimination rules and proofs of normalization, the categorial characterization of deductions, the relation between Heyting's and Gentzen's approaches to meaning, knowability paradoxes, proof-theoretic foundations of set theory, Dummett's justification of logical laws, Kreisel's theory of constructions, paradoxical reasoning, and the defence of model theory. The field of proof-theoretic semantics has existed for almost 50 years, but the term (...) itself was proposed by Schroeder-Heister in the 1980s. Proof-theoretic semantics explains the meaning of linguistic expressions in general and of logical constants in particular in terms of the notion of proof. This volume emerges from presentations at the Second International Conference on Proof-Theoretic Semantics in Tübingen in 2013, where contributing authors were asked to provide a self-contained description and analysis of a significant research question in this area. The contributions are representative of the field and should be of interest to logicians, philosophers, and mathematicians alike. (shrink)

We investigate the initial segments of the Medvedev lattice as Brouwer algebras, and study the propositional logics connected to them.

Metacompleteness is used to prove properties such as the disjunction property and the existence property in the area of relevant logics. On the other hand, the disjunction property of several basic propositional substructural logics over FL has been proved using the cut elimination theorem of sequent calculi and algebraic characterization. The present paper shows that Meyer’s metavaluational technique and Slaney’s metavaluational technique can be applied to basic predicate intuitionistic substructural logics and basic predicate involutive substructural logics, respectively. As a corollary (...) of metacompleteness, the disjunction property, the existence property, and the admissibility of certain rules in such logics can be proved. (shrink)

Visser's rules form a basis for the admissible rules of . Here we show that this result can be generalized to arbitrary intermediate logics: Visser's rules form a basis for the admissible rules of any intermediate logic for which they are admissible. This implies that if Visser's rules are derivable for then has no nonderivable admissible rules. We also provide a necessary and sufficient condition for the admissibility of Visser's rules. We apply these results to some specific intermediate logics and (...) obtain that Visser's rules form a basis for the admissible rules of, for example, De Morgan logic, and that Dummett's logic and the propositional Gödel logics do not have nonderivable admissible rules. (shrink)

The paper considers certain properties of intermediate and moda propositional logics.The first part contains a proof of the theorem stating that each intermediate logic is closed under the Kreisel-Putnam rule xyz/(xy)(xz).

Several proof-theoretic notions of validity have been proposed in the literature, for which completeness of intuitionistic logic has been conjectured. We define validity for intuitionistic propositional logic in a way which is common to many of these notions, emphasizing that an appropriate notion of validity must be closed under substitution. In this definition we consider atomic systems whose rules are not only production rules, but may include rules that allow one to discharge assumptions. Our central result shows that Harrop’s rule (...) is valid under substitution, which refutes the completeness conjecture for intuitionistic logic. (shrink)

LetSKP be the intermediate prepositional logic obtained by adding toI (intuitionistic p.l.) the axiom schemes:S = (( ) ) (Scott), andKP = ()()() (Kreisel-Putnam). Using Kripke's semantics, we prove:1) SKP has the finite model property; 2) SKP has the disjunction property. In the last section of the paper we give some results about Scott's logic S = I+S.

Infinitely many intermediate propositional logics with the disjunction property are defined, each logic being characterized both in terms of a finite axiomatization and in terms of a Kripke semantics with the finite model property. The completeness theorems are used to prove that any two logics are constructively incompatible. As a consequence, one deduces that there are infinitely many maximal intermediate propositional logics with the disjunction property.

In this paper, we give an algebraic completeness theorem for constructive logic with strong negation in terms of finite rough set-based Nelson algebras determined by quasiorders. We show how for a quasiorder R, its rough set-based Nelson algebra can be obtained by applying Sendlewski’s well-known construction. We prove that if the set of all R-closed elements, which may be viewed as the set of completely defined objects, is cofinal, then the rough set-based Nelson algebra determined by the quasiorder R forms (...) an effective lattice, that is, an algebraic model of the logic E 0, which is characterised by a modal operator grasping the notion of “to be classically valid”. We present a necessary and sufficient condition under which a Nelson algebra is isomorphic to a rough set-based effective lattice determined by a quasiorder. (shrink)

If the Visser rules are admissible for an intermediate logic, they form a basis for the admissible rules of the logic. How to characterize the admissible rules of intermediate logics for which not all of the Visser rules are admissible is not known. In this paper we give a brief overview of results on admissible rules in the context of intermediate logics. We apply these results to some well-known intermediate logics. We provide natural examples of logics for which the Visser (...) rule are derivable, admissible but nonderivable, or not admissible. (shrink)

Rybakov proved that the admissible rules of $\mathsf {IPC}$ are decidable. We give a proof of the same theorem, using the same core idea, but couched in the many notions that have been developed in the mean time. In particular, we illustrate how the argument can be interpreted as using refinements of the notions of exactness and extendibility.

Refutation systems are formal systems for inferring the falsity of formulae. These systems can, in particular, be used to syntactically characterise logics. In this paper, we explore the close connection between refutation systems and admissible rules. We develop technical machinery to construct refutation systems, employing techniques from the study of admissible rules. Concretely, we provide a refutation system for the intermediate logics of bounded branching, known as the Gabbay–de Jongh logics. We show that this gives a characterisation of these logics (...) in terms of their admissible rules. To illustrate the technique, we also provide a refutation system for Medvedev’s logic. (shrink)

Complete deductive systems are constructed for the non-valid (refutable) formulae and sequents of some propositional modal logics. Thus, complete syntactic characterizations in the sense of Lukasiewicz are established for these logics and, in particular, purely syntactic decision procedures for them are obtained. The paper also contains some historical remarks and a general discussion on refutation systems.

Attempts to articulate the real meaning or ultimate significance of a famous theorem comprise a major vein of philosophical writing about mathematics. The subfield of mathematical logic has supplie...

There is an ambiguity in the concept of deductive validity that went unnoticed until the middle of the twentieth century. Sometimes an inference rule is called valid because its conclusion is a theorem whenever its premises are. But often something different is meant: The rule's conclusion follows from its premises even in the presence of other assumptions. In many logical environments, these two definitions pick out the same rules. But other environments are context-sensitive, and in these environments the second notion (...) is stronger. Sorting out this ambiguity has led to profound mathematical investigations with applications in complexity theory and computer science. The origins of this ambiguity and the history of its resolution deserve philosophical attention, because our understanding of logic stands to benefit from their details. I am eager to examine together with you, Crito, whether this argument will appear in any way different to me in my present circumstances, or whether it remains the same, whet... (shrink)

I propose a new semantics for intuitionistic logic, which is a cross between the construction-oriented semantics of Brouwer-Heyting-Kolmogorov and the condition-oriented semantics of Kripke. The new semantics shows how there might be a common semantical underpinning for intuitionistic and classical logic and how intuitionistic logic might thereby be tied to a realist conception of the relationship between language and the world.

A proof is given that the set of maximal intermediate propositional logics with the disjunction property and the set of maximal intermediate predicate logics with the disjunction property and the explicit definability property have the power of continuum. To prove our results, we introduce various notions which might be interesting by themselves. In particular, we illustrate a method to generate wide sets of pairwise "constructively incompatible constructive logics". We use a notion of "semiconstructive" logic and define wide sets of "constructive" (...) logics by representing the "constructive" logics as "limits" of decreasing sequences of "semiconstructive" logics. Also, we introduce some generalizations of the usual filtration techniques for propositional logics. For instance, "filtrations over rank formulas" are used to show that any two different logics belonging to a suitable uncountable set of "constructive" logics are "constructively incompatible". (shrink)

This is the first part of a paper concerning intermediate propositional logics with the disjunction property which cannot be properly extended into logics of the same kind, and are therefore called maximal. To deal with these logics, we use a method based on the search of suitable nonstandard logics, which has an heuristic content and has allowed us to discover a wide family of logics, as well as to get their maximality proofs in a uniform way. The present part illustrates (...) infinitely many maximal logics with the disjunction property extending the well-known logic of Scott, and aims to provide a first picture of the method, sufficient for the reader who wish to achieve an overall understanding of it without entering into the further aspects developed in the second part. From this point of view, the latter will not be self-standing, but will be seen as a prosecution and a complement of the former, with the aim that the material presented in the whole paper can be used as a starting point for a classification of the subject. (shrink)

This is the second part of a paper devoted to the study of the maximal intermediate propositional logics with the disjunction property , whose first part has appeared in this journal with the title “A method to single out maximal propositional logics with the disjunction property I”. In the first part we have explained the general results upon which a method to single out maximal constructive logics is based and have illustrated such a method by exhibiting the Kripke semantics of (...) maximal constructive logics extending the logic ST of Scott, for which, in turn, a semantical characterization in terms of Kripke frames has been given. In the present part we complete the illustration of the method of the first part, having in mind some aspects which might be interesting for a classification of the maximal constructive logics, and an application of the heuristic content of the method to detect the nonmaximality of apparently maximal constructive logics. Thus, on the one hand we introduce the logic AST , which is compared with ST and is seen as a logic “alternative” to it, in a sense which will be precisely explained. We provide a Kripke semantics for AST and show that there are maximal constructive logics which neither are extensions of ST nor are extensions of AST. Finally, we give a further application of the results of the first part by exhibiting the Kripke semantics of a maximal constructive logic extending AST. On the other hand, we compare the maximal constructive logics presented in both parts of the paper with a constructive logic introduced by Maksimova , which has been conjectured to be maximal by Chagrov and Zacharyashchev ; from this comparison a disproof of the conjecture arises. (shrink)

In the 80's Pierangelo Miglioli, starting from motivations in the framework of Abstract Data Types and Program Synthesis, introduced semiconstructive theories, a family of large subsystems of classical theories that guarantee the computability of functions and predicates represented by suitable formulas. In general, the above computability results are guaranteed by algorithms based on a recursive enumeration of the theorems of the whole system. In this paper we present a family of semiconstructive systems, we call uniformly semiconstructive, that provide computational procedures (...) only involving formulas with bounded complexity. We present several examples of uniformly semiconstructive systems containing Harrop theories, induction principles and some well-known predicate intermediate principles. Among these, we give an account of semiconstructive and uniformly semiconstructive systems which lie between Intuitionistic and Classical Arithmetic and we discuss their constructive incompatibility. (shrink)

On the Dummettian understanding, anti-realism regarding a particular discourse amounts to (or at the very least, involves) a refusal to accept the determinacy of the subject matter of that discourse and a corresponding refusal to assert at least some instances of excluded middle (which can be understood as expressing this determinacy of subject matter). In short: one is an anti-realist about a discourse if and only if one accepts intuitionistic logic as correct for that discourse. On careful examination, the strongest (...) Dummettian arguments for anti-realism of this sort fail to secure intuitionistic logic as the single, correct logic for anti-realist discourses. Instead, antirealists are placed in a situation where they fail to be justified in asserting monism (that intuitionistic logic is the unique correct logic). Thus, antirealists seem forced either to accept pluralism (i.e. one or more intermediate logic is at least as `correct’ as intuitionistic logic–an option I take to be unattractive from the anti-realist perspective), or they must be anti-realists about the realism/anti-realism debate (and, in particular, must refuse to assert the instance of excluded middle equivalent to logical monism or logical pluralism). (shrink)

The paper is dedicated to the 80th birthday of the outstanding Russian logician A.V. Kuznetsov. It is addressing a history of the ideas and research conducted by him in non-classical and intermediate logics.

In many natural languages, there are clear syntactic and/or intonational differences between declarative sentences, which are primarily used to provide information, and interrogative sentences, which are primarily used to request information. Most logical frameworks restrict their attention to the former. Those that are concerned with both usually assume a logical language that makes a clear syntactic distinction between declaratives and interrogatives, and usually assign different types of semantic values to these two types of sentences. A different approach has been taken (...) in recent work on inquisitive semantics. This approach does not take the basic syntactic distinction between declaratives and interrogatives as its starting point, but rather a new notion of meaning that captures both informative and inquisitive content in an integrated way. The standard way to treat the logical connectives in this approach is to associate them with the basic algebraic operations on these new types of meanings. For instance, conjunction and disjunction are treated as meet and join operators, just as in classical logic. This gives rise to a hybrid system, where sentences can be both informative and inquisitive at the same time, and there is no clearcut division between declaratives and interrogatives. It may seem that these two general approaches in the existing literature are quite incompatible. The main aim of this paper is to show that this is not the case. We develop an inquisitive semantics for a logical language that has a clearcut division between declaratives and interrogatives. We show that this language coincides in expressive power with the hybrid language that is standardly assumed in inquisitive semantics, we establish a sound and complete axiomatization for the associated logic, and we consider a natural enrichment of the system with presuppositional interrogatives. (shrink)

This paper investigates a generalized version of inquisitive semantics. A complete axiomatization of the associated logic is established, the connection with intuitionistic logic and several intermediate logics is explored, and the generalized version of inquisitive semantics is argued to have certain advantages over the system that was originally proposed by Groenendijk (2009) and Mascarenhas (2009).

This paper is a survey of results concerning the disjunction property, Halldén-completeness, and other related properties of intermediate prepositional logics and normal modal logics containing S4.

We extend to the predicate frame a previous characterization of the maximal intermediate propositional constructive logics. This provides a technique to get maximal intermediate predicate constructive logics starting from suitable sets of classically valid predicate formulae we call maximal nonstandard predicate constructive logics. As an example of this technique, we exhibit two maximal intermediate predicate constructive logics, yet leaving open the problem of stating whether the two logics are distinct. Further properties of these logics will be also investigated.

The idea of rejection originated by Aristotle. The notion of rejection was introduced into formal logic by Łukasiewicz [20]. He applied it to complete syntactic characterization of deductive systems using an axiomatic method of rejection of propositions [22, 23]. The paper gives not only genesis, but also development and generalization of the notion of rejection. It also emphasizes the methodological approach to biaspectual axiomatic method of characterization of deductive systems as acceptance (asserted) systems and rejection (refutation) systems, introduced by Łukasiewicz (...) and developed by his student Słupecki, the pioneers of the method, which becomes relevant in modern approaches to logic. (shrink)