In this paper, a theory T H based on combining type freeness with logic is introduced and is then used to build a theory of properties which is applied to determiners and quantifiers.

Typed λ-calculus uses two abstraction symbols which are usually treated in different ways: λx:*.x has as type the abstraction Πx:*.*, yet Πx:*.* has type □ rather than an abstraction; moreover, C is allowed and β-reduction evaluates it, but C is rarely allowed. Furthermore, there is a general consensus that λ and Π are different abstraction operators. While we agree with this general consensus, we find it nonetheless important to allow Π to act as an abstraction operator. Moreover, experience with AUTOMATH (...) and the recent revivals of Π-reduction as in [11, 14], illustrate the elegance of giving Π-redexes a status similar to λ-redexes. However, Π-reduction in the λ-cube faces serious problems as shown in [11, 14]: it is not safe as regards subject reduction, it does not satisfy type correctness, it loses the property that the type of an expression is well-formed and it fails to make any expression that contains a Π-redex well-formed. In this paper, we propose a solution to all those problems. The solution is to use a concept that is heavily present in most implementations of programming languages and theorem provers: abbreviations or let-expressions. We will show that the λ-cube extended with Π-conversion and abbreviations satisfies all the desirable properties of the cube and does not face any of the serious problems of Π-reduction. We believe that this extension of the λ-cube is very useful: it gives a full formal study of two concepts that are useful for theorem proving and programming languages. (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 Russell''s Ramified Theory of Types RTT, two hierarchical concepts dominate:orders and types. The use of orders has as a consequencethat the logic part of RTT is predicative.The concept of order however, is almost deadsince Ramsey eliminated it from RTT. This is whywe find Church''s simple theory of types (which uses the type concept without the order one) at the bottom of the Barendregt Cube rather than RTT. Despite the disappearance of orders which have a strong correlation with predicativity, predicative (...) logic still plays an influential role in Computer Science.An important example is the proof checker Nuprl, which is basedon Martin-Löf''s Type Theory which uses type universes. Those type universes,and also degrees of expressions in AUTOMATH, are closely related toorders. In this paper, we show that orders have not disappeared from modern logic and computer science, rather, orders play a crucial role in understanding the hierarchy of modern systems. In order to achieve our goal, we concentrate on a subsystem of Nuprl.The novelty of our paper lies in: (1) a modest revival of Russell's orders, (2) the placing of the historical system RTT underlying the famous Principia Mathematica in a context with a modern system of computer mathematics (Nuprl) and modern type theories (Martin-Löf''s type theory and PTSs), and (3) the presentation of acomplex type system (Nuprl) as a simple and compact PTS. (shrink)

In this paper we consider a type system with a universal type $omega$ where any term (whether open or closed, $beta$-normalising or not) has type $omega$. We provide this type system with a realisability semantics where an atomic type is interpreted as the set of $lambda$-terms saturated by a certain relation. The variation of the saturation relation gives a number of interpretations to each type. We show the soundness and completeness of our semantics and that for different notions of saturation (...) (based on weak head reduction and normal $beta$-reduction) we obtain the same interpretation for types. Since the presence of $omega$ prevents typability and realisability from coinciding and creates extra difficulties in characterizing the interpretation of a type, we define a class ${mathbb U}^+$ of the so-called positive types (where $omega$ can only occur at specific positions). We show that if a term inhabits a positive type, then this term is $beta$-normalisable and reduces to a closed term. In other words, positive types can be used to represent abstract data types. The completeness theorem for ${mathbb U}^+$ becomes interesting indeed since it establishes a perfect equivalence between typable terms and terms that inhabit a type. In other words, typability and realisability coincide on ${mathbb U}^+$. We give a number of examples to explain the intuition behind the definition of ${mathbb U}^+$ and to show that this class cannot be extended while keeping its desired properties. (shrink)

The purpose of this paper is to provide a simple type-free set theory which can be used to give the various readings of collective/distributive sentences.

We provide a syntax and a derivation system fora formal language of mathematics called Weak Type Theory (WTT). We give the metatheory of WTT and a number of illustrative examples.WTT is a refinement of de Bruijn''s Mathematical Vernacular (MV) and hence:– WTT is faithful to the mathematician''s language yet isformal and avoids ambiguities.

Types were invented by Russell to solve the logical paradoxes that resulted from Frege’s generalisaton of the notion of function. Since, the past 100 years saw new formalisations of the notions of functions and types that extend and put to better use Frege’s and Russell ’s inventions. Most such formalisations are extensions of Church’s simply typed λ-calculus. Currently, types and functions are the heart of logic and computation and not only are they so closely intertwined, but their evolution demands that (...) they be treated in the same manner. Both are usually constructed, abstracted over and instantiated and the operations for abstraction, construction, instantiation and substitution act alike on both. This paper aims to give a framework where the relationship between functions and types takes into account the similarity of their construction, abstraction, instantiation and substitution. For such a “types as functions” framework to work, special forms of function abstraction need to be included. (shrink)

In this article, we study the prehistory of type theory up to 1910 and its development between Russell and Whitehead's Principia Mathematica ([71], 1910-1912) and Church's simply typed λ-calculus of 1940. We first argue that the concept of types has always been present in mathematics, though nobody was incorporating them explicitly as such, before the end of the 19th century. Then we proceed by describing how the logical paradoxes entered the formal systems of Frege, Cantor and Peano concentrating on Frege's (...) Grundgesetze der Arithmetik for which Russell applied his famous paradox and this led him to introduce the first theory of types, the Ramified Type Theory (RTT). We present RTT formally using the modern notation for type theory and we discuss how Ramsey, Hilbert and Ackermann removed the orders from RTT leading to the simple theory of types STT. We present STT and Church's own simply typed λ-calculus (λ → C) and we finish by comparing RTT, STT and λ → C. (shrink)

The past decade has seen an explosion of work on calculi of explicit substitutions. Numerous works have illustrated the usefulness of these calculi for practical notions like the implementation of typed functional programming languages and higher order proof assistants. It has also been shown that eta-reduction is useful for adapting substitution calculi for practical problems like higher order unification. This paper concentrates on rewrite rules for eta-reduction in three different styles of explicit substitution calculi: λσ, λse and the suspension calculus. (...) Both λσ and λse when extended with eta-reduction rules, have proved useful for solving higher order unification. We enlarge the suspension calculus with an adequate eta-reduction rule which we show to preserve termination and confluence of the associated substitution calculus and to correspond to the eta rules of the other two calculi. We prove that λσ and λse as well as λσ and the suspension calculus are non-comparable while λse is more adequate than the suspension calculus in simulating one-step beta-reduction. After defining the eta-reduction rule in the suspension calculus, and after comparing these three calculi of explicit substitutions , we then concentrate on the implementation of the rewrite rules of eta-reduction in these calculi. We note that it is usual practice when implementing the eta rule for substitution calculi, to mix isolated applications of eta-reduction with the application of other rules of the corresponding substitution calculi. The main disadvantage of this practice is that the eta rewrite rules so obtained are unclean because they have an operational semantics different from that of the eta-reduction of the λ-calculus. For the three calculi in question enlarged with adequate eta rules we show how to implement these eta rules. For the λse we build a clean implementation of the eta rule and we prove that it is not possible to follow the same approach for the λσ and λsusp. (shrink)

This paper described a formal theory of type judgments for propositional logic notations of PM; I felt the need of my own automated type checker to check their examples. The type checker I wrote did indeed serve to help me referee the paper, but also took a rather different approach to notation and typing for propositional functions of PM, which proved worth writing up independently in our own paper: Holmes, M. Randall, “Polymorphic type– checking for the ramified theory of types (...) of Principia Mathematica”, in Fairouz Kamareddine, ed., Thirty–five Years of Automating Mathematics, Kluwer, 2003, pp. 173-215. (shrink)

In philosophical interpretations of the Laozi the function of the ‘sage’ is a relatively under concentrated on topic. Although nearly every scholar does have something to say about the sage, comments are usually brief and often revolve around the sage as some particular character-type; for example highlighting the sage as a ‘sage-ruler’. In this article we will argue that the sage serves as a tool for understanding the major concepts, thinking, and logic of the Laozi. While the sage does often (...) refer to the sage-ruler this does not mean all references are politically orientated, and even those that are can easily be applied to a host of social situations. This paper thus seeks to appreciate the context for what the Laozi says by looking at how the text itself envisions the embodiment of its ideas through reference to the sage. (shrink)

The paper studies many-dimensional modal logics corresponding to products of Kripke frames. It proves results on axiomatisability, the finite model property and decidability for product logics, by applying a rather elaborated modal logic technique: p-morphisms, the finite depth method, normal forms, filtrations. Applications to first order predicate logics are considered too. The introduction and the conclusion contain a discussion of many related results and open problems in the area.

This paper examines methodological issues raised by revealed preference theory in economics: particularly contemporary revealed preference theory. The paper has three goals. First, to make the case that revealed preference theory is a broad research program in choice theory—not a single theory—and understanding this diversity is essential to any methodological analysis of the program. Second, to explore some of the existing criticisms of revealed preference theory in a way that emphasizes how the effectiveness of the critique depends on the particular (...) version of revealed preference under consideration. Finally, three additional criticisms are presented that are aimed specifically at contemporary revealed preference theory. (shrink)

There is strong reason to doubt that the intuitions Chalmers' meta-problem focuses on are widespread or independent of proto-theoretical prompting. So it's unlikely that they result from factors connected to the nature of consciousness. In any case, it's only the accuracy of the problem intuitions that matters for evaluating theories of consciousness or revealing the nature of consciousness, not an explanation of how they arise. Unless we determine that they're accurate about consciousness, we mustn't assume that realism about consciousness incorporates (...) them, or that denying them means denying that consciousness exists. And we must assess whether they're accurate independently of how they arise. (shrink)

Background: The traditional approach to resolving ethics concerns may not address underlying organisational issues involved in the evolution of these concerns. This represents a missed opportunity to improve quality of care “upstream”. The purpose of this study was to understand better which organisational issues may contribute to ethics concerns. Methods: Directed content analysis was used to review ethics consultation notes from an academic children’s hospital from 1996 to 2006 (N = 71). The analysis utilised 18 categories of organisational issues derived (...) and modified from published quality improvement protocols. Results: Organisational issues were identified in 68 of the 71 (96%) ethics consult notes across a range of patient settings and reasons for consultation. Thirteen of the 18 categories of organisational issues were identified and there was a median of two organisational issues per consult note. The most frequently identified organisational issues were informal organisational culture (eg, collective practices and approaches to situations with ethical dimensions that are not guided by policy), policies and procedures (eg, staff knows policy and/or procedural guidelines for an ethical concern but do not follow it) and communication (eg, communication about critical information, orders, or hand-offs repeatedly does not occur among services). Conclusions: Organisational issues contribute to ethical concerns that result in clinical ethics consults. Identifying and addressing organisational issues such as informal culture and communication may help decrease the recurrence of future similar ethics concerns. (shrink)

This study aimed to determine if people would use social usefulness as a criterion when allocating a kidney to potential recipients. Participants ranked hypothetical patients in order of priority to receive the kidney, using only information on the patients’ volunteering record, intelligence, emotional intelligence, and attractiveness. The results showed that volunteers were prioritized over nonvolunteers, highly intelligent patients over those with average intelligence, patients with high emotional intelligence over those with average emotional intelligence, and good-looking patients over average-looking patients. There (...) was little evidence of personal favoritism. Implications and limitations are discussed. (shrink)

It is almost universally believed that in quantum theory the two following statements hold: all transformations are achieved by a unitary interaction followed by a von-Neumann measurement; all mixed states are marginals of pure entangled states. I name this doctrine the dogma of purification ontology. The source of the dogma is the original von Neumann axiomatisation of the theory, which largely relies on the Schrődinger equation as a postulate, which holds in a nonrelativistic context, and whose operator version holds only (...) in free quantum field theory, but no longer in the interacting theory. In the present paper I prove that both ontologies of unitarity and state-purity are unfalsifiable, even in principle, and therefore axiomatically spurious. I propose instead a minimal four-postulate axiomatisation: associate a Hilbert space \ to each system \; compose two systems by the tensor product rule \; associate a transformation from system \ to \ to a quantum operation, i.e. to a completely positive trace-non-increasing map between the trace-class operators of \ and \; evaluate all joint probabilities through that of a special type of quantum operation: the state preparation. I then conclude that quantum paradoxes—such as the Schroedinger-cat’s, and, most relevantly, the information paradox—are originated only by the dogma of purification ontology, and they are no longer paradoxes of the theory in the minimal formulation. For the same reason, most interpretations of the theory interpret the same dogma, not the strict theory stripped of the spurious postulates. (shrink)

The point of education is to support students to be able to live meaningful, autonomous lives, filled with rich experiences. The arts and aesthetic education are vital to such flourishing lives in that they afford bold, beautiful, moving experiences of awe, wonder and the sublime that are connected to the central human functional capability Nussbaum labels senses, imagination and thought. Everyone ought to have the opportunity to learn about art, to appreciate and create art, to critique art and to understand (...) how we are connected to the culture of our society. A life without art is unimaginable, and to the extent that people lack aesthetic experiences, their lives are impoverished, not ‘fully human’. Given that the distinctive value of art objects is that they afford aesthetic experience, it is upon this foundation that an argument ought to be mounted as to why schooling needs the arts, specialised teachers, and all students deserve aesthetic education. Therefore, in this paper, I offer a defence of compulsory aesthetic education across the curriculum on the basis of the aesthetic experiences the arts afford, and the central role such experiences play in eudaimonia—the flourishing life. (shrink)

Educating against extremism doesn't just involve seeking to prevent individuals from becoming extremists or radicalized, although that, of course, is a significant concern. There is also an important role for education in teaching the rest of us, the general populace, the best way to react and respond when we learn of a terrorist attack or consider the potential risk of violent extremism in our community, or even worldwide, given we are connected globally via technology. In this article, Laura D'Olimpio argues (...) that educators have a central role to play in teaching young people to respond to the news of violent extremism and the worry about terrorists and terrorism in ways that support our sense of community and personal well-being. Among the ways in which educators may support such aims is by educating the emotions. There are practical and moral reasons to temper our fearful reactions, and it is in our best interest to educate pupils to avoid allowing fear of terrorists or violent extremism to interfere with their daily lives and actions. D'Olimpio claims that our best response to extremism, both representationally and practically, is to refuse to be terrified. By not being overwhelmed by fear or altering our day-to-day activities, we not only better support a well-functioning democracy and our own happiness or flourishing, but we also disempower rather than empower extremists. (shrink)

SummaryThe crux of Quine's argument against synonymy— and therewith for a version of pragmatism, and independent/y against mentalism — is his challenge to the other side to explain the behavioural difference between the disposition to employ two predicates, say, interchangeably because of habitually “believing“ them coextensive, and the disposition to do so because of “meaning” the same by each. Since synonymy is taught behaviourally, the distinction in question must make a difference behaviourally, but not necessarily one explainable wholly non‐mentalistically. The (...) distinction is drawn in terms of what would extinguish the disposition. The resultant concept of cognitive synonymy is then used to clarify the difference between trivial and non‐trivial necessary truth, and explain how logical deduction by tautological steps can lead to new knowledge.RésuméLe noeud de I'argumentation de Quine contre la synonymie— et donc pour une version de pragmatisme et indépendamment contre le mentalisme — réside dans le défi lancéà la partie adverse d'expliquer en termes de comportement la différence entre d'une part la disposition à utiliser deux prédicats de façon »interchangeable« parce qu'on les »tcroit« habituellement coextensifs, et d'autre part la disposition à le faire parce que l'un et l'autre »signifiant« la même chose. Puisque la synonymie est prise dans un sens comportemental, cette distinction doit se manifester par une différence de comportement, mais n'est pas nécessairement totalement explicable sans recourir au mental. La distinction est faite en considérant ce qui supprimerait la disposition à les utiliser de façon interchangeable. Le concept de “lsynonymie cognitive” qui se dégage de cette analyse est ensuite utilisé pour clarifier la différence entre des várités nécessaires triviales et non triviales et pour expliquer comment une deduction logique par pas tautologiques peut conduire à des connaissances nouvelles.ZusammenfassungDer entscheidende Punkt in Quines Argument gegen die Synonymitrtt— und damit für eine bestimmte Version des Pragmatismus und unabhängig davon gegen den Mentalismus — ist seine Aufforderung, den verhaltensmässigen Unterschied zu erklaen zwischen einerseits der Disposition, zwei Prädikate in austauschbarer Weise zu verwenden, weil man sie gewohnheitsmässig für Koextensiv hält, und andererseits der Disposition, dies zu tun, weil sie gleiche »Bedeutung« haben. Da die Synonymitlit behaviouristisch gelehrt und gelernt wird, muss die zur Diskussion stehende Unterscheidung verhaltensmässig einen Unterschied ausmachen, welcher jedoch nicht notwendigerweise ganz in nicht‐mentalistischer Termen erklärbar ist. Die Unterscheidung wird in Termen formuliert die die Disposition aufheben warden. Der Begriff der kognitiven Synonyrnitlft. der daraus resultiert, wird dann verwendet, urn den Unterschied zwischen trivialen und nicht‐trivialen notwendigen Wahrheiten zu erläutern und um zu erkläen, wie eine logische Deduktion durch tautologische Schritte zu neuem Wissen führen kann. (shrink)

In an attempt to be rational and objective, and, possibly, to avoid the charge of moral relativism, ethicists seek to categorise and characterise ethical dilemmas. This approach is intended to minimise the effect of the confusing individuality of the context within which ethically challenging problems exist. Despite and I argue partly as a result of this attempt to be rational and objective, even when the logic of the argument is accepted—for example, by healthcare professionals—those same professionals might well respond by (...) stating that the conclusions are unacceptable to them. In this paper, I argue that an interpretative approach to ethical analysis, involving an examination of the ways in which ethical arguments are constructed and shared, can help ethicists to understand the origins of this gap between logic and intuition. I suggest that an argument will be persuasive either if the values underpinning the proposed argument accord with the reader’s values and worldview, or if the argument succeeds in persuading the reader to alter these. A failure either to appreciate or to acknowledge those things that give meaning to the lives of all the interested parties will make this objective far harder, if not impossible, to achieve. If, as a consequence, the narratives ethicists use to make their arguments seem to be about people living in different circumstances, and faced with different choices and challenges, from those the readers or listeners consider important or have to face in their own lives, then the argument is unlikely to seem either relevant or applicable to those people. The conclusion offered by the ethicist will be, for that individual, counterintuitive. Abortion, euthanasia and cadaveric organ donation are used as examples to support my argument. (shrink)

Wesley Newcomb Hohfeld's account of legal rights is now 100 years old. It has been much discussed, and remains very influential with philosophers and lawyers alike. Yet it is still sometimes misunderstood in crucial respects. This article offers a rigorous exposition of Hohfeld's framework; discusses its claims to comprehensiveness and fundamentality, reviewing recent work on the topic; and highlights the argumentative uses of Hohfeld's most important distinction.

Berkowitz and Garrett (2020) raise important arguments in favor of consent for apnea testing used in determining death by neurological criteria (DNC); and yet, a fundamental consideration is left u...

In a recent article [Mertz 2001] in this journal I argued for the virtues of a realist ontology of relation instances (unit attributes). A major strength of this ontology is an assay of ontic ('material') predication that yields an account of individuation without the necessity of positing and defending 'bare particulars'. The crucial insight is that it is the unifying agency or combinatorial aspect of a relation instance as predicable that is for ontology the principium individuationis [Mertz 2002; 1996]. Or (...) in short, what is ontically predicable, precisely as such, is the cause of individuation. As a preface to this positive doctrine I offered arguments against the coherence of bare particulars as defended in an article by J. P. Moreland [1998]. In a reply contained in this issue Moreland and Timothy Pickavance (hereafter M/P) propose to answer my objections [2002]. The response that follows provides reasons why, I contend, M/P have not succeeded in parrying my objections to bare particulars. (shrink)

Current guidelines on investigators' responsibilities to communicate research results to study participants may differ on whether investigators should proactively re-contact participants, the type of results to be offered, the need for clinical relevance before disclosure, and the stage of research at which results should be offered. Lack of consistency on these issues, however, does not undermine investigators' obligation to offer to disclose research results: an obligation rooted firmly in the principle of respect for research participants.

From the first months of life, human infants produce “protophones,” speech-like, non-cry sounds, presumed absent, or only minimally present in other apes. But there have been no direct quantitative comparisons to support this presumption. In addition, by 2 months, human infants show sustained face-to-face interaction using protophones, a pattern thought also absent or very limited in other apes, but again, without quantitative comparison. Such comparison should provide evidence relevant to determining foundations of language, since substantially flexible vocalization, the inclination to (...) explore vocalization, and the ability to interact socially by means of vocalization are foundations for language. Here we quantitatively compare data on vocalization rates in three captive bonobo (Pan paniscus) mother–infant pairs with various sources of data from our laboratories on human infant vocalization. Both humans and bonobos produced distress sounds (cries/screams) and laughter. The bonobo infants also produced sounds that were neither screams nor laughs and that showed acoustic similarities to the human protophones. These protophone-like sounds confirm that bonobo infants share with humans the capacity to produce vocalizations that appear foundational for language. Still, there were dramatic differences between the species in both quantity and function of the protophone and protophone-like sounds. The bonobo protophone-like sounds were far less frequent than the human protophones, and the human protophones were far less likely to be interpreted as complaints and more likely as vocal play. Moreover, we found extensive vocal interaction between human infants and mothers, but no vocal interaction in the bonobo mother–infant pairs—while bonobo mothers were physically responsive to their infants, we observed no case of a bonobo mother vocalization directed to her infant. Our cross-species comparison focuses on low- and moderate-arousal circumstances because we reason the roots of language entail vocalization not triggered by excitement, for example, during fighting or intense play. Language appears to be founded in flexible vocalization, used to regulate comfortable social interaction, to share variable affective states at various levels of arousal, and to explore vocalization itself. (shrink)

This article provides an ISCT analysis of commercial bribery focused on transaction cost economics. In the language of Antitrust, commercial bribery is a form of vertical arrangement subject to the same efficiency analysis that has found other vertical arrangements potentially beneficial to consumers. My analysis shows that actions condemned as commerical bribery in the Honda case may well have benefited Honda's dealer network once promotional free riding and other forms of rent seeking by dealers are considered. I propose that the (...) term "commercial bribery" should be avoided until after an ISCT analysis shows that the community is likely to have been harmed. The term "third-party payments" is a more ethically neutral term with which to begin the analysis. (shrink)