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

  • $\begingroup$ 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). $\endgroup$ – Mauro ALLEGRANZA Feb 4 '19 at 7:16
  • $\begingroup$ See page 3 : statement forms $\mathscr A$ vs statement letters $A$. And page 28 for the axioms. $\endgroup$ – Mauro ALLEGRANZA Feb 4 '19 at 7:48
  • $\begingroup$ @MauroALLEGRANZA, yes, I agree, that here is something else than the use of an axiom $\endgroup$ – PeptideChain Feb 4 '19 at 8:52

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

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

  • $\begingroup$ 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. $\endgroup$ – 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.

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.