I'm a beginner in Automated Theorem Proving, and I want to proof using the induction principle from the syntactic definition of propositional formulae, define the meta-function $V[\phi]$ which gives set of propositional variables of the propositional formula $\phi$.
Other problem for solving is: Using the induction principle from the syntactic definition of propositional formulae, dene the meta-function $L[\phi]$ which gives the length of the propositional formula $\phi$.
Induction definition of $V[ϕ] = \text { the set of propositional variables of the formula } ϕ$.
(i) If $ϕ$ is atomic, i.e. $ϕ := p_i$ for some propositional variable $p_i$, then : $V[ϕ] = \{ p_i \}$.
(ii) For $ϕ = \lnot \psi$, we have : $V[ϕ] = V[\psi]$.
(iii) For $ϕ = \chi \cdot \psi$, where $\cdot = \{ \to, \leftrightarrow, \land, \lor \}$, we have : $V[ϕ] = V[\chi] \cup V[\psi]$.