A formal language for propositional logic

A formal logical language; formal assertions; parse trees; induction on formulas; unique readability

Now that we are able to work with truth tables and other logical matters that we learned in last week’s post, let us begin to discuss certain issues a little more carefully—we have gotten ahead of ourselves on several points. Namely, although we have been discussing truth, validity, and logical entailment for assertions in the formal language of propositional logic, we haven't actually yet defined this language precisely or said much of substance about it. What exactly counts as an assertion in the formal language?

To my way of thinking, one learns a language best simply by immersing oneself in it; one gains familiarity and fluency through ordinary use long before studying the fine points of its formal grammar. And so I find it perfectly fine for us to have been using the language until now without having had a formal account of its grammatical rules.

But perhaps by now we might begin to describe a little more precisely the syntax and grammar of the formal language of propositional logic. Assertions are fundamentally syntactic objects—an assertion is a certain kind of finite sequence of symbols.