Date: Apr 17, 2013 10:36 AM
Author: Frederick Williams
Subject: Re: Matheology S 224

Nam Nguyen wrote:

> "x is in a non-empty subset of S" could be _expressed_ as a FOL language
> expression: x e S' /\ Ay[ y e S' -> y e S].
>
> On the other hand, in "x is proven to be in a non-empty subset of S",
> the _meta phrase_ "is proven" can not be expressed by a FOL language:
> "is proven" pertains to a meta truth, which in turns can't be equated
> to a language expression: truth and semantics aren't the same.


"x is in a non-empty subset of S" can be expressed in the language of a
first order theory with a binary predicate e. The intended meaning of e
is given by the non-logical axioms of that theory.

What reason is there to suppose that "x is proven" cannot be expressed
in the language of a first order theory with a unary predicate p (say)?
The intended meaning of p would then be given by the non-logical axioms
of that theory.

Note that set theory can express its own provability predicate.

--
When a true genius appears in the world, you may know him by
this sign, that the dunces are all in confederacy against him.
Jonathan Swift: Thoughts on Various Subjects, Moral and Diverting