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)

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 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 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)

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)

After presenting a variety of arguments in support of the idea that ordinary names are indexical, I respond to John Perry's recent arguments against the indexicality of names. I conclude by indicating some connections between the theory of names defended here and Wittgenstein's observations on naming, and suggest that the latter may have been misconstrued in the literature.

The passing on of information to GPs by genito-urinary doctors is to be encouraged but is not always possible and ultimately the patient's wishes and confidentiality must be respected if sexually transmitted diseases and HIV infection are to be controlled. Infected health-care workers should seek counselling and medical support and clear guidelines from professional organisations which are in existence. However, they will only do so if strict confidentiality is maintained and assurance about future employment can be given.

The influence of Goethe on Wittgenstein is just beginning to be appreciated. Hacker and Baker, Westphal, Monk, and Haller have all drawn attention to significant affinities between the two men's work, and the number of explicit citations of Goethe in Wittgenstein's texts supports the idea that we are not dealing simply with a matter of deeplying similarities of aim and method, but of direct and major influence. These scholarly developments are encouraging because they help to place Wittgenstein's work within an (...) important tradition of German letters which goes far beyond his contemporaries and immediate forebears in Vienna; and they show that Wittgenstein's profound interest in literature and music is ceasing to be merely a matter of biographical anecdote, and is being used to illuminate some of the most central areas of his work. (shrink)