FOM: The meaning of truth
ketland at ketland.fsnet.co.uk
Tue Nov 7 16:56:31 EST 2000
Charles Silver wrote:
>On the other hand, if (2) is thought worthy of attention, it
>seems to me the only recourse would be to eliminate any reference to
>the standard model when invoking the notion of truth for first-order
>sentences of PA. This would require a revamping of the usual truth
>definition. As a start, let's say that closed formulas of the
>language of PA are flat-out true or flat-out false, depending on
>whether they're true of the natural numbers or false of them. So,
>(the universal closure of) 'S(x) = S(y) -> x = y' would be flat-out
>true. So far, no reference to "models". But, if we wanted to spell
>this out thoroughly, how would we continue? What would the metatheory
>look like (Would there even be a metatheory?)? Does Kanovei, or
>anyone else, have an idea how one might fill in the details?
Dear Charlie - I think the sort of details you're after have been discussed
(see below) and some are even well-known. I seem to remember that Martin
Davis mentioned writing about this in his PhD thesis!!
We're talking about Formalized Truth Theories. I like these. Even better -
they're *common ground* for formalists/nominalists and realists/platonists.
They're just formal systems which prove some appropriate (sub-)set of
instances of Tarski's disquotation scheme Tr(#A) <--> A.
Of course, no consistent formal system (extending Q) contains a predicate
B(x) such that it proves all instances of B(#A) <--> A.
(If you take Tr(x) as a primitive predicate, and add the scheme Tr(#A) <-->
A (for all arithmetic A) to PA, the result is a conservative extension. But
that's a really boring truth theory).
I think the most interesting formalized truth theories are PA(S) and a
weakening which I call PA(S)_0. (See below).
Contemporary stuff on such matters, e.g., see
 Boolos &Jeffrey 1989 ("Computability and Logic"), Chapter 15 (I think),
"On Defining Arithmetic Truth".
(constructs the truth definition for first-order arithmetic *within* Z_2).
 Sol Feferman 1991 "Reflecting on Incompleteness" (JSL).
(adds a primitive truth predicate Tr(x), plus axioms).
 Couple of books in 1994, 1996 (in German : ( ), and several papers by
Volker Halbach on disquotational Tarskian truth definitions for arithmetic.
 Last (and probably least), see Ketland 1999 "Deflationism and Tarski's
Paradise", Mind 108.
The formal system known (to model theorists) as PA(S) (i.e., PA +
is discussed in:
 Richard Kaye 1991: "Models of Peano Arithmetic" (Chapter 15, "Recursive
(Roughly, the main result is this (due to Krajewski, et al 1981): take a
weaker system than PA(S) but without induction on the new formulas. Call
Then: any countable model M of PA can be extended to a recursively saturated
expansion (M*, S) which is a model of PA(S)_0. In particular, it follows
that PA(S)_0 is a conservative extension of PA. I'm not aware of a
proof-theoretic version of this conservation theorem.
OK. Here's one way of writing down PA(S) - from memory. The base axioms are
PA in the language L of arithmetic. Using the pairing function, you code up
sequences (n_1, n_2, ...n_k) as numbers. Then you define a valuation
v(t, s) meaning "the value of term t in sequence s". More detail is given in
Kaye's book .
Then you introduce a *primitive satisfaction predicate* Sat(x, y), with new
(i) Sat(("t1 = t2", s) <--> v(t1, s) = v(t2, s)
This is a disquotational axiom. Using the properties of v(t, s), you can
prove nice disquotational theorems like:
(ia) Sat("t = 0", s) <--> v(t, s) = 0
(ib) Sat("t = 1", s) <--> v(t, s) = 1
(ic) Sat("t1 = t2 + t3", s) <--> v(t1, s) = v(t2, s) + v(t3, s))
(id) Sat("t1 = t2 x t3", s) <--> v(t1, s) = v(t2, s) x v(t3, s))
The important truth-theoretic axioms are:
(ii) Sat(neg(f), s) <--> ~Sat(f, s)
(iii) Sat(conj(f, g), s) <--> Sat(f, s) & Sat(g, s)
(iv) Sat("Exi f", s) <--> Es*("s and s* differ at most at ith place" &
[These just say that "truth commutes through the logical operators". A big
debate between realists and constructivists is whether *proof* commutes with
the logical operators]
(v) Tr(x) <--> (Sent_L(x) & for all s, Sat(x, s))
[So this is the definition of disquotational truth: a sentence A is an
arithmetic truth iff
it's a sentence of L and it's satisfied by all sequences. Basically Tarski's
Definition 23 in his 1935/36 paper].
The resulting formal system is called PA(S). It includes full induction on
formulas containing Sat(x, y).
Some properties of PA(S):
(1) Convention T: PA(S) proves all instances of Tr(#A) <-> A, with A
(2) Liar sentences: Using the Diagonal Lemma, PA(S) also proves a sentence
~~Tr(#X) <-> X. This X is the "liar sentence". Interestingly, PA(S) proves X
as well!! (Because X is constructed by diagonalization on the truth
predicate. So, X contains the truth predicate. So, X isn't a sentence of L.
This is represented in PA. PA |- ~Sent(#X). It follows that PA(S) |-
~~Tr(#X). Hence, PA(S) |- X.)
(3) Conservativeness: Unlike PA(S)_0, PA(S) is a *non-conservative*
extension of PA.
(4) PA(S) |- forall x (Prov_PA(x) --> Tr(x))
(this requires the induction scheme).
(5) A corollary is that if G is a goedel sentence for PA, then PA(S) |- G.
(6) Standard model: If you take the standard model |N for PA, and you take S
to be the standard satisfaction relation on |N, then (|N, S) is the standard
model of PA(S).
But - as you required - PA(S) itself doesn't mention models or anything like
that - it doesn't mention the "standard model". In a sense, PA(S) contains
both PA and a *disquotational* semantic meta-theory for PA, in a single
formal system. Of course, the meta-theory for PA(S) itself is not included
(but you might want to formalize this e-mail message!).
As you required, the formula Tr("for all x, y (S(x) = S(y) -> x = y)") is
(trivially) provable in PA(S).
Best - Jeff
~~~~~~~~~~~ Jeffrey Ketland ~~~~~~~~~
Dept of Philosophy, University of Nottingham
Nottingham NG7 2RD United Kingdom
Tel: 0115 951 5843
Home: 0115 922 3978
E-mail: jeffrey.ketland at nottingham.ac.uk
Home: ketland at ketland.fsnet.co.uk
More information about the FOM