Well-formed formula
Encyclopedia
In mathematical logic
, a well-formed formula, shortly wff, often simply formula, is a word
(i.e. a finite sequence
of symbols
from a given alphabet) which is part of a formal language
. A formal language can be considered to be identical to the set containing all and only its formulas.
A formula is a syntactic
formal object that can be informally given a semantic meaning.
s 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, 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 being expressed, with the marks being a token
instance of formula. It is not necessary for the existence of a formula that there be any actual tokens of it. A formal language may thus have an infinite number of formulas regardless whether each formula has a token instance. Moreover, a single formula may have more than one token instance, if it is written more than once.
Formulas are quite often interpreted
as proposition
s (as, for instance, in propositional logic). However formulas are syntactic entities
, and as such must be specified in a formal language without regard to any interpretation
of them. An interpreted formula may be the name
of something, an adjective
, an adverb
, a preposition, a phrase
, a clause
, an imperative sentence, a string
of sentences, a string of names, etc.. A formula may even turn out to be nonsense
, if the symbols of the language are specified so that it does. Furthermore, a formula need not be given any interpretation.
, also called propositional formula
s, are expressions such as
. Their definition begins with the arbitrary choice of a set V of propositional variable
s. The alphabet consists of the letters in V along with the symbols for the propositional connective
s and parentheses "(" and ")", all of which are assumed to not be in V. The formulas will be certain expressions (that is, strings of symbols) over this alphabet.
The formulas are inductively defined as follows:
This definition can also be written as a formal grammar in Backus–Naur form
, provided the set of variables is finite:
Using this grammar, the sequence of symbols
(r 
s)) 
(
q 
s))
is a formula, because it is grammatically correct. The sequence of symbols
(qq))p))
is not a formula, because it does not conform to the grammar.
A complex formula may be difficult to read, owing to, for example, the proliferation of parentheses. To alleviate this last phenomenon, precedence rules
are assumed among the operators, making some operators more binding than others. For example, assuming the precedence (from most binding to least binding) 1.
2. 
3. 
4. 
. Then the formula 
(r 
s)) 
(
q 
s))
may be abbreviated as
This is, however, only a convention used to simplify the written representation of a formula.
is relative to the signature of the theory at hand. This signature specifies the constant symbols, relation symbols, and function symbols of the theory at hand, along with the arities of the function and relation symbols.
The definition of a formula comes in several parts. First, the set of terms is defined recursively. Terms, informally, are expressions that represent objects from the domain of discourse.
The next step is to define the atomic formula
s.
Finally, the set of formulas is defined to be the smallest set containing the set of atomic formulas such that the following holds:
If a formula has no occurrences of
or 
, for any variable 
, then it is called quantifier-free. An existential formula is a formula starting with a sequence of existential quantification followed by a quantifier-free formula.
s nor quantifiers
, or equivalently a formula that has no strict subformulas.
The precise form of atomic formulas depends on the formal system under consideration; for propositional logic, for example, the atomic formulas are the propositional variable
s. For predicate logic
, the atoms are predicate symbols together with their arguments, each argument being a term.
According to some terminology, an open formula is formed by combining atomic formulas using only logical connectives, to the exclusion of quantifiers. This has not to be confused with a formula which is not closed.
formula or sentence, is a formula in which there are no free occurrences of any variable
. If A is a formula of a first-order language in which the variables v1, ..., vn have free occurrences, then A preceded by v1 ... vn is a closure of A.
Several authors simply say formula. Modern usages (especially in the context of computer science with mathematical software such as model checkers, automated theorem provers, interactive theorem provers
) tend to retain of the notion of formula only the algebraic concept and to leave the question of well-formedness, i.e. of the concrete string representation of formulas (using this or that symbol for connectives and quantifiers, using this or that parenthesizing convention
, using Polish
or infix
notation, etc.) as a mere notational problem.
However, the expression well-formed formulas can still be found in various works, these authors using the name well-formed formula without necessarily opposing it to the old sense of formula as arbitrary string of symbols so that it is no longer common in mathematical logic to refer to arbitrary strings of symbols in the old sense of formulas.
The expression "well-formed formulas" (WFF) also pervaded in popular culture. Indeed, WFF is part of an esoteric pun used in the name of "WFF 'N PROOF: The Game of Modern Logic," by Layman Allen, developed while he was at Yale Law School
(he was later a professor at the University of Michigan
). The suite of games is designed to teach the principles of symbolic logic to children (in Polish notation
). Its name is an echo of whiffenpoof
, a nonsense word
used as a cheer
at Yale University
made popular in The Whiffenpoof Song and The Whiffenpoofs
.
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, a well-formed formula, shortly wff, often simply formula, is a word
String (computer science)
In formal languages, which are used in mathematical logic and theoretical computer science, a string is a finite sequence of symbols that are chosen from a set or alphabet....
(i.e. a finite sequence
Sequence
In mathematics, a sequence is an ordered list of objects . Like a set, it contains members , and the number of terms is called the length of the sequence. Unlike a set, order matters, and exactly the same elements can appear multiple times at different positions in the sequence...
of symbols
Symbol (formal)
For other uses see Symbol In logic, symbols build literal utility to illustrate ideas. A symbol is an abstraction, tokens of which may be marks or a configuration of marks which form a particular pattern...
from a given alphabet) which is part of a formal language
Formal language
A formal language is a set of words—that is, finite strings of letters, symbols, or tokens that are defined in the language. The set from which these letters are taken is the alphabet over which the language is defined. A formal language is often defined by means of a formal grammar...
. A formal language can be considered to be identical to the set containing all and only its formulas.
A formula is a syntactic
Syntax (logic)
In logic, syntax is anything having to do with formal languages or formal systems without regard to any interpretation or meaning given to them...
formal object that can be informally given a semantic meaning.
Introduction
A key use of formulas is in propositional logic and predicate logicPredicate logic
In mathematical logic, predicate logic is the generic term for symbolic formal systems like first-order logic, second-order logic, many-sorted logic or infinitary logic. This formal system is distinguished from other systems in that its formulae contain variables which can be quantified...
s such as first-order logic
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate 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, proof
Mathematical proof
In mathematics, a proof is a convincing demonstration that some mathematical statement is necessarily true. Proofs are obtained from deductive reasoning, rather than from inductive or empirical arguments. That is, a proof must demonstrate that a statement is true in all cases, without a single...
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 being expressed, with the marks being a token
Type-token distinction
In disciplines such as philosophy and knowledge representation, the type-token distinction is a distinction that separates an abstract concept from the objects which are particular instances of the concept...
instance of formula. It is not necessary for the existence of a formula that there be any actual tokens of it. A formal language may thus have an infinite number of formulas regardless whether each formula has a token instance. Moreover, a single formula may have more than one token instance, if it is written more than once.
Formulas are quite often interpreted
Interpretation (logic)
An interpretation is an assignment of meaning to the symbols of a formal language. Many formal languages used in mathematics, logic, and theoretical computer science are defined in solely syntactic terms, and as such do not have any meaning until they are given some interpretation...
as proposition
Proposition
In logic and philosophy, the term proposition refers to either the "content" or "meaning" of a meaningful declarative sentence or the pattern of symbols, marks, or sounds that make up a meaningful declarative sentence...
s (as, for instance, in propositional logic). However formulas are syntactic entities
Syntax (logic)
In logic, syntax is anything having to do with formal languages or formal systems without regard to any interpretation or meaning given to them...
, and as such must be specified in a formal language without regard to any interpretation
Interpretation (logic)
An interpretation is an assignment of meaning to the symbols of a formal language. Many formal languages used in mathematics, logic, and theoretical computer science are defined in solely syntactic terms, and as such do not have any meaning until they are given some interpretation...
of them. An interpreted formula may be the name
Name
A name is a word or term used for identification. Names can identify a class or category of things, or a single thing, either uniquely, or within a given context. A personal name identifies a specific unique and identifiable individual person, and may or may not include a middle name...
of something, an adjective
Adjective
In grammar, an adjective is a 'describing' word; the main syntactic role of which is to qualify a noun or noun phrase, giving more information about the object signified....
, an adverb
Adverb
An adverb is a part of speech that modifies verbs or any part of speech other than a noun . Adverbs can modify verbs, adjectives , clauses, sentences, and other adverbs....
, a preposition, a phrase
Phrase
In everyday speech, a phrase may refer to any group of words. In linguistics, a phrase is a group of words which form a constituent and so function as a single unit in the syntax of a sentence. A phrase is lower on the grammatical hierarchy than a clause....
, a clause
Clause
In grammar, a clause is the smallest grammatical unit that can express a complete proposition. In some languages it may be a pair or group of words that consists of a subject and a predicate, although in other languages in certain clauses the subject may not appear explicitly as a noun phrase,...
, an imperative sentence, a string
String (computer science)
In formal languages, which are used in mathematical logic and theoretical computer science, a string is a finite sequence of symbols that are chosen from a set or alphabet....
of sentences, a string of names, etc.. A formula may even turn out to be nonsense
Nonsense
Nonsense is a communication, via speech, writing, or any other symbolic system, that lacks any coherent meaning. Sometimes in ordinary usage, nonsense is synonymous with absurdity or the ridiculous...
, if the symbols of the language are specified so that it does. Furthermore, a formula need not be given any interpretation.
Propositional calculus
The formulas of propositional calculusPropositional calculus
In mathematical logic, a propositional calculus or logic is a formal system in which formulas of a formal language may be interpreted as representing propositions. A system of inference rules and axioms allows certain formulas to be derived, called theorems; which may be interpreted as true...
, also called propositional formula
Propositional formula
In propositional logic, a propositional formula is a type of syntactic formula which is well formed and has a truth value. If the values of all variables in a propositional formula are given, it determines a unique truth value...
s, are expressions such as
. Their definition begins with the arbitrary choice of a set V of propositional variablePropositional variable
In mathematical logic, a propositional variable is a variable which can either be true or false...
s. The alphabet consists of the letters in V along with the symbols for the propositional connective
Logical connective
In logic, a logical connective is a symbol or word used to connect two or more sentences in a grammatically valid way, such that the compound sentence produced has a truth value dependent on the respective truth values of the original sentences.Each logical connective can be expressed as a...
s and parentheses "(" and ")", all of which are assumed to not be in V. The formulas will be certain expressions (that is, strings of symbols) over this alphabet.
The formulas are inductively defined as follows:
- Each propositional variable is, on its own, a formula.
- If φ is a formula, then
φ is a formula. - If φ and ψ are formulas, and • is any binary connective, then ( φ • ψ) is a formula. Here • could be (but is not limited to) the usual operators ∨, ∧, →, or ↔.
This definition can also be written as a formal grammar in Backus–Naur form
Backus–Naur form
In computer science, BNF is a notation technique for context-free grammars, often used to describe the syntax of languages used in computing, such as computer programming languages, document formats, instruction sets and communication protocols.It is applied wherever exact descriptions of...
, provided the set of variables is finite:
::= p | q | r | s | t | u | ... (the arbitrary finite set of propositional variables)
Using this grammar, the sequence of symbols
(r s)) (q s))is a formula, because it is grammatically correct. The sequence of symbols
(qq))p))is not a formula, because it does not conform to the grammar.
A complex formula may be difficult to read, owing to, for example, the proliferation of parentheses. To alleviate this last phenomenon, precedence rules
Order of operations
In mathematics and computer programming, the order of operations is a rule used to clarify unambiguously which procedures should be performed first in a given mathematical expression....
are assumed among the operators, making some operators more binding than others. For example, assuming the precedence (from most binding to least binding) 1.
2. 3. 4. . Then the formula (r s)) (q s))may be abbreviated as
- p
q 
r 
s 
q 
s
This is, however, only a convention used to simplify the written representation of a formula.
Predicate logic
The definition of a formula in first-order logicFirst-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
is relative to the signature of the theory at hand. This signature specifies the constant symbols, relation symbols, and function symbols of the theory at hand, along with the arities of the function and relation symbols.The definition of a formula comes in several parts. First, the set of terms is defined recursively. Terms, informally, are expressions that represent objects from the domain of discourse.
- Any variable is a term.
- Any constant symbol from the signature is a term
- an expression of the form f(t1,...,tn), where f is an n-ary function symbol, and t1,...,tn are terms, is again a term.
The next step is to define the atomic formula
Atomic formula
In mathematical logic, an atomic formula is a formula with no deeper propositional structure, that is, a formula that contains no logical connectives or equivalently a formula that has no strict subformulas. Atoms are thus the simplest well-formed formulas of the logic...
s.
- If t1 and t2 are terms then t1=t2 is an atomic formula
- If R is an n-ary relation symbol, and t1,...,tn are terms, then R(t1,...,tn) is an atomic formula
Finally, the set of formulas is defined to be the smallest set containing the set of atomic formulas such that the following holds:
is a formula when 
is a formula
and 
are formulas when 
and 
are formulas;
is a formula when 
is a variable and 
is a formula;
is a formula when 
is a variable and 
is a formula (alternatively, 
could be defined as an abbreviation for 
).
If a formula has no occurrences of
or , for any variable , then it is called quantifier-free. An existential formula is a formula starting with a sequence of existential quantification followed by a quantifier-free formula.Atomic and open formulas
An atomic formula is a formula that contains no logical connectiveLogical connective
In logic, a logical connective is a symbol or word used to connect two or more sentences in a grammatically valid way, such that the compound sentence produced has a truth value dependent on the respective truth values of the original sentences.Each logical connective can be expressed as a...
s nor quantifiers
Quantification
Quantification has several distinct senses. In mathematics and empirical science, it is the act of counting and measuring that maps human sense observations and experiences into members of some set of numbers. Quantification in this sense is fundamental to the scientific method.In logic,...
, or equivalently a formula that has no strict subformulas.
The precise form of atomic formulas depends on the formal system under consideration; for propositional logic, for example, the atomic formulas are the propositional variable
Propositional variable
In mathematical logic, a propositional variable is a variable which can either be true or false...
s. For predicate logic
Predicate logic
In mathematical logic, predicate logic is the generic term for symbolic formal systems like first-order logic, second-order logic, many-sorted logic or infinitary logic. This formal system is distinguished from other systems in that its formulae contain variables which can be quantified...
, the atoms are predicate symbols together with their arguments, each argument being a term.
According to some terminology, an open formula is formed by combining atomic formulas using only logical connectives, to the exclusion of quantifiers. This has not to be confused with a formula which is not closed.
Closed formulas
A closed formula, also groundGround expression
In mathematical logic, a ground term of a formal system is a term that does not contain any variables at all, and a closed term is a term that has no free variables...
formula or sentence, is a formula in which there are no free occurrences of any variable
Variable (mathematics)
In mathematics, a variable is a value that may change within the scope of a given problem or set of operations. In contrast, a constant is a value that remains unchanged, though often unknown or undetermined. The concepts of constants and variables are fundamental to many areas of mathematics and...
. If A is a formula of a first-order language in which the variables v1, ..., vn have free occurrences, then A preceded by v1 ... vn is a closure of A.
Properties applicable to formulas
- A formula A in a language
is validSatisfiability and validityIn mathematical logic, satisfiability and validity are elementary concepts of semantics. A formula is satisfiable if it is possible to find an interpretation that makes the formula true. A formula is valid if all interpretations make the formula true...
if it is true for every interpretationInterpretation (logic)An interpretation is an assignment of meaning to the symbols of a formal language. Many formal languages used in mathematics, logic, and theoretical computer science are defined in solely syntactic terms, and as such do not have any meaning until they are given some interpretation...
of
. - A formula A in a language
is satisfiableSatisfiability and validityIn mathematical logic, satisfiability and validity are elementary concepts of semantics. A formula is satisfiable if it is possible to find an interpretation that makes the formula true. A formula is valid if all interpretations make the formula true...
if it is true for some interpretationInterpretation (logic)An interpretation is an assignment of meaning to the symbols of a formal language. Many formal languages used in mathematics, logic, and theoretical computer science are defined in solely syntactic terms, and as such do not have any meaning until they are given some interpretation...
of
. - A formula A of the language of arithmetic is decidable if it represents a decidable set, i.e. if there is an effective methodEffective methodIn computability theory, an effective method is a procedure that reduces the solution of some class of problems to a series of rote steps which, if followed to the letter, and as far as may be necessary, is bound to:...
which, given a substitutionSubstitutionSubstitution may refer to:- Sciences :* Substitution , a syntactic transformation on strings of symbols of a formal language* Substitution of variables* Substitution cipher, a method of encryption...
of the free variables of A, says that either the resulting instance of A is provable or its negation is.
Usage of the terminology
In earlier works on mathematical logic (e.g. by Church), formulas referred to any strings of symbols and among these strings, well-formed formulas were the strings that followed the formation rules of (correct) formulas.Several authors simply say formula. Modern usages (especially in the context of computer science with mathematical software such as model checkers, automated theorem provers, interactive theorem provers
Interactive theorem proving
In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by man-machine collaboration...
) tend to retain of the notion of formula only the algebraic concept and to leave the question of well-formedness, i.e. of the concrete string representation of formulas (using this or that symbol for connectives and quantifiers, using this or that parenthesizing convention
Order of operations
In mathematics and computer programming, the order of operations is a rule used to clarify unambiguously which procedures should be performed first in a given mathematical expression....
, using Polish
Polish notation
Polish notation, also known as prefix notation, is a form of notation for logic, arithmetic, and algebra. Its distinguishing feature is that it places operators to the left of their operands. If the arity of the operators is fixed, the result is a syntax lacking parentheses or other brackets that...
or infix
Infix notation
Infix notation is the common arithmetic and logical formula notation, in which operators are written infix-style between the operands they act on . It is not as simple to parse by computers as prefix notation or postfix notation Infix notation is the common arithmetic and logical formula notation,...
notation, etc.) as a mere notational problem.
However, the expression well-formed formulas can still be found in various works, these authors using the name well-formed formula without necessarily opposing it to the old sense of formula as arbitrary string of symbols so that it is no longer common in mathematical logic to refer to arbitrary strings of symbols in the old sense of formulas.
The expression "well-formed formulas" (WFF) also pervaded in popular culture. Indeed, WFF is part of an esoteric pun used in the name of "WFF 'N PROOF: The Game of Modern Logic," by Layman Allen, developed while he was at Yale Law School
Yale Law School
Yale Law School, or YLS, is the law school of Yale University in New Haven, Connecticut, United States. Established in 1824, it offers the J.D., LL.M., J.S.D. and M.S.L. degrees in law. It also hosts visiting scholars, visiting researchers and a number of legal research centers...
(he was later a professor at the University of Michigan
University of Michigan
The University of Michigan is a public research university located in Ann Arbor, Michigan in the United States. It is the state's oldest university and the flagship campus of the University of Michigan...
). The suite of games is designed to teach the principles of symbolic logic to children (in Polish notation
Polish notation
Polish notation, also known as prefix notation, is a form of notation for logic, arithmetic, and algebra. Its distinguishing feature is that it places operators to the left of their operands. If the arity of the operators is fixed, the result is a syntax lacking parentheses or other brackets that...
). Its name is an echo of whiffenpoof
Whiffenpoof
The word whiffenpoof can refer to:* an imaginary or indefinite animal; e.g. "the great-horned whiffenpoof;"* a device used for tracking exercises;...
, a nonsense word
Nonsense word
A nonsense word, unlike a sememe, may have no definition. If it can be pronounced according to a language's phonotactics, it is a logatome. Nonsense words are used in literature for poetic or humorous effect. Proper names of real or fictional entities are sometimes nonsense words.-See...
used as a cheer
Cheering
Cheering is the uttering or making of sounds encouraging, stimulating or exciting to action, indicating approval or acclaiming or welcoming persons, announcements of events and the like....
at Yale University
Yale University
Yale University is a private, Ivy League university located in New Haven, Connecticut, United States. Founded in 1701 in the Colony of Connecticut, the university is the third-oldest institution of higher education in the United States...
made popular in The Whiffenpoof Song and The Whiffenpoofs
The Whiffenpoofs
The Yale Whiffenpoofs are the oldest collegiate a cappella group in the United States, established in 1909. Best known for "The Whiffenpoof Song", based on a tune written by Tod Galloway and adapted with lyrics by Meade Minnigerode & George S Pomeroy , the group comprises college...
.
External links
- Well-Formed Formula for First Order Predicate Logic - includes a short JavaJava (programming language)Java is a programming language originally developed by James Gosling at Sun Microsystems and released in 1995 as a core component of Sun Microsystems' Java platform. The language derives much of its syntax from C and C++ but has a simpler object model and fewer low-level facilities...
quiz. - Well-Formed Formula at ProvenMath
- WFF N PROOF game site