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