Working in the fragment of Martin-Löfs extensional type theory [12] which has products (but not sums) of dependent types, we consider two additional assumptions: firstly, that there are (strong) equality types; and secondly, that there is a type which is universal in the sense that terms of that type name all types, up to isomorphism. For such a type theory, we give a version of Russell's paradox showing that each type possesses a closed term and (hence) that all terms of (...) each type are provably equal. We consider the kind of category theoretic structure which corresponds to this kind of type theory and obtain a categorical version of the paradox. A special case of this result is the degeneracy of a locally cartesian closed category with a morphism which is generic in the sense that every other morphism in the category can be obtained from it via pullback. (shrink)
We prove the following surprising property of Heyting's intuitionistic propositional calculus, IpC. Consider the collection of formulas, φ, built up from propositional variables (p,q,r,...) and falsity $(\perp)$ using conjunction $(\wedge)$ , disjunction (∨) and implication (→). Write $\vdash\phi$ to indicate that such a formula is intuitionistically valid. We show that for each variable p and formula φ there exists a formula Apφ (effectively computable from φ), containing only variables not equal to p which occur in φ, and such that for (...) all formulas ψ not involving $p, \vdash \psi \rightarrow A_p\phi$ if and only if $\vdash \psi \rightarrow \phi$ . Consequently quantification over propositional variables can be modelled in IpC, and there is an interpretation of the second order propositional calculus, IpC2, in IpC which restricts to the identity on first order propositions. An immediate corollary is the strengthening of the usual interpolation theorem for IpC to the statement that there are least and greatest interpolant formulas for any given pair of formulas. The result also has a number of interesting consequences for the algebraic counterpart of IpC, the theory of Heyting algebras. In particular we show that a model of IpC2 can be constructed whose algebra of truth-values is equal to any given Heyting algebra. (shrink)
The cosmic singularity provides negligible evidence for creation in the finite past, and hence theism. A physical theory might have no metric or multiple metrics, so a ‘beginning’ must involve a first moment, not just finite age. Whether one dismisses singularities or takes them seriously, physics licenses no first moment. The analogy between the Big Bang and stellar gravitational collapse indicates that a Creator is required in the first case only if a Destroyer is needed in the second. The need (...) for and progress in quantum gravity and the underdetermination of theories by data make it difficult to take singularities seriously. The singularity exemplifies the sort of gap that is likely to be closed by scientific progress, obviating special divine action. The apparent irrelevance of cardinality to practices of counting infinite sets in classical field theory and Fourier analysis is noted. Introduction The Doctrine of Creation and Its Warrant Cardinality and Sizes of Infinity Modern Cosmology and Creation Tolerance or Intolerance toward Singularities? Leibniz against Incompetent Watchmaker? Induction from Earlier Theories' Breakdown? Stellar Collapse Implies Theistic Destroyer Stacking the Deck for GTR Quantum Gravity Tends to Resolve Singularities Vicious God-of-the-Gaps Character Fluctuating or Inaccessible Warrant Big Bang Cosmology Not Especially Congenial to Faith CiteULike Connotea Del.icio.us What's this? (shrink)
A. M. Pitts in [Pi] proved that HA op fp is a bi-Heyting category satisfying the Lawrence condition. We show that the embedding $\Phi: HA^\mathrm{op}_\mathrm{fp} \longrightarrow Sh(\mathbf{P_0,J_0})$ into the topos of sheaves, (P 0 is the category of finite rooted posets and open maps, J 0 the canonical topology on P 0 ) given by $H \longmapsto HA(H,\mathscr{D}(-)): \mathbf{P_0} \longrightarrow \text{Set}$ preserves the structure mentioned above, finite coproducts, and subobject classifier, it is also conservative. This whole structure on HA (...) op fp can be derived from that of Sh(P 0 ,J 0 ) via the embedding Φ. We also show that the equivalence relations in HA op fp are not effective in general. On the way to these results we establish a new kind of duality between HA op fp and a category of sheaves equipped with certain structure defined in terms of Ehrenfeucht games. Our methods are model-theoretic and combinatorial as opposed to proof-theoretic as in [Pi]. (shrink)
The aim of the paper is to show and document the husserlian concern to validate a position of ontological realism, and the inappropriateness of his method to this task. It is precisley the scientific charachter of his philosophy that drew Husserl to idealism and solipsism, despite his original intentions and motivations.
I review ornithological literature in order to demonstrate that conventions of description and illustration, as well as some aspects of biological theory relating to birds, put a strong focus on male birds. I criticize the sexist aspects of ornithology from the standpoint of recent feminist philosophy of science, establishing connections between the ways in which we view animals and the ways in which we viewourselves and arguing that it is costly to humans, specifically women, to suggest that females of the (...) nonhuman species are biologically inadequate in relation to their male counterparts. Finally, I note that failure to notice and excise residual sexism in animal science also encourages people to be inattentive to and less considerate of a large and significant part of nature. I conclude with some suggestionsfor reform. (shrink)
Call a thought whose expression involves the utterance of an indexical an indexical thought . Thus, my thoughts that I’m annoyed, that now is not the right time, that this is not acceptable, are all indexical thoughts. Such thoughts present a prima facie problem for the thesis that thought contents are phenomenally individuated – i.e., that each distinct thought type has a proprietarily cognitive phenomenology such that its having that phenomenology makes it the thought that it is – given the (...) assumption that phenomenology is intrinsically determined (i.e. (shrink)
: Philosophers of science turned to historical case studies in part in response to Thomas Kuhn's insistence that such studies can transform the philosophy of science. In this issue Joseph Pitt argues that the power of case studies to instruct us about scientific methodology and epistemology depends on prior philosophical commitments, without which case studies are not philosophically useful. Here I reply to Pitt, demonstrating that case studies, properly deployed, illustrate styles of scientific work and modes of argumentation that are (...) not well handled by currently standard philosophical analyses. I illustrate these claims with exemplary findings from case studies dealing with exploratory experimentation and with interdisciplinary cooperation across sciences to yield multiple independent means of access to theoretical entities. The latter cases provide examples of ways that scientists support claims about theoretical entities that are not available in work performed within a single discipline. They also illustrate means of correcting systematic biases that stem from the commitments of each discipline taken separately. These findings illustrate the transformative power of case study methods, allow us to escape from the horns of Pitt's "dilemma of case studies," and vindicate some of the post-Kuhn uses to which case studies have been put. (shrink)
