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.
|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)|
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)