A proposition with $n$ connectives has at most $2n + 1$ subformulas I am wondering how to show that a proposition with $n$ connectives has at most $2n + 1$ subformulas.
Subformulas of a proposition $\varphi$ (wff = well formed formula) are all the formulas created using the inductive definition so as to create $\varphi$, including $\varphi$ itself.
For example $\varphi_1$ and $\varphi_2$ are subformulas of $\varphi_1 \wedge \varphi_2$.
I want to show that $\forall n \in \Bbb{N}$ and $\forall \varphi$, if in $\varphi$ there are $n$ connectives, then there are at most $2n+1$ subformulas of $\varphi$.
Initially I thought that it could be proven by induction but I am not so sure now.
 A: You can show this by induction on the number of connectives $n$ in your formula $\varphi$.


*

*Base case $n=0$: then $\varphi$ is an atomic formula, so it has exactly $1 = 2\cdot 0 +1$ subformula, namely itself.

*Inductive case, unary, $n>0$ and $\varphi$ is of the form $\neg \psi$ for some $\psi$: The subformulas of $\varphi$ are then $\varphi$ itself along with all the subformulas of $\psi$. But $\psi$ has $n - 1$ connectives, so by inductive assumption it has no more than $2(n - 1) + 1 = 2n - 1$ subformulas. So the number of subformulas of $\varphi$ is $(2n - 1) + 1 = 2n < 2n+1$.

*Inductive case, binary, $n > 0$ and $\varphi$ is of the form $\psi_1 \wedge \psi_2$ ($\psi_1 \vee \psi_2$, etc.). The subformulas of $\varphi$ are then $\varphi$ itself, along with all subformulas of $\psi_1$ and all subformulas of $\psi_2$. Let $k<n$ denote the number of connectives in $\psi_1$. Then $\psi_2$ has $n-1-k < n$ connectives. By inductive assumption $\psi_1$ has no more than $2k + 1$, and $\psi_2$ has no more than $2(n-1-k) + 1$ subformulas, so the total number of subformulas of $\varphi$ is no more than $(2k+1) + (2(n-1-k) + 1) + 1 = 2n+1$.

A: Your recursive definition of formulas must be treating operators like $\land$ and $\lor$ strictly as binary operators, because otherwise you run into the problem as indicated in the Comments.
But yes, assuming strict binary operators, structural induction over the recursive definition should work just fine. For example: when creating a formula $( \phi \land \psi)$ out of formulas $\phi$ and $\psi$, then assuming the inductive hypothesis holds for $\phi$ and $\psi$ (i.e. With $\phi$ having $n$ operators, $\phi$ has at most $2n+1$ subformulas, and with $\psi$ having $m$ operators, $\psi$ has at most $2m+1$ operators), we can show that the claim holds for $(\phi \land \psi)$ as well: it has $n+m+1$ operators, and it has at most $2n+1+2m+1+1=2(n+m+1)+1$ subformulas.
