When can we do induction over the language defined by a formal grammar?

Question

We can define the grammar of propositional calculus as $G=(\{S\},V_T,D,S)$ where $V_T=\{(,),\land,\lor,\Rightarrow,\Leftrightarrow,\lnot\}\cup\mathcal{P}$. $\mathcal{P}$ is the set of propositional variables and $D$ is the set of the following rules :

• $S\rightarrow(S\land S)$
• $S\rightarrow(S\lor S)$
• $S\rightarrow(S\Rightarrow S)$
• $S\rightarrow(S\Leftrightarrow S)$
• $S\rightarrow\lnot S$
• $S\rightarrow P_i$ where $P_i\in\mathcal{P}$.

Thus, we obtain $L_G$ the language of propositional calculus.

There is an obviously well-founded relation on $L_G$ which is $F\mathcal{R}F'$ if and only if $F$ is a proper immediate subformula of $F'$. $\mathcal{R}$-induction is the usual induction on the formulas and given a truth distribution $\delta$ on $\mathcal{P}$, we in fact use $\mathcal{R}$-recursion to define $\delta$ on $L_G$.

I want to understand the relation between the grammar $G$ and the relation $\mathcal{R}$, if any. If there is one, what is the peculiarity of $G$ that enables the construction of such a well-founded relation (we can do the same with the terms of first order logic and the formulas of first order logic) ?

Answer 1

A context-free grammar like $G$ determines a set of parse trees for sentences in a language. You can always do well-founded induction over parse trees. So a very relevant peculiarity of $G$ is that it is context-free.

Answer 2

A formal grammar is a formalism to describe a set of strings. There is no meaning associated to the strings by the grammar. Any meaning (semantics) is purely external.