There is no consensus concerning how to understand the ‘two-step proof structure’ (§§15–20, 21–7) of the Transcendental Deduction in the B-edition of the Critique of Pure Reason. This disagreement invites a closer examination of what Kant might have meant by a ‘transcendental deduction’. I argue that the transcendental deduction consists of three tasks that parallel Kant’s broader project of a ‘critique’ of pure reason; first, an origin task to justify reason’s authority to use them; second, an analytical (...) task that determines the conditions under which this authority can be legitimately exercised; and third, a dialectical task to determine the conditions under which this authority cannot be legitimately exercised. So long as we continue to read the B-Deduction solely in terms of its two-step proof structure, we overlook how Kant’s notion of ‘critique’ constitutes the real grounds for his argumentative strategy there. (shrink)

Kant wrote two versions of the Transcendental Deduction, the first, “A-”Deduction in 1781, and the second, “B-”Deduction in 1787. Since Henrich's “The Proof Structure of Kant's Transcendental Deduction”, most work on the Transcendental Deduction attempts to make sense of the B-Deduction's two-step argument structure. Though the A-Deduction has suffered comparative neglect, it has received some attention from interpreters who take its extended treatment of the “subjective” side of cognition to amount to a brand of proto-functionalism. Whatever (...) the merits and demerits of these proto-functionalist approaches, they tend to deemphasize the two arguments that constitute the “objective” side of the A-Deduction, the “argument from above” and then the “argument from below”. Since Kant himself refers to this objective side of the A-Deduction as the “Deduction of the Pure Concepts of the Understanding”, it is surprising that the structure of these arguments has not received closer scrutiny. This is doubly true since Kant actually claims that his revisions for the 1787 version of the Deduction impacted only the “presentation” of it. Any lessons learned from the central arguments of the A-Deduction should help clarify the structure of its younger and more closely studied brother. (shrink)

Since the publication of Dieter Henrich's classic paper, ‘The proof structure of the transcendental deduction’, in The Review of Metaphysics 22 , the transcendental deduction of the pure concepts of the understanding has been under focus in Kant studies in a very special way. The B-deduction seems to be a proof in two steps. Consequently, the focus has been on questions like, ‘What is the structure of the deduction?’, and ‘Why is the deduction carried out in (...) two steps?’ No doubt the structure of the deduction has been the most debated exegetical issue in Kant's theoretical philosophy, and the most important too, while the answers mirror one's overall understanding of Kant. (shrink)

Hence, there is still controversy over which of the two versions of the deduction deserves priority and whether indeed any distinction between them can be maintained that would go beyond questions of presentation and involve the structure of the proof itself. Schopenhauer and Heidegger held that the first edition alone fully expresses Kant's unique philosophy, while Kant himself, as well as many other Kantians, have only seen a difference in the method of presentation.

Kant's A-Edition objective deduction is naturally (and has traditionally been) divided into two arguments: an " argument from above" and one that proceeds " von unten auf." This would suggest a picture of Kant's procedure in the objective deduction as first descending and ascending the same ladder, the better, perhaps, to test its durability or to thoroughly convince the reader of its soundness. There are obvious obstacles to such a reading, however; and in this chapter I will argue that the (...) arguments from above and below constitute different, albeit importantly inter-related, proofs. Rather than drawing on the differences in their premises, however, I will highlight what I take to be the different concerns addressed and, correspondingly, the distinct conclusions reached by each. In particular, I will show that both arguments can be understood to address distinct specters, with the argument from above addressing an internal concern generated by Kant’s own transcendental idealism, and the argument from below seeking to dispel a more traditional, broadly Humean challenge to the understanding’s role in experience. These distinct concerns also imply that these arguments yield distinct conclusions, though I will show that they are in fact complementary. (shrink)

This paper proposes a synthetic presentation of the proof construction paradigm, which underlies most of the research and development in the so-called “logic programming” area. Two essential aspects of this paradigm are discussed here: true non-determinism and partial information. A new formulation of Focussing, the basic property used to deal with non-determinism in proof construction, is presented. This formulation is then used to introduce a general constraint-based technique capable of dealing with partial information in proof construction. One (...) of the baselines of the paper is to avoid to rely on syntax to describe the key mechanisms of the paradigm. In fact, the bipolar decomposition of formulas captures their main structure, which can then be directly mapped into a sequent system that uses only atoms. This system thus completely “dissolves” the syntax of the formulas and retains only their behavioural content as far as proof construction is concerned. One step further is taken with the so-called “abstract” proofs, which dissolves in a similar way the specific tree-like syntax of the proofs themselves and retains only what is relevant to proof construction. (shrink)

Structural proof theory is a branch of logic that studies the general structure and properties of logical and mathematical proofs. This book is both a concise introduction to the central results and methods of structural proof theory, and a work of research that will be of interest to specialists. The book is designed to be used by students of philosophy, mathematics and computer science. The book contains a wealth of results on proof-theoretical systems, including extensions of (...) such systems from logic to mathematics, and on the connection between the two main forms of structural proof theory - natural deduction and sequent calculus. The authors emphasize the computational content of logical results. A special feature of the volume is a computerized system for developing proofs interactively, downloadable from the web and regularly updated. (shrink)

Introduction:Healthcare workers facing the threatening COVID-19 can experience severe difficulties. Despite the need to evaluate both the psychological distress and positive protective resources, brief and reliable assessment tools are lacking.Aim:Study 1 aimed at developing a new assessment tool to measure psychological distress and esteem in healthcare workers during the COVID-19 pandemic. Study 2 aimed to explore and compare the psychological reactions of healthcare workers of the COVID-19 and the non-COVID-19 wards.Methods:In Study 1, psychologists created 25 items based on their clinical (...) experience. A preliminary qualitative evaluation selected the best 15 items for the new tool assessing the COVID-19 psychological impact with 2 scales: psychological distress and esteem. The CPI-HP was administered to 110 healthcare professionals to study its psychometric properties and the internal structure with exploratory graph analysis and confirmatory factor analysis. Study 2 compared two groups of healthcare professionals of the COVID-19 and non-COVID-19 departments.Results:In Study 1, the CPI-HP showed satisfying psychometric properties, and the two-factor structure was confirmed with good fit indices. In Study 2, the two groups of healthcare workers showed comparable levels of psychological distress and resilient coping, but the COVID-19 group displayed significantly higher esteem and appreciation of the experience.Discussion:All operators showed high psychological distress during the emergency, but the COVID-19 group reported higher resources, probably due to stronger group cohesion and greater esteem, perceived meaning, and own work value.Conclusion:Assessing the psychological distress and resources of healthcare professionals with specific tools is important. Psychological interventions should promote their psychological health. (shrink)

ABSTRACT This part of the series has a dual purpose. In the first place we will discuss two kinds of theories of proof. The first kind will be called a theory of linear proof. The second has been called a theory of suppositional proof. The term "natural deduction" has often and correctly been used to refer to the second kind of theory, but I shall not do so here because many of the theories so-called are not of (...) the second kind--they must be thought of either as disguised linear theories or theories of a third kind (see postscript below). The second purpose of this part is 25 to develop some of the main ideas needed in constructing a comprehensive theory of proof. The reason for choosing the linear and suppositional theories for this purpose is because the linear theory includes only rules of a very simple nature, and the suppositional theory can be seen as the result of making the linear theory more comprehensive. CORRECTION: At the time these articles were written the word ‘proof’ especially in the phrase ‘proof from hypotheses’ was widely used to refer to what were earlier and are now called deductions. I ask your forgiveness. I have forgiven Church and Henkin who misled me. (shrink)

We present sound and complete sequent calculi for the modal mu-calculus with converse modalities, aka two-way modal mu-calculus. Notably, we introduce a cyclic proof system wherein proofs can be represented as finite trees with back-edges, i.e., finite graphs. The sequent calculi incorporate ordinal annotations and structural rules for managing them. Soundness is proved with relative ease as is the case for the modal mu-calculus with explicit ordinals. The main ingredients in the proof of completeness are isolating a class (...) of non-wellfounded proofs with sequents of bounded size, called slim proofs, and a counter-model construction that shows slimness suffices to capture all validities. Slim proofs are further transformed into cyclic proofs by means of re-assigning ordinal annotations. (shrink)

The problem of algorithmic structuring of proofs in the sequent calculi LK and LKB ( LK where blocks of quantifiers can be introduced in one step) is investigated, where a distinction is made between linear proofs and proofs in tree form. In this framework, structuring coincides with the introduction of cuts into a proof. The algorithmic solvability of this problem can be reduced to the question of k-l-compressibility: "Given a proof of length k , and l ≤ (...) k : Is there is a proof of length ≤ l ?" When restricted to proofs with universal or existential cuts, this problem is shown to be (1) undecidable for linear or tree-like LK-proofs (corresponds to the undecidability of second order unification), (2) undecidable for linear LKB-proofs (corresponds to the undecidability of semi-unification), and (3) decidable for tree-like LKB -proofs (corresponds to a decidable subprob- lem of semi-unification). (shrink)

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)

The aim of this essay is twofold. First, it outlines the concept of ontological frame. Secondly, two models are distinguished on this structure. The first one is connected to Kant’s concept of possible object and the second one relates to Leibniz’s. Leibniz maintains that the source of possibility is the mere logical consistency of the notions involved, so that possibility coincides with analytical possibility. Kant, instead, argues that consistency is only a necessary component of possibility. According to Kant, something (...) is possible if there is a cause capable of bringing it into existence; to this end consistency alone is not sufficient. Thus, while the Leibnizian notion of consistency is at the root of the concept of analytical possibility, the Kantian notion of possibility is the source of real possibility. This difference plays an important role in the discussion of Gödel’s ontological proof, which can be formally interpreted on the ontological frame of the pure perfections. While this proof, under some emendation condition, is conclusive in the context of Leibniz’s ontological model, it is not so within the Kantian one. This issue will be the subject of the second part of the present essay. (shrink)

We prove a number of consistency results complementary to the ZFC results from our paper [J. Cummings, M. Foreman, M. Magidor, Canonical structure in the universe of set theory: part one, Annals of Pure and Applied Logic 129 211–243]. We produce examples of non-tightly stationary mutually stationary sequences, sequences of cardinals on which every sequence of sets is mutually stationary, and mutually stationary sequences not concentrating on a fixed cofinality. We also give an alternative proof for the consistency (...) of the existence of stationarily many non-good points, show that diagonal Prikry forcing preserves certain stationary reflection properties, and study the relationship between some simultaneous reflection principles. Finally we show that the least cardinal where square fails can be the least inaccessible, and show that weak square is incompatible in a strong sense with generic supercompactness. (shrink)

S(zp,zp) performs an innovative analysis of one of modern logic's most celebrated cornerstones: the proof of Gödel's first incompleteness theorem. The book applies the semiotic theories of French post- structuralists such as Julia Kristeva, Jacques Derrida and Gilles Deleuze to shed new light on a fundamental question: how do mathematical signs produce meaning and make sense? S(zp,zp) analyses the text of the proof of Gödel's result, and shows that mathematical language, like other forms of language, enjoys the full (...) complexity of language as a process, with its embodied genesis, constitutive paradoxical forces and unbounded shifts of meaning. These effects do not infringe on the logico-mathematical validity of Gödel's proof. Rather, they belong to a mathematical unconscious that enables the successful function of mathematical texts for a variety of different readers. S(zp,zp) breaks new ground by synthesising mathematical logic and post-structural semiotics into a new form of philosophical fabric, and offers an original way of bridging the gap between the "two cultures". (shrink)

The article presents proofs of the context freeness of a family of typelogical grammars, namely all grammars that are based on a uni- ormultimodal logic of pure residuation, possibly enriched with thestructural rules of Permutation and Expansion for binary modes.

This paper defends the thesis of the analyticity of the principle of apperception, as developed in the first part of the B-Deduction, against recent criticisms by Paul Guyer and Patricia Kitchen The first part presents these criticisms, the most important of which being that the analyticity thesis is incompatible with both the avowed goal of which being that the Deduction of establishing the vahdity of the categories and Üie account of apperception in the A-Deduction. The second part argues that Kant's (...) procedure in the B-Deduction of beginning with an abstract analysis of a discursive understanding, independentiy of its relation to the specifically human forms of sensibility, requires him to regard the principle as analytic and that this explains the difference from the A-Deduction. By appealing to the model of a deduction in Kant's moral theory and the two step in one proof structure of the B-Deduction, the third part argues that the analyticity thesis is in fact compatible with the goal of the Deduction. (shrink)

Anti-realist epistemic conceptions of truth imply what is called the knowability principle: All truths are possibly known. The principle can be formalized in a bimodal propositional logic, with an alethic modality ${\diamondsuit}$ and an epistemic modality ${\mathcal{K}}$, by the axiom scheme ${A \supset \diamondsuit \mathcal{K} A}$. The use of classical logic and minimal assumptions about the two modalities lead to the paradoxical conclusion that all truths are known, ${A \supset \mathcal{K} A}$. A Gentzen-style reconstruction of the Church–Fitch paradox is presented (...) following a labelled approach to sequent calculi. First, a cut-free system for classical bimodal logic is introduced as the logical basis for the Church–Fitch paradox and the relationships between ${\mathcal {K}}$ and ${\diamondsuit}$ are taken into account. Afterwards, by exploiting the structural properties of the system, in particular cut elimination, the semantic frame conditions that correspond to KP are determined and added in the form of a block of nonlogical inference rules. Within this new system for classical and intuitionistic “knowability logic”, it is possible to give a satisfactory cut-free reconstruction of the Church–Fitch derivation and to confirm that OP is only classically derivable, but neither intuitionistically derivable nor intuitionistically admissible. Finally, it is shown that in classical knowability logic, the Church–Fitch derivation is nothing else but a fallacy and does not represent a real threat for anti-realism. (shrink)

This paper and its sequel “look under the hood” of the usual sorts of proof-theoretic systems for certain well-known intuitionistic and classical propositional modal logics. Section 1 is preliminary. Of most importance: a marked formula will be the result of prefixing a formula in a propositional modal language with a step-marker, for this paper either 0 or 1. Think of 1 as indicating the taking of “one step away from 0.” Deductions will be constructed using marked formulas. (...) Section 2 presents the model-theoretic concepts, based on those in [7], that guide the rest of this paper. Section 3 presents Natural Deduction systems IK and CK, formalizations of intuitionistic and classical one-step versions of K. In these systems, occurrences of step-markers allow deductions to display deductive structure that is covered over in familiar “no step” proof-theoretic systems for such logics. Box and Diamond are governed by Introduction and Elimination rules; the familiar K rule and Necessitation are derived (i.e. admissible) rules. CK will be the result of adding the 0-version of the Rule of Excluded Middle to the rules which generate IK. Note: IK is the result of merely dropping that rule from those generating CK, without addition of further rules or axioms (as was needed in [7]). These proof-theoretic systems yield intuitionistic and classical consequence relations by the obvious definition. Section 4 provides some examples of what can be deduced in IK. Section 5 defines some proof-theoretic concepts that are used in Section 6 to prove the soundness of the consequence relation for IK (relative to the class of models defined in Section 2.) Section 7 proves its completeness (relative to that class). Section 8 extends these results to the consequence relation for CK. (Looking ahead: Part 2 will investigate one-step proof-theoretic systems formalizing intuitionistic and classical one-step versions of some familiar logics stronger than K.). (shrink)

Current models of insulin binding to the insulin receptor (IR) propose (i) that there are two binding sites on the surface of insulin which engage with two binding sites on the receptor and (ii) that ligand binding involves structural changes in both the ligand and the receptor. Many of the features of insulin binding to its receptor, namely B‐chain helix interactions with the leucine‐rich repeat domain and A‐chain residue interactions with peptide loops from another part of the receptor, are also (...) seen in models of relaxin and insulin‐like peptide 3 binding to their receptors. We show that these principles can likely be extended to the group of mimetic peptides described by Schäffer and coworkers, which are reported to have no sequence identity with insulin. This review summarizes our current understanding of ligand‐induced activation of the IR and highlights the key issues that remain to be addressed. (shrink)

This paper defends the thesis of the analyticity of the principle of apperception, as developed in the first part of the B-Deduction, against recent criticisms by Paul Guyer and Patricia Kitchen The first part presents these criticisms, the most important of which being that the analyticity thesis is incompatible with both the avowed goal of which being that the Deduction of establishing the validity of the categories and Üie account of apperception in the A-Deduction. The second part argues that Kant's (...) procedure in the B-Deduction of beginning with an abstract analysis of a discursive understanding, independentiy of its relation to the specifically human forms of sensibility, requires him to regard the principle as analytic and that this explains the difference from the A-Deduction. By appealing to the model of a deduction in Kant's moral theory and the two step in one proof structure of the B-Deduction, the third part argues that the analyticity thesis is in fact compatible with the goal of the Deduction. (shrink)

The introduction of automated vehicles promises an increase in traffic safety. Prior to its launch proof of the anticipated reduction in the sense of a positive risk balance compared with human driving performance is required from various stakeholders such as the European Union Commission, the German Ethic Commission, and the ISO TR 4804. To meet this requirement and to generate acceptance by the public and the regulatory authorities, a qualitative Risk- Benefit framework has been defined. This framework is based (...) on literature research on approaches applied in other disciplines. This report depicts the framework, adapted from the pharmaceutical sector called PROACT-URL which serves as a structured procedure to demonstrate a positive risk balance in an understandable and transparent manner. The qualitative framework needs to be turned in quantitative methods once it should be applied. Therefore, two steps of the framework are discussed in more detail: First, the definition of adequate development thresholds that are required at an early stage of the development. Second the simulation-based assessment to prove the positive risk balance prior to the market introduction. (shrink)

Although ‘glue semantics’ is the most extensively developed theory of semantic composition for LFG, it is not very well integrated into the LFG projection architecture, due to the absence of a simple and well-explained correspondence between glue-proofs and f-structures. In this paper I will show that we can improve this situation with two steps: (1) Replace the current quantificational formulations of glue (either Girard’s system F, or first order linear logic) with strictly propositional linear logic (the quantifier, unit and exponential (...) free version of either MILL or ILL, depending on whether or not tensors are used). (2) Reverse the direction of the standard σ-projection from f-structure to meaning, giving one going from the (atomic nodes of) the glue-proof to the f-structure, rather than from the f-structure to a ‘semantic projection’ which is itself somehow related to the glue-proof. As a side effect, the standard semantic projection of LFG glue semantics can be dispensed with. A result is that LFG sentence structures acquire a level composed of strictly binary trees, constructed out of nodes representing function application and lambda abstraction, with a significant resemblance to external and internal merge in the Minimalist Program. This increased resemblance between frameworks might assist in making useful comparisons. (shrink)

In lieu of an abstract, here is a brief excerpt of the content:Advocates, Not Problem ParentsAnonymous TwoNothing could have prepared us for the shock of hearing that our son had a brain tumor.Rob* was 13½, an active, healthy eighth grader, when he developed a headache so bad he couldn’t get out of bed in the morning. We saw the pediatrician three times over the next ten days. On the third visit, after ruling out problems at home, stress at school, strep (...) throat and mono, he sent us for an MRI. When the radiology tech handed me the films and told us to drive back to the pediatrician’s office, I knew we were in trouble. Sure enough, after all the other patients had left, our long–time doctor called us into his tiny office, shut the door and fumbled with the films as he pointed to a white spot that he said was a brain tumor.So began the experience that would change the course of our lives. We remember the diagnosis in detail and relive it in slow motion. We recall packing suitcases, driving to the hospital, waiting to be seen in the emergency room, and walking through doors marked “Pediatric Hematology/Oncology” for the first time.We date everything “BC” (Before Cancer) or “AD” (After Diagnosis). We are grateful every day that [End Page 13] our son is alive, but we know he is forever changed. We are changed: Our nuclear family, our extended family, everyone who knew us and supported us at the time was affected. A pediatric cancer diagnosis is a bomb that shatters your world without warning. If you’re lucky, you can pick up a lot of the pieces, maybe even most of them, but the world you re–enter is never the one you inhabited before.Our doctor delivered the diagnosis to Rob and me at the same time. I’ve thought about this many times and perhaps one day will ask him: Why did he choose to do it that way? Was it a conscious decision or just happenstance? Was it kinder, in the long run—like pulling off a band–aid quickly—or terribly risky? What if I had collapsed at the news? I asked to step into the hall to use the phone. In a state of numbness, I called my husband. He knew we had had an MRI a few hours earlier. “Come quickly,” I said. “There’s a mass.”We chose to go to a top-ranked major medical center and were admitted that evening. A couple of days later, the discovery of tumor markers in Rob’s cerebrospinal fluid and blood confirmed a central nervous system mixed germ cell tumor. We were told he would require six cycles of chemotherapy, followed by six weeks of radiation, and possibly second–look surgery and high-dose chemo with stem cell rescue on top of that. We were given a consent form listing a catalogue of short–and long–term side effects, among them the likelihood of infertility. We were urged to start treatment as soon as possible.By sheer coincidence I had just completed a project for a small, nonprofit organization that existed to inform young adult cancer patients about their fertility rights and options. I knew that infertility concerns were usually pushed aside at diagnosis to make way for other priorities, namely the urgency of starting treatment. And that’s exactly the kind of pressure we were facing.But my husband and I were not ready to sign away our son’s fertility in what felt like a no–confidence vote, a capitulation. We needed to believe that he would survive and put this horror behind him, that he would look forward to marriage and starting a family. We were willing to cede nothing to the disease at this early stage of the game. Was this rational, naive or selfish on our part? I don’t know.The medical team seemed surprised when we asked for a delay in treatment in order to collect sperm samples. They warned that our son’s condition could decline suddenly—and that postponing treatment by even several days might be dangerous. However, at our insistence, they agreed to the delay... (shrink)

Among philosophers in the period of change between the late 18th and early 19th centuries it was a widespread conviction that, because the status of a demonstrative theory made up of axioms and proofs was neither available nor desirable for philosophy, philosophical critique would also not be external to the business of philosophy. Rather it was to belong to the essence of philosophy itself. Against this background Hegel occupied himself almost from the beginning of his philosophical thinking with the question (...) of how a critique that is also able to convince an adherent of a theory differing from one’s own should proceed. Initially it must provide him with a description of his standpoint that he himself can accept. Moreover, the critique must tie up with a method of examination that is part of this standpoint itself, because its adherent would not otherwise have to agree to the procedure. Hegel is interested in this matter not only as a description of the hermeneutic situation in which the adherents of two particular, opposing positions find themselves. Rather, he asks himself whether an idea for the procedure of philosophical critique that commits itself to such considerations can also be generalized. This would require giving a minimalist description of the starting point in a way that allows as large a spectrum as possible of positions that are to be the object of the critique to recognize themselves within it. And the procedure of the critique must be able to be developed from this description itself. (shrink)

Part 1 [Hodes, 2021] “looked under the hood” of the familiar versions of the classical propositional modal logic K and its intuitionistic counterpart. This paper continues that project, addressing some familiar classical strengthenings of K and GL), and their intuitionistic counterparts. Section 9 associates two intuitionistic one-step proof-theoretic systems to each of the just mentioned intuitionistic logics, this by adding for each a new rule to those which generated IK in Part 1. For the systems associated with the (...) intuitionistic counterparts of D and T, these rules are “pure one-step”: their schematic formulations does not use □ or ♢. For the systems associated with the intuitionistic counterparts of K4, etc., these rules meet these conditions: neither □ nor ♢ is iterated; none use both □ and ♢. The join of the two systems associated with each of these familiar logics is the full one-step system for that intuitionistic logic. And further “blended” intuitionistic systems arise from joining these systems in various ways. Adding the 0-version of Excluded Middle to their intuitionistic counterparts yields the one-step systems corresponding to the familiar classical logics. Each proof-theoretic system defines a consequence relation in the obvious way. Section 10 examines inclusions between these consequence relations. Section 11 associates each of the above consequence relations with an appropriate class of models, and proves them sound with respect to their appropriate class. This allows proofs of some failures of inclusion between consequence relations. Section 12 proves that the each consequence relation is complete or weakly complete, that relative to its appropriate class of models. The Appendix presents three further results about some of the intuitionistic consequence relations discussed in the body of the paper. For Keywords, see Part 1. (shrink)

The epistemic probability of A given B is the degree to which B evidentially supports A, or makes A plausible. This paper is a first step in answering the question of what determines the values of epistemic probabilities. I break this question into two parts: the structural question and the substantive question. Just as an object’s weight is determined by its mass and gravitational acceleration, some probabilities are determined by other, more basic ones. The structural question asks what probabilities (...) are not determined in this way—these are the basic probabilities which determine values for all other probabilities. The substantive question asks how the values of these basic probabilities are determined. I defend an answer to the structural question on which basic probabilities are the probabilities of atomic propositions conditional on potential direct explanations. I defend this against the view, implicit in orthodox mathematical treatments of probability, that basic probabilities are the unconditional probabilities of complete worlds. I then apply my answer to the structural question to clear up common confusions in expositions of Bayesianism and shed light on the “problem of the priors.”. (shrink)

In lieu of an abstract, here is a brief excerpt of the content:Reviewed by:Kant's Transcendental Deduction by Alison LaywineKatherine DunlopAlison Laywine. Kant's Transcendental Deduction. Oxford: Oxford University Press, 2020. Pp. iv + 318. Hardback, $80.00.Alison Laywine's contribution to the rich literature on Kant's "Transcendental Deduction of the Categories" stands out for the novelty of its approach and conclusions. Laywine's declared "strategy" is "to compare and contrast" the Deduction with the Duisburg Nachlaß, an important set of manuscript jottings from the 1770s (...) (10). But her approach is also deeply informed by Kant's writings on metaphysics from the 1750s and 1760s; moreover, she gives attention to ancient Greek geometry and its importance for Kant's thought.I believe Laywine's most important interpretative claim is that the Transcendental Deduction's "final step" addresses "the question of how nature is possible" (210). Here, 'nature' is understood in what Kant calls the "formal sense," as "the totality of rules under which appearances must stand if they are to be thought as joined in one experience" (Prolegomena, §36; cf. B 165). This constitutes a novel answer to the problem posed in Dieter Henrich's landmark 1969 paper "The Proof Structure of the Transcendental Deduction" (Review of Metaphysics 22 [1969]: 640–59): how to understand §§21–26 of the (B-edition) Deduction as proving more than the thesis already stated in §20 (that the manifold in an intuition necessarily stands under the categories).Crucial support for Laywine's interpretation comes from §26 of the Deduction, which claims the possibility of cognizing objects "a priori through categories... as far as the laws of their combination are concerned, thus the possibility of as it were prescribing the law to nature and even making [nature] possible," is now "to be explained" (B 159). Kant does not use the term 'world' in this passage (as he does in Prolegomena §36). But Laywine contends that here the word 'nature' "has unmistakable, deliberate, cosmological connotations," and in fact "means 'world' in the sense of Kant's early cosmology": roughly, a whole unified by means of laws (12–13).The "cosmological" language of §26 does not recur in the following, officially concluding, section of the Deduction. So, we might ask whether Kant's explanation of how the understanding prescribes laws to nature is integral to the Deduction; Henry Allison, for instance, describes this explanation as an "appendix" (Kant's Transcendental Deduction: An Analytical-Historical Commentary [Oxford: Oxford University Press, 2015], 9). The question of whether it belongs integrally has bite because, as Laywine makes clear in her "Conclusion," the universal laws at issue are just the Analogies of Experience. Thus, the passage could be read as the "promissory note with a forward-looking reference to the System of Principles" that she finds missing from the Deduction (289). Laywine meets such worries by arguing that "the reappropriation [from the pre-Critical period] of the general cosmology is actually [End Page 162] doing... a lot of hard work" in the Deduction (13). This sustained argument comes to a head in chapter 4, which contends that each of the two steps into which Laywine divides the first half of the (B-edition) Deduction, treated in chapters 2 and 3 (respectively), relies on cosmological presuppositions.Chapter 2 analyzes the conception of knowledge as relation to an object that is asserted (in §17) to rely on the synthetic unity of apperception. Laywine traces this conception to the Duisburg Nachlaß's account of "exposition," which relates concepts a priori to appearances, in something like the way that geometrical construction relates them to pure intuition. (Laywine further connects the Latin term expositio to the Greek ekthesis, which expositio translates in the context of geometrical proof. She thereby gives the notion of ekthesis broader importance than does Jaakko Hintikka, who noted its relevance to Kant's philosophy of mathematics in "Kant on the Mathematical Method" [Monist 51 (1967): 352–75]. Laywine claims that Borelli's edition of Euclid could have been Kant's source for the term, but I doubt it was known to Kant and his contemporaries, since it is not among the editions cited by Christian Wolff; Commandino seems likelier to me. Chapter 2 is concerned to articulate the notion of... (shrink)

Teaching research methods is especially challenging because we not only wish to convey formal knowledge and encourage critical thinking, as with any course, but also to enable our students dream up meaningful research projects, translate them into logical steps, conduct the research in a professional manner, analyze the data, and write up the project in APA style. We also wish to spark interest in the topics of research papers, and in the intellectual challenge of creating a research report, but we (...) have learned just how difficult these goals can be from teaching undergraduates and from serving as journal reviewers: many submissions contain flaws such as elementary errors of logic (e.g., using a null control condition instead of a placebo or dummy treatment), tangled statistics, a lack of graphs, and ungrammatical, unclear writing that violates APA rules. Yet these manuscripts are written by university faculty, often with doctorates and years of experience. Even published papers may contain egregious faults (Standing & McKelvie, 1986). And although we have both published widely, we still hone our skills. It requires optimism to expect that a typical undergraduate will do better, on the basis of just a year or two of studies in psychology. In this paper, we describe a systematic set of methodology courses and two specific practices that we think can help. Methodology Courses as the Backbone of our Psychology Program How can methodology courses promote undergraduate involvem... (shrink)

Classical proof forests are a proof formalism for first-order classical logic based on Herbrand’s Theorem and backtracking games in the style of Coquand. First described by Miller in a cut-free setting as an economical representation of first-order and higher-order classical proof, defining features of the forests are a strict focus on witnessing terms for quantifiers and the absence of inessential structure, or ‘bureaucracy’.This paper presents classical proof forests as a graphical proof formalism and investigates (...) the possibility of composing forests by cut-elimination. Cut-reduction steps take the form of a local rewrite relation that arises from the structure of the forests in a natural way. Yet reductions, which are significantly different from those of the sequent calculus, are combinatorially intricate and do not exclude the possibility of infinite reduction traces, of which an example is given.Cut-elimination, in the form of a weak normalisation theorem, is obtained using a modified version of the rewrite relation inspired by the game-theoretic interpretation of the forests. It is conjectured that the modified reduction relation is, in fact, strongly normalising. (shrink)

Mathematical proofs are not sequences of arbitrary deductive steps—each deductive step is, to some extent, rational. This paper aims to identify and characterize the particular form of rationality at play in mathematical proofs. The approach adopted consists in viewing mathematical proofs as reports of proof activities—that is, sequences of deductive inferences—and in characterizing the rationality of the former in terms of that of the latter. It is argued that proof activities are governed by specific norms of rational (...) planning agency, and that a deductive step in a mathematical proof qualifies as rational whenever the corresponding deductive inference in the associated proof activity figures in a plan that has been constructed rationally. It is then shown that mathematical proofs whose associated proof activities violate these norms are likely to be judged as defective by mathematical agents, thereby providing evidence that these norms are indeed present in mathematical practice. We conclude that, if mathematical proofs are not mere sequences of deductive steps, if they possess a rational structure, it is because they are the product of rational planning agents. (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)

Charles Peirce’s alpha system \ is reformulated into a deep inference system where the rules are given in terms of deep graphical structures and each rule has its symmetrical rule in the system. The proof analysis of \ is given in terms of two embedding theorems: the system \ and Brünnler’s deep inference system for classical propositional logic can be embedded into each other; and the system \ and Gentzen sequent calculus \ can be embedded into each other.

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 consider the problem of finding and classifying representations in algebraic logic. This is approached by letting two players build a representation using a game. Homogeneous and universal representations are characterized according to the outcome of certain games. The Lyndon conditions defining representable relation algebras (for the finite case) and a similar schema for cylindric algebras are derived. Finite relation algebras with homogeneous representations are characterized by first order formulas. Equivalence games are defined, and are used to establish whether an (...) algebra is ω-categorical. We have a simple proof that the perfect extension of a representable relation algebra is completely representable. An important open problem from algebraic logic is addressed by devising another two-player game, and using it to derive equational axiomatisations for the classes of all representable relation algebras and representable cylindric algebras. Other instances of this approach are looked at, and include the step by step method. (shrink)

The two major options on which the current debate on the interpretation of quantum mechanics relies, namely realism and empiricism, are far from being exhaustive. There is at least one more position available, which is metaphysically as agnostic as empiricism, but which shares with realism a committment to considering the structure of theories as highly significant. The latter position has been named transcendentalism after Kant. In this paper, a generalized version of Kant's method is used. This yields a reasoning (...) that one is entitled to call a transcendental deduction of some major formal features of quantum mechanics. (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)

A combination of epistemic logic and dynamic logic of programs is presented. Although rich enough to formalize some simple game-theoretic scenarios, its axiomatization is problematic as it leads to the paradoxical conclusion that agents are omniscient. A cut-free labelled Gentzen-style proof system is then introduced where knowledge and action, as well as their combinations, are formulated as rules of inference, rather than axioms. This provides a logical framework for reasoning about games in a modular and systematic way, and to (...) give a step-by-step reconstruction of agents omniscience. In particular, its semantic assumptions are made explicit and a possible solution can be found in weakening the properties of the knowledge operator. (shrink)

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)

We present a setting in which the search for a proof of B or a refutation of B can be carried out simultaneously: in contrast, the usual approach in automated deduction views proving B or proving ¬B as two, possibly unrelated, activities. Our approach to proof and refutation is described as a two-player game in which each player follows the same rules. A winning strategy translates to a proof of the formula and a counter-winning strategy translates to (...) a refutation of the formula. The game is described for multiplicative and additive linear logic . A game theoretic treatment of the multiplicative connectives is intricate and our approach to it involves two important ingredients. First, labeled graph structures are used to represent positions in a game and, second, the game playing must deal with the failure of a given player and with an appropriate resumption of play. This latter ingredient accounts for the fact that neither player might win. (shrink)

This is a first course in propositional modal logic, suitable for mathematicians, computer scientists and philosophers. Emphasis is placed on semantic aspects, in the form of labelled transition structures, rather than on proof theory. The book covers all the basic material - propositional languages, semantics and correspondence results, proof systems and completeness results - as well as some topics not usually covered in a modal logic course. It is written from a mathematical standpoint. To help the reader, the (...) material is covered in short chapters, each concentrating on one topic. These are arranged into five parts, each with a common theme. An important feature of the book is the many exercises and an extensive set of solutions is provided. (shrink)

The INBIOSA project brings together a group of experts across many disciplines who believe that science requires a revolutionary transformative step in order to address many of the vexing challenges presented by the world. It is INBIOSA’s purpose to enable the focused collaboration of an interdisciplinary community of original thinkers. This paper sets out the case for support for this effort. The focus of the transformative research program proposal is biology-centric. We admit that biology to date has been more (...) fact-oriented and less theoretical than physics. However, the key leverageable idea is that careful extension of the science of living systems can be more effectively applied to some of our most vexing modern problems than the prevailing scheme, derived from abstractions in physics. While these have some universal application and demonstrate computational advantages, they are not theoretically mandated for the living. A new set of mathematical abstractions derived from biology can now be similarly extended. This is made possible by leveraging new formal tools to understand abstraction and enable computability. [The latter has a much expanded meaning in our context from the one known and used in computer science and biology today, that is "by rote algorithmic means", since it is not known if a living system is computable in this sense (Mossio et al., 2009).] Two major challenges constitute the effort. The first challenge is to design an original general system of abstractions within the biological domain. The initial issue is descriptive leading to the explanatory. There has not yet been a serious formal examination of the abstractions of the biological domain. What is used today is an amalgam; much is inherited from physics (via the bridging abstractions of chemistry) and there are many new abstractions from advances in mathematics (incentivized by the need for more capable computational analyses). Interspersed are abstractions, concepts and underlying assumptions “native” to biology and distinct from the mechanical language of physics and computation as we know them. A pressing agenda should be to single out the most concrete and at the same time the most fundamental process-units in biology and to recruit them into the descriptive domain. Therefore, the first challenge is to build a coherent formal system of abstractions and operations that is truly native to living systems. Nothing will be thrown away, but many common methods will be philosophically recast, just as in physics relativity subsumed and reinterpreted Newtonian mechanics. -/- This step is required because we need a comprehensible, formal system to apply in many domains. Emphasis should be placed on the distinction between multi-perspective analysis and synthesis and on what could be the basic terms or tools needed. The second challenge is relatively simple: the actual application of this set of biology-centric ways and means to cross-disciplinary problems. In its early stages, this will seem to be a “new science”. This White Paper sets out the case of continuing support of Information and Communication Technology (ICT) for transformative research in biology and information processing centered on paradigm changes in the epistemological, ontological, mathematical and computational bases of the science of living systems. Today, curiously, living systems cannot be said to be anything more than dissipative structures organized internally by genetic information. There is not anything substantially different from abiotic systems other than the empirical nature of their robustness. We believe that there are other new and unique properties and patterns comprehensible at this bio-logical level. The report lays out a fundamental set of approaches to articulate these properties and patterns, and is composed as follows. -/- Sections 1 through 4 (preamble, introduction, motivation and major biomathematical problems) are incipient. Section 5 describes the issues affecting Integral Biomathics and Section 6 -- the aspects of the Grand Challenge we face with this project. Section 7 contemplates the effort to formalize a General Theory of Living Systems (GTLS) from what we have today. The goal is to have a formal system, equivalent to that which exists in the physics community. Here we define how to perceive the role of time in biology. Section 8 describes the initial efforts to apply this general theory of living systems in many domains, with special emphasis on crossdisciplinary problems and multiple domains spanning both “hard” and “soft” sciences. The expected result is a coherent collection of integrated mathematical techniques. Section 9 discusses the first two test cases, project proposals, of our approach. They are designed to demonstrate the ability of our approach to address “wicked problems” which span across physics, chemistry, biology, societies and societal dynamics. The solutions require integrated measurable results at multiple levels known as “grand challenges” to existing methods. Finally, Section 10 adheres to an appeal for action, advocating the necessity for further long-term support of the INBIOSA program. -/- The report is concluded with preliminary non-exclusive list of challenging research themes to address, as well as required administrative actions. The efforts described in the ten sections of this White Paper will proceed concurrently. Collectively, they describe a program that can be managed and measured as it progresses. (shrink)

In order to develop efficient tools for automated reasoning with inconsistency (theorem provers), eventually making Logics of Formal inconsistency (_LFI_) a more appealing formalism for reasoning under uncertainty, it is important to develop the proof theory of the first-order versions of such _LFI_s. Here, we intend to make a first step in this direction. On the other hand, the logic _Ciore_ was developed to provide new logical systems in the study of inconsistent databases from the point of view (...) of _LFI_s. An interesting fact about _Ciore_ is that it has a _strong_ consistency operator, that is, a consistency operator which (forward/backward) propagates inconsistency. Also, it turns out to be an algebraizable logic (in the sense of Blok and Pigozzi) that can be characterized by means of a 3-valued logical matrix. Recently, a first-order version of _Ciore_, namely _QCiore_, was defined preserving the spirit of _Ciore_, that is, without introducing unexpected relationships between the quantifiers. Besides, some important model-theoretic results were obtained for this logic. In this paper we study some proof–theoretic aspects of both _Ciore_ and _QCiore_ respectively. In first place, we introduce a two-sided sequent system for _Ciore_. Later, we prove that this system enjoys the cut-elimination property and apply it to derive some interesting properties. Later, we extend the above-mentioned system to first-order languages and prove completeness and cut-elimination property using the well-known Shütte’s technique. (shrink)

Proof requires a dialogue between agents to clarify obscure inference steps, fill gaps, or reveal implicit assumptions in a purported proof. Hence, argumentation is an integral component of the discovery process for mathematical proofs. This work presents how argumentation theories can be applied to describe specific informal features in the development of proof-events. The concept of proof-event was coined by Goguen who described mathematical proof as a public social event that takes place in space and (...) time. This new meta-methodological concept is designed to cover not only “traditional” formal proofs but all kinds of proofs and inference steps, including incomplete or purported proofs. Our approach attempts to make proof-events more comprehensive to express the complete trajectory of a mathematical proof-event until the ultimate validation of the proving outcome. Thus, we advance an extended version of proof-event calculus which is built on argumentation theories designed to capture the internal and external structure of collaborative mathematical practice and highlight the relationship between proof, human reasoning, and cognitive processes. In addition, another area in which argumentation can make a significant contribution is dealing with the defeasible knowledge of the Web which is a product of its open and ubiquitous nature. This approach seems to be sufficient for the presentation of Web-based proving processes as manifested in the case of the Mini-Polymath 4 project. (shrink)

We consider the problem of finding and classifying representations in algebraic logic. This is approached by letting two players build a representation using a game. Homogeneous and universal representations are characterized according to the outcome of certain games. The Lyndon conditions defining representable relation algebras and a similar schema for cylindric algebras are derived. Finite relation algebras with homogeneous representations are characterized by first order formulas. Equivalence games are defined, and are used to establish whether an algebra is $\omega$-categorical. We (...) have a simple proof that the perfect extension of a representable relation algebra is completely representable. An important open problem from algebraic logic is addressed by devising another two-player game, and using it to derive equational axiomatisations for the classes of all representable relation algebras and representable cylindric algebras. Other instances of this approach are looked at, and include the step by step method. (shrink)

Purity is known as an ideal of proof that restricts a proof to notions belonging to the ‘content’ of the theorem. In this paper, our main interest is to develop a conception of purity for formal (natural deduction) proofs. We develop two new notions of purity: one based on an ontological notion of the content of a theorem, and one based on the notions of surrogate ontological content and structural content. From there, we characterize which (classical) first-order natural (...) deduction proofs of a mathematical theorem are pure. Formal proofs that refer to the ontological content of a theorem will be called ‘fully ontologically pure’. Formal proofs that refer to a surrogate ontological content of a theorem will be called ‘secondarily ontologically pure’, because they preserve the structural content of a theorem. We will use interpretations between theories to develop a proof-theoretic criterion that guarantees secondary ontological purity for formal proofs. (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)

This paper analyzes Kent Bach’s representational theory of action, one of the causal theories of action. Bach’s theory sets requirements not only for the cause of an action, but also for how it unfolds in time and transitions into another action. These requirements suggest a sequential emergence of two components of the agent’s action awareness: the representation of the prepared movement and the perception of its sensory consequences. Bach introduces the concepts of “effective representation” (ER) and “receptive representation” (RR) to (...) denote these components of awareness. According to representational theory, action has a cyclic three-step causal structure, where ER is the cause of a movement, the movement is the cause of RR, and RR is the cause of ER of subsequent movement. In constructing his theory, Bach tries to take into account the problem of deviant causal chains and to introduce the so-called minimal actions into the purview of the philosophy of action. Relying on the behavioral data on blindfolded deafferentated patients, in this paper I argue that RRs are not a necessary element of action. I also analyze Bach’s distinction between ER and RR and compare it with J. Searle’s approach, placing Bach’s theory within the context of studies of the structure of intentional states. I show that Bach’s theory occupies a unique position among views on the structure of action awareness. At the same time, I conclude that the frameworks of Bach and Searle are insufficient for describing the metaphysical difference between the two kinds of intentional states, and I also point out the difficulties facing the notion of ER. Based on this reasoning and the data on deafferentated patients, I propose a modification of the causal structure of action proposed by Bach, making a remark about the inadequate definition of ER. In the proposed modification, RR and the agent’s prior intention serve as alternative components of action awareness. (shrink)