Well-formed formula

In mathematical logic, propositional logic and predicate logic, a well-formed formula, abbreviated WFF or wff, often 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. In mathematical logic, propositional logic and predicate logic, a well-formed formula, abbreviated WFF or wff, often 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. Two key uses of formulas are in propositional logic and predicate logic. 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. 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 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.