The book presents a thoroughly elaborated logical theory of generalized truth-values understood as subsets of some established set of truth values. After elucidating the importance of the very notion of a truth value in logic and philosophy, we examine some possible ways of generalizing this notion. The useful four-valued logic of first-degree entailment by Nuel Belnap and the notion of a bilattice constitute the basis for further generalizations. By doing so we elaborate the idea of a multilattice, and most notably, (...) a trilattice of truth values – a specific algebraic structure with information ordering and two distinct logical orderings, one for truth and another for falsity. Each logical order not only induces its own logical vocabulary, but determines also its own entailment relation. We consider both semantic and syntactic ways of formalizing these relations and construct various logical calculi. (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)

Whether assent ("acceptance") and dissent ("rejection") are thought of as speech acts or as propositional attitudes, the leading idea of rejectivism is that a grasp of the distinction between them is prior to our understanding of negation as a sentence operator, this operator then being explicable as applying to A to yield something assent to which is tantamount to dissent from A. Widely thought to have been refuted by an argument of Frege's, rejectivism has undergone something of a revival in (...) recent years, especially in writings by Huw Price and Timothy Smiley. While agreeing that Frege's argument does not refute the position, we shall air some philosophical qualms about it in Section 5, after a thorough examination of the formal issues in Sections 1-4. This discussion draws on - and seeks to draw attention to - some pertinent work of Kent Bendall in the 1970s. (shrink)

Only propositional logics are at issue here. Such a logic is contra-classical in a superficial sense if it is not a sublogic of classical logic, and in a deeper sense, if there is no way of translating its connectives, the result of which translation gives a sublogic of classical logic. After some motivating examples, we investigate the incidence of contra-classicality (in the deeper sense) in various logical frameworks. In Sections 3 and 4 we will encounter, originally as an example of (...) what (in Section 2) we call a contra-classical modal logic, an unusual logic boasting a connective (" demi-negation" ) whose double application is equivalent to a single application of the negation connective. Pondering the example points the way to a general characterization of contra-classicality (Theorems 3.3 and 4.6). In an Appendix (Section 5), we look at one alternative to classical logic as the target for such translational assimilation, intuitionistic logic, calling logics which resist the assimilation, in this case, contra- intuitionistic. We will show that one such logic is classical logic itself, thereby strengthening a result of Wojcicki's to the effect that the consequence relation of classical logic cannot be faithfully embedded by any connective-by-connective translation into that of intuitionistic logic. (What the "faithfully" means here is that not only is the translation of anything provable in the 'source' logic.. (shrink)

Kripke-style models with two accessibility relations, one intuitionistic and the other modal, are given for analogues of the modal systemK based on Heyting's prepositional logic. It is shown that these two relations can combine with each other in various ways. Soundness and completeness are proved for systems with only the necessity operator, or only the possibility operator, or both. Embeddings in modal systems with several modal operators, based on classical propositional logic, are also considered. This paper lays the ground for (...) an investigation of intuitionistic analogues of systems stronger thanK. A brief survey is given of the existing literature on intuitionistic modal logic. (shrink)

If a certain semantic relation (which we call 'local consequence') is allowed to guide expectations about which rules are derivable from other rules, these expectations will not always be fulfilled, as we illustrate. An alternative semantic criterion (based on a relation we call 'global consequence'), suggested by work of J.W. Garson, turns out to provide a much better - indeed a perfectly accurate - guide to derivability.

This paper, a sequel to Models for normal intuitionistic modal logics by M. Boi and the author, which dealt with intuitionistic analogues of the modal system K, deals similarly with intuitionistic analogues of systems stronger than K, and, in particular, analogues of S4 and S5. For these prepositional logics Kripke-style models with two accessibility relations, one intuitionistic and the other modal, are given, and soundness and completeness are proved with respect to these models. It is shown how the holding of (...) formulae characteristic for particular logics is equivalent to conditions for the relations of the models. Modalities in these logics are also investigated. (shrink)

By means of models in toposes of C-sets (where C is a small category), necessary conditions are found for the minimum quantified extension of a propositional (intermediate, modal) logic to be complete with respect to Kripke semantics; in particular, many well-known systems turn out to be incomplete.

This paper considers the question: what becomes of the notion of a logic as a way of codifying valid arguments when the customary assumption is dropped that the premisses and conclusions of these arguments are statements from some single language? An elegant treatment of the notion of a logic, when this assumption is in force, is that provided by Dana Scott's theory of consequence relations; this treatment is appropriately generalized in the present paper to the case where we do not (...) make this assumption of linguistic homogeneity. Several applications of the resulting concept of a heterogeneous logic are suggested, but the main emphasis is on the formal development. One topic touched on is a certain contrast between the boolean and the intensional sentence-connectives in this more general setting. (shrink)

We define a propositionally quantified intuitionistic logic Hπ + by a natural extension of Kripke's semantics for propositional intutionistic logic. We then show that Hπ+ is recursively isomorphic to full second order classical logic. Hπ+ is the intuitionistic analogue of the modal systems S5π +, S4π +, S4.2π +, K4π +, Tπ +, Kπ + and Bπ +, studied by Fine.

Versions and extensions of intuitionistic and modal logic involving biHeyting and bimodal operators, the axiom of constant domains and Barcan's formula, are formulated as structured categories. Representation theorems for the resulting concepts are proved. Essentially stronger versions, requiring new methods of proof, of known completeness theorems are consequences. A new type of completeness result, with a topos theoretic character, is given for theories satisfying a condition considered by Lawvere . The completeness theorems are used to conclude results asserting that certain (...) logics are conservatively interpretable in others. (shrink)

We study logic translations from an abstract perspective, without any commitment to the structure of sentences and the nature of logical entailment, which also means that we cover both proof- theoretic and model-theoretic entailment. We show how logic translations induce notions of logical expressiveness, consistency strength and sublogic, leading to an explanation of paradoxes that have been described in the literature. Connectives and quantifiers, although not present in the definition of logic and logic translation, can be recovered by their abstract (...) properties and are preserved and reflected by translations under suitable conditions. (shrink)

Various natural deduction formulations of classical, minimal, intuitionist, and intermediate propositional and first-order logics are presented and investigated with respect to satisfaction of the separation and subformula properties. The technique employed is, for the most part, semantic, based on general versions of the Lindenbaum and Lindenbaum–Henkin constructions. Careful attention is paid to which properties of theories result in the presence of which rules of inference, and to restrictions on the sets of formulas to which the rules may be employed, restrictions (...) determined by the formulas occurring as premises and conclusion of the invalid inference for which a counterexample is to be constructed. We obtain an elegant formulation of classical propositional logic with the subformula property and a singularly inelegant formulation of classical first-order logic with the subformula property, the latter, unfortunately, not a product of the strategy otherwise used throughout the article. Along the way, we arrive at an optimal strengthening of the subformula results for classical first-order logic obtained as consequences of normalization theorems by Dag Prawitz and Gunnar Stålmarck. (shrink)

Jean-Yves Béziau (‘Classical Negation can be Expressed by One of its Halves’, Logic Journal of the IGPL 7 (1999), 145–151) has given an especially clear example of a phenomenon he considers a sufficiently puzzling to call the ‘paradox of translation’: the existence of pairs of logics, one logic being strictly weaker than another and yet such that the stronger logic can be embedded within it under a faithful translation. We elaborate on Béziau’s example, which concerns classical negation, as well as (...) giving some additional background (especially from intuitionistic logic) to the example. Our interest is more on the logical exploration of the phenomenon Béziau’s case exemplifies than on the question of whether that phenomenon is (even prima facie ) paradoxical, though in Section 5 we do approach the latter question – somewhat obliquely – by considering an analogous phenomenon which it is hard to find puzzling. (shrink)

We prove that the positive fragment of first-order intuitionistic logic in the language with two individual variables and a single monadic predicate letter, without functional symbols, constants, and equality, is undecidable. This holds true regardless of whether we consider semantics with expanding or constant domains. We then generalise this result to intervals \ and \, where QKC is the logic of the weak law of the excluded middle and QBL and QFL are first-order counterparts of Visser’s basic and formal logics, (...) respectively. We also show that, for most “natural” first-order modal logics, the two-variable fragment with a single monadic predicate letter, without functional symbols, constants, and equality, is undecidable, regardless of whether we consider semantics with expanding or constant domains. These include all sublogics of QKTB, QGL, and QGrz—among them, QK, QT, QKB, QD, QK4, and QS4. (shrink)

Recent studies in semantics of modal and superintuitionistic predicate logics provided many examples of incompleteness, especially for Kripke semantics. So there is a problem: to find an appropriate possible- world semantics which is equivalent to Kripke semantics at the propositional level and which is strong enough to prove general completeness results. The present paper introduces a new semantics of Kripke metaframes' generalizing some earlier notions. The main innovation is in considering "n"-tuples of individuals as abstract "n"-dimensional vectors', together with some (...) transformations of these vectors. Soundness of the semantics is proved to be equivalent to some non- logical properties of metaframes; and thus we describe the maximal semantics of Kripke- type. (shrink)

Modern belief revision theory is based to a large extent on partial meet contraction that was introduced in the seminal article by Carlos Alchourrón, Peter Gärdenfors, and David Makinson that appeared in 1985. In the same year, Alchourrón and Makinson published a significantly different approach to the same problem, called safe contraction. Since then, safe contraction has received much less attention than partial meet contraction. The present paper summarizes the current state of knowledge on safe contraction, provides some new results (...) and offers a list of unsolved problems that are in need of investigation. (shrink)

Algebraic approach to study of classical and non-classical logical calculi was developed and systematically presented by Helena Rasiowa in [48], [47]. It is very fruitful in investigation of non-classical logics because it makes possible to study large families of logics in an uniform way. In such research one can replace logics with suitable classes of algebras and apply powerful machinery of universal algebra. In this paper we present an overview of results on interpolation and definability in modal and positive logics,and (...) also in extensions of Johansson's minimal logic. All these logics are strongly complete under algebraic semantics. It allows to combine syntactic methods with studying varieties of algebras and to flnd algebraic equivalents for interpolation and related properties. Moreover, we give exhaustive solution to interpolation and some related problems for many families of propositional logics and calculi. (shrink)

Inquisitive first order logic is an extension of first order classical logic, introducing questions and studying the logical relations between questions and quantifiers. It is not known whether is recursively axiomatizable, even though an axiomatization has been found for fragments of the logic. In this paper we define the \—classical antecedent—fragment, together with an axiomatization and a proof of its strong completeness. This result extends the ones presented in the literature and introduces a new approach to study the axiomatization problem (...) for fragments of the logic. (shrink)

We prove that the two-variable fragment of first-order intuitionistic logic is undecidable, even without constants and equality. We also show that the two-variable fragment of a quantified modal logic L with expanding first-order domains is undecidable whenever there is a Kripke frame for L with a point having infinitely many successors (such are, in particular, the first-order extensions of practically all standard modal logics like K, K4, GL, S4, S5, K4.1, S4.2, GL.3, etc.). For many quantified modal logics, including those (...) in the standard nomenclature above, even the monadic two-variable fragments turn out to be undecidable. (shrink)

In the paper we consider complexity of intuitionistic propositional logic and its natural fragments such as implicative fragment, finite-variable fragments, and some others. Most facts we mention here are known and obtained by logicians from different countries and in different time since 1920s; we present these results together to see the whole picture.

In this paper we treat metasequents—objects which stand to sequents as sequents stand to formulas—as first class logical citizens. To this end we provide a metasequent calculus, a sequent calculus which allows us to directly manipulate metasequents. We show that the various metasequent calculi we consider are sound and complete w.r.t. appropriate classes of tetravaluations where validity is understood locally. Finally we use our metasequent calculus to give direct syntactic proofs of various collapse results, closing a problem left open in (...) French (Ergo, 3(5), 113–131 2016). (shrink)

In this paper we treat metasequents—objects which stand to sequents as sequents stand to formulas—as first class logical citizens. To this end we provide a metasequent calculus, a sequent calculus which allows us to directly manipulate metasequents. We show that the various metasequent calculi we consider are sound and complete w.r.t. appropriate classes of tetravaluations where validity is understood locally. Finally we use our metasequent calculus to give direct syntactic proofs of various collapse results, closing a problem left open in (...) French (Ergo, 3(5), 113–131 2016). (shrink)

Under some assumptions on an equational theory S , we give a necessary and sufficient condition so that S admits a model completion. These assumptions are often met by the equational theories arising from logic. They say that the dual of the category of finitely presented S-algebras has some categorical stucture. The results of this paper combined with those of [7] show that all the 8 theories of amalgamable varieties of Heyting algebras [12] admit a model completion. Further applications to (...) varieties of modal algebras are given in [8]. (shrink)

The logic CD is an intermediate logic which exactly corresponds to the Kripke models with constant domains. It is known that the logic CD has a Gentzen-type formulation called LD and rules are replaced by the corresponding intuitionistic rules) and that the cut-elimination theorem does not hold for LD. In this paper we present a modification of LD and prove the cut-elimination theorem for it. Moreover we prove a “weak” version of cut-elimination theorem for LD, saying that all “cuts” except (...) some special forms can be eliminated from a proof in LD. From these cut-elimination theorems we obtain some corollaries on syntactical properties of CD: fragments collapsing into intuitionistic logic. Harrop disjunction and existence properties, and a fact on the number of logical symbols in the axiom of CD. (shrink)

In [Ono 1987] H. Ono put the question about axiomatizing the intermediate predicate logicLFin characterized by the class of all finite Kripke frames. It was established in [ Skvortsov 1988] thatLFin is not recursively axiomatizable. One can easily show that for any finite posetM, the predicate logic characterized byM is recursively axiomatizable, and its axiomatization can be constructed effectively fromM. Namely, the set of formulas belonging to this logic is recursively enumerable, since it is embeddable in the two-sorted classical predicate (...) calculusCPC 2. Thus the logicLFin is II 2 0 -arithmetical.Here we give a more explicit II 2 0 -description ofLFin: it is presented as the intersection of a denumerable sequence of finitely axiomatizable Kripke-complete logics. Namely, we give an axiomatization of the logicLB n P m + characterized by the class of all posets of the finite height m and the finite branching n. A finite axiomatization of the predicate logicLP m + characterized by the class of all posets of the height m is known from [Yokota 1989]. We prove thatLB n P m + =,B n being the propositional axiom of the branching n. (shrink)

Intervals in boolean algebras enter into the study of conditional assertions (or events) in two ways: directly, either from intuitive arguments or from Goodman, Nguyen and Walker's representation theorem, as suitable mathematical entities to bear conditional probabilities, or indirectly, via a representation theorem for the family of algebras associated with de Finetti's three-valued logic of conditional assertions/events. Further representation theorems forge a connection with rough sets. The representation theorems and an equivalent of the boolean prime ideal theorem yield an algebraic (...) completeness theorem for the three-valued logic. This in turn leads to a Henkin-style completeness theorem. Adequacy with respect to a family of Kripke models for de Finetti's logic, Łukasiewicz's three-valued logic and Priest's Logic of Paradox is demonstrated. The extension to first-order yields a short proof of adequacy for Körner's logic of inexact predicates. (shrink)

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.

Fine and Kripke extended S5, S4, S4.2 and such to produce propositionally quantified systems , , : given a Kripke frame, the quantifiers range over all the sets of possible worlds. is decidable and, as Fine and Kripke showed, many of the other systems are recursively isomorphic to second-order logic. In the present paper I consider the propositionally quantified system that arises from the topological semantics for S4, rather than from the Kripke semantics. The topological system, which I dub , (...) is strictly weaker than its Kripkean counterpart. I prove here that second-order arithmetic can be recursively embedded in . In the course of the investigation, I also sketch a proof of Fine's and Kripke's results that the Kripkean system is recursively isomorphic to second-order logic. (shrink)

Quantified propositional intuitionistic logic is obtained from propositional intuitionistic logic by adding quantifiers ∀p, ∃p, where the propositional variables range over upward-closed subsets of the set of worlds in a Kripke structure. If the permitted accessibility relations are arbitrary partial orders, the resulting logic is known to be recursively isomorphic to full second-order logic (Kremer, 1997). It is shown that if the Kripke structures are restricted to trees of at height and width at most ω, the resulting logics are decidable. (...) This provides a partial answer to a question by Kremer. The result also transfers to modal S4 and some Gödel-Dummett logics with quantifiers over propositions. (shrink)

In Section 2 I give a criterion of decidability that can be applied to logics (i.e. Tarski consequence operators) without the finite model property. In Section 3 I study ukasiewicz-style refutation procedures as a method of obtaining decidability results.This method also proves to be more general than Harrop's criterion.

Some properties of Kripke-sheaf semantics for super-intuitionistic predicate logics are shown. The concept ofp-morphisms between Kripke sheaves is introduced. It is shown that if there exists ap-morphism from a Kripke sheaf 1 into 2 then the logic characterized by 1 is contained in the logic characterized by 2. Examples of Kripke-sheaf complete and finitely axiomatizable super-intuitionistic (and intermediate) predicate logics each of which is Kripke-frame incomplete are given. A correction to the author's previous paper Kripke bundles for intermediate predicate logics (...) and Kripke frames for intuitionistic modal logics (Studia Logica, 49(1990), pp. 289–306 ) is stated. (shrink)

The notion of that information is relative to a context is important in many different ways. The idea that the context is small — that is, not necessarily a consistent and complete possible world — plays a role not only in situation theory, but it is also an enlightening perspective from which to view other areas, such as modal logics, relevant logics, categorial grammar and much more. In this article we will consider these areas, and focus then on one further (...) question: How can we account for information about one thing giving us information about something else? This is a question addressed by channel theory. We will look at channel theory and then see how the issues of information flow and conditionality play a role in each of the different domains we have examined. (shrink)

The logic of the weak law of excluded middleKC p is obtained by adding the formula A A as an axiom scheme to Heyting's intuitionistic logicH p . A cut-free sequent calculus for this logic is given. As the consequences of the cut-elimination theorem, we get the decidability of the propositional part of this calculus, its separability, equality of the negationless fragments ofKC p andH p , interpolation theorems and so on. From the proof-theoretical point of view, the formulation presented (...) in this paper makes clearer the relations betweenKC p ,H p , and the classical logic. In the end, an interpretation of classical propositional logic in the propositional part ofKC p is given. (shrink)

Propositional logics in general, considered as a set of sentences, can be undecidable even if they have “nice” representations, e.g., are given by a calculus. Even decidable propositional logics can be computationally complex (e.g., already intuitionistic logic is PSPACE-complete). On the other hand, finite-valued logics are computationally relatively simple—at worst NP. Moreover, finite-valued semantics are simple, and general methods for theorem proving exist. This raises the question to what extent and under what circumstances propositional logics represented in various ways can (...) be approximated by finite-valued logics. It is shown that the minimal m-valued logic for which a given calculus is strongly sound can be calculated. It is also investigated under which conditions propositional logics can be characterized as the intersection of (effectively given) sequences of finite-valued logics. (shrink)

After some generalities about connections between functions and relations in Sections 1 and 2 recalls the possibility of taking the semantic values of ‐ary Boolean connectives as ‐ary relations among truth‐values rather than as ‐ary truth functions. Section 3, the bulk of the paper, looks at correlates of these truth‐value relations as applied to formulas, and explores in a preliminary way how their properties are related to the properties of “logical relations” among formulas such as equivalence, implication (entailment) and contrariety (...) (logical incompatibility), concentrating for illustrative purposes on binary logical relations such as those just listed. To avoid an excess of footnotes, some points have been deferred to an Appendix as “Longer Notes”. (shrink)

We illustrate, with three examples, the interaction between boolean and modal connectives by looking at the role of truth-functional reasoning in the provision of completeness proofs for normal modal logics. The first example (§ 1) is of a logic (more accurately: range of logics) which is incomplete in the sense of being determined by no class of Kripke frames, where the incompleteness is entirely due to the lack of boolean negation amongst the underlying non-modal connectives. The second example (§ 2) (...) focusses on the breakdown, in the absence of boolean disjunction, of the usual canonical model argument for the logic of dense Kripke frames, though a proof of incompleteness with respect to the Kripke semantics is not offered. An alternative semantic account is developed, in terms of which a completeness proof can be given, and this is used (§ 3) in the discussion of the third example, a bimodal logic which is, as with the first example, provably incomplete in terms of the Kripke semantics, the incompleteness being due to the lack of disjunction (as a primitive or defined boolean connective). (shrink)

The language of the propositional calculus is extended by two families of propositional probability operators, inductively applicable to the formulae, and the set of all formulae provable in an arbitrary superintuitionistic propositional logic is extended by the probability measure axioms concerning those probability operators. A logical system obtained in such a way, similar to a kind of polymodal logic, makes possible to express a probability measure of truthfulness of any formula. The paper contains a description of the Kripke-type possible worlds (...) semantics covering the considered logical systems, being followed by the corresponding completeness results. (shrink)

Section 1 recalls a point noted by A. N. Prior forty years ago: that a certain formula in the language of a purely implicational intermediate logic investigated by R. A. Bull is unprovable in that logic but provable in the extension of the logic by the usual axioms for conjunction, once this connective is added to the language. Section 2 reminds us that every formula is interdeducible with (i.e. added to intuitionistic logic, yields the same intermediate logic as) some conjunction-free (...) formula. Thus it would seem that any detour going via formulas with conjunction can be avoided, which raises a puzzle: how is this consistent with the point from Section 1? Sections 3 and 4 raise and discuss this puzzle. In fact, the puzzle turns out on closer inspection not to be so puzzling after all, but it does serve as a convenient centrepiece around which to organize a discussion of the phenomenon illustrated by the Bull–Prior example. Section 5 notes that Prior's observation can be extended to the case of the result of adding disjunction to Bull's logic, while Section 6 includes some further remarks aimed at diagnosing one source of possible residual puzzlement. A subtext of our discussion—spanning several of the notes—is that this work by Bull and Prior has been overlooked, their results having to be rediscovered, by many algebraists and logicians in more recent years. (shrink)

In his 1964 note, ‘Two Additions to Positive Implication’, A. N. Prior showed that standard axioms governing conjunction yield a nonconservative extension of the pure implicational intermediate logic OIC of R. A. Bull. Here, after reviewing the situation with the aid of an adapted form of the Kripke semantics for intuitionistic and intermediate logics, we proceed to illuminate this example by transposing it to the setting of modal logic, and then relate it to the propositional logic of what have been (...) called ‘Hilbert algebras with infimum’. (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.

This discussion explores the possibility of distinguishing a tighter notion of contrariety evident in the Square of Opposition, especially in its modal incarnations, than as that binary relation holding statements that cannot both be true, with or without the added rider ‘though can both be false’. More than one theorist has voiced the intuition that the paradigmatic contraries of the traditional Square are related in some such tighter way—involving the specific role played by negation in contrasting them—that distinguishes them from (...) other pairs of incompatible statements constructed from the same conceptual materials. Prominent among examples, these other nonstandard pairs are the ‘new contraries’ presented by Robert Blanché’s hexagon(s) of opposition. With special, though not exclusive, attention to these cases, we investigate whether contrariety in the distinguished sense can be captured by adding to the incompatibility condition the further demand that the pair of statements concerned can be represented as the results of applying some sentence operator to the content in its scope, for one of the pair, and, for the other, the application of that same operator to the negation of that content. For one of the two cases, a Blanché case, of nonstandard contrariety singled out for attention, the question of whether such a representation is available is settled at the end of Section 4, and then in a more satisfying way in Section 5, though for the other case, noticed by Peter Simons, the question remains open, after some tentative discussion in one subsection, 6.2, of an Appendix (Section 6). (shrink)

Defines and examines a notion of logical friendliness, a broadening of the familiar notion of classical consequence. Also reviews familiar notions and operations with which friendliness makes contact, providing a new light in which they may be seen.

In distinction from the well-known double-negation embeddings of the classical logic we consider some variants of single-negation embeddings and describe some classes of superintuitionistic first-order predicate logics in which the classical first-order calculus is interpretable in such a way. Also we find the minimal extensions of Heyting's logic in which the classical predicate logic can be embedded by means of these translations.