Nam Nguyen wrote: > > On 19/04/2013 8:42 AM, Frederick Williams wrote: > > 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). > > Which specific way that I've used the symbol 'e' contrary to its usual > interpretation? > > > 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. > > If "provability logic" isn't First Order Logic, then it's not relevant > to the context I'm talking _here about Def-1, Def-2_ .
If. My remark was about your claim that "x is in a non-empty subset of S" could be expressed as a FOL formula, but "x is proven to be in a non-empty subset of S" could not. It depends on what predicate and relation symbols are in the language and how they are interpreted. My 'px' may be a formula in a FO language, just as your 'x e y' may be.
-- 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