[FOM] The Natural Language Thesis and Formalization

Vaughan Pratt pratt at cs.stanford.edu
Fri Jan 25 23:26:10 EST 2008

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

More information about the FOM mailing list