> [DARYL] > Fix a coding for arithmetic, that is, a way to associate a unique > natural number with each statement of arithmetic. In terms of this > coding, a truth predicate Tr(x) is a formula with the following > property: For any statement S in the language of arithmetic, > Tr(#S) <-> S > holds (where #S means the natural number coding the sentence S). > If Tr(x) is a formula of arithmetic, then using techniques > developed by Godel, we can construct a sentence L such that > L <-> ~Tr(#L) > > [JESSE] > Goedel *explicitly* constructed a formula P and showed > that both (1) and (2) were true of P.
"We can construct a formula" /\ || \/ "We can construct *ANY* formula"
T |- any formula
ex contradictione sequitur quodlibet from a contradiction, anything follows