Well-formed formula

This diagram shows the syntactic entities which may be constructed from formal languages. The symbols and strings of symbols may be broadly divided into nonsense and well-formed formulas. A formal language can be thought of as identical to the set of its well-formed formulas. The set of well-formed formulas may be broadly divided into theorems and non-theorems. However, quite often, a formal system will simply define all of its well-formed formula as theorems.^[1]

In mathematical logic, a well-formed formula (often abbreviated wff) is a word (i.e. a finite sequence of symbols from a given alphabet) which is part of a formal language.^[2] It is a syntactic object that can be given a semantic meaning. A formal language can be considered to be identical to the set containing all and only its wffs.

In more recent usage well-formed formulas are simply called formulas^[3], because it is no longer common in this context to refer to arbitrary words in this way.

Introduction

A key use of wffs is in propositional logic and predicate logics 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 wffs with certain properties, and the final wff in the sequence is what is proven.

Although the term "well-formed 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 well-formed formula that there be any actual tokens of it. A formal language may thus have an infinite number of well-formed 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.

Well-formed formulas are quite often interpreted as propositions (as, for instance, in propositional logic). However wffs are syntactic entities, and as such must be specified in a formal language without regard to any interpretation of them. An interpreted well-formed 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, etcetera. A well-formed formula may even turn out to be nonsense, if the symbols of the language are specified so that it does. Furthermore, a well-formed formula need not be given any interpretation.

Propositional calculus

The well-formed formulas of propositional calculus are expressions such as $A \land (B \lor C)$ . Their definition begins with the arbitrary choice of a set of V propositional variables. 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. The wffs will be certain expressions (that is, strings of symbols) over this alphabet.

The well-formed formulas are inductively defined as follows:

Each propositional variable is, on its own, a wff.
If φ is a wff, then $\lnot$ φ is a wff.
If φ and ψ are wffs, and • is any binary connective, then ( φ • ψ) is a wff. Here • could be ∨, ∧, →, or ↔.

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

<alpha set> ::= p | q | r | s | t | u | ... (the arbitrary finite set of propositional variables)

Using this grammar, the sequence of symbols

(((p $\rightarrow$ q) $\wedge$ (r $\rightarrow$ s)) $\vee$ ( $\neg$ q $\wedge$ $\neg$ s))

is a WFF, because it is grammatically correct. The sequence of symbols

((p $\rightarrow$ q) $\rightarrow$ (qq))p))

is not a WFF, because it does not conform to the grammar.

A complex wff 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. $\neg$ 2. $\rightarrow$ 3. $\wedge$ 4. $\vee$ . Then the wff

(((p $\rightarrow$ q) $\wedge$ (r $\rightarrow$ s)) $\vee$ ( $\neg$ q $\wedge$ $\neg$ s))

may be abbreviated as

p $\rightarrow$ q $\wedge$ r $\rightarrow$ s $\vee$ $\neg$ q $\wedge$ $\neg$ s

This is, however, only a convention used to simplify the written representation of a wff.

Predicate logic

The definition of a formula in first-order logic $\mathcal{QS}$ 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(t₁,...,t_n), where f is an n-ary function symbol, and t₁,...,t_n are terms, is again a term.

The next step is to define the atomic formulas.

If t₁ and t₂ are terms then t₁=t₂ is an atomic formula
If R is an n-ary relation symbol, and t₁,...,t_n are terms, then R(t₁,...,t_n) is an atomic formula

Finally, the set of WFFs is defined to be the smallest set containing the set of atomic WFFs such that the following holds:

$\neg\phi$ is a WFF when $\ \phi$ is a WFF
$(\phi \land \psi)$ and $(\phi \lor \psi)$ are WFFs when $\ \phi$ and $\ \psi$ are WFFs;
$\exists x\, \phi$ is a WFF when x is a variable and $\ \phi$ is a WFF;
$\forall x\, \phi$ is a WFF when $\ x$ is a variable and $\ \phi$ is a WFF (alternatively, $\forall x\, \phi$ could be defined as an abbreviation for $\neg\exists x\, \neg\phi$ ).

If a formula has no occurrences of $\exists x$ or $\forall x$ , for any variable $\ x$ , then it is called quantifier-free. An existential formula is a string of existential quantification followed by a quantifier-free formula.

Atomic and open formulas

Main article: Atomic formula

An atomic formula is a formula that contains no logical connectives or equivalently a formula that has no strict subformulas.

An open formula is formed by combining atomic formulas using logical connectives.

The precise form of atomic formulas depends on the formal system under consideration; for propositional logic, for example, the atomic formulas are the propositional variables. For predicate logic, the atoms are predicate symbols together with their arguments, each argument being a term.

Closed formulas

Main articles: Closed formula and Sentence (mathematical logic)

A closed formula is a formula in which there are no free occurrences of any variable.

Valid formula

Main article: Validity

A formula A of a first order language $\mathcal{Q}$ is valid if it is true for every interpretation of $\mathcal{Q}$ .

Closure of a formula

If A is a formula of a first-order language in which the variables v₁, ... , v_n have free occurrences, then A preceded by $\forall$ v₁ ... $\forall$ v_n is a closure of A.

Satisfiable formula

Main article: Satisfiability

A formula A of a first order language $\mathcal{Q}$ is satisfiable iff there is some interpretation $\mathcal{I}$ of $\mathcal{Q}$ for which A is satisfied (i.e. there is an interpretation $\mathcal{I}$ such that A is satisfied by at least one denumerable sequence of members of the domain of $\mathcal{I}$ .)

Undecidable formula

Main article: Decidability (logic)

A formula A is decidable in a first-order system $\mathcal{QS}$ iff either A or its negation is a theorem of $\mathcal{QS}$ .

Wffs in popular culture

WFF is part of an esoteric pun used in the name of "WFF 'N PROOF: The Game of Modern Logic," by Layman Allen^[4], 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)^[5]. 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^[6].

Notes

^ Hofstadter 1980
^ Wffs are a standard topic in introductory logic, and are covered by all introductory textbooks, including Enderton (2001), Gamut (1990), and Kleene (1967)
^ Hodges 2001
^ Ehrenburg 2002
^ More technically, propositional logic using the Fitch-style calculus.
^ Allen (1965) acknowledges the pun.

References

Allen, Layman E. (1965), "Toward Autotelic Learning of Mathematical Logic by the WFF 'N PROOF Games", Mathematical Learning: Report of a Conference Sponsored by the Committee on Intellective Processes Research of the Social Science Research Council, Monographs of the Society for Research in Child Development 30 (1): 29–41
Boolos, George; Burgess, John; Jeffrey, Richard (2002), Computability and Logic (4th ed.), Cambridge University Press, ISBN 9780521007580 (pb.)
Ehrenberg, Rachel (Spring 2002). "He's Positively Logical". Michigan Today (University of Michigan). http://www.umich.edu/~newsinfo/MT/02/Spr02/mt9s02.html. Retrieved 2007-08-19.
Enderton, Herbert (2001), A mathematical introduction to logic (2nd ed.), Boston, MA: Academic Press, ISBN 978-0-12-238452-3
Gamut, L.T.F. (1990), Logic, Language, and Meaning, Volume 1: Introduction to Logic, University Of Chicago Press, ISBN 0226280853
Goble, Lou, ed. (2001), The Blackwell Guide to Philosophical Logic, Blackwell, ISBN 978-0-631-20692-7
Hofstadter, Douglas (1980), Gödel, Escher, Bach: An Eternal Golden Braid, Penguin Books, ISBN 978-0-14-005579-5
Kleene, Stephen Cole (2002) [1967], Mathematical logic, New York: Dover Publications, MR 1950307, ISBN 978-0-486-42533-7

External links

Well-Formed Formula for First Order Predicate Logic - includes a short Java quiz.
Well-Formed Formula at ProvenMath
WFF N PROOF game site

Logic

Academic areas	Argumentation theory · Axiology · Critical thinking · Computability theory · Formal semantics · History of logic · Informal logic · Logic in computer science · Mathematical logic · Mathematics · Metalogic · Metamathematics · Model theory · Philosophical logic · Philosophy · Philosophy of logic · Philosophy of mathematics · Proof theory · Set theory

Foundational concepts	Abduction · Analytic truth · Antinomy · A priori · Deduction · Definition · Description · Entailment · Induction · Inference · Logical consequence · Logical form · Logical implication · Logical truth · Name · Necessity · Meaning · Paradox · Possible world · Presupposition · Probability · Reason · Reasoning · Reference · Semantics · Statement · Substitution · Syntax · Truth · Truth value · Validity

Philosophical logic

Critical thinking and Informal logic	Analysis · Ambiguity · Belief · Credibility · Evidence · Explanation · Explanatory power · Fact · Fallacy · Inquiry · Opinion · Parsimony · Premise · Propaganda · Prudence · Reasoning · Relevance · Rhetoric · Rigor · Vagueness

Theories of deduction	Constructivism · Dialetheism · Fictionalism · Finitism · Formalism · Intuitionism · Logical atomism · Logicism · Nominalism · Platonic realism · Pragmatism · Realism

Metalogic and Metamathematics

Cantor's theorem · Church's theorem · Church's thesis · Consistency · Effective method · Foundations of mathematics · Gödel's completeness theorem · Gödel's incompleteness theorems · Soundness · Completeness · Decidability · Interpretation · Löwenheim–Skolem theorem · Metatheorem · Satisfiability · Independence · Type-token distinction · Use–mention distinction ·

Mathematical logic

General	Formal language · Formation rule · Formal system · Deductive system · Formal proof · Formal semantics · Well-formed formula · Set · Element · Class · Classical logic · Axiom · Natural deduction · Rule of inference · Relation · Theorem · Logical consequence · Axiomatic system · Type theory · Symbol · Syntax · Theory

Traditional logic	Proposition · Inference · Argument · Validity · Cogency · Syllogism · Square of opposition · Venn diagram

Propositional logic and Boolean logic	Boolean functions · Propositional calculus · Propositional formula · Logical connectives · Quantifiers · Truth tables

Predicate	First-order · Quantifiers · Predicate · Second-order · Monadic predicate calculus

Set theory	Set · Empty set · Enumeration · Extensionality · Finite set · Function · Subset · Power set · Countable set · Recursive set · Domain · Range · Ordered pair · Uncountable set

Model theory	Model · Interpretation · Non-standard model · Truth value · Validity

Proof theory	Formal proof · Deductive system · Formal system · Formal theorem · Logical consequence · Rule of inference · Syntax

Computability theory	Recursion · Recursive set · Recursively enumerable set · Decision problem · Church–Turing thesis · Computable function · Primitive recursive function ·

Non-classical logic

Logicians

Anderson · Aristotle · Averroes · Avicenna · Barwise · Bernays · Boole · Boolos · Cantor · Carnap · Church · Chrysippus · Curry · De Morgan · Frege · Geach · Gentzen · Gödel · Hilbert · Kleene · Kripke · Leibniz · Löwenheim · Peano · Peirce · Putnam · Quine · Russell · Scotus · Skolem · Smullyan · Tarski · Turing · Whitehead · William of Ockham · Wittgenstein · Zermelo

Lists

Topics	Outline of logic · Index of logic articles · Mathematical logic · Boolean algebra · Set theory

Other	Logicians · Rules of inference · Paradoxes · Fallacies · Logic symbols

Portal · Category · Outline · WikiProject · Talk · changes