It has been known for six years that the restriction of Girard's polymorphic system $\text{\bfseries\upshape F}$ to atomic universal instantiations interprets the full fragment of the intuitionistic propositional calculus. We firstly observe that Tait's method of “convertibility” applies quite naturally to the proof of strong normalization of the restricted Girard system. We then show that each $\beta$-reduction step of the full intuitionistic propositional calculus translates into one or more $\beta\eta$-reduction steps in the restricted Girard system. As a consequence, we obtain (...) a novel and perspicuous proof of the strong normalization property for the full intuitionistic propositional calculus. It is noticed that this novel proof bestows a crucial role to $\eta$-conversions. (shrink)

In an attempt to accommodate natural language phenomena involving nominalization and self-application, various researchers in formal semantics have proposed abandoning the hierarchical type system which Montague inherited from Russell, in favour of more flexible type regimes. We briefly review the main extant proposals, and then develop a new approach, based semantically on Aczel's notion of Frege structure, which implements a version ofsubsumption polymorphism. Nominalization is achieved by virtue of the fact that the types of predicative and propositional complements (...) are contained in the type of individuals. Russell's paradox is avoided by placing a type-constraint on lambda-abstraction, rather than by restricting comprehension. (shrink)

In a previous paper we investigated the extraction of proof-theoretic properties of natural deduction derivations from their impredicative translation into System F. Our key idea was to introduce an extended equational theory for System F codifying at a syntactic level some properties found in parametric models of polymorphic type theory. A different approach to extract proof-theoretic properties of natural deduction derivations was proposed in a recent series of papers on the basis of an embedding of intuitionistic propositional logic into a (...) predicative fragment of System F, called atomic System F. In this paper we show that this approach finds a general explanation within our equational study of second-order natural deduction, and a clear semantic justification in terms of parametricity. (shrink)

It is known that there is a sound and faithful translation of the full intuitionistic propositional calculus into the atomic polymorphic system F at, a predicative calculus with only two connectives: the conditional and the second-order universal quantifier. The faithfulness of the embedding was established quite recently via a model-theoretic argument based in Kripke structures. In this paper we present a purely proof-theoretic proof of faithfulness. As an application, we give a purely proof-theoretic proof of the disjunction property of (...) the intuitionistic propositional logic in which commuting conversions are not needed. (shrink)

A class of models is presented, in the form of continuation monads polymorphic for first-order individuals, that is sound and complete for minimal intuitionistic predicate logic . The proofs of soundness and completeness are constructive and the computational content of their composition is, in particular, a β-normalisation-by-evaluation program for simply typed lambda calculus with sum types. Although the inspiration comes from Danvyʼs type-directed partial evaluator for the same lambda calculus, the use of delimited control operators is avoided. The role of (...) polymorphism is crucial – dropping it allows one to obtain a notion of model complete for classical predicate logic. (shrink)

ABSTRACT A computational logic, PLPR (Predicate Logic using Polymorphism and Recursion) is presented. Actually this logic is the object language of an automated deduction system designed as a tool for proving mathematical theorems as well as specify and verify properties of functional programs. A useful denotationl semantics and two general deduction methods for PLPR are defined. The first one is a tableau algorithm proved to be complete and also used as a guideline for building complete calculi. The second is (...) a sound and complete natural deduction system. Moreover a fixed point induction rule is introduced for formulas called continuous. The strategies for mechanizing the proofs of the final automated system are based on the previous deduction methods. As the examples of the use of the system show, the implemented theorem prover outperforms humans to a certain extent, retaining logic and calculi generality. (shrink)

Bioassessment is the process of using living organisms to assess the ecological health of a particular ecosystem. It typically relies on identifying specific organisms that are sensitive to changes in environmental conditions. Benthic macroinvertebrates are widely used for examining the ecological status of freshwaters. However, a time-consuming process of species identification that requires high expertise represents one of the key obstacles to more precise bioassessment of aquatic ecosystems. Partial automation of this process using deep learning-based image classification is the goal (...) of an ongoing project AIAQUAMI we are participating in. One of the project goals is to develop software support for image classification with visualization and reporting. For that purpose, we developed desktop and web applications that we open-sourced as Imagelytics Suite. Both desktop and web applications rely on a convolutional neural network (CNN) to classify images and the Grad-CAM algorithm to produce heatmaps of the image areas that mostly influenced the network decision. Along with the source code of the applications, we also open-sourced scripts that can be used to train CNN on an arbitrary dataset and produce required metadata, so it can be used with Imagelytics applications. In this article, we presented technical details regarding the design of the applications and the training method that will enable their general use for image classification tasks. As a part of the evaluation, we will show a use case related to species identification of non-biting midges (Diptera: Chironomidae). (shrink)

Homeostatic Property Cluster (HPC) theory suggests that species and other biological taxa consist of organisms that share certain similarities. HPC theory acknowledges the existence of Darwinian variation within biological taxa. The claim is that “homeostatic mechanisms” acting on the members of such taxa nonetheless ensure a significant cluster of similarities. The HPC theorist’s focus on individual similarities is inadequate to account for stable polymorphism within taxa, and fails properly to capture their historical nature. A better approach is to treat (...) distributions of traits in species populations as irreducible facts, explained in terms of selection pressures, genealogy, and other evolutionary factors. We call this view Population Structure Theory (PST). PST accommodates the view, implicit in biological systematics, that species are identified by reference to particular historical populations. (shrink)

The investigations on higher-order type theories and on the related notion of parametric polymorphism constitute the technical counterpart of the old foundational problem of the circularity of second and higher-order logic. However, the epistemological significance of such investigations has not received much attention in the contemporary foundational debate.We discuss Girard’s normalization proof for second order type theory or System F and compare it with two faulty consistency arguments: the one given by Frege for the logical system of the Grundgesetze (...) and the one given by Martin-Löf for the intuitionistic type theory with a type of all types.The comparison suggests that the question of the circularity of second order logic cannot be reduced to Russell’s and Poincaré’s 1906 “vicious circle” diagnosis. Rather, it reveals a bunch of mathematical and logical ideas hidden behind the hazardous idea of impredicative quantification, constituting a vast domain for foundational research. (shrink)

Transparent intensional logic (TIL) is a well-explored type-theoretical framework for semantics of natural language. However, its treatment of polymorphic functions, which are essential for the analysis of various natural language phenomena, is still underdeveloped. In this paper, we address this issue and propose an extension of TIL that introduces polymorphism via type variables ranging over types and generalized variables ranging over constructions and types. Furthermore, we offer an analysis of sentences involving non-specific notional attitudes of the general form ‘_A_ (...) considers (believes, desires, wants, seeks,...) something’. (shrink)

This paper provides a framework, based on Peircean pragmatism and a supplemental metaphysical principle, for reconciling realism and antirealism. Peircean polymorphism, the resultant position defended in the paper, is a realist position, accepting that there is a world that exists and has characteristics of its own, independently of our experience of it. The position denies, however, what I call the uniqueness assumption about truth -- that it is possible for one, unique representational approach to adequately represent reality. While Peirce (...) does not explicitly address the uniqueness assumption, his account is sufficiently ambiguous on this point to have been understood as a uniqueness account. The supplemental metaphysical principle introduced here, that reality is polymorphic, serves to fortify Peirce's pragmatism against uniqueness. Briefly, the paper outlines some implications of accepting the fortified Peircean position, including greater explanatory power and more compelling motivation for continued scientific inquiry. (shrink)

In Pure Inductive Logic, the rational principle of Predicate Exchangeability states that permuting the predicates in a given language L and replacing each occurrence of a predicate in an L-sentence phi according to this permutation should not change our belief in the truth of phi. In this paper we study when a prior probability function w on a purely unary language L satisfying Predicate Exchangeability also satisfies the principle of Unary Language Invariance.

Plural predication is a pervasive part of ordinary language. We can say that some people are fifty in number, are surrounding a building, come from many countries, and are classmates. These predicates can be true of some people without being true of any one of them; they are non-distributive predications. However, the apparatus of modern logic does not allow a place for them. Thomas McKay here explores the enrichment of logic with non-distributive plural predication and quantification. His book will be (...) of great interest to philosophers of language, linguists, metaphysicians, and logicians. (shrink)

I articulate and defend a necessary and sufficient condition for predication. The condition is that a term or term-occurrence stands in the relation of ascription to its designatum, ascription being a fundamental semantic relation that differs from reference. This view has dramatically different semantic consequences from its alternatives. After outlining the alternatives, I draw out these consequences and show how they favour the ascription view. I then develop the view and elicit a number of its virtues.

Whether a predicate is a referential expression depends upon what reference is conceived to be. Even if it is granted that reference is a relation between words and worldly items, the referents of expressions being the items to which they are so related, this still leaves considerable scope for disagreement about whether predicates refer. One of Frege's great contributions to the philosophy of language was to introduce an especially liberal conception of reference relative to which it is unproblematic to suppose (...) that predicates are referring expressions. According to this liberal conception, each significant expression in a language has its own distinctive semantic role or power, a power to effect the truth-value of the sentences in which it occurs. (shrink)

This clearly written book makes logic interesting and easier to learn without sacrificing content or rigor. It covers symbolization, proofs, counterexamples, and truth trees. These topics are presented in graded steps, beginning with the symbolization of categorical propositions and concluding with the properties of relations. Logic is applied to materials with which readers will be familiar; both examples and exercises are drawn from newspapers, television, and other popular sources. For individuals intrigued by the formal study of logic.

This paper explores the possibility of developing a hybrid version of dispositional theories of aesthetic values. On such a theory, uses of aesthetic predicates express relational second-order dispositional properties. If the theory is not absolutist, it allows for the relativity of aesthetic values. But it may be objected to on the grounds that it fails to explain disagreement among subjects who are not disposed alike. This paper explores the possibility of adapting recent proposals of hybrid expressivist theories for moral predicates (...) to the case of aesthetic predicates. Hybrid expressivist theories make no explicit commitment about the kind of property expressed by the predicate, but make explicit commitments to implicated (or presupposed)expressive content. It is argued that dispositionalism about the properties expressed by aesthetic predicates, combined with expressive implicatures (or presuppositions), can account for aesthetic disagreements even in cases where subjects are not relevantly alike. (shrink)

Predicativity is a notable example of fruitful interaction between philosophy and mathematical logic. It originated at the beginning of the 20th century from methodological and philosophical reflections on a changing concept of set. A clarification of this notion has prompted the development of fundamental new technical instruments, from Russell's type theory to an important chapter in proof theory, which saw the decisive involvement of Kreisel, Feferman and Schütte. The technical outcomes of predica-tivity have since taken a life of their own, (...) but have also produced a deeper understanding of the notion of predicativity, therefore witnessing the " light logic throws on problems in the foundations of mathematics. " (Feferman 1998, p. vii) Predicativity has been at the center of a considerable part of Feferman's work: over the years he has explored alternative ways of explicating and analyzing this notion and has shown that predicative mathematics extends much further than expected within ordinary mathematics. The aim of this note is to outline the principal features of predicativity, from its original motivations at the start of the past century to its logical analysis in the 1950-60's. The hope is to convey why predicativity is a fascinating subject, which has attracted Feferman's attention over the years. (shrink)

After the birth of thermodynamics’ second principle—outlined in Carnot's Réflexions sur la puissance motrice du feu —several studies provided new arguments in the field. Mainly, they concerned the thermodynamics’ first principle—including energy conceptualisation—, the analytical aspects of the heat propagation, the statistical aspects of the mechanical theory of heat. In other words, the second half of nineteenth century was marked by an intense interdisciplinary research activity between physics and chemistry: new disciplines applied to the heat developed in the form of (...) analytical, mechanical and statistical theories. Inside all these theories, entropy—the brand-new function that Clausius coined in his Mechanical theory of heat—started to play a central epistemic role. In the present paper, we analyse some steps of the historical process of conceptualisation of such function from 1850 to 1902. Particularly, we retrace the historical–foundational path that—starting from Clausius’ Second Law—lead Boltzmann and Gibbs to their distinguished formulations of statistical entropy. As usual, our research has been unrolled through the analyses of primary sources and by leaning on critical readings of the secondary literature. As for the methodological approach, text analysis of historical documents constituted our privileged modus operandi. This paper is the expression of a collaborative historical research program focused on the thermodynamic foundations of physics–chemistry relationship; early results have already been published by the same authors upon the concepts of reversibility––and––thermal equilibrium. (shrink)

Here, we present a category ${\mathbf {pEff}}$ which can be considered a predicative variant of Hyland's Effective Topos ${{\mathbf {Eff} }}$ for the following reasons. First, its construction is carried in Feferman’s predicative theory of non-iterative fixpoints ${{\widehat {ID_1}}}$. Second, ${\mathbf {pEff}}$ is a list-arithmetic locally cartesian closed pretopos with a full subcategory ${{\mathbf {pEff}_{set}}}$ of small objects having the same categorical structure which is preserved by the embedding in ${\mathbf {pEff}}$ ; furthermore subobjects in ${{\mathbf {pEff}_{set}}}$ are (...) classified by a non-small object in ${\mathbf {pEff}}$. Third ${\mathbf {pEff}}$ happens to coincide with the exact completion of the lex category defined as a predicative rendering in ${{\widehat {ID_1}}}$ of the subcategory of ${{\mathbf {Eff} }}$ of recursive functions and it validates the Formal Church’s thesis. Hence pEff turns out to be itself a predicative rendering of a full subcategory of ${{\mathbf {Eff} }}$. (shrink)

We discuss the challenge to truth-conditional semantics presented by apparent shifts in extension of predicates such as ‘red’. We propose an explicit indexical semantics for ‘red’ and argue that our account is preferable to the alternatives on conceptual and empirical grounds.

I argue that maps do not feature predication, as analyzed by Frege and Tarski. I take as my foil (Casati and Varzi, Parts and places, 1999), which attributes predication to maps. I argue that the details of Casati and Varzi’s own semantics militate against this attribution. Casati and Varzi emphasize what I call the Absence Intuition: if a marker representing some property (such as mountainous terrain) appears on a map, then absence of that marker from a map coordinate signifies absence (...) of the corresponding property from the corresponding location. Predication elicits nothing like the Absence Intuition. “F(a)” does not, in general, signify that objects other than a lack property F. On the basis of this asymmetry, I argue that attaching a marker to map coordinates is a different mode of semantic composition than attaching a predicate to a singular term. (shrink)

The article proposes a renewed analysis of the texts in which Aristotle claims that the term ‘good’ is spoken of in many ways and more precisely in as many ways as there are categories. After a revision of the traditional interpretations, a new reading of the texts is advanced in the light of the theory of predication described in Top. 103 b20-38 and Metaph. 1017 a7-30. The conclusion is that in the Aristotelian passages on the multivocity of ‘good’, the word (...) ‘good’ should not be meant as the predicate of categorially distinct realities, and therefore as a qualifying adjective, but itself as the subject of the question what is it? (τί ἐστι;) In this way, it is possible to advance the hypothesis that the homonymous notion of ‘good’ performs a predicative function, useful to the formulation of practical and prescriptive propositions. (shrink)

Nelson Goodman's new riddle of induction wears many faces. In one of its guises the new riddle of induction appears as the problem of providing a general account of the distinction between projectible and non-projectible predicates. This is the form of the riddle which is supposed to point up a lacuna in the foundations of confirmation theories such as Carnap's which, Goodman charges, work only to the extent that one builds into them just the right predicates. As a new riddle (...) of induction, the problem of distinguishing projectible from non-projectible predicates has the virtue that it is in fact new—a virtue not shared by some other forms of the riddle.Philosophers had recognized previously that some predicates are more projectible than others in the sense that, for instance, the prediction that a certain toss of a die will turn up an even face is safer and more likely to be true than the prediction that the same toss will turn up six. (shrink)

According to indexical contextualism, the perspectival element of taste predicates and epistemic modals is part of the content expressed. According to nonindexicalism, the perspectival element must be conceived as a parameter in the circumstance of evaluation, which engenders “thin” or perspective-neutral semantic contents. Echoing Evans, thin contents have frequently been criticized. It is doubtful whether such coarse-grained quasi-propositions can do any meaningful work as objects of propositional attitudes. In this paper, I assess recent responses by Recanati, Kölbel, Lasersohn and MacFarlane (...) to the “incompleteness worry”. None of them manages to convince. Particular attention is devoted to an argument by John MacFarlane, which states that if perspectives must be part of the content, so must worlds, which would make intuitively contingent propositions necessary. I demonstrate that this attempt to defend thin content views such as nonindexical contextualism and relativism conflates two distinct notions of necessity, and that radical indexicalist accounts of semantics, such as Schaffer’s necessitarianism, are in fact quite plausible. (shrink)

This paper sets out a predicative response to the Russell-Myhill paradox of propositions within the framework of Church’s intensional logic. A predicative response places restrictions on the full comprehension schema, which asserts that every formula determines a higher-order entity. In addition to motivating the restriction on the comprehension schema from intuitions about the stability of reference, this paper contains a consistency proof for the predicative response to the Russell-Myhill paradox. The models used to establish this consistency also (...) model other axioms of Church’s intensional logic that have been criticized by Parsons and Klement: this, it turns out, is due to resources which also permit an interpretation of a fragment of Gallin’s intensional logic. Finally, the relation between the predicative response to the Russell-Myhill paradox of propositions and the Russell paradox of sets is discussed, and it is shown that the predicative conception of set induced by this predicative intensional logic allows one to respond to the Wehmeier problem of many non-extensions. (shrink)

Nucleotide diversity of the human Y chromosome is much lower than that in the rest of the genome. A new hypothesis postulates that this invariance may result from mutations in maternally inherited mitochondrial DNA (mtDNA), leading to impaired reproduction among males and lowered male effective population size. If correct, we should expect to see low levels of polymorphism in the male‐specific Y chromosome of many organisms but not necessarily in the female‐specific W chromosome in organisms with female heterogamety. However, (...) recent observations from birds suggest that the avian W chromosome is very low in nucleotide diversity. This indicates that mtDNA mutations cannot broadly explain the evolution of the sex‐limited chromosome. Other work has suggested that sexual selection at loci involved in sex determination or secondary sexual characteristics might reduce levels of genetic variability on Y through hitch‐hiking effects. Although the W chromosome does not seen to play a dominant role for sex determination in birds, it cannot be excluded that selective sweeps arising from natural or sexual selection contribute to the low levels of genetic variability seen on this chromosome. BioEssays 25:163–167, 2003. © 2003 Wiley Periodicals, Inc. (shrink)

This paper addresses the question, which sex ratio will evolve in a population that is subject to mutation and drift. The problem is analyzed using a simulation model as well as analytical methods. A detailed simulation model for the evolution of a population's allele distribution shows that for the sex ratio game a wide spectrum of different population states may evolve from on the one hand a monomorphic state with one predominant allele and with all other alleles suppressed by the (...) forces of selection, to on the other hand a polymorphism determined by recurrent mutations. Which of these states will evolve depends on the population size, the mating system and the rate of mutations. For the sex ratio game the evolutionarily stable strategy (ESS), as defined by evolutionary game theory, can only predict the population sex ratio but not the underlying stable population state. A comparison of different approaches to the problem shows that false predictions of the stable population states might result from two simplifying assumptions that are fairly common in evolutionary biology:a) it is assumed that mutations are rare events and there is never more than one mutant gene present in a population at any one time; b) a deterministic relationship is assumed between the fitness assigned to an individual's strategy and the individual's contribution to the gene pool of future generations. (shrink)

Most studies examining gene-environment effects on self-regulation focus on outcomes early childhood or adulthood. However, only a few studies investigate longitudinal effects during middle childhood and adolescence and compare two domains of early caregiving. In a longitudinal follow-up with a sample of N = 87, we studied the effects of differences in the DRD4 tandem repeat polymorphisms and two domains of early maternal caregiving quality on children’s personality development using Block’s California Child Q-Set at age six and age 12 and (...) on problem behavior at ages six and seven. Early maternal regulation quality predicted later ego-resiliency and aggressiveness. In addition, significant gene-environment interactions revealed that children with the 7+ DRD4 tandem repeat polymorphism and poor maternal regulation quality in infancy showed lower scores in ego-resiliency and higher scores in ego-undercontrol and CCQ aggressiveness. In contrast, children who had experienced effective maternal regulation in infancy showed a comparable level in personality traits and problem behavior as the DRD4 7- group independent of the levels of maternal regulatory behavior. Similarly, longitudinal caregiving × DRD4 interactions were found for behavior problems in middle childhood, especially for oppositional-aggression, inattentive-hyperactivity, and social competence. Early caregiving effects were only found for maternal regulation quality, but not for maternal responsiveness. Effective early maternal regulation in infancy can moderate the negative effect of DRD4 7+ on children’s self-regulation in middle childhood and adolescence. However, maternal responsiveness has no comparable effects. It seems relevant to consider several dimensions of early caregiving and to also measure the environment in more detail in gene-environment studies. (shrink)

One reason to think that names have a predicate-type semantic value is that they naturally occur in count-noun positions: ‘The Michaels in my building both lost their keys’; ‘I know one incredibly sharp Cecil and one that's incredibly dull’. Predicativism is the view that names uniformly occur as predicates. Predicativism flies in the face of the widely accepted view that names in argument position are referential, whether that be Millian Referentialism, direct-reference theories, or even Fregean Descriptivism. But names are predicates (...) in all of their occurrences; they are predicates that are true of their bearers. When a name appears as a bare singular in argument position, it really occupies the predicate position of what in this essay is called a denuded definite description: a definite description with an unpronounced definite article. Sloat provided good evidence for this. The definite article is sometimes pronounced with names in the singular: ‘The Ivan we all love doesn't feel well’. Sloat proposed a disjunctive generalization of when the definite article must be pronounced with a singular name. This essay shows that by slightly revising Sloat's generalization, we arrive at a simple, nondisjunctive, syntactic rule that governs the overt appearance of the definite article with singular names. But Ivan does not necessarily bear the name ‘Ivan’, so one might worry that the sentence “Ivan might not have had ‘Ivan’ as a name” would incorrectly be predicted false. This essay shows that Predicativism does not have this consequence by showing that incomplete definite descriptions in general and incomplete denuded descriptions, such as ‘Øthe Ivan’, in particular are rigid designators. (shrink)

Acetyltransferase enzymes expressed in hepatic and extrahepatic tissues are products of an acetyltransferase gene locus. Acetylation capacity is regulated by simple autosomal Mendelian inheritance of two codominant alleles at this locus. Human slow acetylators are predisposed to bladder cancer from arylamine chemicals. The role of the bladder in arylamine metabolism and of bladder acetyltransferases in the etiology of bladder cancer is not fully understood, but the acetylator genotype‐dependent expression of arylamine N‐acetyltransferase and N‐hydroxyarylamine O‐acetyltransferase in bladder cytosol may contribute towards (...) the genetic predisposition of human slow acetylators to arylamine‐induced bladder cancer. (shrink)

Lonergan's account of human consciousness as polymorphic self-presence differs significantly from both the variety of contemporary reductionistic accounts and phenomenological treatments still influenced strongly by Cartesian suppositions and/or Kantian restrictions. It is argued that Lonergan's account grounds not only a critical meta-philosophy, but also provides a heuristic structure for a nuanced genetic account of philosophic differences. In this regard, Lonergan's account is claimed to be an adequate grounding for a thorough contemporary response to the Hegelian requirement that philosophers account not (...) only for their own views but for the existence of contrary and differing philosophic convictions. (shrink)

We show that Martin Hyland's effective topos can be exhibited as the homotopy category of a path category EFF. Path categories are categories of fibrant objects in the sense of Brown satisfying two additional properties and as such provide a context in which one can interpret many notions from homotopy theory and Homotopy Type Theory. Within the path category EFF one can identify a class of discrete fibrations which is closed under push forward along arbitrary fibrations (in other words, this (...) class is polymorphic or closed under impredicative quantification) and satisfies propositional resizing. This class does not have a univalent representation, but if one restricts to those discrete fibrations whose fibres are propositions in the sense of Homotopy Type Theory, then it does. This means that, modulo the usual coherence problems, it can be seen as a model of the Calculus of Constructions with a univalent type of propositions. We will also build a more complicated path category in which the class of discrete fibrations whose fibres are sets in the sense of Homotopy Type Theory has a univalent representation, which means that this will be a model of the Calculus of Constructions with a univalent type of sets. (shrink)