I see two concerns being conflated here: (0) how to motivate the study of a formal system, and (1) how to actually study the formal system.<p>To <i>motivate</i> the study of a formal system, that is, to convince someone that the system is <i>useful</i>, obviosuly you need examples and applications. To a non-mathematician like me, that motivation must come from outside mathematics, e.g., how to design and write reliable programs that are easy to understand and maintain.<p>But, once you have decided that a formal system is useful, you really need to understand it in its own terms. You seem to view formulas as “too abstract”, and in need of “explanation” (not just motivation) in terms of something “more concrete”. I don&#x27;t see why. By itself, a formula is nothing but a well-formed syntax tree, that is, a data structure just like lists or arrays (though usually with more complex internal invariants). Do you think lists and arrays are in need of “explanation”? The rules for manipulating formulas are themselves also fairly mechanical and concrete, just like the rules for manipulating lists and arrays.<p>Or am I missing something?