In this paper I will develop a lambda-term calculus, lambda-2Int, for a bi-intuitionistic logic and discuss its implications for the notions of sense and denotation of derivations in a bilateralist setting. Thus, I will use the Curry-Howard correspondence, which has been well-established between the simply typed lambda-calculus and natural deduction systems for intuitionistic logic, and apply it to a bilateralist proof system displaying two derivability relations, one for proving and one for refuting. The basis will be the natural deduction system (...) of Wansing's bi-intuitionistic logic 2Int, which I will turn into a term-annotated form. Therefore, we need a type theory that extends to a two-sorted typed lambda-calculus. I will present such a term-annotated proof system for 2Int and prove a Dualization Theorem relating proofs and refutations in this system. On the basis of these formal results I will argue that this gives us interesting insights into questions about sense and denotation as well as synonymy and identity of proofs from a bilateralist point of view. (shrink)

Some thirty years ago, two proposals were made concerning criteria for identity of proofs. Prawitz proposed to analyze identity of proofs in terms of the equivalence relation based on reduction to normal form in natural deduction. Lambek worked on a normalization proposal analogous to Prawitz's, based on reduction to cut-free form in sequent systems, but he also suggested understanding identity of proofs in terms of an equivalence relation based on generality, two derivations having the (...) same generality if after generalizing maximally the rules involved in them they yield the same premises and conclusions up to a renaming of variables. These two proposals proved to be extensionally equivalent only for limited fragments of logic. The normalization proposal stands behind very successful applications of the typed lambda calculus and of category theory in the proof theory of intuitionistic logic. In classical logic, however, it did not fare well. The generality proposal was rather neglected in logic, though related matters were much studied in pure category theory in connection with coherence problems, and there are also links to low-dimensional topology and linear algebra. This proposal seems more promising than the other one for the general proof theory of classical logic. (shrink)

Dag Prawitz (1971) put forward the idea that an admissible reduction process does not affect the identity of proofs represented by derivations in natural deduction. The idea relies on his conjecture that two derivations represent the same proof if and only if they are equivalent in the sense that they are reflexive, transitive and symmetric closure of the immediate reducibility relation. Schroeder-Heister and Tranchini (2017) accept Prawitz’s conjecture and propose the triviality test as the criterion for admissible reductions. (...) In the present paper, we will consider two main troubles of the triviality test. The first is the obscurity of a method of evaluating admissible reductions. The second is the circularity problem that the triviality test already assumes the set of admissible reduction procedures. For the solution of the problems, we will propose the spoiler test which immunes the problems of the triviality test and has the role of the criterion for admissible reductions. At last, we shall cover a plausible problem of the spoiler test that can be caused by Crabbé’s case. (shrink)

We propose a novel, ontological approach to studying mathematical propositions and proofs. By “ontological approach” we refer to the study of the categories of beings or concepts that, in their practice, mathematicians isolate as fruitful for the advancement of their scientific activity (like discovering and proving theorems, formulating conjectures, and providing explanations). We do so by developing what we call a “formal ontology” of proofs using semantic modeling tools (like RDF and OWL) developed by the computer science community. (...) In this article, (i) we describe this new approach and, (ii) to provide an example, we apply it to the problem of the identity of proofs. We also describe open issues and further applications of this approach (for example, the study of purity of methods). We lay some foundations to investigate rigorously and at large scale intellectual moves and attitudes that underpin the advancement of mathematics through cognitive means (carving out investigationally valuable concepts and techniques) and social means (like communication, collaboration, revision, and criticism of specific categories, inferential patterns, and levels of analysis). Our approach complements other types of analysis of proofs such as reconstruction in a deductive system and examination through a proof-assistant. (shrink)

This article is a methodological discussion of formal approaches to the question of identity of proofs from a philosophical standpoint. First, an introduction to the question of identity of proofs itself is given, followed by a brief reconstruction of the so-called normalisation thesis, proposed by Dag Prawitz in 1971, in which some of its core mathematical and conceptual traits are presented. After that, a comparison between the normalisation thesis and the more well-known Church-Turing thesis on computability (...) is carried out in three main parts: the first dedicated to highlighting some of the analogies between them; the second, their most remarkable differences; and the third, to the possible relations of dependence between the two. Based on these considerations, some concluding remarks concerning the potential of the normalisation thesis and similar approaches to the question of identity of proofs are made in the last section. (shrink)

This open access book investigates the role played by identity of proofs in proof-theoretic semantics. It develops a conception of proof-theoretic semantics as primarily concerned with the relationship between proofs (understood as abstract entities) and derivations (the linguistic representations of proofs). It demonstrates that identity of proof is a key both to clarify some —still not wholly understood— notions at the core of proof-theoretic semantics, such as harmony; and to broaden the range of the phenomena (...) which can be analyzed using the tools of this semantic paradigm, so as to include for instance paradoxes. The volume covers topics such as the philosophical significance of different criteria of identity of proofs, and adequacy conditions for an intensional account of the notion of harmony. The author also examines the Prawitz-Tennant analysis of paradoxes by investigating on the one hand the prospects of turning it into a theory of meaning for paradoxical languages, and on the other hand two distinct kinds of phenomena, first observed by Crabbe and Ekman, showing that the Tennant-Prawitz criterion for paradoxicality overgenerates. This volume is of interest to scholars in formal and philosophical logic. (shrink)

The generality of a derivation is an equivalence relation on the set of occurrences of variables in its premises and conclusion such that two occurrences of the same variable are in this relation if and only if they must remain occurrences of the same variable in every generalization of the derivation. The variables in question are propositional or of another type. A generalization of the derivation consists in diversifying variables without changing the rules of inference. This paper examines in the (...) setting of categorial proof theory the conjecture that two derivations with the same premises and conclusions stand for the same proof if and only if they have the same generality. For that purpose generality is defined within a category whose arrows are equivalence relations on finite ordinals, where composition is rather complicated. Several examples are given of deductive systems of derivations covering fragments of logic, with the associated map into the category of equivalence relations of generality. This category is isomorphically represented in the category whose arrows are binary relations between finite ordinals, where composition is the usual simple composition of relations. This representation is related to a classical representation result of Richard Brauer. (shrink)

The essential structure of proofs is proposed as the basis for a measure of complexity of formulas in FOL. The motivating idea was the recognition that distinct theorems can have the same derivation modulo some non essential details. Hence the difficulty in proving them is identical and so their complexity should be the same. We propose a notion of complexity of formulas capturing this property. With this purpose, we introduce the notions of schema calculus, schema derivation and description complexity (...) of a schema formula. Based on these concepts we prove general robustness results that relate the complexity of introducing a logical constructor with the complexity of the component schema formulas as well as the complexity of a schema formula across different schema calculi. (shrink)

Families of types are fundamental objects in Martin-Löf type theory. When extending the notion of setoid (type with an equivalence relation) to families of setoids, a choice between proof-relevant or proof-irrelevant indexing appears. It is shown that a family of types may be canonically extended to a proof-relevant family of setoids via the identity types, but that such a family is in general proof-irrelevant if, and only if, the proof-objects of identity types are unique. A similar result is (...) shown for fibre representations of families. The ubiquitous role of proof-irrelevant families is discussed. (shrink)

Leibniz propôs que demonstrações fossem reformuladas como deduções a partir de identidades, e que proposições do tipo A = A fossem a fonte única de verdade. Neste artigo, procuro explicar essa teoria da prova (e do conhecimento), assim como seus conceitos elementares, ou seja, os conceitos de identidade, verdade (ou possibilidade) e proposição (inclusive a teoria leibniziana da redutibilidade a proposições sujeito-predicado). Leibniz proposed that demonstrations be reformulated as deductions from identities, and that propositions of the type A = A (...) be the only source of truth. In this article, I aim to explain this theory of proof (and knowledge), as well as its elementary concepts, such as identity, truth (or possibility) and proposition (including Leibniz's theory of reducibility of propositions to subject-predicate form). (shrink)

This is an abstract of the paper to be submitted to Houston Journal of Mathematics. Our nomenclature and notation will be basically those of [3]. We shall consider algebras of type : T ! N, where T is a nonempty set, and N the set of all positive integers. By V we denote the set of all variables occurring in a polynomial symbol p. An identity p = q is called strongly non-regular if it is of the form p (...) = x for some binary polynomial symbol p, such that x; y 2 V and x =6 y. Let R denote the set of all regular identities of type . If K is a class of algebras of type , then E denotes the set of all identities satised by all algebras in K. We put R = E \ R. A variety K is called strongly non-regular if E contains some strongly non-regular identity. If is a set of identities of type , then K denotes the variety of algebras of type generated by ; E() will be the set of all identities which are consequences of . We put R() = E() \ R. We write ` e if there exists a nite proof of e starting from. (shrink)

We present two proof systems for first-order logic with identity and without function symbols. The first one is an extension of the Rasiowa-Sikorski system with the rules for identity. This system is a validity checker. The rules of this system preserve and reflect validity of disjunctions of their premises and conclusions. The other is a Tableau system, which is an unsatisfiability checker. Its rules preserve and reflect unsatisfiability of conjunctions of their premises and conclusions. We show that the (...) two systems are dual to each other. The duality is expressed in a formal way which enables us to define a transformation of proofs in one of the systems into the proofs of the other. (shrink)

This paper draws attention to a proof of the necessity of identity given by Arthur Prior. In its simplicity, it is comparable to a proof of Quine's, popularised by Kripke, but it is slightly different. Prior's Polish notation is transcribed into a more familiar idiom. Prior's proof is followed by a proof of the necessity of difference, possibly the first such proof in the literature, which is also repeated here and transcribed. The paper concludes with a brief discussion of (...) Prior's views on identity and difference over time. (shrink)

Lindström’s theorem obviously fails as a characterization of first-order logic without identity ( $\mathcal {L}_{\omega \omega }^{-} $ ). In this note, we provide a fix: we show that $\mathcal {L}_{\omega \omega }^{-} $ is a maximal abstract logic satisfying a weak form of the isomorphism property (suitable for identity-free languages and studied in [11]), the Löwenheim–Skolem property, and compactness. Furthermore, we show that compactness can be replaced by being recursively enumerable for validity under certain conditions. In the (...) proofs, we use a form of strong upwards Löwenheim–Skolem theorem not available in the framework with identity. (shrink)

Saint Anselm’s proof for God’s existence in his Proslogion, as the label “ontological” retrospectively hung on it indicates, is usually treated as involving some sophisticated problem of, or a much less sophisticated tampering with, the concept of existence. In this paper I intend to approach Saint Anselm’s reasoning from a somewhat different angle.

A resurgence of scholarly work on proof of God?s existence is noticeable over the past decade, with considerable emphasis on attempts to provide?analytic proof? based on the meanings and logic of various identity statements which constitute premises of the syllogisms of the?proof?. Most recently perhaps, Emmanuel Rutten?s?modal-epistemic proof? has drawn serious academic attention. Like other?analytic? and strictly logical proofs of God?s existence, Rutten?s proof has been found flawed. In this paper I discuss the possibility of an?ethics-based? identity (...) proof of God?s existence. Such a proof, the first version of which, I believe, has been offered, indirectly, by Nikolai Lossky, utilizes the form and structure of the analytic proof, but fundamentally rests on the perception of moral values we associate with God and Godliness. The nature of the proof shifts the focus of the very attempt to?prove? God?s existence from what I believe is an unreasonable standard, unattainable even in?proving? the existence of the more mundane world, towards a more functional, practical and attainable standard. The proof proposed initially by Lossky, and in a more systematic form here, I believe, shows the indubitable existence of God in the sense of his moral presence in the lives of the faithful, at least with the same degree of certainty as the presence or?existence? of anything else that can be epistemically proven in principle. (shrink)

In considering the possibility that the fundamental particles of matter might violate Leibniz's Principle, one is confronted with logical proofs that the Principle is a Theorem of Logic. This paper shows that the proof of that theorem is not universal enough to encompass entities that might not be unique, and also strongly suggests that photons, for example, do violate Leibniz's Principle. It also shows that the existence of non-individuals would imply the breakdown of Quine's criterion of ontological commitment.

In his Grundgesetze, §32, Frege launched the idea that the meaning of a sentence is given by its truth condition, or, in his particular version, the condition under which it will be a name of the True. This, indeed, was only one of the many roles in which truth has to serve within the Fregean system. In particular, truth is an absolute notion in the sense that bivalence holds: every Gedanke is either true or false, in complete independence of any (...) conative activity, whether by God or man. Thus various epistemological notions, such as the correctness of an assertion made, or judgement passed, are reducible to this absolute notion of truth: an assertion made through the utterance of a declarative sentence is correct when the proposition expressed by the sentence in question is true. Given this absolute status of truth it is not surprising that Frege is of the opinion that truth is a sui generis notion which has to be left unanalyzed and, indeed, which is indefinable. (shrink)

We consider an approach to propositional synonymy in proof-theoretic semantics that is defined with respect to a bilateral G3-style sequent calculus \(\mathtt{SC2Int}\) for the bi-intuitionistic logic \(\mathtt{2Int}\). A distinctive feature of \(\mathtt{SC2Int}\) is that it makes use of two kind of sequents, one representing proofs, the other representing refutations. The structural rules of \(\mathtt{SC2Int}\), in particular its cut rules, are shown to be admissible. Next, interaction rules are defined that allow transitions from proofs to refutations, and vice versa, (...) mediated through two different negation connectives, the well-known implies-falsity negation and the less well-known coimplies-truth negation of \(\mathtt{2Int}\). By assuming that the interaction rules have no impact on the identity of derivations, the concept of inherited identity between derivations in \(\mathtt{SC2Int}\) is introduced and the notions of positive and negative synonymy of formulas are defined. Several examples are given of distinct formulas that are either positively or negatively synonymous. It is conjectured that the two conditions cannot be satisfied simultaneously. (shrink)

The topic of identity of proofs was put on the agenda of general (or structural) proof theory at an early stage. The relevant question is: When are the differences between two distinct proofs (understood as linguistic entities, proof figures) of one and the same formula so inessential that it is justified to identify the two proofs? The paper addresses another question: When are the differences between two distinct formulas so inessential that these formulas admit of identical (...) proofs? The question appears to be especially natural if the idea of working with more than one kind of derivations is taken seriously. If a distinction is drawn between proofs and disproofs (or refutations) as primitive entities, it is quite conceivable that a proof of one formula amounts to a disproof of another formula, and vice versa. A notion of inherited identity of derivations is introduced for derivations in a cut-free sequent system for Almukdad and Nelson’s constructive paraconsistent logic N4 with strong negation. The notion is obtained by identifying sequent rules the application of which has no effect on the identity of derivations. Then the notion of inherited identity is used to define a bilateralist notion of synonymy between formulas, which is a relation drawing more fine-grained distinctions between formulas than strong equivalence. (shrink)

We introduce three formal theories of increasing strength for linear algebra in order to study the complexity of the concepts needed to prove the basic theorems of the subject. We give what is apparently the first feasible proofs of the Cayley–Hamilton theorem and other properties of the determinant, and study the propositional proof complexity of matrix identities such as AB=I→BA=I.

The aim of this chapter is to explore to some extent the relationship between identity and necessity in logic and metaphysics. First, I provide a historically-based summary of proofs of the necessity of identity, highlighting the importance of the role that self-identity plays. Second, I introduce two examples of metaphysical topics where the necessity of identity has played a pivotal role: the necessary a posteriori, and the coincidence of material objects. I argue that important aspects (...) of these debates rest on how we represent identity. Third, I consider some recent work on generalized identity. This opens up new prospects for explaining why identity is necessary. (shrink)

I explore, from a proof-theoretic perspective, the hierarchy of classical and paraconsistent logics introduced by Barrio, Pailos and Szmuc in (Journal o f Philosophical Logic,49, 93-120, 2021). First, I provide sequent rules and axioms for all the logics in the hierarchy, for all inferential levels, and establish soundness and completeness results. Second, I show how to extend those systems with a corresponding hierarchy of validity predicates, each one of which is meant to capture “validity” at a different inferential level. Then, (...) I point out two potential philosophical implications of these results. (i) Since the logics in the hierarchy differ from one another on the rules, I argue that each such logic maintains its own distinct identity (contrary to arguments like the one given by Dicher and Paoli in 2019). (ii) Each validity predicate need not capture “validity” at more than one metainferential level. Hence, there are reasons to deny the thesis (put forward in Barrio, E., Rosenblatt, L. & Tajer, D. (Synthese, 2016)) that the validity predicate introduced in by Beall and Murzi in (Journal o f Philosophy,110(3), 143–165, 2013) has to express facts not only about what follows from what, but also about the metarules, etc. (shrink)

I conclude that it is more accurate to say that, rather than trying to make logic metaphysical, Leibniz tries, in the context of a theistic system, to make metaphysics logical. ;I begin with a study of the principle of identity of indiscernibles, and show how it is best thought of as a principle which follows from a metaphysical interpretation of the principle of sufficient reason. It has been traditional to interpret the principle of identity of indiscernibles as primarily (...) a merely logical principle, and thus as either trivially true, if Leibniz succeeds in proving it, or else false or contingently true. I argue that it is instead necessarily true in a non-trivial or metaphysical sense, because the principles on which it is based are themselves of this metaphysical character, contrary to what is often assumed. ;In the second chapter, I show how God's activity and a metaphysical interpretation of the principle of sufficient reason underlie Leibniz's account of space and time. ;In the third chapter, I discuss the principle of sufficient reason in detail, showing that it actually consists of three separate principles: the principle of grounds, that every true proposition has a proof a priori; the principle of reason, that God does nothing without a sufficient reason; and the principle of causation, that every event has a cause. That each of these is considered a principle of sufficient reason is explained by Leibniz's equivocal use of the term 'reason.' I show that, of the various versions of the principle of sufficient reason, only the principle of reasons provides an adequate foundation for Leibniz's principle of identity of indiscernibles and theory of space and time. Furthermore, since chapters one and two show how the activity of God is presupposed by Leibniz's metaphysics, for Leibniz to derive his metaphysics from his logic, as some would have us suppose, he would have to provide a satisfactory a priori demonstration of God's existence. But this, I argue, he cannot do. Thus God's existence and rationality, rather than subject-predicate logic, are the foundations of Leibniz's metaphysics. ;It is commonplace, when writing about Leibniz, to give primacy to his logic over his metaphysics, and indeed to try to assimilate the latter to the former. In this essay, however, I give priority to Leibniz's metaphysical pronouncements, apart, as much as possible, from logical and linguistic considerations. (shrink)

Normal 0 false false false MicrosoftInternetExplorer4 /* Style Definitions */ table.MsoNormalTable {mso-style-name:"Table Normal"; mso-tstyle-rowband-size:0; mso-tstyle-colband-size:0; mso-style-noshow:yes; mso-style-parent:""; mso-padding-alt:0in 5.4pt 0in 5.4pt; mso-para-margin:0in; mso-para-margin-bottom:.0001pt; mso-pagination:widow-orphan; font-size:10.0pt; font-family:"Times New Roman"; mso-ansi-language:#0400; mso-fareast-language:#0400; mso-bidi-language:#0400;} Focusing mainly on a number of unpublished texts by Collingwood, especially his “Lectures on the Ontological Proof of the Existence of God,” the study examines the English philosopher’s innovative interpretation of the Anselm’s main contribution to the philosophical-theological tradition. Collingwood insightfully shows how the ontological argument can be used in (...) analyzing and discussing the religious experience, not in trying to formulate a logical proof of God’s existence. When abstracted from the individual’s practical religious life, that is, from the experience of prayer, worship, and the like, mind’s awareness of God cannot be understood. Resorting mainly to Anselm, Augustine, Thomas Aquinas, and Descartes, Collingwood argues that the externality of the Platonic absolute is that of an absolute transcendent whereas the Christian God is not only conceived as the transcendent cause of all things, but also as the immanent spirit in them. By asserting the unity of the mind—regarded as identical with its acts—this interpretation is meant to serve both as a means towards self-knowledge, and as a starting point for a future conceptual unification of religion and philosophy. (shrink)

In lieu of an abstract, here is a brief excerpt of the content:Feminist Studies 41, no. 3. © 2015 by Feminist Studies, Inc. 623 Jaye Cee Whitehead, Kath Bassett, Leia Franchini, and Michael Iacolucci “The Proof Is in the Pudding”: How Mental Health Practitioners View the Power of “Sex Hormones” in the Process of Transition In the United States today, popular discourse touts the power of “sex hormones” and hormone receptors in the brain to chemically produce gender expressions (manifested in (...) physical sex traits, behaviors, and attitudes) and identities (a sense of self as feminine or masculine). These accounts range from common assumptions that Western ideals of femininity (such as empathy understanding, cooperative orientation, nurturing behavior) and masculinity (rational/spatial understanding, competitive orientation, violent behavior) are produced by corresponding sex hormones, to studies that reduce complex gender identities and macrosocial economic phenomena to presocial, binary, hormonal processes.1 For sociologists, accounts that reduce complex identities to internal hormonal reactions are problematic for two primary reasons: first, they are inaccurate because they fail to examine how hormonal reactions are embedded in a complex cultural process of meaning and interpretation; second, they operate as bioreductive ideologies that obscure the social power inherent to the process of gender identity construction. In what follows, we extend both of these insights by examining mental health 1. For an example of a hybrid popular-scientific account of the power of sex hormones to destabilize economic structures, see Jon Coates and Joe Herbert, “Endogenous Steroids and Financial Risk Taking on a London Trading Floor,” Proceedings of the National Academy of Sciences 105, no. 16 (April 2008): 6167–72. 624 Whitehead, Bassett, Franchini, and Iacolucci practitioners’ divergent interpretations of the power of sex hormones in the process of gender transition.2 In doing so, we examine the cultural power of sex hormones in crafting gender identities without reproducing reductionist interpretations of trans embodiment. Perhaps what is most perplexing about the way we speak of sex hormones is that we know it is inaccurate to describe these hormones as sexed; scientists have acknowledged since the 1930s that they are neither sex specific in their function, nor in terms of their location in male or female bodies.3 In her extensive historicization of sex hormones, Anne Fausto-Sterling concludes that it is more accurate to call androgen- and estrogen-based hormones, “steroid hormones” as they have functions that are not confined to corresponding sexed bodies. In fact she urges scientists to “break out of the sex hormone straightjacket” and to look at steroids as just one of a number of components that are important to the creation of sex and gender, including environment and experience.4 Scholars also point to an inextricable link between the chemical operation of hormones and the social process of constructing meaning, both at the level of social interaction and macrocultural constructions of sex categories and gender ideologies.5 While brain organization/activation theory attributes sex and gender differences to hormonal interactions within the developing brain, Fausto-Sterling questions the distinction between activation and organization by pointing out how “the brain can respond to hormonal stimuli with anatomical changes…hormonal systems, after all, respond exquisitely to experience, be it in the form of nutrition, stress, or sexual activity (to name but a few possibilities ).”6 Drawing from Elizabeth Grosz, Fausto-Sterling argues that the power of hormones is best understood according to the model of the 2. “Gender transition” is a controversial phrase, as it implies that transgendered individuals who receive hormone therapy are changing identities. We are only using it for lack of clear alternative phrasing, not because we believe body modifications change gender identities. 3. See Anne Fausto-Sterling, Sexing the Body: Gender Politics and the Construction of Sexuality (New York: Basic Books, 2000); Rebecca Jordan-Young, Brainstorm: The Flaws in the Science of Sex Differences (Cambridge, MA: Harvard University Press, 2010); and Nelly Oudshoorn, Beyond the Natural Body: An Archeology of Sex Hormones (New York: Routledge, 1994). 4. Fausto-Sterling, Sexing the Body, 193–94. 5. Fausto-Sterling, Sexing the Body. 6. Ibid., 232. Whitehead, Bassett, Franchini, and Iacolucci 625 Möbius strip, wherein internal components of the self are always connected to and continuous with outer components such as culture and environment.7 In other... (shrink)

The analysis of identity as coreference is strongly associated with Frege ; it is the view in Begriffsschrift, and, some have argued, henceforth throughout his work. This thesis is incorrect: Frege never held that identity is coreference. The case is made not by interpretation of “proof-quotes”, but rather by exploring how Frege actually deploys the concept. Two cases are considered. The first, from Grundgesetze, are the definitions of the core concepts, zero and truth; the second, from Begriffsschrift, is (...) the validity of Leibniz's Law. In both cases, if identity is coreference, results ensue that would be unacceptable to Frege. (shrink)

It has been argued that reduction procedures are closely connected to the question about identity of proofs and that accepting certain reductions would lead to a trivialization of identity of proofs in the sense that every derivation of the same conclusion would have to be identified. In this paper it will be shown that the question, which reductions we accept in our system, is not only important if we see them as generating a theory of proof (...) identity but is also decisive for the more general question whether a proof has meaningful content. There are certain reductions which would not only force us to identify proofs of different arbitrary formulas but which would render derivations in a system allowing them meaningless. To exclude such cases, a minimal criterion is proposed which reductions have to fulfill to be acceptable. (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)

The “erasing race” effect is the reduction of the salience of “race” as an alliance cue when recalling coalition membership, once more accurate information about coalition structure is presented. We conducted a random-effects model meta-analysis of this effect using five United States studies (containing nine independent effect sizes). The effect was found (ρ = 0.137, K = 9, 95% CI = 0.085 to 0.188). However, no decline effect or moderation effects were found (a “decline effect” in this context would be (...) a decrease in the effect size over time). Furthermore, we found little evidence of publication bias. Synthetically correcting the effect size for bias stemming from the use of an older method for calculating error base rates reduced the magnitude of the effect, but the it remained significant. Taken together, these findings indicate that the “erasing race” effect generalizes quite well across experimental contexts and would, therefore, appear to be quite robust. We reinterpret the theoretical basis for these effects in line with Brunswikian evolutionary-developmental theory and present a series of predictions to guide future research in this area. (shrink)

The traditional standard quantum mechanics theory is unable to solve the spin–statistics problem, i.e. to justify the utterly important “Pauli Exclusion Principle”. A complete and straightforward solution of the spin–statistics problem is presented on the basis of the “conformal quantum geometrodynamics” theory. This theory provides a Weyl-gauge invariant formulation of the standard quantum mechanics and reproduces successfully all relevant quantum processes including the formulation of Dirac’s or Schrödinger’s equation, of Heisenberg’s uncertainty relations and of the nonlocal EPR correlations. When the (...) conformal quantum geometrodynamics is applied to a system made of many identical particles with spin, an additional constant property of all elementary particles enters naturally into play: the “intrinsic helicity”. This property, not considered in the Standard Quantum Mechanics, determines the correct spin–statistics connection observed in Nature. (shrink)

Since the beginning of human history, there has been no society that did not have any religion. Man meets his need to believe, encoded in his nature by turning to God. God has not left humans alone in their journey on earth, and from time to time, He has intervened in the world through his prophets. The prophethood, which constitutes one of the main subjects of theology, is an important institution in God-human communication. The messengers chosen by God convey to (...) people the information that they received through revelation and offer teachings that will bring them to salvation. The idea of salvation by God when suffering or feeling helpless has driven people to the expectation of a savior. Nearly all religions except Shintoism have the awaited savior belief in the world. Accordingly, the savior will emerge in an environment of chaos where disasters are experienced, and a moral collapse is observed. The expected savior will drive people away from this turmoil, bring them happiness, well-being, and lead them to salvation. Although there is a savior belief in Judaism and Christianity, Muslims claim that the awaited savior in these religions is Muhammad. Muslim thinkers who believe that Muhammad was heralded in previous scripts, tried to find evidence on the subject from the Bible. One of the Islamic scholars who did researches for this purpose is Shamsuddin al-Samarqandi. Shamsuddin Mohammed b. Ashraf al-Husayni al-Samarqandi is an important Turkish-Islamic scholar who lived in Turkestan at the end of the 7th century and the first quarter of the 8th century. Samarqandi is a versatile scholar who produced important works in various fields such as philosophy, logic, mathematics, discussion, debate and astronomy. Shamsuddin al-Samarqandi is one of the eminent scholars who have written his name in the history of science and philosophy with his works. He adopted a critical and analytical style in almost every field, putting the science of logic at the center of his system. His constructive criticisms had an important function in understanding and interpreting the ideas of numerous thinkers, from Greek philosophers to Islamic philosophers and representatives of philosophical theology. In addition to all these, Samarqandi did not hesitate to criticize the Christian and Jewish belief systems, religions such as Sanawiyyah and Zoroastrianism, and the teachings of the naturalist philosophers regarding the relationship between God and the world in the light of rational and scriptural evidence. Samarqandi, who distinguished himself in rational sciences, also showed himself with his background in theology. Due to his exceptional intellectual interest, he analyzes some key concepts and divine codes related to the Bible, making original inferences about the loyalty of Muhammad, the prophet of Islam. Samarqandi interprets some passages of the Torah and the New Testament, which he considers as signs of Muhammad's prophethood, in the axis of language, logic and the rules of shariah, and concludes that Muhammad is the last prophet to be announced. The conceptual framework that he mostly focuses on in this regard contains Mount Paran, Paraklite, comparison with Moses, and the good news given to the Ishmaelites. Samarqandi makes inferences about the environment in which Muhammad appeared, his qualities, and his lineage, based on the aforementioned concepts. Samarqandi also responds to the criticisms raised by the Ahl al-Kitab about the principles, such as the abolition of other religious rules constituting the basis of Muhammad's legitimacy and establishment of Islam instead, and him being a universal prophet. An important privilege of Samarqandi is that he not only grounds his claims on a theoretical scale but also engages in debates with the leaders of the Ahl al-Kitab. Although Samarqandi exhibits a satisfactory analytical attitude in most of his claims, he displays a sophisticated approach based on the method of coercion (ilzām) in some of his claims. Although he adheres to the tradition of beshair al-nubuwwah in general, he gives a different perspective and strong reasoning to the same evidence within the tradition with the effect of his identity as a verifier (muhaqqik). (shrink)

I give an account of proof terms for derivations in a sequent calculus for classical propositional logic. The term for a derivation δ of a sequent Σ≻Δ encodes how the premises Σ and conclusions Δ are related in δ. This encoding is many–to–one in the sense that different derivations can have the same proof term, since different derivations may be different ways of representing the same underlying connection between premises and conclusions. However, not all proof terms for a sequent Σ≻Δ (...) are the same. There may be different ways to connect those premises and conclusions. -/- Proof terms can be simplified in a process corresponding to the elimination of cut inferences in sequent derivations. However, unlike cut elimination in the sequent calculus, each proof term has a unique normal form (from which all cuts have been eliminated) and it is straightforward to show that term reduction is strongly normalising—every reduction process terminates in that unique normal form. Further- more, proof terms are invariants for sequent derivations in a strong sense—two derivations δ1 and δ2 have the same proof term if and only if some permutation of derivation steps sends δ1 to δ2 (given a relatively natural class of permutations of derivations in the sequent calculus). Since not every derivation of a sequent can be permuted into every other derivation of that sequent, proof terms provide a non-trivial account of the identity of proofs, independent of the syntactic representation of those proofs. (shrink)

Some people think that grounding is a type of identity. And some people think that grounding connections hold necessarily. I show that, under plausible assumptions, if grounding is a type of identity, then grounding connections hold necessarily.

At some step in proving the Liar Paradox in natural language, a sentence is derived that seems overdetermined with respect to its semantic value. This is complemented by Tarski’s Theorem that a formal language cannot consistently contain a naive truth predicate given the laws of logic used in proving the Liar paradox. I argue that proofs of the Eubulidean Liar either use a principle of truth with non-canonical names in a fallacious way or make a fallacious use of substitution (...) of identicals. Tarski never committed the first fallacy and may have himself considered it fallacious. Nevertheless, I clarify that it is fallacious. I then argue substitution of identicals needs to be restricted within the scope of the truth predicate. A logic for truth implementing this restriction is a monotonic extension of a classical first order logic, or indeed a formalizable fragment of natural language. Proofs of Tarski’s Indefinability of Truth theorem are invalid in this logic. This approach generalizes to invalidate proofs of Liar-like paradoxes, particularly the predicate form of the Knower paradox. Consequently, such a logic can be further extended in a way that avoids Montague’s theorem for such a system. Yet, the semantic status of a Liar sentence is not fully resolved. It is no longer overdetermined; it is now underdetermined. (shrink)

From the point of view of proof-theoretic semantics, we examine the logical background invoked by Neil Tennant's abstractionist realist account of mathematical existence. To prepare the way, we must first look closely at the rule of existential elimination familiar from classical and intuitionist logics and at rules governing identity. We then examine how well free logics meet the harmony and uniqueness constraints familiar from the proof-theoretic semantics project. Tennant assigns a special role to atomic formulas containing singular terms. This, (...) we find, secures harmony and uniqueness but militates against the putative realism. (shrink)

I explain why model theory is unsatisfactory as a semantic theory and has drawbacks as a tool for proofs on logic systems. I then motivate and develop an alternative, the truth-valuational substitutional approach (TVS), and prove with it the soundness and completeness of the first order Predicate Calculus with identity and of Modal Propositional Calculus. Modal logic is developed without recourse to possible worlds. Along the way I answer a variety of difficulties that have been raised against TVS (...) and show that, as applied to several central questions, model-theoretic semantics can be considered TVS in disguise. The conclusion is that the truth-valuational substitutional approach is an adequate tool for many of our logic inquiries, conceptually preferable over model-theoretic semantics. Another conclusion is that formal logic is independent of semantics, apart from its use of the notion of truth, but that even with respect to it its assumptions are minimal. (shrink)

A Neuroscientist Offers Evidence of Where the Brain Ends and Consciousness Begins.