# Substitution in deduction - Propositional logic

Consider the following deduction step: $$((\neg\neg\beta\to\neg\neg\alpha)\to((\neg\neg\beta\to\neg\alpha)\to\neg\beta)$$ $$((\beta\to\alpha)\to((\beta\to\neg\alpha)\to\neg\beta)$$ I have applied $$\neg\neg\gamma\vdash\gamma$$ (proved before) three times.

Intuitively it makes sense. Is it correct in the framework of deduction in an axiomatic system in propositional logic?

How can I justify/proof this passage? It is not axiom, it is not an MP, it is not the deduction or resolution theorem. Is there something like a "Substitution theorem" (similar to the one used with truth assignments)?

In Mendelson2015 I do not find a statement/theorem justifying this passage (perhaps he does not use it at all, I have found no occurrence).

• That kind of substitution is allowed in axioms and theorems (i.e. when we have $\vdash \varphi$). In Mendelson's book, the axioms (and the theorems) are schema: when he write that $A \to (B \to A)$ is a tautology, he means that every formula obtained from it by (uniform) substitution is a tautology (and the same for axioms). – Mauro ALLEGRANZA Feb 4 '19 at 7:16
• See page 3 : statement forms $\mathscr A$ vs statement letters $A$. And page 28 for the axioms. – Mauro ALLEGRANZA Feb 4 '19 at 7:48
• @MauroALLEGRANZA, yes, I agree, that here is something else than the use of an axiom – PeptideChain Feb 4 '19 at 8:52

Replacement Theorem : If $$\mathscr C$$ is a subformula of $$\mathscr B$$, $$\mathscr B'$$ is the result of replacing zero or more occurrences of $$\mathscr C$$ in $$\mathscr B$$ by a wf $$\mathscr D$$, and every free variable [proviso needed for the quantificational case omitted], then:

if $$⊢ \mathscr C ⇔ \mathscr D$$, then $$⊢ \mathscr B ⇔ \mathscr B'$$.

Thus, you have to use $$\vdash \lnot \lnot \beta ⇔ \beta$$ (you have it already : Lemma 1.11 a) and b)), and then apply the Repl.Th to : $$((¬¬β → ¬¬α) → ((¬¬β → ¬α) → ¬β)$$ to get the equivalent :

$$((β → ¬¬α) → ((β → ¬α) → ¬β)$$.

Then, using $$\vdash \lnot \lnot \alpha ⇔ \alpha$$ :

$$((β → α) → ((β → ¬α) → ¬β)$$.

• The definition of a proof given by Mendelson does not allow for the use of meta-theorems in proofs. So, this answer is not correct for what got asked. – Doug Spoonwood Feb 6 '19 at 22:42

I don't follow either as a deduction step. Neither of the first two strings are wfs.

((¬¬β→¬¬α)→((¬¬β→¬α)→¬β)

((β→α)→((β→¬α)→¬β)

In both cases you have for left parenthesis and three right parenthesis. All wfs have the same number of left parenthesis and right parenthesis.