This paper responds to recent work in the philosophy of Homotopy Type Theory by James Ladyman and Stuart Presnell. They consider one of the rules for identity, path induction, and justify it along ‘pre-mathematical’ lines. I give an alternate justification based on the philosophical framework of inferentialism. Accordingly, I construct a notion of harmony that allows the inferentialist to say when a connective or concept is meaning-bearing and this conception unifies most of the prominent conceptions of harmony through category theory. (...) This categorical harmony is stated in terms of adjoints and says that any concept definable by iterated adjoints from general categorical operations is harmonious. Moreover, it has been shown that identity in a categorical setting is determined by an adjoint in the relevant way. Furthermore, path induction as a rule comes from this definition. Thus we arrive at an account of how path induction, as a rule of inference governing identity, can be justified on mathematically motivated grounds. (shrink)

Natural Formalization proposes a concrete way of expanding proof theory from the meta-mathematical investigation of formal theories to an examination of “the concept of the specifically mathematical proof.” Formal proofs play a role for this examination in as much as they reflect the essential structure and systematic construction of mathematical proofs. We emphasize three crucial features of our formal inference mechanism: (1) the underlying logical calculus is built for reasoning with gaps and for providing strategic directions, (2) the mathematical frame (...) is a definitional extension of Zermelo–Fraenkel set theory and has a hierarchically organized structure of concepts and operations, and (3) the construction of formal proofs is deeply connected to the frame through rules for definitions and lemmas. To bring these general ideas to life, we examine, as a case study, proofs of the Cantor–Bernstein Theorem that do not appeal to the principle of choice. A thorough analysis of the multitude of “different” informal proofs seems to reduce them to exactly one. The natural formalization confirms that there is one proof, but that it comes in two variants due to Dedekind and Zermelo, respectively. In this way it enhances the conceptual understanding of the represented informal proofs. The formal, computational work is carried out with the proof search system AProS that serves as a proof assistant and implements the above inference mechanism; it can be fully inspected at (see link below). (shrink)

Inductively defined structures are ubiquitous in mathematics; their specification is unambiguous and their properties are powerful. All fields of mathematical logic feature these structures prominently: the formula of a language, the set of theorems, the natural numbers, the primitive recursive functions, the constructive number classes and segments of the cumulative hierarchy of sets. -/- This dissertation gives a mathematical characterization of a species of inductively defined structures, called accessible domains, which include all of the above examples except the set of (...) theorems. The concept of an accessible domain comes from Wilfried Sieg's analysis of proof-theoretic practices, starting with his dissertation. In particular, he noticed the special epistemological character of elements of an accessible domain: they can always be uniquely identified with their build-up. Generally, the unique build-up of elements justifies the principles of induction and recursion. -/- I use category theory to give an abstract characterization of accessible domains. I claim that accessible domains are all instances of initial algebras for endofunctors. Grounded in the historical roots of Sieg's discussions, this dissertation shows how the properties of initial algebras for endofunctors and accessible domains coincide in a satisfying and natural way. -/- Filling out this characterization, I show how important examples of accessible domains fit into this broad characterization. I first characterize some accessible domains by relatively simple functors (e.g. finite, polynomial, those that preserve certain colimits) where we can see how iterating the functor can produce the accessible domain. Then I describe accessible domains that result from more involved specifications (e.g. ordinals and segments of the cumulative hierarchies associated with CZF, IZF, and ZF) by relying heavily on algebraic set theory. I end with a discussion of some of the methodological features of category theory in particular that helped characterize accessible domains. (shrink)

Patrick D Walsh; Education: one concept in many uses, Journal of Philosophy of Education, Volume 19, Issue 2, 30 May 2006, Pages 167–180, https://doi.org/10.111.

Patrick D Walsh; Open and Loaded Uses of ‘Education’—and objectivism, Journal of Philosophy of Education, Volume 22, Issue 1, 30 May 2006, Pages 23–35, https://.

This volume examines the ethical issues that arise as a result of national security intelligence collection and analysis. Powerful new technologies enable the collection, communication, and analysis of national security data on an unprecedented scale. Data collection now plays a central role in intelligence practice, yet this development raises a host of ethical and national security problems, such as: privacy; autonomy; threats to national security and democracy by foreign states; and accountability for liberal democracies. This volume provides a comprehensive set (...) of in-depth ethical analyses of these problems by combining contributions from both ethics scholars and intelligence practitioners. It provides the reader with a practical understanding of relevant operations, the issues that they raise, and analysis of how responses to these issues can be informed by a commitment to liberal democratic values. This combination of perspectives is crucial in providing an informed appreciation of ethical challenges that is also grounded in the realities of the practice of intelligence. This book will be of great interest to all students of intelligence studies, ethics, security studies, foreign policy, and International Relations. (shrink)

While French biologists were turning a cold shoulder to On the Origin of Species in the 1860s, Charles Darwin was earnestly pursuing a professional connection with one French physiologist in particular: Charles Brown-Séquard. Darwin had been closely following Brown-Séquard’s startling experiments on guinea pigs, which demonstrated that experimentally induced epilepsy could pass from parent to offspring. In Darwin’s mind, Brown-Séquard had produced the most convincing evidence to date that acquired traits could be inherited. Darwin saw opportunities in Brown-Séquard and his (...) work. If Brown-Séquard realized the evolutionary implications of his experiments, and then endorsed the Origin in Paris, Darwin could be well on his way to securing a French audience for his theories. Darwin quickly mobilized his powers of correspondence to make this French connection, but Brown-Séquard received Darwin’s advances with caution. A connection with Darwin could be useful in London and America, where he was increasingly spending time, but to publicly support Darwin would be professionally damaging back home in Paris. This paper examines the dance of letters between Darwin and Brown-Séquard, the politics of citation, and the delicacy of sustaining a transnational biological career between France and Britain in the 1860s. This paper casts a new perspective on an old debate in the history of biology. I show that from within the “heavy cloud” of anti-evolutionary thought in France, there existed a live wire between Brown-Séquard and Darwin. I argue that British evolutionary theory in the age of Darwin was built, in part, with French participation. (shrink)

When positionally cloned in late 1989, it was anticipated that mutations within the Wilms' tumour suppressor gene (WT1) would prove responsible for this common solid kidney cancer of childhood. Characterisation of the WT1 expression pattern and of the structure of the encoded protein isoforms and their mode of action has now spanned almost a decade. WT1 proteins act as nucleic acid-binding zinc finger-containing transcription factors involved in both transactivation and repression. These activities are facilitated and constrained by interactions with other (...) proteins. Expression analyses and knockout mice indicate that WT1 protein plays a critical role in normal kidney and gonad development. Specific constitutional WT1 mutations results in several urogenital anomaly syndromes. While only 10% of sporadic Wilms' tumours do display WT1 mutation, WT1 is mutated in other cancers, including acute myeloid leukaemia. Much is still to be determined in WT1 biology. The next decade will see at least three streams of attention. The first two, elucidation of the role of WT1 in RNA metabolism and the characterisation of further protein partners, may together explain the distinct tissue-specific functions of WT1. Finally, further research into the role of WT1 in haematopoiesis will improve our understanding of WT1 in leukaemia. BioEssays 21:191-202, 1999. (C) 1999 John Wiley & Sons, Inc. (shrink)