FOM: The meaning of truth

[Jeffrey Ketland]

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

[1] 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).

[2] Sol Feferman 1991 "Reflecting on Incompleteness" (JSL).
(adds a primitive truth predicate Tr(x), plus axioms).
[3] Couple of books in 1994, 1996 (in German : (  ), and several papers by
Volker Halbach on disquotational Tarskian truth definitions for arithmetic.
[4] 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 +
satisfaction).
is discussed in:

[6] Richard Kaye 1991: "Models of Peano Arithmetic" (Chapter 15, "Recursive
Saturation").
(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
this PA(S)_0.
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
finite
sequences (n_1, n_2, ...n_k) as numbers. Then you define a valuation
function
v(t, s) meaning "the value of term t in sequence s". More detail is given in
Kaye's book [6].
Then you introduce a *primitive satisfaction predicate* Sat(x, y), with new
axioms:

    (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" &
Sat(f, s*))

[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
arithmetic.

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

Indeed,
(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
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~