Online research in philosophy

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)

A bracket abstraction algorithm is a means of translating λ-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 λ-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)

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.

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)

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.

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)