On 4/17/2013 11:29 AM, Frederick Williams wrote: > 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. >>> >>> 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. >>> >> >> Really? Are you referring to, say, Kunen's discussion of >> Tarski's undefinability of truth by representing formulas >> with their Goedel numbers? > > Yes, that is what I had in mind. Have I misrepresented Kunen? >
Ran across this yesterday. It has a mention about set theory that is relevant to your statement.
It is not much. Just that truth definitions do not really help since one needs something stronger than set theory upon which to base the construction. I guess the arithmetic of natural numbers relies on the Gentzen consistency proof as a basis for the sensibility of truth predicates. But, I would need to learn more to be sure.
I do not really know much about arithmetic and its metamathematics.