[FOM] illative logic
peklund at cs.umu.se
Tue Mar 27 06:07:50 EDT 2012
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.
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
More information about the FOM