> > "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