[FOM] sentences talking about themselves
Randall Holmes
holmes at diamond.boisestate.edu
Fri Oct 17 12:42:19 EDT 2003
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
More information about the FOM
mailing list