"Mathematical Logic" by Cori and Lascar: Incomplete proof of Lemma 1.9?

I have a question on the book "Mathematical Logic: Propositional calculus, Boolean Algebras, predicate calculus" by Rene Cori and Daniel Lascar.

Proof of Lemma 1.9 given on this page is in three parts (bulleted list). Part 2 is where they prove that $\displaystyle o[\neg F] \geq c[\neg F]$ for any propositional formula $\displaystyle F$. $\displaystyle o[\neg F]$ is the number of opening parentheses in $\displaystyle \neg F$ and $\displaystyle c[\neg F]$ is the number of closing parentheses in $\displaystyle \neg F$.

My argument is that this cannot be proven YET for ANY formula $\displaystyle F$, because it hasn't been proven yet for formulas containing parentheses or the symbols $\displaystyle \wedge , \vee , \Rightarrow , \Leftrightarrow$. That is done in part 3. Part 2 proof is only correct for formulas containing propositional variables (since part 1 proves $\displaystyle o[\neg P] \geq c[\neg P]$ for any propositional variable $\displaystyle P$ ) and the symbol $\displaystyle \neg$.

Propositional formulas and propositional variables are defined in this page.

Am I correct or am I missing something?

Reasonable question. The three parts of the proof are not done consecutively; they are mutually recursive. Part 2 assumes that the induction hypothesis already holds for F. This IH could have been proved by any of the parts, including part 3. Part 2 then extends the claim from F to ¬F.

For example, consider the formula ¬(p /\ ¬q) for propositional variables p and q. Let P(F) denotes the induction statement, i.e., for every initial segment W of F we have o(W) >= c(W). Then the proof proceeds as follows (bottom up).

1. P(p) base case
2. P(q) base case
3. P(¬q) induction step from 2
4. P((p /\ ¬q)) induction step from 1 and 3
5. P(¬(p /\ ¬q)) induction step from 4.

Viewed top down, it can be represented as a tree.

Code:

---

P(¬(p ∧ ¬q))
      |
 P((p ∧ ¬q))
  /    \
 P(p)  P(¬q)
        |
        P(q)

---

So, part 2 uses IH that could have been proved by part 3, and part 3 uses two IHs that could have been proved by part 2, etc.

But shouldn't they mention it in the proof?

Strictly speaking, no. Part 2 starts with the induction hypothesis: "Let F be a formula such that for every initial segment W of F, we have o(W) >= c(W)." If this is assumed, then the proof in part 2 goes through. One does not even have to know why this IH is true. A natural question is, why such reasoning (simply assuming the IH and proving the statement for a larger formula) works. This is guaranteed by Lemma 1.6 (or Lemma 1.7, which is not in the preview).

What I described in the previous post is the rationale, how the proof by induction looks like when it is fully unfolded. However, after one proves that the principle of structural induction is correct, there is no need to ask why induction hypothesis is true; this is simply assumed.

Oh, OK. I understand now. I was wondering what the lemmas 1.6 and 1.7 are used for. Thanks.