fom
Posts:
1,968
Registered:
12/4/12


Re: Matheology S 224
Posted:
Apr 17, 2013 10:48 AM


On 4/17/2013 9:36 AM, Frederick Williams wrote: > Nam Nguyen wrote: > >> "x is in a nonempty 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 nonempty 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 nonempty 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 nonlogical 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 nonlogical 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?
I tried to warn Nam that your question would come up.
news://news.giganews.com:119/aoSdnaXPlOO2gfPMnZ2dnUVZ_sKdnZ2d@giganews.com

