Formula

https://en.wikipedia.org/wiki/Atomic_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.