Speranza
The inverted iota means "the" in symbolizing a definite description.
Is it an operator?
Word doesn't include it in the operators but in the Letter-like Symbols group, where some are italic and some aren't.
Unicode does not specify it as italic.
Logicians generally prefer to see it as italic, starting with Principia Mathematica 1: 30, and perhaps even with Peano (who did his own typesetting).
Subscribe to:
Post Comments (Atom)
Posts
In Church's Simple Type Theory, a really neat simplification of Russell's Theory of types, iota is just a (higher order) function (of type (i,(o,I)), I.e. a function which takes a property and returns a value which might have that property. The axiom of choice is optional, if you don't include it in the logic then Iota is indefinite description, I.e. "an", but when you add the axiom of choice (in the prescribed way) it becomes definite description (" the").
ReplyDeleteIts more common of course, to use Hilbert's epsilon for choice, and of course you can tweak Church's system to use iota just for indefinite and epsilon for definite descriptions.
As to italics, ... the systems I work with don't usually support italics!
In Church's Simple Type Theory, a really neat simplification of Russell's Theory of types, iota is just a (higher order) function (of type (i,(o,I)), I.e. a function which takes a property and returns a value which might have that property. The axiom of choice is optional, if you don't include it in the logic then Iota is indefinite description, I.e. "an", but when you add the axiom of choice (in the prescribed way) it becomes definite description (" the").
ReplyDeleteIts more common of course, to use Hilbert's epsilon for choice, and of course you can tweak Church's system to use iota just for indefinite and epsilon for definite descriptions.
As to italics, ... the systems I work with don't usually support italics!
Some corrections (to my previous comments)!
ReplyDeleteThe Church type annotations should not have the commas in, he just used juxtaposition for the function space, with the codomain first I think, so "oi" is the type of functions from individuals (i) to propositions (o) and the type of definite description should be "i(oi)" these days more often written ((i->o)->i).
Without choice iota is definite description not indefinite, and adding choice turns it into indefinite description (which entails choice). Alternatively instead of expressing choice as an axiom which makes iota a choice operator, you can use a new symbol (Hilbert's epsilon, which is these days typographically distinct from the epsilon used for set membership) for indefinite description in the choice axiom and leave iota as definite description.