[FOM] sentences talking about themselves

[Randall Holmes]

Dear FOM Colleagues,

In particular, in a type theory one of whose base types is the
collection of expressions in its own language (or a supertype of this,
such as the collection of character strings), it is perfectly possible
to define exactly what is meant by a sentence A expressing the fact
that A itself is provable (with a given collection of proof rules),
since "A is provable (with a given set of rules)" can be expressed in
the language of this theory, and so can the function taking an
expression A to the expression meaning "A is provable".

--Randall Holmes