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