In this paper I outline an argument for the existence of God. This argument suggests that, if an all-good supernatural agent were to exist, such as the God of Theism, then He could not perform an immoral act. From this premise alone a formal proof for the existence of God can be derived. Perhaps unsurprisingly, when this argument is examined closely it is revealed to be fallacious. However, what we find is that the fallacy involves a special type of (...) equivocation; one that illustrates the difference between non-truth-functional subjunctive conditionals and truth-functional material conditionals. (shrink)

This paper urges the importance of including conditional proof as an inference rule in the teaching of elementary symbolic logic. The paper explains how to make clear to students that conditional proof is valid. This is done by a little proof that shows that hypothetical syllogism (or the chain rule) is both intuitively valid yet redundant. Teaching conditional proof not only aids in a deeper understanding of the meaning of “if” but also provides (...) a strong reminder to the student that they have not proved that the conclusion is true but instead have shown that the conclusion follows from the premises. (shrink)

ABSTRACT In our response Field's ‘Properties, Propositions and Conditionals’, we explore the methodology of Field's program. We begin by contrasting it with a proof-theoretic approach and then commenting on some of the particular choices made in the development of Field's theory. Then, we look at issues of property identity in connection with different notions of equivalence. We close with some comments relating our discussion to Field's response to Restall’s [2010] ‘What Are We to Accept, and What Are We to (...) Reject, While Saving Truth from Paradox?’. (shrink)

We discuss the problem raised by Miller to re-prove the well-known equivalences of some Lindenbaum theorems for deductive systems without an application of the Axiom of Choice. We present five special constructions of deductive systems, each of them providing some partial solutions to the mathematical problem. We conclude with a short discussion of the underlying philosophical problem of deciding, whether a given proof satisfies our demand that the Axiom of Choice is not applied.

Dynamic and proof-conditional approaches to discourse (exemplified by Discourse Representation Theory and Type-Theoretical Grammar, respectively) are related through translations and transitions labeled by first-order formulas with anaphoric twists. Type-theoretic contexts are defined relative to a signature and instantiated modeltheoretically, subject to change.

In the recent literature on proof-theoretic semantics, there is mention of a generality condition on defining rules. According to this condition, the schematic formulation of the defining rules must be maximally general, in the sense that no restrictions should be placed on the contexts of these rules. In particular, context variables must always be present in the schematic rules and they should range over arbitrary collections of formulae. I argue against imposing such a condition, by showing that it has (...) undesirable results and that it is ill-supported by the arguments brought in its favour. (shrink)

The aim of this paper is to present a modified version of the notion of strong proof from hypotheses (definition D2), and to give three deduction theorems for the relevant logicsR (theoremsT1, andT2) andE (theoremT3).

In Part I of this paper, we identified and compared various schemes for trivalent truth conditions for indicative conditionals, most notably the proposals by de Finetti and Reichenbach on the one hand, and by Cooper and Cantwell on the other. Here we provide the proof theory for the resulting logics DF/TT and CC/TT, using tableau calculi and sequent calculi, and proving soundness and completeness results. Then we turn to the algebraic semantics, where both logics have substantive limitations: DF/TT allows (...) for algebraic completeness, but not for the construction of a canonical model, while CC/TT fails the construction of a Lindenbaum-Tarski algebra. With these results in mind, we draw up the balance and sketch future research projects. (shrink)

The paper presents a proof-theoretic semantics (PTS) for a fragment of natural language, providing an alternative to the traditional model-theoretic (Montagovian) semantics (MTS), whereby meanings are truth-condition (in arbitrary models). Instead, meanings are taken as derivability-conditions in a dedicated natural-deduction (ND) proof-system. This semantics is effective (algorithmically decidable), adhering to the meaning as use paradigm, not suffering from several of the criticisms formulated by philosophers of language against MTS as a theory of meaning. In particular, Dummett’s manifestation argument (...) does not obtain, and assertions are always warranted, having grounds of assertion. The proof system is shown to satisfy Dummett’s harmony property, justifying the ND rules as meaning conferring. The semantics is suitable for incorporation into computational linguistics grammars, formulated in type-logical grammar. (shrink)

Planning with incomplete knowledge becomes a very active research area since late 1990s. Many logical formalisms introduce sensing actions and conditional plans to address the problem. The action language $\mathcal{A}_{K}$ invented by Son and Baral is a well-known framework for this purpose. In this paper, we propose so-called cautious and weakly cautious semantics for $\mathcal{A}_{K}$ , in order to allow an agent to generate and execute reliable plans in safety-critical environments. Intuitively speaking, cautious and weakly cautious semantics enable the (...) agent to know exactly what happens after the execution of an action. Computational complexity analysis shows that cautious semantics reduces the reasoning complexity of $\mathcal{A}_{K}$ , it is also worth to point out that many useful domains could still be expressed with this setting. Another important contribution of our work is the development of Hoare style proof systems. These proof systems are served as inference mechanisms for the verification of conditional plans, and proved to be sound and complete. In addition, they could also be used for plan generation, in the sense that constructing a derivation is indeed a procedure to finding a plan. We point out that the proof systems posses a nice property for off-line planning, that is, the agent could generate and store short proofs in her spare time, and perform quick plan query by easily constructing a long proof from the stored shorter ones (under the assumption that sufficient proofs are stored). (shrink)

This short essay seeks to identify and prevent a pitfall that attends less careful inquiries into “physiosemiosis.” It is emphasized that, in order to truly establish the presence of sign-action in the non-living world, all the components of a triadic sign - including the interpretant - would have to be abiotic (that is, not dependent on a living organism). Failure to heed this necessary condition can lead one to hastily confuse a natural sign (like smoke coming from fire) for an (...) instance of abiotic semiosis. A more rigorous and reserved approach to the topic is called for. (shrink)

Many theorists hold that outright verdicts based on bare statistical evidence are unwarranted. Bare statistical evidence may support high credence, on these views, but does not support outright belief or legal verdicts of culpability. The vignettes that constitute the lottery paradox and the proof paradox are marshalled to support this claim. Some theorists argue, furthermore, that examples of profiling also indicate that bare statistical evidence is insufficient for warranting outright verdicts.I examine Pritchard's and Buchak's treatments of these three kinds (...) of case. Pritchard argues that his safety condition explains the insufficiency of bare statistical evidence for outright verdicts in each of the three cases, while Buchak argues that her treatment of the distinction between credence and belief explains this. In these discussions the three kinds of cases – lottery, proof paradox, and profiling – are treated alike. The cases are taken to exhibit the same epistemic features. I identity significant overlooked epistemic differences amongst these three cases; these differences cast doubt on Pritchard's explanation of the insufficiency of bare statistical evidence for outright verdicts. Finally, I raise the question of whether we should aim for a unified explanation of the three paradoxes. (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)

Relatively little is known about those who consistently produce the valid response to Modus Tollens (MT) problems. In two studies, people who responded correctly to MT problems indicated how “convinced” they were by proofs of conditional reasoning conclusions. The first experiment showed that MT competent reasoners found accurate proofs of MT reasoning more convincing than similar “proofs” of invalid reasoning. Similarly, there was a tendency for MT competent reasoners to find an initial counterfactual supposition more convincing than did people (...) who were less competent in MT. The second experiment showed that when individuals produced the correct MT response, and found correct MT proofs to be more convincing than “bogus” proofs, they were also less likely to find the conclusions to Denying the Antecedent, or Affirming the Consequent problems valid, compared to individuals who could not discriminate between valid and bogus MT proofs. These findings are discussed in terms of both their implications for the mental logic and mental models positions, and individual differences in System 1 and System 2 reasoning. (shrink)

By maintaining that a conditional sentence can be taken to express the validity of a rule of inference, we offer a solution to the Miners Paradox that leaves both modus ponens and disjunction elimination intact. The solution draws on Sundholm's recently proposed account of Fitch's Paradox.

Using labelled formulae, a cut-free sequent calculus for intuitionistic propositional logic is presented, together with an easy cut-admissibility proof; both extend to cover, in a uniform fashion, all intermediate logics characterised by frames satisfying conditions expressible by one or more geometric implications. Each of these logics is embedded by the Gödel–McKinsey–Tarski translation into an extension of S4. Faithfulness of the embedding is proved in a simple and general way by constructive proof-theoretic methods, without appeal to semantics other than (...) in the explanation of the rules. (shrink)

The proof paradox results from conflicting intuitions concerning different types of fallible evidence in a court of law. We accept fallible individual evidence but reject fallible statistical evidence even when the conditional probability that the defendant is guilty given the evidence is the same, a seeming inconsistency. This paper defends a solution to the proof paradox, building on a sensitivity account of checking and settling a question. The proposed sensitivity account of legal proof not only requires (...) sensitivity simpliciter but sensitivity of each relevant step of the proof procedure and/or sensitivity concerning all relevant alternatives. This account avoids problems that have been identified for other sensitivity views of legal proof. Moreover, it is argued that sensitivity, rather than safety, is the crucial modal condition for legal proof. It is, finally, shown that the provided account can fruitfully support very different existing views on the relationship between knowledge and legal proof. (shrink)

The paper introduces a proof-theoretic semantics for adjectival modification as an alternative to the traditional model-theoretic semantics basing meaning on truth-conditions. The paper considers the proof-theoretic meaning of modification by means of the three traditional adjective classes: intersective, subsective and privative. It does so by introducing a meaning-conferring natural-deduction proof system for such modification. The PTS theory of meaning is not polluted by ontological commitments, for example, a scale for beauty and a yardstick for being beautiful. It (...) only uses syntactic artefacts of the proof language. The paper also defines, by suitable rules, iterated modification, shedding light on the relationship between iteration and adjectival classes. Modification via coordinated adjectives is covered too. An appendix delineates briefly the main ingredients of PTS. (shrink)

In the division problem with single-peaked preferences, an allocation rule is strategy-proof for same tops if no one can gain by reporting a false preference relation having the true peak. This new condition is so weak that it is implied by strategy-proofness and tops-only. We show that the uniform rule is the only rule satisfying this mild property under efficiency and envy-freeness. We then analyze how largely the preference domain can be extended with admitting a rule satisfying the three (...) axioms, and show that the single-plateaued domain is the unique such maximal domain. (shrink)

In this paper, we suggest the broader concept of proof-event, introduced by Joseph Goguen, as a fundamental methodological tool for studying proofs in history of mathematics. In this framework, proof is understood not as a purely syntactic object, but as a social process that involves at least two agents; this highlights the communicational aspect of proving. We claim that historians of mathematics essentially study proof-events in their research, since the mathematical proofs they face in the extant sources (...) involve many informal components, often not completely formalizable, and convey some kind of semantic content calling for understanding and verification. We illustrate the application of this methodological approach in some outstanding historical cases, paying particular attention to the process of proof interpretation that makes a proof-event alive. Finally, we suggest a classification of proof-events, according to the conditions imposed upon problem-solving. This enables us to speak about broad classes of proof-events in history of mathematics that share a common characteristic. (shrink)

The paper suggests a revision of the notion of harmony, a major necessary condition in proof-theoretic semantics for a natural-deduction proof-system to qualify as meaning conferring, when moving to a bilateral proof-system. The latter considers both forces of assertion and denial as primitive, and is applied here to positive logics, lacking negation altogether. It is suggested that in addition to the balance between (positive) introduction and elimination rules traditionally imposed by harmony, a balance should be imposed also (...) on: (i) negative introduction and elimination rules, and (ii) positive and negative introduction rules. The paper suggests a proof-theoretical definition of duality (not referring to truthtables), using which double harmony is defined. The paper proves that in a doubly-harmonious system, the coordination rule, typical to bilateral systems, is admissible. (shrink)

A cut-free Gentzen sequent calculus for Ewald’s intuitionistic tense logic \ is established. By the proof-theoretic method, we prove that, for every set of strictly positive implications S, the classical tense logic \ is embedded into its intuitionistic analogue \ via Kolmogorov, Gödel–Genzten and Kuroda translations respectively. A sufficient and necessary condition for Glivenko type theorem in tense logics is established.

Ever since antiquity, attempts have been made at defining knowledge through belief augmented by additional properties such as truth and justification. These characterizations have been challenged by Gettier counterexamples and their variants. A modern proposal, what is known as defeasibility theory, characterizes knowledge through stability under revision of beliefs on the basis of true or arbitrary information. A formal investigation of such a proposal calls for the methods of dynamic epistemic logic: well developed semantic approaches to dynamic epistemic logic have (...) been given through the plausibility models, but a corresponding proof theory is still in its infancy. We shall recast plausibility models in terms of more general neighbourhood models and develop on their basis complete proof systems. An inferential treatment of epistemic and doxastic notions such as safe belief will give a new way to study their relationships; among these, the characterization of knowledge as belief stable under arbitrary revision will be grounded through formal labelled sequent calculus derivations. (shrink)

This paper proposes an account of why proof is the only way to acquire knowledge of some mathematical proposition’s truth. Admittedly, non-deductive arguments for mathematical propositions can be strong and play important roles in mathematics. But this paper proposes a necessary condition for knowledge that can be satisfied by putative proofs (and proof sketches), as well as by non-deductive arguments in science, but not by non-deductive arguments from mathematical evidence. The necessary condition concerns whether we can justly expect (...) that if the mathematical proposition is actually false, despite the evidence for its truth, then this fact has an explanation. (shrink)

This book is the first detailed study of Kant's method of 'transcendental reflection' and its use in the Critique of Pure Reason to identify our basic human cognitive capacities, and to justify Kant's transcendental proofs of the necessary a priori conditions for the possibility of self-conscious human experience. Kenneth Westphal, in a closely argued internal critique of Kant's analysis, shows that if we take Kant's project seriously in its own terms, the result is not transcendental idealism but realism regarding physical (...) objects. Westphal attends to neglected topics - Kant's analyses of the transcendental affinity of the sensory manifold, the 'lifelessness of matter', fallibilism, the semantics of cognitive reference, four externalist aspects of Kant's views, and the importance of Kant's Metaphysical Foundations for the Critique of Pure Reason - that illuminate Kant's enterprise in new and valuable ways. His book will appeal to all who are interested in Kant's theoretical philosophy. (shrink)

The logic of Conditional Beliefs has been introduced by Board, Baltag, and Smets to reason about knowledge and revisable beliefs in a multi-agent setting. In this article both the semantics and the proof theory for this logic are studied. First, a natural semantics forCDLis defined in terms of neighbourhood models, a multi-agent generalisation of Lewis’ spheres models, and it is shown that the axiomatization ofCDLis sound and complete with respect to this semantics. Second, it is shown that the (...) neighbourhood semantics is equivalent to the original one defined in terms of plausibility models, by means of a direct correspondence between the two types of models. On the basis of neighbourhood semantics, a labelled sequent calculus forCDLis obtained. The calculus has strong proof-theoretic properties, in particular admissibility of contraction and cut, and it provides a decision procedure for the logic. Furthermore, its semantic completeness is used to obtain a constructive proof of the finite model property of the logic. Finally, it is shown that other doxastic operators can be easily captured within neighbourhood semantics. This fact provides further evidence of the naturalness of neighbourhood semantics for the analysis of epistemic/doxastic notions. (shrink)

The aim of this paper is to reconsider several proposals that have been put forward in order to develop a Proof-Theoretical Semantics, from the by now classical neo-verificationist approach provided by D. Prawitz and M. Dummett in the Seventies, to an alternative, more recent approach mainly due to the work of P. Schroeder-Heister and L. Hallnäs, based on clausal definitions. Some other intermediate proposals are very briefly sketched. Particular attention will be given to the role played by the so-called (...) Fundamental Assumption. We claim that whereas, in the neo-verificationist proposal, the condition expressed by that Assumption is necessary to ensure the completeness of the justification procedure ( from the outside , so to speak), within the definitional framework it is a built-in feature of the proposal. The latter approach, therefore, appears as an alternative solution to the problem which prompted the neo-verificationists to introduce the Fundamental Assumption. (shrink)

Curry's paradox for "if.. then.." concerns the paradoxical features of sentences of the form "If this very sentence is true, then 2+2=5". Standard inference principles lead us to the conclusion that such conditionals have true consequents: so, for example, 2+2=5 after all. There has been a lot of technical work done on formal options for blocking Curry paradoxes while only compromising a little on the various central principles of logic and meaning that are under threat. -/- Once we have a (...) sense of the technical options, though, a philosophical choice remains. When dealing with puzzles in the logic of conditionals, a natural place to turn is independently motivated semantic theories of the behaviour of "if... then...". This paper argues that the closest-worlds approach outlined in Nolan 1997 offers a philosophically satisfying reason to deny conditional proof and so block the paradoxical Curry reasoning, and can give the verdict that standard Curry conditionals are false, along with related "contraction conditionals". (shrink)

Motivated by a recent proof of free choices in linking equations to the experiments they describe, I clarify some relations among purely mathematical entities featured in quantum mechanics (probabilities, density operators, partial traces, and operator-valued measures), thereby allowing applications of these entities to the modeling of a wider variety of physical situations. I relate conditional probabilities associated with projection-valued measures to conditional density operators identical, in some cases but not in others, to the usual reduced density operators. (...) While a fatal obstacle precludes associating conditional density operators with general non-projective measures, tensor products of general positive operator-valued measures (POVMs) are associated with conditional density operators. This association together with the free choice of probe particles allows a postulate of state reductions to be replaced by a theorem. An application shows an equivalence between one form of quantum key distribution and another with respect to certain eavesdropping attacks. (shrink)

Questions concerning the proof-theoretic strength of classical versus nonclassical theories of truth have received some attention recently. A particularly convenient case study concerns classical and nonclassical axiomatizations of fixed-point semantics. It is known that nonclassical axiomatizations in four- or three-valued logics are substantially weaker than their classical counterparts. In this paper we consider the addition of a suitable conditional to First-Degree Entailment—a logic recently studied by Hannes Leitgeb under the label HYPE. We show in particular that, by formulating (...) the theory PKF over HYPE, one obtains a theory that is sound with respect to fixed-point models, while being proof-theoretically on a par with its classical counterpart KF. Moreover, we establish that also its schematic extension—in the sense of Feferman—is as strong as the schematic extension of KF, thus matching the strength of predicative analysis. (shrink)

Proof nets provide abstract counterparts to sequent proofs modulo rule permutations; the idea being that if two proofs have the same underlying proof-net, they are in essence the same proof. Providing a convincing proof-net counterpart to proofs in the classical sequent calculus is thus an important step in understanding classical sequent calculus proofs. By convincing, we mean that there should be a canonical function from sequent proofs to proof nets, it should be possible to check (...) the correctness of a net in polynomial time, every correct net should be obtainable from a sequent calculus proof, and there should be a cut-elimination procedure which preserves correctness.Previous attempts to give proof-net-like objects for propositional classical logic have failed at least one of the above conditions. In Richard McKinley [22], the author presented a calculus of proof nets satisfying and ; the paper defined a sequent calculus corresponding to expansion nets but gave no explicit demonstration of . That sequent calculus, called LK⁎LK⁎ in this paper, is a novel one-sided sequent calculus with both additively and multiplicatively formulated disjunction rules. In this paper [22]), we give a full proof of for expansion nets with respect to LK⁎LK⁎, and in addition give a cut-elimination procedure internal to expansion nets – this makes expansion nets the first notion of proof-net for classical logic satisfying all four criteria. (shrink)

This paper presents a justification counterpart for dyadic deontic logic, which is often argued to be better than Standard Deontic Logic at representing conditional and contrary-to-duty obligations, such as those exemplified by the notorious Chisholm’s puzzle. We consider the alethic-deontic system (E) and present the explicit version of this system (JE) by replacing the alethic Box-modality with proof terms and the dyadic deontic Circ-modality with justification terms. The explicit representation of strong factual detachment (SFD) is given and finally (...) soundness and completeness of the system (JE) with respect to basic models and preference models is established. (shrink)

The current paper studies the formal properties of the Global Reflection Principle, to wit the assertion “All theorems of$\mathrm {Th}$are true,” where$\mathrm {Th}$is a theory in the language of arithmetic and the truth predicate satisfies the usual Tarskian inductive conditions for formulae in the language of arithmetic. We fix the gap in Kotlarski’s proof from [15], showing that the Global Reflection Principle for Peano Arithmetic is provable in the theory of compositional truth with bounded induction only ($\mathrm {CT}_0$). Furthermore, (...) we extend the above result showing that$\Sigma _1$-uniform reflection over a theory of uniform Tarski biconditionals ($\mathrm {UTB}^-$) is provable in$\mathrm {CT}_0$, thus answering the question of Beklemishev and Pakhomov [2]. Finally, we introduce the notion of a prolongable satisfaction class and use it to study the structure of models of$\mathrm {CT}_0$. In particular, we provide a new model-theoretical characterization of theories of finite iterations of uniform reflection and present a new proof characterizing the arithmetical consequences of$\mathrm {CT}_0$. (shrink)

Sufficient conditions for first-order-based sequent calculi to admit cut elimination by a Schütte–Tait style cut elimination proof are established. The worst case complexity of the cut elimination is analysed. The obtained upper bound is parameterized by a quantity related to the calculus. The conditions are general enough to be satisfied by a wide class of sequent calculi encompassing, among others, some sequent calculi presentations for the first order and the propositional versions of classical and intuitionistic logic, classical and intuitionistic (...) modal logic S4, and classical and intuitionistic linear logic and some of its fragments. Moreover the conditions are such that there is an algorithm for checking if they are satisfied by a sequent calculus. (shrink)

Despite recent controversies surrounding the principle that knowledge entails truth (KT), this paper aims to prove that the principle is true. It offers a proof of (KT) in the following sense. It advances a deductively valid argument for (KT), whose premises are, by most lights, obviously true. Moreover, each premise is buttressed by at least two supporting arguments. And finally, all premises and supporting arguments can be rationally accepted by people who don’t already accept (KT).

In the first chapter, we discuss Dummett’s idea that the notion of truth arises from the one of the correctness of an assertion. We argue that, in a first-order language, the need of defining truth in terms of the notion of satisfaction, which is yielded by the presence of quantifiers, is structurally analogous to the need of a notion of truth as distinct from the one of correctness of an assertion. In the light of the analogy between predicates in Frege (...) and open formulas in Tarksi, we concentrate on the semantic status of predicates. We register a dual attitude of Dummett towards Frege’s ascription of reference to predicates. On the one it is needed to endow quantifiers with their appropriate meaning. On the other hand, the introduction of concepts, as semantic correlate of predicates, smuggles a realist flavor in the overall semantic picture. In concluding the excursus (and with it the chapter), we stress Dummett’s will of developing a semantic picture free from this realist trait. In the second chapter, we present the idea of a proof-theoretic semantics. As for Frege true sentences denotes the truth-value True, so here closed' (i.e. categorical) valid argumentations denotes proofs. If a language contains implication-like operators, in order to characterize the condition of validity of a closed argumentation one has to introduce a notion of validity applying to ‘open’ (i.e. hypothetical) argumentations. We argue that this problem is analogous to the one posed by quantifiers in Frege-Tarksi’s style semantics. That is, implication forces one to introduce notion of validity for argumentations, which is more substantial than the correctness of the assertion of their conclusions. As we saw, the corresponding claim in the truth-based approach—that quantifiers require one to introduce a notion of truth, which is more substantial than the one of an assertion being correct—was the source of realism. Hence, Dummett proposes to reduce the semantic contribution of open argumentations to the one of their ‘closed instances’. In the truth-based perspective, this would correspond to the denial of the need of introducing concepts as the semantic correlates of predicates. We argue that Dummett’s fear, that an irreducible notion of function (represented by the need of ascribing validity to open argumentations) would lead to realism, turns out to be ill-founded. In the third chapter, we discuss the role played by the notion of truth in the anti-realist account. The notion of truth is what the anti-realist needs to cope with the so-called paradox of deduction. The analysis of the paradox yields to distinguishing between the truth of a sentence and the truth of a sentence being recognized. In terms of these conceptual couple, we reconsider the relationship between truth and assertion in an anti-realist perspective. Grounds are provided for a thesis (which was already advanced in chapter two), according to which the notion of the assertion of a sentence being correct is primarily connected only with the canonical means of establishing a sentence. The possibility of establishing a sentence by indirect means is conceptually dependent on the practice of establishing logical relationship of dependence among sentences. That is, the notion of a closed valid non-canonical argumentation is of any theoretical relevance only in presence of a notion of validity applying to open argumentations. In the fourth chapter, we discuss the possibility of characterizing in the proof-theoretic-semantics a notion of refutation. We develop an original characterization of refutations starting from an informal inductive specification of the condition of refutations of logically complex sentences. A sub-structural logic, called dual-intuitionistic logic, stands to this notion in the same relationship in which intuitionistic logic stands to the notion of proof so far consdered. All notions developed in chapter 2 have their corresponding (dual) ones in the framework developed. In particular, the distinctions canonical/non-canonical and closed/open argumentations. In the refutation based perspective, elimination rules have priority over introductions and the (only) assumption over the (many) conclusions. In the conclusions, we indicate the ingredients that an anti-realist approach to meaning should incorporate, in order to avoid the difficulties we registered. The core of an alternative view is a different conception of the relationship between categorical and hypothetical notions, in which the validity of open argumentations is not reduced to that of their instances, but rather it is directly defined. As a limit case, one would get a notion of validity applying to closed argumentations. (shrink)

This mathematics textbook covers the fundamental ideas used in writing proofs. Proof techniques covered include direct proofs, proofs by contrapositive, proofs by contradiction, proofs in set theory, proofs of existentially or universally quantified predicates, proofs by cases, and mathematical induction. Inductive and deductive reasoning are explored. A straightforward approach is taken throughout. Plenty of examples are included and lots of exercises are provided after each brief exposition on the topics at hand. The text begins with a study of symbolic (...) logic, deductive reasoning, and quantifiers. Inductive reasoning and making conjectures are examined next, and once there are some statements to prove, techniques for proving conditional statements, disjunctions, biconditional statements, and quantified predicates are investigated. Terminology and proof techniques in set theory follow with discussions of the pick-a-point method and the algebra of sets. Cartesian products, equivalence relations, orders, and functions are all incorporated. Particular attention is given to injectivity, surjectivity, and cardinality. The text includes an introduction to topology and abstract algebra, with a comparison of topological properties to algebraic properties. This book can be used by itself for an introduction to proofs course or as a supplemental text for students in proof-based mathematics classes. The contents have been rigorously reviewed and tested by instructors and students in classroom settings. (shrink)

A proof by Allan Gibbard (Ifs: Conditionals, beliefs, decision, chance, time. Reidel, Dordrecht, 1981) seems to demonstrate that if indicative conditionals have truth conditions, they cannot be stronger than material implication. Angelika Kratzer's theory that conditionals do not denote two-place operators purports to escape this result [see Kratzer (Chic Linguist Soc 22(2):1–15, 1986, 2012)]. In this note, I raise some trouble for Kratzer’s proposed method of escape and then show that her semantics avoids this consequence of Gibbard’s proof (...) by denying modus ponens. I also show that the same holds for Anthony Gillies’ semantics (Philos Rev 118(3):325–349, 2009) and argue that this consequence of these theories is not obviously prohibitive—hence, both remain viable theories of indicative conditionals. (shrink)

A modified Young double-slit experiment proposed by Wootters and Zurek is considered in which a system P of parallel plates covered with a photographic emulsion has been set up in the region where we would normally expect the central interference fringes. Because under certain conditions P makes it possible to conclude with much more than50% certainty through which of the two slits each particular photon passed, the relevant interference pattern becomes blurred. It is proved that this implies a retroactive effect (...) because the setup of P and the interaction of photons with P appear to influence the momentum transferred to the photons by the edges of the slits at an earlier stage of the experiment. (shrink)

Constructive mathematics is based on the thesis that the meaning of a mathematical formula is given, not by its truth-conditions, but in terms of what constructions count as a proof of it. However, the meaning of the terms 'construction' and 'proof' has never been adequately explained (although Kreisel, Goodman and Martin-Löf have attempted axiomatisations). This monograph develops precise (though not wholly formal) definitions of construction and proof, and describes the algorithmic substructure underlying intuitionistic logic. Interpretations of Heyting (...) arithmetic and constructive analysis are given. The philosophical basis of constructivism is explored thoroughly in Part I. The author seeks to answer objections from platonists and to reconcile his position with the central insights of Hilbert's formalism and logic. Audience: Philosophers of mathematics and logicians, both academic and graduate students, particularly those interested in Brouwer and Hilbert; theoretical computer scientists interested in the foundations of functional programming languages and program correctness calculi. (shrink)

Inquiry into the metaphysics of essence tends to be pursued in a realist and model-theoretic spirit, in the sense that metaphysical vocabulary is used in a metalanguage to model truth conditions for the object-language use of essentialist vocabulary. This essay adapts recent developments in proof-theoretic semantics to provide a nominalist analysis for a variety of essentialist vocabularies. A metalanguage employing explanatory inferences is used to individuate introduction and elimination rules for atomic sentences. The object-language assertions of sentences concerning essences (...) are then interpreted as devices for marking off structural features of the explanatory inferences that, under a given interpretation, constitute the contents of the atoms of the language. On this proposal, object-language essentialist vocabulary is mentioned in a proof-theoretic metalanguage that uses a vocabulary of explanation. The result is a nominalist interpretation of essence as a modality, understood in the grammatical sense as a modification of the copula, and a view of metaphysical inquiry that is closely connected to the explanatory commitments present in first-order inquiry into things like sets, chemicals, and organisms. This result illustrates that some of the presuppositions that have animated analytic metaphysics over the last few decades can be profitably substituted with more practice-oriented conceptions of the forms of reasoning at work in different domains of human knowledge. (shrink)

The initial premise of this paper is that the structure of a proof is inherent in the definition of the proof. Side conditions to deal with the discharging of assumptions means that this does not hold for systems of natural deduction, where proofs are given by monotone inductive definitions. We discuss the idea of using higher order definitions and the notion of a functional closure as a foundation to avoid these problems. In order to focus on structural issues (...) we introduce a more abstract perspective, where a structural proof theory becomes part of a more general theory of functional closures. A notion of proof equations is discussed as a structural classifier and we compare the Russell and Ekman paradoxes to illustrate this. (shrink)

Proof-theoretic semantics (P-tS) is an innovative approach to grounding logical meaning in terms of proofs rather than traditional truth-conditional semantics. The point is not that one provides a proof system, but rather that one articulates meaning in terms of proofs and provability. To elucidate this paradigm shift, we commence with an introduction that contrasts the fundamental tenets of P-tS with the more prevalent model-theoretic approach to semantics. The contribution of this paper is a P-tS for a substructural (...) logic, intuitionistic multiplicative linear logic (IMLL). Specifically, we meticulously examine and refine the established P-tS for intuitionistic propositional logic. Subsequently, we present two novel and comprehensive forms of P-tS for IMLL. Notably, the semantics for IMLL in this paper embodies its resource interpretation through its number-of-uses reading (restricted to atoms). This stands in contrast to the conventional model-theoretic semantics of the logic, underscoring the value that P-tS brings to substructural logics. (shrink)

In different papers, Carnielli, W. & Rodrigues, A., Carnielli, W. Coniglio, M. & Rodrigues, A. and Rodrigues & Carnielli, present two logics motivated by the idea of capturing contradictions as conflicting evidence. The first logic is called BLE and the second—that is a conservative extension of BLE—is named LETJ. Roughly, BLE and LETJ are two non-classical logics in which the Laws of Explosion and Excluded Middle are not admissible. LETJ is built on top of BLE. Moreover, LETJ is a Logic (...) of Formal Inconsistency. This means that there is an operator that, roughly speaking, identifies a formula as having classical behavior. Both systems are motivated by the idea that there are different conditions for accepting or rejecting a sentence of our natural language. So, there are some special introduction and elimination rules in the theory that are capturing different conditions of use. Rodrigues & Carnielli’s paper has an interesting and challenging idea. According to them, BLE and LETJ are incompatible with dialetheia. It seems to show that these paraconsistent logics cannot be interpreted using truth-conditions that allow true contradictions. In short, BLE and LETJ talk about conflicting evidence avoiding to talk about gluts. I am going to argue against this point of view. Basically, I will firstly offer a new interpretation of BLE and LETJ that is compatible with dialetheia. The background of my position is to reject the one canonical interpretation thesis: the idea according to which a logical system has one standard interpretation. Then, I will secondly show that there is no logical basis to fix that Rodrigues & Carnielli’s interpretation is the canonical way to establish the content of logical notions of BLE and LETJ. Furthermore, the system LETJ captures inside classical logic. Then, I am also going to use this technical result to offer some further doubts about the one canonical interpretation thesis. (shrink)

The existence of objects external to the mind is a proof-condition for the type of object demonstration Moore provided in his famous lecture. Affirming the existence of objects external to the mind is just a way of saying that one person can show (present, demonstrate) something to another to prove it is so, to prove it exists, Demonstrations like that are conclusive and immune to scepticism.