Here's my sketch of a Tarski result about truth not being reflected. 
(Tarski's Truth Theorem)

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

http://www.cs.cornell.edu/Info/People/sfa/
---------
(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)