## 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

3 hours 39 min ago

5 hours 2 min ago

5 hours 42 min ago

6 hours 6 min ago

7 hours 2 min ago

7 hours 52 min ago

14 hours 55 sec ago

14 hours 34 min ago

14 hours 45 min ago

1 day 6 hours ago