[FOM] The Natural Language Thesis and Formalization
pratt at cs.stanford.edu
Fri Jan 25 23:26:10 EST 2008
> Concerning Steven Gubkin's "perplexity" about can whether the statement
> Ex(Natx) & Func(x)), I think a simple resolution is to adopt the point
> of view that a function f is, by definition, an ordered triple <A,B,G>
> where G is the graph of f, that is Gubkin's set of ordered pairs
> definition and A is the source and B is the target of f.
This is pretty much equivalent to how category theory keeps things
straight. A morphism has a domain, a codomain, and enough information
to distinguish it from the other morphisms in its homset, making it
essentially a triple as above.
Absent that explicitly given information, telling whether two functions
compose becomes a bit of a hit-or-miss guessing game.
In enriched category theory homsets become homobjects. A preordered set
(reflexive transitive binary relation) is a category enriched in the
2-element chain. Only two homobjects are possible, 0 and 1, making it
obvious that the homobjects need to be tagged with additional
information, namely their domain and codomain, in order to describe an
arbitrary preordered set.
More information about the FOM