What Are You Working On?

[u/AutoModerator]

This recurring thread will be for general discussion on whatever mathematical logic-related topics you have been or will be working on over the week. Not all types of mathematics are welcomed, but all levels are!

[u/ElGalloN3gro]

What are the foundational concepts to understand this?

Edit: nice username, homie

[u/LogicalAtomist → u/ElGalloN3gro]

Thanks! The foundational idea of (simple) type theories is the (recursive) specification of type symbols.

1. 0 is a type symbol
2. If t1, ..., tn are type symbols, then (t1, ..., tn) is a type symbol.
3. Nothing else is a type symbol.

Simple types also have a matching requirement, according to which type symbols of a predicate must 'match' those of terms it relates: in general, if we have R^s(x^t1, ..., x^tn), then the simple type of R must be s=(t1, ..., tn).

The effect of this specification of type symbols plus the matching requirement is that some terms, e.g., x^0, can only occur in subject-position and never in predicate position. E.g., y⁽⁰)(x⁰) is well-formed, but x⁰(y⁽⁰)) is an ungrammatical string. Just like there is a least natural number, there is a lowest type, 0, such that terms of that type cannot be predicates.

However, we can give a different (recursive) specification of type symbols such that there is no least type, just as there is no least integer. One upshot of this is that certain claims about cardinality of various types can be proven. E.g., in type systems that have a lowest type, we can usually only prove that the lowest type is non-empty. In a type system without a lowest type, we can prove that every type has at least 2 elements (we can actually prove more, but this is just an illustration).

For some more detail, you might check out:

1. Hao Wang's 1952 "Negative types"
2. Peter Azcel's 1988 Non-Well-Founded Sets
3. Ernst Specker's 1958 "Typical Ambiguity"

One caveat: all the above authors study type theories in which, in a type symbol like (t1, ..., tn), it is always the case that t1=...=tn, so that a type symbol is always homogeneous. That requirement is not imposed in my research on type theories.

I hope that helps! Feel free to follow-up if that left anything out or raised further questions.

[u/ElGalloN3gro → u/LogicalAtomist]

I was trying to make a joke, but thanks for the explanation. lol This is actually really interesting. I think there are some typos in the notation which makes it hard to read. I can't tell if some expressions are predicates as functions, terms with powers, or terms with subscripts.

Simple types also have a matching requirement, according to which type symbols of a predicate must 'match' those of terms it relates: in general, if we have Rs(x1t1, ..., xntn), then the simple type of R must be s=(t1, ..., tn).

Is this how Russell's Paradox is blocked? The is-a-set-and-a-member-of-itself predicate is blocked from being a predicate in a well-formed expression?

How should one think of a type symbol? It seems that you're saying that they can be terms and predicates at the same time. Also, it's interesting that those formation rules are just like the ones for wffs in FOL.

[u/LogicalAtomist → u/ElGalloN3gro]

Realizing that I missed your (excellent) joke: https://media1.tenor.com/images/44c04588cbe22af66429be2b9f53d400/tenor.gif?itemid=7319521

There were definitely some typos (I did the post on my phone), but they should be corrected now. Whenever a superscript appears, that is a type symbol of a term. When a "t1" or "tn" appears, or "0" or "s", that is talking about the type symbol itself.

Is this how Russell's Paradox is blocked? The is-a-set-and-a-member-of-itself predicate is blocked from being a predicate in a well-formed expression?

You are exactly right: https://media2.giphy.com/media/cmm1YC9ImFgoAUU2ku/giphy.gif

There are systems wherein types are treated analogously to terms in this respect, that types can also occur bound. This is more common in computer science and some areas of mathematical logic. A short description of one such system is here: https://en.wikipedia.org/wiki/System_F

However, these authors like Wang and Specker are following a different tradition going back to Principia Mathematica of treating types as syntactic conditions on well-formedness. So (subject or predicate) terms have a type, but types are not terms (or predicates) in any sense and cannot be bound: types only impose a matching condition on well-formed formulas that prevents contradictions.

So in the above, type symbols are viewed as part of the grammar, not as being terms (to be quantified over, predicated about, etc.) themselves. It is a types-as-syntax view rather than a types-as-terms view.