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)