 It should noted that the Greek letter \(\varphi\) stands for the syntactic category of formula. So this definition says: an atom p is a formula; \(\neg\varphi\) is a formula if \(\varphi\) is a formula (read \(\neg\) as ‘it is not the case that’); \((\varphi\wedge\varphi)\) is a formula whenever any two formulas are connected by the \(\wedge\) symbol (read \(\wedge\) as ‘and’); and \(K_{a}\varphi\) and \(B_{a}\varphi\) are formulas whenever \(\varphi\) is a formula (the readings were indicated above).  Note that in a non-BNF recursive specification of the language, the Greek variable \(\varphi\) would be used a metavariable ranging over formulas, and one would normally state the clause for conjunctions as: \((\varphi \wedge \psi)\) is a formula whenever \(\varphi\) and \(\psi\) are formulas. But the BNF let's us get away with just using \(\varphi\) to get the same effect.