David Corfield types

Aristotle and “tode ti”, this such.

Sellars: we see things as instances of kinds, $a:A$.

Everything is typed, but don’t most things have several types? Tibbles is a cat and so a mammal and an animal and so a living being and a thing. Do we need an Aristotelian style tree of types?

Perhaps we introduce a lower level type by forming dependent sums on properties possessed by terms of higher type. So

• $Mammal : Type$
• $Cat = Mammals which ...: Type$, where this is a dependent sum.

Then a term of type Cat is a pair consisting of term of type mammal and a proof that this thing is a cat. Perhaps this is unlikely. CHildren certainly learn ‘Cat’ before ‘Mammal’.

Full story

Kingdom: Animalia Phylum: Chordata Class: Mammalia Order: Carnivora Family: Felidae Genus: Felis Species: Felis catus

What of Redding’s distinction between actualizing a concept and exercizing one? In “This cube is red”, supposedly cube is actualized and red exercized.

Would it need to be that various types are in place, and a shape mapping? So ‘cube’ is ‘object shaped like a cube’.

$$\sum_{x: Object} (shape x = cube)$$

where $cube: Shape$.

But does all this need to happen explicitly, i.e., as exercised, before it can be actualized? Won’t I have to have made the judgement (perhaps of something else) ‘This is a cube’?

On the other hand, doesn’t this belong to a present-at-hand treatment, which ought to rest ultimately on a ready-at-hand? Could I have actualizing as intermediate between ready-at-hand and exercized? What of ‘This eikosohedron is red’ or ‘This chordate is fast’ or ‘This Rose Leaf Miner/Stigmella anomalella is small’?

What of Aristotle’s idea of the essence of a thing, e.g., it’s an accidental property of the cube to be red. Should one only exercise an essential property? Can one say ‘This red cube is large’. On the other hand, ‘This red shade is darker than that’ would be fine as the redness would be part of its essence.

See Aronson, Harre and Way Realism Rescued.