Friday, 29 April 2011

Validity and Truth-Preservation

The weak theory of validity contains Peano arithmetic, $PA$, plus the scheme (V-Out), and the weak introduction rule (V-Intro). But this theory is consistent, as it already lives inside Peano Arithmetic. Can one consistently add to it the following two truth-theoretic principles?
(a) $\mathbf{Val}(\ulcorner A \urcorner, \ulcorner B \urcorner) \rightarrow (\mathbf{T}(\ulcorner A \urcorner) \rightarrow \mathbf{T}(\ulcorner B \urcorner))$.
(b) $\mathbf{T}(\ulcorner A \rightarrow B \urcorner) \rightarrow (\mathbf{T}(\ulcorner A \urcorner) \rightarrow \mathbf{T}(\ulcorner B \urcorner))$.
The first says that valid inferences preserve truth. The second says, in effect, that Modus Ponens preserves truth. (N.B., everything here is classical first-order logic.) There is a consistent truth extension of $PA$ including axioms:
(i) $\forall x (\mathbf{Prov}_{log}(x) \rightarrow \mathbf{T}(x))$
(ii) $\forall x \forall y(\mathbf{T}(x \dot{\rightarrow} y) \rightarrow (\mathbf{T}(x) \rightarrow \mathbf{T}(y)))$.
These are two of the (three) truth-involving axioms of the theory called $Base_{T}$ in H. Friedman & M. Sheard 1987, "An Axiomatic Approach to Self-Referential Truth", Annals of Pure and Applied Logic 33; it is mentioned also in Sheard's ``A Guide to Truth Predicates in the Modern Era", JSL 59 (1994) and in Sheard's "Weak and Strong Theories of Truth", Studia Logica. Certain kinds of revision-theoretic models for $Base_{T}$ are described in Friedman & Sheard 1987, Sheard 2001 and in Graham Leigh's 2010 PhD thesis, "Proof-Theoretic Investigations into the Friedman-Sheard Theories and Other Theories of Truth". Such models interpret $\mathbf{T}$ using Herzberger sequences - i.e., using the revision operator.
Let $S$ be the theory in $\mathcal{L}_{\mathbf{T}}$ which has the axioms of $PA$, plus (i) and (ii) as additional axioms, with full induction on all formulas in $\mathcal{L}_{\mathbf{T}}$. $S$ is a subtheory of $Base_{T}$ and so is consistent. As noted before, $S$ already proves the (unrestricted) scheme (V-Out) $\mathbf{Val}(\ulcorner A \urcorner, \ulcorner B \urcorner) \rightarrow (A \rightarrow B)$; also, if $A \vdash B$, then $S \vdash \mathbf{Val}(\ulcorner A \urcorner, \ulcorner B \urcorner)$. So, $S$ is closed under the weak introduction rule (V-Intro) for $\mathbf{Val}$. (There is a technical subtlety here. Showing that $PA$ satisfies (V-Out) requires that $PA$ be essentially reflexive. So, one needs to be careful that (V-Out) remains provable after adding new axioms containing $\mathbf{T}$.)
Here's a demonstration that $S$ also proves (a).
1. $S \vdash \forall x (\mathbf{Prov}_{log}(x) \rightarrow \mathbf{T}(x))$ (ax (i)).
2. $S \vdash \mathbf{Prov}_{log}(\ulcorner A \rightarrow B \urcorner) \rightarrow \mathbf{T}(\ulcorner A \rightarrow B \urcorner))$ (from (1)).
3. $S \vdash \mathbf{Prov}_{log}(\ulcorner A \rightarrow B \urcorner) \leftrightarrow \mathbf{Val}(\ulcorner A \urcorner, \ulcorner B \urcorner))$ (defn of $\mathbf{Val}$).
4. $S \vdash \mathbf{Val}(\ulcorner A \urcorner, \ulcorner B \urcorner) \rightarrow \mathbf{T}(\ulcorner A \rightarrow B \urcorner))$ (from (2), (3)).
5. $S \vdash \forall x \forall y(\mathbf{T}(x \dot{\rightarrow} y) \rightarrow (\mathbf{T}(x) \rightarrow \mathbf{T}(y)))$ (ax. (ii)).
6. $S \vdash \mathbf{T}(\ulcorner A \urcorner \dot{\rightarrow} \ulcorner B \urcorner) \rightarrow (\mathbf{T}(\ulcorner A \urcorner) \rightarrow \mathbf{T}(\ulcorner B \urcorner))$ (from (5)).
7. $S \vdash \ulcorner A \urcorner \dot{\rightarrow} \ulcorner B \urcorner = \ulcorner A \rightarrow B \urcorner$ (syntax inside $PA$).
8. $S \vdash \mathbf{T}(\ulcorner A \rightarrow B \urcorner) \rightarrow (\mathbf{T}(\ulcorner A \urcorner) \rightarrow \mathbf{T}(\ulcorner B \urcorner))$ (from (6), (7).
9. $S \vdash \mathbf{Val}(\ulcorner A \urcorner, \ulcorner B \urcorner) \rightarrow (\mathbf{T}(\ulcorner A \urcorner) \rightarrow \mathbf{T}(\ulcorner B \urcorner))$ (from (4), (8)).

No comments:

Post a Comment