On 17/04/2013 8:48 AM, fom wrote: > On 4/17/2013 9:36 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 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.
Frederick seemed to be confused: what I'm doing here has nothing to do with formal systems, theories, axioms of formal systems.
And I _already_ gave clear caveats about that!
>> >> 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. >>
Again, I already made caveat that formal systems, theories aren't relevant to my discussion. > > Really? Are you referring to, say, Kunen's discussion of > Tarski's undefinability of truth by representing formulas > with their Goedel numbers? > > I tried to warn Nam that your question would come up.
No need to warn me. Whatever Frederick has said has no bearing on what I'm talking about here, in which formal systems, theories, axioms of formal systems are irrelevant.
-- ---------------------------------------------------- There is no remainder in the mathematics of infinity.