[FOM] illative logic

[Patrik Eklund]

Schönfinkel's work is usually seen as 'untyped', but those words, and 
distinctions between 'simple typing' and 'untyping' was obviously not done 
at that time when he was working on his Bausteine. Most of his ideas are 
obviously produced at the early years of Hilbert's lectures.

The concept of type constructors does now exist at that time, not does 
Curry and Church in their 1934 and 1940 papers handle with enough rigour.

If you do it categorically, the underlying signature Sigma can be seen as 
residing at "level 1", and then one can introduce 'type' as a sort in a 
"Sigma-superceding" signature at "level 2", so that sorts on level 1 
become constants of sort 'type' at level 2, and so on, and so so forth. 
This is where the type constructors reside as operators in that 
superceding signature. Terms over this signature then become the 
"constructucted types" at "level 3", and here we have to be careful not 
to mix levels 1 and 3. Traditional lambda calculus has a "don't care" 
attitude about levels 1 and 3, and this is basically the reason why 
hygienic aspects like those for renaming have to considered. Modern 
views on the Howard-Curry isomorphism is also "don't care" about these 
things. We can avoid these issues if we respect what actually belongs to 
respective levels, and no not throw e.g. variables and terms from one 
level to another as we please, and as lambda calculus is doing in the 
calculus definition of "set of lambda terms". I also think we can improve 
our understanding of the formal aspects of the the Howard-Curry 
isomorphism by repsectung the levels.

In this view, Schönfinkel's functions I, C, T, Z and S can be 'simply 
typed', so that both I and C can be seen as having counterparts both on 
level 2 and level 3, whereas for T, Z and S it is not clear what they mean 
as type constructors, i.e. on level 2.

Similar level aspects can be pointed out for Curry's F in his 1934 paper.

Church's 1940 paper involving his iota an o is then interesting in this 
discussion. His iota is clearly 'type', and Church says "o is the type of 
propositions". Church further says: "We purposely refrain from making
more definite the nature of the types o and iota, the formal theory 
admitting of a variety of interpretations in this regard. Of course the 
matter of interpretation is in any case irrelevant to the abstract 
construction of the theory, and indeed other and quite different
interpretations are possible (formal consistency assumed).".

I think modern type theory hasn't solved these things properly. Some 
functional languages try to see it as 'prop' is an additional new type, 
but there are little if any discussions about where such a type would 
reside if proceeding with the level discussions. Obviously, this scratches 
the surface on the nature of quantifiers as well.

We have a recent paper on "Modern eyes on lambda terms" that includes the 
level discussion above and showing what happens when looking at 
Schönfinkel's, Curry's and Church's 1924, 1934 and 1940 papers. If anybody 
is interested, just let me know.

These are 'lative' steps still just looking at the formal aspects of the 
underlying signatures and their related terms, so all this is clearly 
before we go it the 'illative' logic of it all.

Cheers,

Patrik



On Mon, 26 Mar 2012, Alasdair Urquhart wrote:

>
> "The second phase of combinatory logic will be called
> *illative* because we have to deal with concepts
> such as quantification, implication, and categories,
> which are characteristic of logic in the more
> orthodox sense, and there is some precedent for
> using `illation' in connection with logical deduction.
> The word comes from the past participle of Latin
> 'inferre'; the word 'inferential', which
> has acquired a somewhat different meaning, comes
> from the present participle of the same verb."
> 	Curry and Feys, Combinatory Logic, Vol. 1, pp. 257-258.
>
> On Mon, 26 Mar 2012, Arnold Neumaier wrote:
>
>> What is the origin of the term ''illative'' in illative combinatory logic? 
>> What does it mean?
>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>