Here's my sketch of a Tarski result about truth not being reflected. (Tarski's Truth Theorem)
See tarski.txt if this page lays out poorly.

We're assuming we have the type of terms and a representation relation "reps" between terms.

 a) We assume that if t reps s then t is closed.

Notation and some simple corrolaries (indicated by "Thus"):
There are also assumptions about substitution into SUBX(?,?) and Q(?).
 -x- is a variable (and a term) t/e is substitution of term e for variable -x- in t SUBX(t,r) reps t'/r' if t reps t', and r reps r' SUBX(t,r)/e = SUBX(t/e,r/e)) q(t) reps t Q(t) reps q(r) if t reps r. b) Thus, Q(q(t)) reps q(t). Q(t)/e = Q(t/e) f(t) is SUBX(q(t),SUBX(-x-,Q(-x-))) ) s(t) is f(t)/q(f(t)) Thus, s(t) is SUBX( q(t), SUBX( q(f(t)), Q(q(f(t)))) ) ) by (a) on q(t) Thus, s(t) reps t/(f(t)/q(f(t))) by (b) *) Thus, s(t) reps t/s(t) Not(t) is the term built from term t by the negation-denoting operator c) Thus Not(t)/e = Not(t/e).

The Tarskian Argument:

Let F(L,T,tr), where L and T are properties of terms and tr is a term, mean
 1) forall S:term. L(tr/S) if S reps some term 2) & forall t:term. T(Not(t)) iff L(t) and not T(t) 3) & forall S,t:term. if S reps t then ( T(tr/S) iff T(t))

This is meant to be part of the criterion for T being truth on L,
and for tr to denote T (in -x-).
L is supposed to be the class of sentences, T the purported truth predicate.

Glosses of 1,2,3 are:

1) says that inserting any term-representing term into tr forms a sentence; 2) says that negation is faithfully interpreted by the purported truth predicate (we don't need the faithful interpretation of other connective for this proof); 3) says that (substitution into) term tr represents the purported truth predicate itself under the purported truth interpretation.
Then there are no L,T,tr such that F(L,T,tr) because:

 4) Assume F(L,T,tr) 5) let S = s(Not(tr)) 6) S reps Not(tr/S) by (5,*,c) 7) L(tr/S) by (4,1,6) 8) T(tr/S) iff T(Not(tr/S)) by (4,3,6) 9) T(Not(tr/S)) iff L(tr/S) & not T(tr/S) by (4,2) 10) T(Not(tr/S)) iff not T(tr/S) by (9,7) T(tr/S) iff not T(tr/S) by (8,10)

which is false so (4) is false.

qed

sfa Feb 2003
---------
(modifications from previous versions:
- moving the "Not" stuff to after f.p. construction.
- and simplifying substitution notation.
- changed "FU" to "F"
- made L an explicit argument to F
- provided glosses of the clauses in the def of F)