# Well-formed formula

formulaformulaswell-formedformulaewell formed formulalogical expressionsLogical formulassubformulaclosedexistential 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.wikipedia
166 Related Articles

### Formal language

formal language theoryformal languageslanguage
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.
Each string concatenated from symbols of this alphabet is called a word, and the words that belong to a particular formal language are sometimes called well-formed words or well-formed formulas.

### Syntax (logic)

syntaxsyntacticlogical syntax
A formula is a syntactic object that can be given a semantic meaning by means of an interpretation.
The symbols, formulas, systems, theorems, proofs, and interpretations expressed in formal languages are syntactic entities whose properties may be studied without regard to any meaning they may be given, and, in fact, need not be given any.

### Symbol (formal)

symbolsymbolsletters
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 symbol or string of symbols may comprise a well-formed formula if it is consistent with the formation rules of the language.

### Propositional formula

algebra of propositionsBooleanBoolean formulas
The formulas of propositional calculus, also called propositional formulas, are expressions such as.
In propositional logic, a propositional formula is a type of syntactic formula which is well formed and has a truth value.

### Propositional calculus

propositional logicpropositionalsentential logic
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. The formulas of propositional calculus, also called propositional formulas, are expressions such as.
Propositional logic may be studied through a formal system in which formulas of a formal language may be interpreted to represent propositions.

### Mathematical logic

formal logicsymbolic logiclogic
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.
Its syntax involves only finite expressions as well-formed formulas, while its semantics are characterized by the limitation of all quantifiers to a fixed domain of discourse.

### First-order logic

predicate logicfirst-orderpredicate calculus
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. For predicate logic, the atoms are predicate symbols together with their arguments, each argument being a term.
The set of formulas (also called well-formed formulas or WFFs) is inductively defined by the following rules:

### Term (logic)

termstermfirst-order terms
First, the set of terms is defined recursively.
In analogy to natural language, where a noun phrase refers to an object and a whole sentence refers to a fact, in mathematical logic, a term denotes a mathematical object and a formula denotes a mathematical fact.

### Atomic formula

atomatomicatomic expressions
The next step is to define the atomic formulas.
In mathematical logic, an atomic formula (also known simply as an atom) 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.

### Logical connective

logical operatorconnectivesconnective
The alphabet consists of the letters in V along with the symbols for the propositional connectives and parentheses "(" and ")", all of which are assumed to not be in V.
See well-formed formula for the rules which allow new well-formed formulas to be constructed by joining other well-formed formulas using truth-functional connectives.

### Satisfiability

satisfiablesatisfiability problemsatisfies
A formula A in a language \mathcal{Q} is valid if it is true for every interpretation of \mathcal{Q}.
A formula is satisfiable if it is possible to find an interpretation (model) that makes the formula true.

### Interpretation (logic)

interpretationinterpretationsinterpreted
A formula A in a language \mathcal{Q} is valid if it is true for every interpretation of \mathcal{Q}.
A formal language consists of a possibly infinite set of sentences (variously called words or formulas) built from a fixed set of letters or symbols.

### Ground expression

ground termgroundground atom
A closed formula, also ground formula or sentence, is a formula in which there are no free occurrences of any variable.
Similarly, a ground formula is a formula that does not contain any free variables.

### Recursive definition

inductive definitionrecursively defineddefined inductively
The formulas are inductively defined as follows:
For example, a well formed formula (wff) can be defined as:

### Formation rule

term
For predicate logic, the atoms are predicate symbols together with their arguments, each argument being a term.
A formal grammar determines which symbols and sets of symbols are formulas in a formal language.

Academic ChallengePropaganda, The GameWFF 'N PROOF: The Game of Modern Logic
WFF is part of an esoteric pun used in the name of the academic game "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).
To win the game, you have to write a proof, using the cubes to create "WFFs" (Well-Formed Formulas).

### Automated theorem proving

automated theorem provertheorem provertheorem proving
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.
For a first order predicate calculus, Gödel's completeness theorem states that the theorems (provable statements) are exactly the logically valid well-formed formulas, so identifying valid formulas is recursively enumerable: given unbounded resources, any valid formula can eventually be proven.

### Well-formedness

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.
Well-formed formula

### Sequence

sequencessequentialinfinite sequence
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.

### Alphabet (formal languages)

alphabetalphabetsinput symbol
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.

### Semantics of logic

formal semanticssemanticslogical semantics
A formula is a syntactic object that can be given a semantic meaning by means of an interpretation.

### Mathematical proof

proofproofsprove
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.

### Type–token distinction

typestokentype
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.

### Propositional variable

Their definition begins with the arbitrary choice of a set V of propositional variables.

### Backus–Naur form

BNFBackus–Naur Form (BNF)Backus normal form
This definition can also be written as a formal grammar in Backus–Naur form, provided the set of variables is finite: