This chapter focuses on alternative logics. It discusses a hierarchy of logical reform. It presents case studies that illustrate particular aspects of the logical revisionism discussed in the chapter. The first case study is of intuitionistic logic. The second case study turns to quantum logic, a system proposed on empirical grounds as a resolution of the antinomies of quantum mechanics. The third case study is concerned with systems of relevance logic, which have been the subject of an especially detailed reform (...) program. Finally, the fourth case study is paraconsistent logic, perhaps the most controversial of serious proposals. (shrink)

A simple method is provided for translating proofs in Grentzen's LK into proofs in Gentzen's LJ with the Peirce rule adjoined. A consequence is a simpler cut elimination operator for LJ + Peirce that is primitive recursive.

A minimal theorem in a logic L is an L-theorem which is not a non-trivial substitution instance of another L-theorem. Komori (1987) raised the question whether every minimal implicational theorem in intuitionistic logic has a unique normal proof in the natural deduction system NJ. The answer has been known to be partially positive and generally negative. It is shown here that a minimal implicational theorem A in intuitionistic logic has a unique -normal proof in NJ whenever A is provable without (...) non-prime contraction. The non-prime contraction rule in NJ is the implication introduction rule whose cancelled assumption differs from a propositional variable and appears more than once in the proof. Our result improves the known partial positive solutions to Komori's problem. Also, we present another simple example of a minimal implicational theorem in intuitionistic logic which does not have a unique -normal proof in NJ. (shrink)

Basic Predicate Logic, BQC, is a proper subsystem of Intuitionistic Predicate Logic, IQC. For every formula in the language {, , , , , , }, we associate two sequences of formulas 0,1,... and 0,1,... in the same language. We prove that for every sequent , there are natural numbers m, n, such that IQC , iff BQC n m. Some applications of this translation are mentioned.

We investigate two large families of logics, differing from each other by the treatment of negation. The logics in one of them are obtained from the positive fragment of classical logic (with or without a propositional constant ff for “the false”) by adding various standard Gentzen-type rules for negation. The logics in the other family are similarly obtained from LJ+, the positive fragment of intuitionistic logic (again, with or without ff). For all the systems, we provide simple semantics which is (...) based on non-deterministic four-valued or three-valued structures, and prove soundness and completeness for all of them. We show that the role of each rule is to reduce the degree of non-determinism in the corresponding systems. We also show that all the systems considered are decidable, and our semantics can be used for the corresponding decision procedures. Most of the extensions of LJ+ (with or without ff) are shown to be conservative over the underlying logic, and it is determined which of them are not. (shrink)

Using recent results in topos theory, two systems of higher-order logic are shown to be complete with respect to sheaf models over topological spaces- so -called "topological semantics." The first is classical higher-order logic, with relational quantification of finitely high type; the second system is a predicative fragment thereof with quantification over functions between types, but not over arbitrary relations. The second theorem applies to intuitionistic as well as classical logic.

tic sequenzen-kalkul of Gentzen, into rules for PCc, the classical sequenzenkalkul. We shall limit ourselves here to sequenzen or turnstile statements of the form A„A„..., A„ I- B, where A„A„..., A„(n ~ 0), and B are wffs consisting of propositional variables, zero or more of the connectives '5', "v', ' ', ')', and '=', and zero or more parentheses. One can pass from PCi to PCc by amending the intelim rules for ' a result of long standing, or by amending (...) the intelim rules for either one of.. (shrink)

Issues about information spring up wherever one scratches the surface of logic. Here is a case that raises delicate issues of 'factual' versus 'procedural' information, or 'statics' versus 'dynamics'. What does intuitionistic logic, perhaps the earliest source of informational and procedural thinking in contemporary logic, really tell us about information? How does its view relate to its 'cousin' epistemic logic? We discuss connections between intuitionistic models and recent protocol models for dynamic-epistemic logic, as well as more general issues that emerge.

In this paper we consider an intuitionistic variant of the modal logic S4 (which we call IS4). The novelty of this paper is that we place particular importance on the natural deduction formulation of IS4— our formulation has several important metatheoretic properties. In addition, we study models of IS4— not in the framework of Kirpke semantics, but in the more general framework of category theory. This allows not only a more abstract definition of a whole class of models but also (...) a means of modelling proofs as well as provability. (shrink)

It is shown that axiomatic extensions of intuitionistic propositional calculus defining univocally new connectives, including those proposed by Gabbay, are strongly complete with respect to valuations in Heyting algebras with additional operations. In all cases, the double negation of such a connective is equivalent to a formula of intuitionistic calculus. Thus, under the excluded third law it collapses to a classical formula, showing that this condition in Gabbay's definition is redundant. Moreover, such connectives can not be interpreted in all Heyting (...) algebras, unless they are already equivalent to a formula of intuitionistic calculus. These facts relativize to connectives over intermediate logics. In particular, the intermediate logic with values in the chain of length n may be "completed" conservatively by adding a single unary connective, so that the expanded system does not allow further axiomatic extensions by new connectives. (shrink)

A game for testing the equivalence of Kripke models with respect to finitary and infinitary intuitionistic predicate logic is introduced and applied to discuss a concept of categoricity for intuitionistic theories.

Beth models of analysis are used in model theoretic proofs of the disjunction and (numerical) existence property. By glueing strings of models one obtains a model that combines the properties of the given models. The method asks for a common generalization of Kripke and Beth models. The proof is carried out in intuitionistic analysis plus Markov's Principle. The main new feature is the external use of intuitionistic principles to prove their own preservation under glueing.

Illative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants (and corresponding axioms and rules) intended to capture inference. In a preceding paper, [2], we considered 4 systems of illative combinatory logic that are sound for first order intuitionistic propositional and predicate logic. The interpretation from ordinary logic into the illative systems can be done in two ways: following the propositions-as-types paradigm, in which derivations become combinators, or in a more direct way, in which (...) derivations are not translated. Both translations are closely related in a canonical way. In the cited paper we proved completeness of the two direct translations. In the present paper we prove that also the two indirect translations are complete. These proofs are direct whereas in another version, [3], we proved completeness by showing that the two corresponding illative systems are conservative over the two systems for the direct translations. Moreover we shall prove that one of the systems is also complete for predicate calculus with higher type functions. (shrink)

This paper contains five observations concerning the intended meaning of the intuitionistic logical constants: (1) if the explanations of this meaning are to be based on a non-decidable concept, that concept should not be that of `proof"; (2) Kreisel"s explanations using extra clauses can be significantly simplified; (3) the impredicativity of the definition of can be easily and safely ameliorated; (4) the definition of in terms of `proofs from premises" results in a loss of the inductive character of the definitions (...) of and and (5) the same occurs with the definition of in terms of `proofs with free variables". (shrink)

This is a long-awaited new edition of one of the best known Oxford Logic Guides. The book gives an informal but thorough introduction to intuitionistic mathematics, leading the reader gently through the fundamental mathematical and philosophical concepts. The treatment of various topics has been completely revised for this second edition. Brouwer's proof of the Bar Theorem has been reworked, the account of valuation systems simplified, and the treatment of generalized Beth Trees and the completeness of intuitionistic first-order logic rewritten. Readers (...) are assumed to have some knowledge of classical formal logic and a general awareness of the history of intuitionism. (shrink)

We give a direct proof of admissibility of cut and contraction for the contraction-free sequent calculus G4ip for intuitionistic propositional logic and for a corresponding multi-succedent calculus: this proof extends easily in the presence of quantifiers, in contrast to other, indirect, proofs. i.e., those which use induction on sequent weight or appeal to admissibility of rules in other calculi.

We describe a sequent calculus, based on work of Herbelin, of which the cut-free derivations are in 1-1 correspondence with the normal natural deduction proofs of intuitionistic logic. We present a simple proof of Herbelin's strong cut-elimination theorem for the calculus, using the recursive path ordering theorem of Dershowitz.

Most automated theorem provers have been built around some version of resolution [4]. But resolution is an inherently Classical logic technique. Attempts to extend the method to other logics have tended to obscure its simplicity. In this paper we present a resolution style theorem prover for Intuitionistic logic that, we believe, retains many of the attractive features of Classical resolution. It is, of course, more complicated, but the complications can be given intuitive motivation. We note that a small change in (...) the system as presented here causes it to collapse back to a Classical resolution system. We present the system in some detail for the propositional case, including soundness and completeness proofs. For the first order version we are sketchier. (shrink)

We define notions of homomorphism, submodel, and sandwich of Kripke models, and we define two syntactic operators analogous to universal and existential closure. Then we prove an intuitionistic analogue of the generalized (dual of the) Lyndon-Łoś-Tarski Theorem, which characterizes the sentences preserved under inverse images of homomorphisms of Kripke models, an intuitionistic analogue of the generalized Łoś-Tarski Theorem, which characterizes the sentences preserved under submodels of Kripke models, and an intuitionistic analogue of the generalized Keisler Sandwich Theorem, which characterizes the (...) sentences preserved under sandwiches of Kripke models. We also define several intuitionistic formula hierarchies analogous to the classical formula hierarchies $\forall_n (= \Pi^0_n)$ and $\exists_n (=\Sigma^0_n)$ , and we show how our generalized syntactic preservation theorems specialize to these hierarchies. Each of these theorems implies the corresponding classical theorem in the case where the Kripke models force classical logic. (shrink)

We show that the variety of Heyting algebras has finitary unification type. We also show that the subvariety obtained by adding it De Morgan law is the biggest variety of Heyting algebras having unitary unification type. Proofs make essential use of suitable characterizations (both from the semantic and the syntactic side) of finitely presented projective algebras.

I begin by drawing a parallel between the intuitionistic understanding of quantification over all natural numbers and the generality relativist understanding of quantification over absolutely everything. I then argue that adoption of an intuitionistic reading of relativism not only provides an immediate reply to the absolutist's charge of incoherence but it also throws a new light on the debates surrounding absolute generality.

We propose a new sequent calculus for bi intuitionistic logic which sits somewhere between display calculi and traditional sequent calculi by using nested sequents. Our calculus enjoys a simple (purely syntactic) cut elimination proof as do display calculi. But it has an easily derivable variant calculus which is amenable to automated proof search as are (some) traditional sequent calculi. We first present the initial calculus and its cut elimination proof. We then present the derived calculus, and then present a proof (...) search strategy which allows it to be used for automated proof search. We prove that this search strategy is terminating and complete by showing how it can be used to mimic derivations obtained from an existing calculus GBiInt for bi intuitionistic logic. As far as we know, our new calculus is the first sequent calculus for bi intuitionistic logic which uses no semantic additions like labels, which has a purely syntactic cut elimination proof, and which can be used naturally for backwards proof search. Keywords: Bi-intuitionistic logic, display calculi, proof search. (shrink)

Intuitionists and classical logicians use in common a large number of the logical axioms, even though they supposedly mean different things by the logical connectives and quantifiers — conquans for short. But Wittgenstein says The meaning of a word is its use in the language. We prove that in a definite sense the intuitionistic axioms do indeed characterize the logical conquans, both for the intuitionist and the classical logician.

A purported axiomatization, by P. Gärdenfors, of intuitionistic propositional logic is shown to be incomplete, and that the mistaken claim to completeness is seen to result from carelessness in the choice of primitive logical vocabulary. This leads to a consideration of various ways of conceiving the distinction between primitive and defined vocabularies, along with the bearing of these differences on such matters as are discussed in connection with Gärdenfors.

The interplay of introduction and elimination rules for propositional connectives is often seen as suggesting a distinguished role for intuitionistic logic. We prove three formal results concerning intuitionistic propositional logic that bear on that perspective, and discuss their significance. First, for a range of connectives including both negation and the falsum, there are no classically or intuitionistically correct introduction rules. Second, irrespective of the choice of negation or the falsum as a primitive connective, classical and intuitionistic consequence satisfy exactly the (...) same structural, introduction, and elimination (briefly, elementary) rules. Third, for falsum as primitive only, intuitionistic consequence is the least consequence relation that satisfies all classically correct elementary rules. (shrink)

We explore a relation we call anticipation between formulas, where A anticipates B (according to some logic) just in case B is a consequence (according to that logic, presumed to support some distinguished implicational connective ) of the formula AB. We are especially interested in the case in which the logic is intuitionistic (propositional) logic and are much concerned with an extension of that logic with a new connective, written as a, governed by rules which guarantee that for any formula (...) B, aB is the (logically) strongest formula anticipating B. The investigation of this new logic, which we call ILa, will confront us on several occasions with some of the finer points in the theory of rules and with issues in the philosophy of logic arising from the proposed explication of the existence of a connective (with prescribed logical behaviour) in terms of the conservative extension of a favoured logic by the addition of such a connective. Other points of interest include the provision of a Kripke semantics with respect to which ILa is demonstrably sound, deployed to establish certain unprovability results as well as to forge connections with C. Rauszer's logic of dual intuitionistic negation and dual intuitionistic implication, and the isolation of two relations (between formulas), head-implication and head-linkage, which, though trivial in the setting of classical logic, are of considerable significance in the intuitionistic context. (shrink)

Several philosophers have argued that the logic of set theory should be intuitionistic on the grounds that the open-endedness of the set concept demands the adoption of a nonclassical semantics. This paper examines to what extent adopting such a semantics has revisionary consequences for the logic of our set-theoretic reasoning. It is shown that in the context of the axioms of standard set theory, an intuitionistic semantics sanctions a classical logic. A Kripke semantics in the context of a weaker axiomatization (...) is then considered. It is argued that this semantics vindicates an intuitionistic logic only insofar as certain constraints are put on its interpretation. Wider morals are drawn about the restrictions that this places on the shape of arguments for an intuitionistic revision of the logic of set theory. (shrink)

Anti-realists typically contend that truth is epistemically constrained. Truth, they say, cannot outstrip our capacity to know. Some anti-realists are also willing to make a further claim: if truth is epistemically constrained, classical logic is to be given up in favour of intuitionistic logic. Here we shall be concerned with one argument in support of this thesis - Crispin Wright's Basic Revisionary Argument, first presented in his Truth and Objectivity. We argue that the reasoning involved in the argument, if correct, (...) validates a parallel argument that leads to conclusions that are unacceptable to classicists and intuitionists alike. (shrink)

The intuitionistic consequence operation restricted to the language with (equivalence) and (negation) as the only connectives is axiomatized by means of a finite set of sequential rules of inference.

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.

I argue for a kind of logical pluralism on the basis of a difficulty with defining the meaning of negation in the framework of Dummett's and Prawitz' proof-theoretic semantics.

The focus of this paper are the meaning-theoretical arguments against classical logic that Dummett bases on consideration about the meanings of negation. Using Dummettian principles, I shall outline three such arguments, of increasing strength, and show that they are unsuccessful by giving responses to each argument on behalf of the classical logician. What is crucial is that in responding to these arguments a classicist need not challenge any of the basic assumptions of Dummett's outlook on the theory of meaning. In (...) particular, I shall grant Dummett his general bias towards verificationism or justificationism, encapsulated in the slogan `meaning is use'. The second general assumption I see no need to question is Dummett's particular breed of molecularism. Some of Dummett's assumptions will have to be given up, if classical logic is to be vindicated in his meaning-theoretical framework. A major result of this paper will be that the meaning of negation cannot be defined by rules of inference in the Dummettian framework. (shrink)

The fundamental assumption of Dummett’s and Prawitz’ proof-theoretic justification of deduction is that ‘if we have a valid argument for a complex statement, we can construct a valid argument for it which finishes with an application of one of the introduction rules governing its principal operator’. I argue that the assumption is flawed in this general version, but should be restricted, not to apply to arguments in general, but only to proofs. I also argue that Dummett’s and Prawitz’ project of (...) providing a logical basis for metaphysics only relies on the restricted assumption. (shrink)

In this paper, I'll present a general way of "reading off" introduction/elimination rules from elimination/introduction rules, and define notions of harmony and stability on the basis of it.

In section 1 we argue that the adoption of a tenseless notion of truth entails a realistic view of propositions and provability. This view, in turn, opens the way to the intelligibility of theclassical meaning of the logical constants, and consequently is incompatible with the antirealism of orthodox intuitionism. In section 2 we show how what we call the potential intuitionistic meaning of the logical constants can be defined, on the one hand, by means of the notion of atemporal provability (...) and, on the other, by means of the operator K of epistemic logic. Intuitionistic logic, as reconstructed within this perspective, turns out to be a part of epistemic logic, so that it loses its traditional foundational role, antithetic to that of classical logic. In section 3 we uphold the view that certain consequences of the adoption of atemporal notion of truth, despite their apparent oddity, are quite acceptable from an antirealist point of view. (shrink)

Our starting point is Michael Luntley's falsificationist semantics for the logical connectives and quantifiers: the details of his account are criticised but we provide an alternative falsificationist semantics that yields intuitionist logic, as Luntley surmises such a semantics ought. Next an account of the logical connectives and quantifiers that combines verificationist and falsificationist perspectives is proposed and evaluated. While the logic is again intuitionist there is, somewhat surprisingly, an unavoidable asymmetry between the verification and falsification conditions for negation, the conditional, (...) and the universal quantifier. Lastly we are lead to a novel characterization of realism. (shrink)

Given an intermediate prepositional logic L, denote by L –d its disjuctionless fragment. We introduce an infinite sequence {J n}n1 of propositional formulas, and prove:(1)For any L: L –d =I –d (I=intuitionistic logic) if and only if J n L for every n 1.

Intuitionistic logic is presented here as part of familiar classical logic which allows mechanical extraction of programs from proofs. to make the material more accessible, basic techniques are presented first for propositional logic; Part II contains extensions to predicate logic. This material provides an introduction and a safe background for reading research literature in logic and computer science as well as advanced monographs. Readers are assumed to be familiar with basic notions of first order logic. One device for making this (...) book short was inventing new proofs of several theorems. The presentation is based on natural deduction. The topics include programming interpretation of intuitionistic logic by simply typed lambda-calculus (Curry-Howard isomorphism), negative translation of classical into intuitionistic logic, normalization of natural deductions, applications to category theory, Kripke models, algebraic and topological semantics, proof-search methods, interpolation theorem. The text developed from materal for several courses taught at Stanford University in 1992-1999. (shrink)

Historically, it was the interpretations of intuitionist logic in the modal logic S4 that inspired the standard Kripke semantics for intuitionist logic. The inspiration of this paper is the interpretation of intuitionist logic in the non-normal modal logic S3: an S3 model structure can be ''looked at'' as an intuitionist model structure and the semantics for S3 can be ''cashed in'' to obtain a non-normal semantics for intuitionist propositional logic. This non-normal semantics is then extended to intuitionist quantificational logic.

A semantical proof of Craig's interpolation theorem for the intuitionistic predicate logic and some intermediate prepositional logics will be given. Our proof is an extension of Henkin's method developed in [4]. It will clarify the relation between the interpolation theorem and Robinson's consistency theorem for these logics and will enable us to give a uniform way of proving the interpolation theorem for them.

We prove the following surprising property of Heyting's intuitionistic propositional calculus, IpC. Consider the collection of formulas, φ, built up from propositional variables (p,q,r,...) and falsity $(\perp)$ using conjunction $(\wedge)$ , disjunction (∨) and implication (→). Write $\vdash\phi$ to indicate that such a formula is intuitionistically valid. We show that for each variable p and formula φ there exists a formula Apφ (effectively computable from φ), containing only variables not equal to p which occur in φ, and such that for (...) all formulas ψ not involving $p, \vdash \psi \rightarrow A_p\phi$ if and only if $\vdash \psi \rightarrow \phi$ . Consequently quantification over propositional variables can be modelled in IpC, and there is an interpretation of the second order propositional calculus, IpC2, in IpC which restricts to the identity on first order propositions. An immediate corollary is the strengthening of the usual interpolation theorem for IpC to the statement that there are least and greatest interpolant formulas for any given pair of formulas. The result also has a number of interesting consequences for the algebraic counterpart of IpC, the theory of Heyting algebras. In particular we show that a model of IpC2 can be constructed whose algebra of truth-values is equal to any given Heyting algebra. (shrink)

Bi-intuitionistic logic is the union of intuitionistic and dual intuitionistic logic, and was introduced by Rauszer as a Hilbert calculus with algebraic and Kripke semantics. But her subsequent ‘cut-free’ sequent calculus has recently been shown to fail cut-elimination. We present a new cut-free sequent calculus for bi-intuitionistic logic, and prove it sound and complete with respect to its Kripke semantics. Ensuring completeness is complicated by the interaction between intuitionistic implication and dual intuitionistic exclusion, similarly to future and past modalities in (...) tense logic. Our calculus handles this interaction using derivations and refutations as first class citizens. We employ extended sequents which pass information from premises to conclusions using variables instantiated at the leaves of refutations, and rules which compose certain refutations and derivations to form derivations. Automated deduction using terminating backward search is also possible, although this is not our main purpose. (shrink)

We study the monadic fragment of second order intuitionistic propositional logic in the language containing the standard propositional connectives and propositional quantifiers. It is proved that under the topological interpretation over any dense-in-itself metric space, the considered fragment collapses to Heyting calculus. Moreover, we prove that the topological interpretation over any dense-in-itself metric space of fragment in question coincides with the so-called Pitts' interpretation. We also prove that all the nonstandard propositional operators of the form q $\mapsto \exists$ p (q (...) $\leftrightarrow$ F(p)), where F is an arbitrary monadic formula of the variable p, are definable in the language of Heyting calculus under the topological interpretation of intuitionistic logic over sufficiently regular spaces. (shrink)

We consider propositional operators defined by propositional quantification in intuitionistic logic. More specifically, we investigate the propositional operators of the formA* :p q(p A(q)) whereA(q) is one of the following formulae: (¬¬q q) V ¬¬q, (¬¬q q) (¬¬q V ¬q), ((¬¬q q) (¬¬q V ¬q)) ((¬¬q q) V ¬¬q). The equivalence ofA*(p) to ¬¬p is proved over the standard topological interpretation of intuitionistic second order propositional logic over Cantor space.We relate topological interpretations of second order intuitionistic propositional logic over Cantor (...) space with the interpretation of propositional quantifiers (as the strongest and weakest interpolant in Heyting calculus) suggested by A. Pitts. One of the merits of Pitts' interpretation is shown to be valid for the interpretation over Cantor space. (shrink)

In what does the sense of a sentential connective consist? Like many others, I hold that its sense lies in rules that govern deductions. In the present paper, however, I argue that a classical logician should take the relevant deductions to be arguments involving affirmative or negative answers to yes-or-no questions that contain the connective. An intuitionistic logician will differ in concentrating exclusively upon affirmative answers. I conclude by arguing that a well known intuitionistic criticism of classical logic fails if (...) the answer 'No' is accorded parity with the answer 'Yes'. (shrink)

An algorithm recognizing admissibility of inference rules in generalized form (rules of inference with parameters or metavariables) in the intuitionistic calculus H and, in particular, also in the usual form without parameters, is presented. This algorithm is obtained by means of special intuitionistic Kripke models, which are constructed for a given inference rule. Thus, in particular, the direct solution by intuitionistic techniques of Friedman's problem is found. As a corollary an algorithm for the recognition of the solvability of logical equations (...) in H and for constructing some solutions for solvable equations is obtained. A semantic criterion for admissibility in H is constructed. (shrink)

We consider a logic which is semantically dual (in some precise sense of the term) to intuitionistic. This logic can be labeled as “falsification logic”: it embodies the Popperian methodology of scientific discovery. Whereas intuitionistic logic deals with constructive truth and non-constructive falsity, and Nelson's logic takes both truth and falsity as constructive notions, in the falsification logic truth is essentially non-constructive as opposed to falsity that is conceived constructively. We also briefly clarify the relationships of our falsification logic to (...) some other logical systems. (shrink)

Logic for Philosophy is an introduction to logic for students of contemporary philosophy. It is suitable both for advanced undergraduates and for beginning graduate students in philosophy. It covers (i) basic approaches to logic, including proof theory and especially model theory, (ii) extensions of standard logic that are important in philosophy, and (iii) some elementary philosophy of logic. It emphasizes breadth rather than depth. For example, it discusses modal logic and counterfactuals, but does not prove the central metalogical results for (...) predicate logic (completeness, undecidability, etc.) Its goal is to introduce students to the logic they need to know in order to read contemporary philosophical work. It is very user-friendly for students without an extensive background in mathematics. In short, this book gives you the understanding of logic that you need to do philosophy. (shrink)

Research within the operational approach to the logical foundations of physics has recently pointed out a new perspective in which quantum logic can be viewed as an intuitionistic logic with an additional operator to capture its essential, i.e., non-distributive, properties. In this paper we will offer an introduction to this approach. We will focus further on why quantum logic has an inherent dynamic nature which is captured in the meaning of "orthomodularity" and on how it motivates physically the introduction of (...) dynamic implication operators, each for which a deduction theorem holds with respect to a dynamic conjunction. As such we can offer a positive answer to the many who pondered about whether quantum logic should really be called a logic. Doubts to answer the question positively were in first instance due to the former lack of an implication connective which satisfies the deduction theorem within quantum logic. (shrink)