## User login## Navigation |
## An Intensional Type Theory: Motivation and Cut-EliminationAn Intensional Type Theory: Motivation and Cut-Elimination, Paul C. Gilmore.
Russell showed Frege's original foundations of mathematics inconsistent when he invented Russell's paradox -- does the set of all sets that do not contain themselves contain itself? This paradox arises because Frege's logic contained an unrestricted comprehension principle -- you could create a set from any predicate. This allows you to cook up vicious cycles such as in Russell's paradox, and the traditional method (invented by Russell) for avoiding these cycles is to allow quantification in a predicative hierarchy: when you comprehend a predicate at level i, you create a set at level i+1, and a predicate at a given level can never mention sets at a higher level. This paper claims that you can allow unrestricted impredicative quantification if you keep careful track of Frege's sense-reference distinction, and distinguish between predicates and names of predicates. This (if it really works -- I haven't done more than skim the paper yet) would be a different method of using a predicative hierarchy to avoid the paradoxes. |
## Browse archives## Active forum topics |

## Recent comments

2 days 4 hours ago

2 days 16 hours ago

3 days 1 hour ago

4 days 8 hours ago

4 days 16 hours ago

5 days 2 hours ago

5 days 2 hours ago

5 days 14 hours ago

1 week 2 days ago

2 weeks 6 hours ago