A bracket abstraction algorithm is a means of translating $\lambda$-terms into combinators. Broda and Damas, in [1], introduce a new, rather natural set of combinators and a new form of bracket abstraction which introduces at most one combinator for each $\lambda$-abstraction. This leads to particularly compact combinatory terms. A disadvantage of their abstraction process is that it includes the whole Schonfinkel [4] algorithm plus two mappings which convert the Schonfinkel abstract into the new abstract. This paper shows how the new (...) abstraction can be done more directly, in fact, using only 2n - 1 algorithm steps if there are n occurrences of the variable to be abstracted in the term. Some properties of the Broda-Damas combinators are also considered. (shrink)

Pure Type Systems, PTSs, were introduced as a generalization of the type systems of Barendregt's lambda cube and were designed to provide a foundation for actual proof assistants which will verify proofs. Systems of illative combinatory logic or lambda calculus, ICLs, were introduced by Curry and Church as a foundation for logic and mathematics. In an earlier paper we considered two changes to the rules of the PTSs which made these rules more like ICL rules. This led to four kinds (...) of PTSs. Most importantly PTSs are about statements of the form M:A, where M is a term and A a type. In ICLs there are no explicit types and the statements are terms. In this paper we show that for each of the four forms of PTS there is an equivalent form of ICL, sometimes if certain conditions hold. (shrink)

This paper gives a simple, elegant statement of the condensed detachment rule that is independent of most general unifiers and proves that this is equivalent to the longer, more usual, formulation.

The formulas-as-types isomorphism tells us that every proof and theorem, in the intuitionistic implicational logic $H_\rightarrow$, corresponds to a lambda term or combinator and its type. The algorithms of Bunder very efficiently find a lambda term inhabitant, if any, of any given type of $H_\rightarrow$ and of many of its subsystems. In most cases the search procedure has a simple bound based roughly on the length of the formula involved. Computer implementations of some of these procedures were done in (...) Dekker. In this paper we extend these methods to full classical propositional logic as well as to its various subsystems. This extension has partly been implemented by Oostdijk. (shrink)

The standard deduction theorem or introduction rule for implication, for classical logic is also valid for intuitionistic logic, but just as with predicate logic, other rules of inference have to be restricted if the theorem is to hold for weaker implicational logics.In this paper we look in detail at special cases of the Gentzen rule for and show that various subsets of these in effect constitute deduction theorems determining all the theorems of many well known as well as not well (...) known implicational logics. In particular systems of rules are given which are equivalent to the relevance logics E,R, T, P-W and P-W-I. (shrink)

In the early thirties, Church developed predicate calculus within a system based on lambda calculus. Rosser and Kleene developed Arithmetic within this system, but using a Godelization technique showed the system to be inconsistent.Alternative systems to that of Church have been developed, but so far more complex definitions of the natural numbers have had to be used. The present paper based on a system of illative combinatory logic developed previously by the author, does allow the use of the Church numerals. (...) Given a new definition of equality all the Peano-type axioms of Mendelson except one can be derived. A rather weak extra axiom allows the proof of the remaining Peano axiom. Note. The illative combinatory logic used in this paper is similar to the logic employed in computer languages such as ML. (shrink)

The first system of intersection types, Coppo and Dezani [3], extended simple types to include intersections and added intersection introduction and elimination rules (( $\wedge$ I) and ( $\wedge$ E)) to the type assignment system. The major advantage of these new types was that they were invariant under β-equality, later work by Barendregt, Coppo and Dezani [1], extended this to include an (η) rule which gave types invariant under βη-reduction. Urzyczyn proved in [6] that for both these systems it is (...) undecidable whether a given intersection type is empty. Kurata and Takahashi however have shown in [5] that this emptiness problem is decidable for the sytem including (η), but without ( $\wedge$ I). The aim of this paper is to classify intersection type systems lacking some of ( $\wedge$ I), ( $\wedge$ E) and (η), into equivalence classes according to their strength in typing λ-terms and also according to their strength in possessing inhabitants. This classification is used in a later paper to extend the above (un)decidability results to two of the five inhabitation-equivalence classes. This later paper also shows that the systems in two more of these classes have decidable inhabitation problems and develops algorithms to find such inhabitants. (shrink)

In positive logic the negation of a propositionA is defined byA X whereX is some fixed proposition. A number of standard properties of negation, includingreductio ad absurdum, can then be proved, but not the law of noncontradiction so that this forms a paraconsistent logic. Various stronger paraconsistent logics are then generated by putting in particular propositions forX. These propositions range from true through contingent to false.

A Hilbert-style version of an implicational logic can be represented by a set of axiom schemes and modus ponens or by the corresponding axioms, modus ponens and substitution. Certain logics, for example the intuitionistic implicational logic, can also be represented by axioms and the rule of condensed detachment, which combines modus ponens with a minimal form of substitution. Such logics, for example intuitionistic implicational logic, are said to be D-complete. For certain weaker logics, the version based on condensed detachment and (...) axioms (the condensed version of the logic) is weaker than the original. In this paper we prove that the relevant logic T→, and any logic of which this is a sublogic, is D-complete. (shrink)

In Fiction, Truth and Literature, Lamarque and Olsen argue that if a critic claims or attempts to prove that the outlook of a work of literature is true or false, he is not engaging in literary or aesthetic appreciation. This paper argues against this position by adducing cases where literary critics discuss the truth or falsity of a work’s view, when their opinions are obviously relevant to the work’s aesthetic assessment. The paper considers in detail the way factual errors damage (...) a work’s aesthetic standing, and shows that Lamarque and Olsen’s alternative account of the role of propositional truths in literature only looks plausible because it considers a restricted range of examples. Finally, it considers the role intention, date and genre play in discussions of the aesthetic damage done by literal falsehood. (shrink)

An attitude which hopes to derive aesthetic pleasure from an object is often thought to be in tension with an attitude which hopes to derive knowledge from it. The current article argues that this alleged conflict only makes sense when the aesthetic attitude and knowledge are construed unnaturally narrowly, and that when both are correctly understood there is no tension between them. To do this, the article first proposes a broad and satisfying account of the aesthetic attitude, and then considers (...) and rejects twelve reasons for thinking that deriving knowledge from something is incompatible with maintaining an aesthetic attitude towards it. Two main conclusions are drawn. 1) That the representational arts are often in a good position to communicate non-propositional knowledge about human beings. 2) That while our desire to obtain pleasure from a work's manifest properties, and our desire to obtain knowledge from it, are not the same motive, the formal similarities between them are sufficiently impressive to warrant both being seen as elements of the aesthetic attitude. (shrink)

Precision Medicine has become a common label for data-intensive and patient-driven biomedical research. Its intended future is reflected in endeavours such as the Precision Medicine Initiative in the USA. This article addresses the question whether it is possible to discern a new ‘medical cosmology’ in Precision Medicine, a concept that was developed by Nicholas Jewson to describe comprehensive transformations involving various dimensions of biomedical knowledge and practice, such as vocabularies, the roles of patients and physicians and the conceptualisation of disease. (...) Subsequently, I will elaborate my assessment of the features of Precision Medicine with the help of Michel Foucault, by exploring how precision medicine involves a transformation along three axes: the axis of biomedical knowledge, of biomedical power and of the patient as a self. Patients are encouraged to become the managers of their own health status, while the medical domain is reframed as a data-sharing community, characterised by changing power relationships between providers and patients, producers and consumers. While the emerging Precision Medicine cosmology may surpass existing knowledge frameworks; it obscures previous traditions and reduces research-subjects to mere data. This in turn, means that the individual is both subjected to the neoliberal demand to share personal information, and at the same time has acquired the positive ‘right’ to become a member of the data-sharing community. The subject has to constantly negotiate the meaning of his or her data, which can either enable self-expression, or function as a commanding Superego. (shrink)