KnowledgeBase » SEMINAR » ID = 642

Urelements in Type Theory: New Definition of "Inherence"

by Mark Bickford
2005-2006

The most useful applications of atoms in logic rely on the concept of "inherence" -- that an atom "a" is inherent in (the equivalence class of) a term t (in a type T). In a logic based on propositions as types, we must make sense of the concept of inherence as a type, and we need rules for reasoning about this type. We would like some version of the principle that if "a" is inherent in the application of f to x then "a" is inherent in either f or in x. I will argue that the full constructive version of this principle is not likely to be true (giving a counter-example to my previous construction that attempted to prove it). But a new, simpler definition of inherence does satisfy the contrapositive of the principle, and we will see that this is strong enough for our intended applications.