[FOM] The Natural Language Thesis and Formalization

[Vaughan Pratt]

messing wrote:
> 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.

Vaughan Pratt