The paper studies the logic TL(NBox+-wC) – logic of discrete linear time with current time point clusters. Its language uses modalities Diamond+ (possible in future) and Diamond- (possible in past) and special temporal operations, – Box+w (weakly necessary in future) and Box-w (weakly necessary in past). We proceed by developing an algorithm recognizing theorems of TL(NBox+-wC), so we prove that TL(NBox+-wC) is decidable. The algorithm is based on reduction of formulas to inference rules and converting the rules in special reduced (...) normal form, and, then, on checking validity of such rules in models of singleexponential size in the rules. Also we consider the admissibility problem for TL(NBox+-wC) and show how to reduce the problem for admissibility to the decidability of TL(NBox+-wC) itself using definable universal modalities. (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)

With each superintuitionistic propositional logic L with a disjunction property we associate a set of modal logics the assertoric fragment of which is L . Each formula of these modal logics is interdeducible with a formula representing a set of rules admissible in L . The smallest of these logics contains only formulas representing derivable in L rules while the greatest one contains formulas corresponding to all admissible in L rules. The algebraic semantic for these logics is described.

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).

Relevant logics infamously have the property that they only validate a conditional when some propositional variable is shared between its antecedent and consequent. This property has been strengthened in a variety of ways over the last half-century. Two of the more famous of these strengthenings are the strong variable sharing property and the depth relevance property. In this paper I demonstrate that an appropriate class of relevant logics has a property that might naturally be characterized as the supremum of these (...) two properties. I also show how to use this fact to demonstrate that these logics seem to be constructive in previously unknown ways. (shrink)

A term td is called a ternary deductive term for a variety of algebras V if the identity td≈r holds in V and ∈θ yields td≈td for any A∈V and any principal congruence θ on A. A connective f is called td-distributive if td)≈ f,…,td). If L is a propositional logic and V is a corresponding variety that has a TD term td, then any admissible in L rule, the premises of which contain only td-distributive operations, is derivable, and the (...) substitution r↦td is a projective L-unifier for any formula containing only td-distributive connectives. The above substitution is a generalization of the substitution introduced by T. Prucnal to prove structural completeness of the implication fragment of intuitionistic propositional logic. (shrink)

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)

Miller, D., G. Nadathur, F. Pfenning and A. Scedrov, Uniform proofs as a foundation for logic programming, Annals of Pure and Applied Logic 51 125–157. A proof-theoretic characterization of logical languages that form suitable bases for Prolog-like programming languages is provided. This characterization is based on the principle that the declarative meaning of a logic program, provided by provability in a logical system, should coincide with its operational meaning, provided by interpreting logical connectives as simple and fixed search instructions. The (...) operational semantics is formalized by the identification of a class of cut-free sequent proofs called uniform proofs. A uniform proof is one that can be found by a goal-directed search that respects the interpretation of the logical connectives as search instructions. The concept of a uniform proof is used to define the notion of an abstract logic programming language, and it is shown that first-order and higher-order Horn clauses with classical provability are examples of such a language. Horn clauses are then generalized to hereditary Harrop formulas and it is shown that first-order and higher-order versions of this new class of formulas are also abstract logic programming languages if the inference rules are those of either intuitionistic or minimal logic. The programming language significance of the various generalizations to first-order Horn clauses is briefly discussed. (shrink)

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)

This paper discusses the relation between the minimal positive relevant logic B and intersection and union type theories. There is a marvelous coincidence between these very differently motivated research areas. First, we show a perfect fit between the Intersection Type Discipline ITD and the tweaking BT of B, which saves implication and conjunction but drops disjunction . The filter models of the -calculus (and its intimate partner Combinatory Logic CL) of the first author and her coauthors then become theory models (...) of these calculi. (The logician's "theory" is the algebraist's "filter".) The coincidence extends to a dual interpretation of key particles—the subtype translates to provable , type intersection to conjunction , function space to implication, and whole domain to the (trivially added but trivial) truth T. This satisfying ointment contains a fly. For it is right, proper, and to be expected that type union should correspond to the logical disjunction of B. But the simulation of functional application by a fusion (or modus ponens product) operation on theories leaves the key Bubbling lemma of work on ITD unprovable for the -prime theories now appropriate for the modeling. The focus of the present paper lies in an appeal to Harrop theories which are (a) prime and (b) closed under fusion. A version of the Bubbling lemma is then proved for Harrop theories, which accordingly furnish a model of and CL. (shrink)

Prawitz proposed certain notions of proof-theoretic validity and conjectured that intuitionistic logic is complete for them [11, 12]. Considering propositional logic, we present a general framework of five abstract conditions which any proof-theoretic semantics should obey. Then we formulate several more specific conditions under which the intuitionistic propositional calculus turns out to be semantically incomplete. Here a crucial role is played by the generalized disjunction principle. Turning to concrete semantics, we show that prominent proposals, including Prawitz’s, satisfy at least one (...) of these conditions, thus rendering IPC semantically incomplete for them. Only for Goldfarb’s [1] proof-theoretic semantics, which deviates from standard approaches, IPC turns out to be complete. Overall, these results show that basic ideas of proof-theoretic semantics for propositional logic are not captured by IPC. (shrink)

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)

In 1973, Dag Prawitz conjectured that the calculus of intuitionistic logic is complete with respect to his notion of validity of arguments. On the background of the recent disproof of this conjecture by Piecha, de Campos Sanz and Schroeder-Heister, we discuss possible strategies of saving Prawitz's intentions. We argue that Prawitz's original semantics, which is based on the principal frame of all atomic systems, should be replaced with a general semantics, which also takes into account restricted frames of atomic systems. (...) We discard the option of not considering extensions of atomic systems, but acknowledge the need to incorporate definitional atomic bases in the semantic framework. It turns out that ideas and results by Westerståhl on the Carnap categoricity of intuitionistic logic can be applied to Prawitz semantics. This implies that Prawitz semantics has a status of its own as a genuine, though incomplete, semantics of intuitionstic logic. An interesting side result is the fact that every formula satisfiable in general semantics is satisfiable in an axioms-only frame (a frame whose atomic systems do not contain proper rules). We draw a parallel between this seemingly paradoxical result and Skolem's paradox in first-order model theory. (shrink)

The paper studies admissibility of multiple-conclusion rules in positive logics. Using modification of a method employed by M. Wajsberg in the proof of the separation theorem, it is shown that the problem of admissibility of multiple-conclusion rules in the positive logics is equivalent to the problem of admissibility in intermediate logics defined by positive additional axioms. Moreover, a multiple-conclusion rule \ follows from a set of multiple-conclusion rules \ over a positive logic \ if and only if \ follows from (...) \ over \. (shrink)

In this paper, we propose a computational interpretation of the generalized Kreisel–Putnam rule, also known as the generalized Harrop rule or simply the Split rule, in the style of BHK semantics. We will achieve this by exploiting the Curry–Howard correspondence between formulas and types. First, we inspect the inferential behavior of the Split rule in the setting of a natural deduction system for intuitionistic propositional logic. This will guide our process of formulating an appropriate program that would capture the corresponding (...) computational content of the typed Split rule. Our investigation can also be reframed as an effort to answer the following question: is the Split rule constructively valid in the sense of BHK semantics? Our answer is positive for the Split rule as well as for its newly proposed general version called the S rule. (shrink)

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.

While specifications and verifications of concurrent systems employ Linear Temporal Logic , it is increasingly likely that logical consequence in image will be used in the description of computations and parallel reasoning. Our paper considers logical consequence in the standard image with temporal operations image and image . The prime result is an algorithm recognizing consecutions admissible in image, so we prove that image is decidable w.r.t. admissible inference rules. As a consequence we obtain algorithms verifying the validity of consecutions (...) in image and solving the satisfiability problem. We start by a simple reduction of logical consecutions of image to equivalent ones in the reduced normal form . Then we apply a semantic technique based on image-Kripke structures with formula definable subsets. This yields necessary and sufficient conditions for a consecution to be not admissible in image. These conditions lead to an algorithm which recognizes consecutions admissible in image by verifying the validity of consecutions in special finite Kripke structures of size square polynomial in reduced normal forms of the consecutions. As a consequence, this also solves the satisfiability problem for image. (shrink)

Conventionalism about logic is the view that logical principles hold in virtue of some linguistic conventions. According to explicit conventionalism, these conventions have to be stipulated explicitly. Explicit conventionalism is subject to a famous criticism by Quine, who accused it of leading to an infinite regress. In response to the criticism, several authors have suggested reconstructing conventionalism as implicit in our linguistic behaviour. In this paper, drawing on a distinction from proof theory between derivable and admissible rules, I argue that (...) implicit conventionalism has not been stated in a sufficiently precise way, as it leaves open what one needs to say about admissible yet underivable rules. Moreover, it turns out that this challenge cannot be easily met, and that any attempt to meet the challenge makes conventionalism much less attractive a thesis. (shrink)

This is a general account of metavaluations and their applications, which can be seen as an alternative to standard model-theoretic methodology. They work best for what are called metacomplete logics, which include the contraction-less relevant logics, with possible additions of Conjunctive Syllogism, & →.A→C, and the irrelevant, A→.B→A, these including the logic MC of meaning containment which is arguably a good entailment logic. Indeed, metavaluations focus on the formula-inductive properties of theorems of entailment form A→B, splintering into two types, M1- (...) and M2-, according to key properties of negated entailment theorems. Metavaluations have an inductive presentation and thus have some of the advantages that model theory does, but they represent proof rather than truth and thus represent proof-theoretic properties, such as the priming property, if ├ A $\vee$ B then ├ A or ├ B, and the negated-entailment properties, not-├ ∼ and ├ ∼ iff ├ A and ├ ∼ B. Topics to be covered are their impact on naive set theory and paradox solution, and also Peano arithmetic and Godel’s First and Second Theorems. Interesting to note here is that the familiar M1- and M2-metacomplete logics can be used to solve the set-theoretic paradoxes and, by inference, the Liar Paradox and key semantic paradoxes. For M1-logics, in particular, the final metavaluation that is used to prove the simple consistency is far simpler than its correspondent in the model-theoretic proof in that it consists of a limit point of a single transfinite sequence rather than that of a transfinite sequence of such limit points, as occurs in the model-theoretic approach. Additionally, it can be shown that Peano Arithmetic is simply consistent, using metavaluations that constitute finitary methods. Both of these results use specific metavaluational properties that have no correspondents in standard model theory and thus it would be highly unlikely that such model theory could prove these results in their final forms. (shrink)

The Visser rules form a basis of admissibility for the intuitionistic propositional calculus. We show how one can characterize the existence of covers in certain models by means of formulae. Through this characterization, we provide a new proof of the admissibility of a weak form of the Visser rules. Finally, we use this observation, coupled with a description of a generalization of the disjunction property, to provide a basis of admissibility for the intermediate logics BD2 and GSc.

Positive logics are $\{ \wedge, \vee, \to \}$-fragments of intermediate logics. It is clear that the positive fragment of $Int$ is not structurally complete. We give a description of all hereditarily structurally complete positive logics, while the question whether there is a structurally complete positive logic which is not hereditarily structurally complete, remains open.

In this paper we study the admissible rules of intermediate logics. We establish some general results on extensions of models and sets of formulas. These general results are then employed to provide a basis for the admissible rules of the Gabbay–de Jongh logics and to show that these logics have finitary unification type.

Propositional logic is understood as a set of theorems defined by a deductive system: a set of axioms and a set of rules. Superintuitionistic logic is a logic extending intuitionistic propositional logic \. A rule is admissible for a logic if any substitution that makes each premise a theorem, makes the conclusion a theorem too. A deductive system \ is structurally complete if any rule admissible for the logic defined by \ is derivable in \. It is known that any (...) logic can be defined by a structurally complete deductive system—its structural completion. The main goal of the paper is to study the following problem: given a superintuitionistic logic L, is the structural completion of L hereditarily structurally complete? It is shown that, on the one hand, there is continuum many of such logics, including \, and many of its standard extensions. On the other hand, there is continuum many superintutitionistic logics structural completion of which is not hereditarily structurally complete. It is observed that the class of hereditarily structurally complete superintuitionistic consequence relations does not have the smallest element and it contains continuum many members lacking the finite model property. The following statement is instrumental in obtaining negative results: if a Lindenbaum algebra of formulas on one variable is finite and has more than 15 elements, then a structural completion of such a logic is not hereditarily structurally complete. (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.

Questions connected with the admissibility of rules of inference and the solvability of the substitution problem for modal and intuitionistic logic are considered in an algebraic framework. The main result is the decidability of the universal theory of the free modal algebra imageω extended in signature by adding constants for free generators. As corollaries we obtain: there exists an algorithm for the recognition of admissibility of rules with parameters in the modal system Grz, the substitution problem for Grz and for (...) the intuitionistic calculus H is decidable, intuitionistic propositional calculus H is decidable with respect to admissibility . A semantical criterion for the admissibility of rules of inference in Grz is given. (shrink)

It is shown that the intuitionistic propositional calculus is sound and complete with respect to Kripke-style models that are not quasi-ordered. These models, called rudimentary Kripke models, differ from the ordinary intuitionistic Kripke models by making fewer assumptions about the underlying frames, but have the same conditions for valuations. However, since accessibility between points in the frames need not be reflexive, we have to assume, besides the usual intuitionistic heredity, the converse of heredity, which says that if a formula holds (...) in all points accessible to a point x, then it holds in x. Among frames of rudimentary Kripke models, particular attention is paid to those that guarantee that the assumption of heredity and converse heredity for propositional variables implies heredity and converse heredity for all propositional formulae. These frames need to be neither reflexive nor transitive. (shrink)

The aim of this paper is to investigate a Curry-Howard interpretation of the intersection and union type inference system for Combinatory Logic. Types are interpreted as formulas of a Hilbert-style logic L, which turns out to be an extension of the intuitionistic logic with respect to provable disjunctive formulas (because of new equivalence relations on formulas), while the implicational-conjunctive fragment of L is still a fragment of intuitionistic logic. Moreover, typable terms are translated in a typed version, so that --typed (...) combinatory logic terms are proved to completely codify the associated logical proofs. (shrink)

In this paper1 we study admissible consecutions in multi-modal logics with the universal modality. We consider extensions of multi-modal logic S4n augmented with the universal modality. Admissible consecutions form the largest class of rules, under which a logic is closed. We propose an approach based on the context effective finite model property. Theorem 7, the main result of the paper, gives sufficient conditions for decidability of admissible consecutions in our logics. This theorem also provides an explicit algorithm for recognizing such (...) consecutions. Some applications to particular logics with the universal modality are given. (shrink)