Date: Apr 19, 2013 10:42 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 a first order
language which has a binary relation symbol 'e' interpreted as the 'is
an element of' relation between sets (though not in the way you have
written). What makes you think that there is no first order language
with a unary predicate (say) 'p' with 'px' interpreted as 'x is proven'
among formulae? I refer you to provability logic.

When you wrote 'truth and semantics aren't the same' did you mean 'truth
and syntax aren't the same'? Or, perhaps, syntax and semantics aren't
the same; though G\"odel and Carnap taught us that a lot of semantics
can be reduced to syntax (but not all, pace Tarski).

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