Editing Well-formed formula (section)

==Introduction==
A key use of formulas is in [[propositional logic]] and [[Higher-order logic|predicate logic]] such as [[first-order logic]].  In those contexts, a formula is a string of symbols φ for which it makes sense to ask "is &phi; true?", once any [[free variable]]s in φ have been instantiated.  In formal logic, [[Mathematical proof|proof]]s can be represented by sequences of formulas with certain properties, and the final formula in the sequence is what is proven.

Although the term "formula" may be used for written marks (for instance, on a piece of paper or chalkboard), it is more precisely understood as the sequence of symbols being expressed, with the marks being a [[type-token distinction|token]] instance of formula. This distinction between the vague notion of "property" and the inductively-defined notion of well-formed formula has roots in Weyl's 1910 paper "Uber die Definitionen der mathematischen Grundbegriffe".<ref>W. Dean, S. Walsh, The Prehistory of the Subsystems of Second-order Arithmetic (2016), p.6</ref> Thus the same formula may be written more than once, and a formula might in principle be so long that it cannot be written at all within the physical universe.

Formulas themselves are syntactic objects. They are given meanings by interpretations. For example, in a propositional formula, each propositional variable may be interpreted as a concrete proposition, so that the overall formula expresses a relationship between these propositions. A formula need not be interpreted, however, to be considered solely as a formula.