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

Your blog is very informative, finally, I found exactly what I want. Paypal is an excellent service for online payments but lots of its users confront issues while they access Paypal. If you want to resolve your problems then must visit Paypal ondersteuningsnummer.

ReplyDeleteYour blog is very informative and interesting to read, finally, I found exactly what I searching for. There are lots of users of Macfee antivirus in the world because of its features and easy interface. If you want to explore more interesting facts about Mcafee antivirus or want to resolve your technical issues then must visit bellen Mcafee Nederland.

ReplyDeleteHi, Thank you for sharing such a good and valuable information,It is very important for me. Gmail is the worldwide used email service but sometimes user faces some problems in it. If you want to get some information about the Gmail then you can visit Gmail asiakaspalvelu suomi.

ReplyDelete