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.

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)