Substitution in deduction - Propositional logic

Question

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

Answer 1

See Mendelson, page 76 :

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$ :

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

Answer 2

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.

You also asked specifically:

Is it correct in the framework of deduction in an axiomatic system in propositional logic?

The answer is no, given that you mean Mendelson's "L" or any system which uses a similar definition of proof. Mendelson's L system is very clear in two respects.

1. Every step of a proof for system L has to be a wf. Thus, there is NOT a single proof in Mendelson's book in L (or any other system for that matter), despite his repeated assertions, including his argument for 1.8, since not every step is a wf.
2. Every wf in a proof has to be an axiom/instance of an axiom schema or an application of modus ponens applied to axioms or previously proved wfs. Thus, using something ¬¬γ⊢γ is not legal in L. It's neither an axiom, nor does it consist of an application of modus ponens. So, using it is not legal. This also entails that Mendelson's repeated use of 'corollaries' and 'deduction theorem', both of which consist of meta-theorems, are not legal.

However, I do NOT blame you for making this mistake. I blame Mendelson. He has a clear definition of a proof, but refuses to stick to that definition of a proof for a single moment in the text. He doesn't make it clear at all that he is using meta-language techniques and meta-proofs of strings at best. Instead, he jumps all around to meta-theorems and using meta-theroems and then pulls the wool over beginner's eyes leading them to believe that he has 'proved' things, when his own definition clearly indicates he hasn't proved anything at all in the strict sense he uses the term in multiple ways. Thus, that you aren't clear here I feel has more to do with Mendelson than you.