# Formula

[https://en.wikipedia.org/wiki/Atomic\_formula](https://en.wikipedia.org/wiki/Atomic_formula) [https://en.wikipedia.org/wiki/Well-formed\_formula](https://en.wikipedia.org/wiki/Well-formed_formula)

A **well-formed formula** (WFF), or simply formula, is a finite sequence of symbols from a given alphabet that is part of a formal language. A formal language can be identified with the set of formulas in the language.

A formula is a syntactic object that can be given a semantic meaning by means of an interpretation. A key use of formulas is in propositional logic and 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 φ true?", once any free variables in φ have been instantiated.

In formal logic, proofs can be represented by sequences of formulas with certain properties, and the final formula in the sequence is what is proven.

A formula is more precisely understood as the sequence of symbols being expressed, with the marks being a token instance of formula. 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 are _syntactic objects_ that 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.
