This paper formulates a bilateral account of harmony that is an alternative to one proposed by Francez. It builds on an account of harmony for unilateral logic proposed by Kürbis and the observation that reading the rules for the connectives of bilateral logic bottom up gives the grounds and consequences of formulas with the opposite speech act. I formulate a process I call 'inversion' which allows the determination of assertive elimination rules from assertive introduction rules, and rejective elimination rules (...) from rejective introduction rules, and conversely. It corresponds to Francez's notion of vertical harmony. I also formulate a process I call 'conversion', which allows the determination of rejective introduction rules from assertive elimination rules and conversely, and the determination of assertive introduction rules from rejective elimination rules and conversely. It corresponds to Francez's notion of horizontal harmony. The account has a number of features that distinguish it from Francez's. (shrink)

The idea of an ?inversion principle?, and the name itself, originated in the work of Paul Lorenzen in the 1950s, as a method to generate new admissible rules within a certain syntactic context. Some fifteen years later, the idea was taken up by Dag Prawitz to devise a strategy of normalization for natural deduction calculi (this being an analogue of Gentzen's cut-elimination theorem for sequent calculi). Later, Prawitz used the inversion principle again, attributing it with a (...) semantic role. Still working in natural deduction calculi, he formulated a general type of schematic introduction rules to be matched ? thanks to the idea supporting the inversion principle ? by a corresponding general schematic Elimination rule. This was an attempt to provide a solution to the problem suggested by the often quoted note of Gentzen. According to Gentzen ?it should be possible to display the elimination rules as unique functions of the corresponding introduction rules on the basis of certain requirements?. Many people have since worked on this topic, which can be appropriately seen as the birthplace of what are now referred to as ?general elimination rules?, recently studied thoroughly by Sara Negri and Jan von Plato. In this study, we retrace the main threads of this chapter of proof-theoretical investigation, using Lorenzen's original framework as a general guide. (shrink)

. The term inversion principle goes back to Lorenzen who coined it in the early 1950s. It was later used by Prawitz and others to describe the symmetric relationship between introduction and elimination inferences in natural deduction, sometimes also called harmony. In dealing with the invertibility of rules of an arbitrary atomic production system, Lorenzen’s inversion principle has a much wider range than Prawitz’s adaptation to natural deduction. It is closely related to definitional reflection, which is (...) a principle for reasoning on the basis of rule-based atomic definitions, proposed by Hallnäs and Schroeder-Heister. After presenting definitional reflection and the inversion principle, it is shown that the inversion principle can be formally derived from definitional reflection, when the latter is viewed as a principle to establish admissibility. Furthermore, the relationship between definitional reflection and the inversion principle is investigated on the background of a universalization principle, called the ω- principle, which allows one to pass from the set of all defined substitution instances of a sequent to the sequent itself. (shrink)

We assessed how synchronous speech listening and lipreading affects speech recognition in acoustic noise. In simple audiovisual perceptual tasks, inverse effectiveness is often observed, which holds that the weaker the unimodal stimuli, or the poorer their signal-to-noise ratio, the stronger the audiovisual benefit. So far, however, inverse effectiveness has not been demonstrated for complex audiovisual speech stimuli. Here we assess whether this multisensory integration effect can also be observed for the recognizability of spoken words. To that end, we presented audiovisual (...) sentences to 18 native-Dutch normal-hearing participants, who had to identify the spoken words from a finite list. Speech-recognition performance was determined for auditory-only, visual-only (lipreading) and auditory-visual conditions. To modulate acoustic task difficulty, we systematically varied the auditory signal-to-noise ratio. In line with a commonly-observed multisensory enhancement on speech recognition, audiovisual words were more easily recognized than auditory-only words (recognition thresholds of -15 dB and -12 dB, respectively). We here show that the difficulty of recognizing a particular word, either acoustically or visually, determines the occurrence of inverse effectiveness in audiovisual word integration. Thus, words that are better heard or recognized through lipreading, benefit less from bimodal presentation. Audiovisual performance at the lowest acoustic signal-to-noise ratios (45%) fell below the visual recognition rates (60%), reflecting an actual deterioration of lipreading in the presence of excessive acoustic noise. This suggests that the brain may adopt a strategy in which attention has to be divided between listening and lipreading. (shrink)

The inversion principle for logical rules expresses a relationship between introduction and elimination rules for logical constants. Hallnäs & Schroeder-Heister proposed the principle of definitional reflection, which embodies basic ideas of inversion in the more general context of clausal definitions. For the context of admissibility statements, this has been further elaborated by Schroeder-Heister. Using the framework of definitional reflection and its admissibility interpretation, we show that, in the sequent calculus of minimal propositional logic, the left introduction (...) rules are admissible when the right introduction rules are taken as the definitions of the logical constants and vice versa. This generalizes the well-known relationship between introduction and elimination rules in natural deduction to the framework of the sequent calculus. (shrink)

The inversion principle for logical rules expresses a relationship between introduction and elimination rules for logical constants. Hallnäs & Schroeder-Heister proposed the principle of definitional reflection, which embodies basic ideas of inversion in the more general context of clausal definitions. For the context of admissibility statements, this has been further elaborated by Schroeder-Heister . Using the framework of definitional reflection and its admissibility interpretation, we show that, in the sequent calculus of minimal propositional logic, the left (...) introduction rules are admissible when the right introduction rules are taken as the definitions of the logical constants and vice versa. This generalizes the well-known relationship between introduction and elimination rules in natural deduction to the framework of the sequent calculus. (shrink)

This article1 deals with a well-known but still ill-explained fact about German, namely scope inversion under a particular accent contour, as illustrated with the following examples, where “/” and “\” stand for rising and falling accent: (a) Mindestens ein Stu- dent hat jeden Roman gelesen, lit. ‘at least one student has every novel read’, with the reading “For at least one student x: x read every book”, and (b) Mindestens /EIN Student hat \JEDen Roman gelesen, with the additional reading (...) “For every novel y: at least one student read y”. I will derive the scope inversion in this reading from general principles of scope assignment and focus marking in German. In particular, I will argue that focus is assigned to constituents that precede the verbal predicate, which leads to syntactic configurations that in turn result in ambiguous interpretations. This explanation must be couched in a framework of derivational economy that favors shorter derivations. It is argued that the relevant comparison class is defined with respect to phonological form, not, as has been suggested for English, with respect t o identity of semantic interpretation, and that this may be a general property of “free” word order languages. (shrink)

A recent report in Consciousness and Cognition provided evidence from a study of the rubber hand illusion that supports the multisensory principle of inverse effectiveness . I describe two methods of assessing the principle of inverse effectiveness , and discuss how the post-hoc method is affected by the statistical artefact of ‘regression towards the mean’. I identify several cases where this artefact may have affected particular conclusions about the PoIE, and relate these to the historical origins of ‘regression (...) towards the mean’. Although the conclusions of the recent report may not have been grossly affected, some of the inferential statistics were almost certainly biased by the methods used. I conclude that, unless such artefacts are fully dealt with in the future, and unless the statistical methods for assessing the PoIE evolve, strong evidence in support of the PoIE will remain lacking. (shrink)

This paper proposes a unified dependent type analysis of three puzzling phenomena: inversely linked interpretations, weak definite readings in possessives and Haddock-type readings. We argue that the three problematic readings have the same underlying surface structure, and that the surface structure postulated can be interpreted properly and compositionally using dependent types. The dependent type account proposed is the first, to the best of our knowledge, to formally connect the three phenomena. A further advantage of our proposal over previous analyses is (...) that it offers a principled solution to the puzzle of why both inversely linked interpretations and weak definite readings are blocked with certain prepositions. (shrink)

An inverse akratic act is one who believes X, all things considered, is the correct act, and yet performs ~X, where ~X is the correct act. A famous example of such a person is Huck Finn. He believes that he is wrong in helping Jim, and yet continues to do so. In this paper I investigate Huck’s nature to see why he performs such acts contrary to his beliefs. In doing so, I explore the nature of empathy and show how (...) powerful Huck’s empathic feelings are. Drawing from Martin L. Hoffman, I show the relationship between empathy and a principle of justice. This relationship leads to Huck acting virtuously, as Rosalind Hursthouse maintains. (shrink)

Cognitive science typically postulates unconscious mental phenomena, computational or otherwise, to explain cognitive capacities. The mental phenomena in question are supposed to be inaccessible in principle to consciousness. I try to show that this is a mistake, because all unconscious intentionality must be accessible in principle to consciousness; we have no notion of intrinsic intentionality except in terms of its accessibility to consciousness. I call this claim the The argument for it proceeds in six steps. The essential point (...) is that intrinsic intentionality has aspectual shape: Our mental representations represent the world under specific aspects, and these aspectual features are essential to a mental state's being the state that it is. (shrink)

The article presents a full proof‐theoretic semantics for natural deduction based on an extended inversion principle: the elimination rule for an operator q may invert the introduction rule for q, but also vice versa, the introduction rule for a connective q may invert the elimination rule for q. Such an inversion—extending Prawitz' concept of inversion—gives the following theorem: Inversion for two rules of operator q (intro rule, elim rule) exists iff a reduction of a maximum (...) formula for q exists. The inversion theorem is specified to two logics, Lambek calculus (LC) and intuitionistic linear logic (ILL), with four propositional connectives: two multiplicatives (implication and conjunction) and two additives (conjunction and disjunction), with two quantifiers and two modals. LC is defined by using elimination rules by composition. ILL is defined by using usual general elimination rules. Elimination rules by composition are an exciting alternative to general elimination rules; in some cases, they do not need permutations. (shrink)

Over _Principles_ 42-43, Berkeley worried that we might "in truth" see things existing at a distance from us, in which case they could not plausibly be supposed to exist independently of being perceived. He went on to say that he had developed his new theory of vision to address this worry. This paper argues that the worry is serious and that Berkeley was right to think that it would take nothing less than a theory of vision to address it. The (...) paper further argues that Berkeley's theory of vision fails to adequately address the worry. The locus of the failure is Berkeley's account of what he called "situation." The term has an ambiguity that Berkeley exploited. It can refer to how coloured points are localized on a two dimensional visual field or it can mean how the visual field is oriented with respect to the direction of gravity. Berkeley focused on the second when he needed to explain how the first is possible without granting that we originally experience objects as disposed over at least two spatial dimensions. (shrink)

Many have thought that symmetries of a Lagrangian explain the standard laws of energy, momentum, and angular momentum conservation in a rather straightforward way. In this paper, I argue that the explanation of conservation laws via symmetries of Lagrangians involves complications that have not been adequately noted in the philosophical literature and some of the physics literature on the subject. In fact, such complications show that the principles that are commonly appealed to to drive explanations of conservation laws are not (...) generally correct without caveats. I hope here to give a clearer picture of the relationship between symmetries and conservation laws in Lagrangian mechanics via an examination of the bearing that results in the inverse problem in the calculus of variations have on this topic. (shrink)

This paper analyzes the ‘Theory of Inverse Numbers’ that appears in Chapter 3 of the “Shuogua zhuan” 說卦傳 in the I Ching and seeks to apply the findings to the Yi studies of Cheng Yi. The Yi studies of Shao Yong, Zhu Xi, and Cheng Yi are generally explained in the categories of Xiangshu(Image-Number) Yi studies and Yili(Meaning-Principle) Yi studies. However, upon analyzing the ‘Theory of Inverse Numbers’ as a theory representing numbers of principles, it is evident that the (...) framework of this theory is also reflected in Cheng Yi’s Yi studies. The analysis of the ‘Theory of Inverse Numbers’ was conducted through the interpretations of Shao Yong and Zhu Xi, proposing the concept of the ‘Theory of Inverse Numbers’ as a Yi interpretation framework that accounts for what has already occurred [yisheng 已生] and what has not yet occurred [weisheng 未生]. By applying the Yi interpretation framework of what has arisen and what has not, which was developed through the explanations of Shao Yong and Zhu Xi, to Cheng Yi’s Yi studies, it is revealed that even though Cheng Yi does not directly mention Chapter 3 of the “Shuogua zhuan,” the narrative framework of Yichuan Yizhuan 伊川易傳 can be well elucidated by the ‘Theory of Inverse Numbers.’ Accordingly, it suggests that viewing Cheng Yi’s Yi studies merely as a dichotomy of meaning-principle and image-number is limited, and that the concept of Xiangshu Yi is inherent in Cheng Yi’s Yi studies. In other words, the ‘Theory of Inverse Numbers’ as a theory of principle-representing numbers originating from Shao Yong is inherent throughout Cheng Yi’s interpretation of the I Ching as a framework of Yi interpretation for what has arisen and what has not, and this was systematized as the ‘Theory of Inverse Numbers’ by Zhu Xi. (shrink)

In this paper we study a new approach to classify mathematical theorems according to their computational content. Basically, we are asking the question which theorems can be continuously or computably transferred into each other? For this purpose theorems are considered via their realizers which are operations with certain input and output data. The technical tool to express continuous or computable relations between such operations is Weihrauch reducibility and the partially ordered degree structure induced by it. We have identified certain choice (...) principles such as co-finite choice, discrete choice, interval choice, compact choice and closed choice, which are cornerstones among Weihrauch degrees and it turns out that certain core theorems in analysis can be classified naturally in this structure. In particular, we study theorems such as the Intermediate Value Theorem, the Baire Category Theorem, the Banach Inverse Mapping Theorem, the Closed Graph Theorem and the Uniform Boundedness Theorem. We also explore how existing classifications of the Hahn—Banach Theorem and Weak Kőnig's Lemma fit into this picture. Well-known omniscience principles from constructive mathematics such as LPO and LLPO can also naturally be considered as Weihrauch degrees and they play an important role in our classification. Based on this we compare the results of our classification with existing classifications in constructive and reverse mathematics and we claim that in a certain sense our classification is finer and sheds some new light on the computational content of the respective theorems. Our classification scheme does not require any particular logical framework or axiomatic setting, but it can be carried out in the framework of classical mathematics using tools of topology, computability theory and computable analysis. We develop a number of separation techniques based on a new parallelization principle, on certain invariance properties of Weihrauch reducibility, on the Low Basis Theorem of Jockusch and Soare and based on the Baire Category Theorem. Finally, we present a number of metatheorems that allow to derive upper bounds for the classification of the Weihrauch degree of many theorems and we discuss the Brouwer Fixed Point Theorem as an example. (shrink)

The paper focuses on Gottlob Frege’s so called Context Principle (CP hereafter), which counts as one of the most controversial points of his philosophy. Due to its importance and centrality in Frege’s thought, a detailed discussion of the principle requires a detailed analysis of almost all aspects of his philosophy. Obviously, such a task cannot be successfully accomplished here. Thus I limit myself to address only two questions concerning the CP: what role does the principle play (in (...) Grundlagen) and how can we interpret it. Addressing the first problem is required in order to address the second. Most authors interpreted CP from the perspective of Frege’s later distinction between sense and reference, which I will call the ‘semantic interpretation’. Although I accept this perspective as valuable and important, I will initially inverse the action and I will try to approach CP, and generally Grundlagen, in a more natural way, contextually, namely setting them in the initial logicist plan of the Begriffschrift. Finally, I will try to provide an interpretation concerning the alleged conflict between CP and Frege’s compositionality thesis such that they could coherently stay together. (shrink)

Highlighting Hegel's conceptual realism Hoffmann focuses on an undervalued move in his dialectic: inversion. Easily proving completeness for Kant's table of categories, Hoffmann shows how metabolic dialectic substantiates Hegel's claim for his _Logic_: it is indeed the science of absolute form!

Subjectivists hold that you cannot specify color kinds without implicitly or explicitly referring to the dispositions of observers. Even though "yellow" is ascribed to physical items, and presumably there is something physical in each such item causing it to be so characterized, the only physical similarity between all such items is that they all affect an observer in the same way. So the principles organizing the colors are all found within the skin.

Faraday's field concept presupposes that field stresses should share the axial symmetry of the lines of force. In the present article, the field dynamics is similarly required to depend only on field properties that can be tested through the motion of test-particles. Precise expressions of this 'Faradayan' principle in field-theoretical language are shown to severely restrict the form of classical field theories. In particular, static forces must obey the inverse square law in a linear approximation. Within a Minkowskian and (...) Lagrangian framework, the Faradayan principle automatically leads to Maxwell's theory of electromagnetism and to Einstein's theory of gravitation, without appeal to the equivalence principle. A comparison is drawn between this, Feynman's, and Einstein's way to arrive at general relativity. (shrink)

David Lewis (1980) proposed the Principal Principle (PP) and a “reformulation” which later on he called ‘OP’ (Old Principle). Reacting to his belief that these principles run into trouble, Lewis (1994) concluded that they should be replaced with the New Principle (NP). This conclusion left Lewis uneasy, because he thought that an inverse form of NP is “quite messy”, whereas an inverse form of OP, namely the simple and intuitive PP, is “the key to our concept of (...) chance”. I argue that, even if OP should be discarded, PP need not be. Moreover, far from being messy, an inverse form of NP is a simple and intuitive Conditional Principle (CP). Finally, both PP and CP are special cases of a General Principle (GP); it follows that so are PP and NP, which are thus compatible rather than competing. (shrink)

David Lewis (1980) proposed the Principal Principle (PP) and a “reformulation” which later on he called ‘OP’(Old Principle). Reacting to his belief that these principles run into trouble, Lewis (1994) concluded that they should be replaced with the New Principle (NP). This conclusion left Lewis uneasy, because he thought that an inverse form of NP is “quite messy”, whereas an inverse form of OP, namely the simple and intuitive PP, is “the key to our concept of chance”. (...) I argue that, even if OP should be discarded, PP need not be. Moreover, far from being messy, an inverse form of NP is a simple and intuitive Conditional Principle (CP). Finally, both PP and CP are special cases of a General Principle (GP); it follows that so are PP and NP, which are thus compatible rather than competing. (shrink)

In Arrovian social choice theory assuming the independence of irrelevant alternatives, Murakami (1968) proved two theorems about complete and transitive collective choice rules that satisfy strict non-imposition (citizens’ sovereignty), one being a dichotomy theorem about Paretian or anti-Paretian rules and the other a dictator-or-inverse-dictator impossibility theorem without the Pareto principle. It has been claimed in the later literature that a theorem of Malawski and Zhou (1994) is a generalization of Murakami’s dichotomy theorem and that Wilson’s (1972) impossibility theorem is (...) stronger than Murakami’s impossibility theorem, both by virtue of replacing Murakami’s assumption of strict non-imposition with the assumptions of non-imposition and non-nullness. In this note, we first point out that these claims are incorrect: non-imposition and non-nullness are together equivalent to strict non-imposition for all transitive collective choice rules. We then generalize Murakami’s dichotomy and impossibility theorems to the setting of incomplete social preference. We prove that if one drops completeness from Murakami’s assumptions, his remaining assumptions imply (i) that a collective choice rule is either Paretian, anti-Paretian, or dis-Paretian (unanimous individual preference implies noncomparability) and (ii) that adding proposed constraints on noncomparability, such as the regularity axiom of Eliaz and Ok (2006), restores Murakami’s dictator-or-inverse-dictator result. (shrink)

A uniform calculus for linear logic is presented. The calculus has the form of a natural deduction system in sequent calculus style with general introduction and elimination rules. General elimination rules are motivated through an inversion principle, the dual form of which gives the general introduction rules. By restricting all the rules to their single-succedent versions, a uniform calculus for intuitionistic linear logic is obtained. The calculus encompasses both natural deduction and sequent calculus that are obtained as special (...) instances from the uniform calculus. Other instances give all the invertibilities and partial invertibilities for the sequent calculus rules of linear logic. The calculus is normalizing and satisfies the subformula property for normal derivations. (shrink)

This article develops the Pure Logic of Iterated Full Ground (PLIFG), a logic of ground that can deal with claims of the form “ϕ grounds that (ψ grounds θ)”—what we call iterated grounding claims. The core idea is that some truths Γ ground a truth ϕ when there is an explanatory argument (of a certain sort) from premisses Γ to conclusion ϕ. By developing a deductive system that distinguishes between explanatory and nonexplanatory arguments we can give introduction rules for operators (...) for factive and nonfactive full ground, as well as for a propositional “identity” connective. Elimination rules are then found by using a proof-theoretic inversion principle. (shrink)

By a valid inference is here understood an inference that succeeds in its aim to justify its conclusion given that its premisses are already justified. For an inference to be valid it is thus not enough that the sentence asserted in the conclusion is a logical consequence of the sentences asserted in the premisses. A proof is understood as a succession of valid inferences that is closed (i.e. all its assumptions are discharged and all its free variables are bound by (...) some of the inferences). On the other hand, in mathematics the justification of an assertion has traditionally been taken to consist in a proof of it, which gives rise to an explanatory circle.In an attempt to avoid this circle, I have in previous works tried to explain the notion of ground for an assertion without referring to valid inferences. However, it turns out that the resulting notion of ground has unwanted consequences like the notion of proof in the so-called BHK-interpretation of intuitionistic logic. For instance, one is guaranteed a ground or a proof of an implication A → B as soon as there is in fact no ground or proof of A, regardless of whether one really knows this fact, and hence without having a real justification of the assertion of the implication.In the absence of a non-circular explanation of the notions of valid inference and proof, I suggest that we should try to formulate a number of principles of how these two epistemic notions depend on each other. A more careful explanation of the validity of an inference results in what I call a heuristic idea about the validity of inference, which is used as a guide to formulate precise principles. One such principle generalizes Gentzen’s idea that his introduction rules define the meaning of the logical constants. Another principle generalizes a previously noted property of Gentzen’s elimination rules that I have called that of satisfying the inversion principle. It results in a notion that I call non-creativity, which implies validity. (shrink)

This volume presents a collection of refereed papers reflecting the state of the art in the area of over-constrained systems. Besides 11 revised full papers, selected from the 24 submissions to the OCS workshop held in conjunction with the First International Conference on Principles and Practice of Constraint Programming, CP '95, held in Marseilles in September 1995, the book includes three comprehensive background papers of central importance for the workshop papers and the whole field. Also included is an introduction by (...) one of the volume editors together with a bibliography listing 243 entries. All in all this is a very useful reference book relevant for all researchers and practitioners interested in hierarchical, partial, and over-constrained systems. (shrink)

Inferentialism claims that expressions are meaningful by virtue of rules governing their use. In particular, logical expressions are autonomous if given meaning by their introduction-rules, rules specifying the grounds for assertion of propositions containing them. If the elimination-rules do no more, and no less, than is justified by the introduction-rules, the rules satisfy what Prawitz, following Lorenzen, called an inversion principle. This connection between rules leads to a general form of elimination-rule, and when the rules have this form, (...) they may be said to exhibit “general-elimination” harmony. Ge-harmony ensures that the meaning of a logical expression is clearly visible in its I-rule, and that the I- and E-rules are coherent, in encapsulating the same meaning. However, it does not ensure that the resulting logical system is normalizable, nor that it satisfies the conservative extension property, nor that it is consistent. Thus harmony should not be identified with any of these notions. (shrink)

In the present paper, the Fregean conception of proof-theoretic semantics that I developed elsewhere will be revised so as to better reflect the different roles played by open and closed derivations. I will argue that such a conception can deliver a semantic analysis of languages containing paradoxical expressions provided some of its basic tenets are liberalized. In particular, the notion of function underlying the Brouwer–Heyting–Kolmogorov explanation of implication should be understood as admitting functions to be partial. As argued in previous (...) work, the correctness of an inference rule should not be defined in terms of transmission of provability, but rather should be grounded on weaker principles, which I show that are motivated by consideration about the content of the inversion principle. In the conclusion, I briefly address the issue of compositionality, arguing that the violation of compositionality induced by paradoxes are no worse than others that are regarded, at least by Dummett, as wholly unproblematic. (shrink)

In this paper we argue that an account of proof-theoretic harmony based on reductions and expansions delivers an inferentialist picture of meaning which should be regarded as intensional, as opposed to other approaches to harmony that will be dubbed extensional. We show how the intensional account applies to any connective whose rules obey the inversion principle first proposed by Prawitz and Schroeder-Heister. In particular, by improving previous formulations of expansions, we solve a problem with quantum-disjunction first posed by (...) Dummett. As recently observed by Schroeder-Heister, however, the specification of an inversion principle cannot yield an exhaustive account of harmony. The reason is that there are more collections of elimination rules than just the one obtained by inversion which we are willing to acknowledge as being in harmony with a given collection of introduction rules. Several authors more or less implicitly suggest that what is common to all alternative harmonious collection of rules is their being interderivable with each other. On the basis of considerations about identity of proofs and formula isomorphism, we show that this is too weak a condition for a given collection of elimination rules to be in harmony with a collection of introduction rules, at least if the intensional picture of meaning we advocate is not to collapse on an extensional one. (shrink)

This volume is dedicated to Prof. Dag Prawitz and his outstanding contributions to philosophical and mathematical logic. Prawitz's eminent contributions to structural proof theory, or general proof theory, as he calls it, and inference-based meaning theories have been extremely influential in the development of modern proof theory and anti-realistic semantics. In particular, Prawitz is the main author on natural deduction in addition to Gerhard Gentzen, who defined natural deduction in his PhD thesis published in 1934. The book opens with an (...) introductory paper that surveys Prawitz's numerous contributions to proof theory and proof-theoretic semantics and puts his work into a somewhat broader perspective, both historically and systematically. Chapters include either in-depth studies of certain aspects of Dag Prawitz's work or address open research problems that are concerned with core issues in structural proof theory and range from philosophical essays to papers of a mathematical nature. Investigations into the necessity of thought and the theory of grounds and computational justifications as well as an examination of Prawitz's conception of the validity of inferences in the light of three “dogmas of proof-theoretic semantics” are included. More formal papers deal with the constructive behaviour of fragments of classical logic and fragments of the modal logic S4 among other topics. In addition, there are chapters about inversion principles, normalization of p roofs, and the notion of proof-theoretic harmony and other areas of a more mathematical persuasion. Dag Prawitz also writes a chapter in which he explains his current views on the epistemic dimension of proofs and addresses the question why some inferences succeed in conferring evidence on their conclusions when applied to premises for which one already possesses evidence. (shrink)

This paper raises a principled objection against the idea that Bayesian confirmation theory can be used to explain the conjunction fallacy. The paper demonstrates that confirmation-based explanations are limited in scope and can only be applied to cases of the fallacy of a certain restricted kind. In particular; confirmation-based explanations cannot account for the inverse conjunction fallacy, a more recently discovered form of the conjunction fallacy. Once the problem has been set out, the paper explores four different ways for the (...) confirmation theorist to come to terms with the problem, and argues that none of them are successful. (shrink)

This collection of papers, celebrating the contributions of Swedish logician Dag Prawitz to Proof Theory, has been assembled from those presented at the Natural Deduction conference organized in Rio de Janeiro to honour his seminal research. Dag Prawitz’s work forms the basis of intuitionistic type theory and his inversion principle constitutes the foundation of most modern accounts of proof-theoretic semantics in Logic, Linguistics and Theoretical Computer Science.

This collection of papers, celebrating the contributions of Swedish logician Dag Prawitz to Proof Theory, has been assembled from those presented at the Natural Deduction conference organized in Rio de Janeiro to honour his seminal research. Dag Prawitz’s work forms the basis of intuitionistic type theory and his inversion principle constitutes the foundation of most modern accounts of proof-theoretic semantics in Logic, Linguistics and Theoretical Computer Science. The range of contributions includes material on the extension of natural deduction (...) with higher-order rules, as opposed to higher-order connectives, and a paper discussing the application of natural deduction rules to dealing with equality in predicate calculus. The volume continues with a key chapter summarizing work on the extension of the Curry-Howard isomorphism, via methods of category theory that have been successfully applied to linear logic, as well as many other contributions from highly regarded authorities. With an illustrious group of contributors addressing a wealth of topics and applications, this volume is a valuable addition to the libraries of academics in the multiple disciplines whose development has been given added scope by the methodologies supplied by natural deduction. The volume is representative of the rich and varied directions that Prawitz work has inspired in the area of natural deduction. (shrink)