text:
Four Freedoms

The Four Freedoms were goals articulated by U.S. President Franklin D. Roosevelt on Monday, January 6, 1941. In an address known as the Four Freedoms speech (technically the 1941 State of the Union address), he proposed four fundamental freedoms that people "everywhere in the world" ought to enjoy:

 * 1) Freedom of speech and expression
 * 2) Freedom of worship
 * 3) Freedom from want
 * 4) Freedom from fear

Roosevelt delivered his speech 11 months before the surprise Japanese attack on Pearl Harbor, which caused the United States to declare war on Japan on December 8, 1941. The State of the Union speech before Congress was largely about the national security of the United States and the threat to other democracies from world war. In the speech, he made a break with the long-held tradition of United States non-interventionism. He outlined the U.S. role in helping allies already engaged in warfare, especially Great Britain and China.

In that context, he summarized the values of democracy behind the bipartisan consensus on international involvement that existed at the time. A famous quote from the speech prefaces those values: "As men do not live by bread alone, they do not fight by armaments alone." In the second half of the speech, he lists the benefits of democracy, which include economic opportunity, employment, social security, and the promise of "adequate health care". The first two freedoms, of speech and religion, are protected by the First Amendment in the United States Constitution. His inclusion of the latter two freedoms went beyond the traditional Constitutional values protected by the U.S. Bill of Rights. Roosevelt endorsed a broader human right to economic security and anticipated what would become known decades later as the "human security" paradigm in studies of economic development. He also included the "freedom from fear" against national aggression and took it to the new United Nations he was setting up.

Historical context
In the 1930s many Americans, arguing that the involvement in World War I had been a mistake, were adamantly against continued intervention in European affairs. With the Neutrality Acts established after 1935, U.S. law banned the sale of armaments to countries that were at war and placed restrictions on travel with belligerent vessels.

When World War II began in September 1939, the neutrality laws were still in effect and ensured that no substantial support could be given to Britain and France. With the revision of the Neutrality Act in 1939, Roosevelt adopted a "methods-short-of-war policy" whereby supplies and armaments could be given to European Allies, provided no declaration of war could be made and no troops committed. By December 1940, Europe was largely at the mercy of Adolf Hitler and Germany's Nazi regime. With Germany's defeat of France in June 1940, Britain and its overseas Empire stood alone against the military alliance of Germany, Italy, and Japan. Winston Churchill, as Prime Minister of Britain, called for Roosevelt and the United States to supply them with armaments in order to continue with the war effort.

The 1939 New York World's Fair had celebrated Four Freedoms – religion, speech, press, and assembly – and commissioned Leo Friedlander to create sculptures representing them. Mayor of New York City Fiorello La Guardia described the resulting statues as the "heart of the fair". Later Roosevelt would declare his own "Four Essential Freedoms" and call on Walter Russell to create a Four Freedoms Monument that was eventually dedicated at Madison Square Garden in New York City.

They also appeared on the reverse of the AM-lira, the Allied Military Currency note issue that was issued in Italy during WWII, by the Americans, that was in effect occupation currency, guaranteed by the American dollar.

Declarations
The Four Freedoms Speech was given on January 6, 1941. Roosevelt's hope was to provide a rationale for why the United States should abandon the isolationist policies that emerged from World War I. In the address, Roosevelt critiqued Isolationism, saying: "No realistic American can expect from a dictator's peace international generosity, or return of true independence, or world disarmament, or freedom of expression, or freedom of religion–or even good business. Such a peace would bring no security for us or for our neighbors. 'Those, who would give up essential liberty to purchase a little temporary safety, deserve neither liberty nor safety.'"

The speech coincided with the introduction of the Lend-Lease Act, which promoted Roosevelt's plan to become the "arsenal of democracy" and support the Allies (mainly the British) with much-needed supplies. Furthermore, the speech established what would become the ideological basis for America's involvement in World War II, all framed in terms of individual rights and liberties that are the hallmark of American politics.

The speech delivered by President Roosevelt incorporated the following text, known as the "Four Freedoms":

"In the future days, which we seek to make secure, we look forward to a world founded upon four essential human freedoms.

The first is freedom of speech, and expression—everywhere in the world.

The second is freedom of every person to worship God in his own way—everywhere in the world.

The third is freedom from want—which, translated into world terms, means economic understandings which will secure to every nation a healthy peacetime life for its inhabitants—everywhere in the world.

The fourth is freedom from fear—which, translated into world terms, means a world-wide reduction of armaments to such a point and in such a thorough fashion that no nation will be in a position to commit an act of physical aggression against any neighbor—anywhere in the world.

That is no vision of a distant millennium.

It is a definite basis for a kind of world attainable in our own time and generation.

That kind of world is the very antithesis of the so-called new order of tyranny which the dictators seek to create with the crash of a bomb." later in the same speech the president went on to specify six basic goals:
 * Equality of opportunity for youth and for others.
 * Jobs for those who can work.
 * Security for those who need it.
 * The ending of special privilege for the few.
 * The preservation of civil liberties for all.
 * The enjoyment of the fruits of scientific progress in a wider and constantly rising standard of living.

Justification for war
The declaration of the Four Freedoms as a justification for war would resonate through the remainder of the war, and for decades longer as a frame of remembrance. The Freedoms became the staple of America's war aims and the center of all attempts to rally public support for the war. With the creation of the Office of War Information (1942), as well as the famous paintings by Norman Rockwell, the Freedoms were advertised as values central to American life and examples of American exceptionalism.

Opposition
The Four Freedoms Speech was popular, and the goals were influential in postwar politics. However, in 1941 the speech received heavy criticism from anti-war elements. Critics argued that the Four Freedoms were simply a charter for Roosevelt's New Deal, social reforms that had already created sharp divisions within Congress. Conservatives who opposed social programs and increased government intervention argued against Roosevelt's attempt to justify and depict the war as necessary for the defense of lofty goals.

While the Freedoms did become a forceful aspect of American thought on the war, they were never the exclusive justification for the war. Polls and surveys conducted by the United States Office of War Information (OWI) revealed that self-defense and vengeance for the attack on Pearl Harbor were still the most prevalent reasons for war.

United Nations
The concept of the Four Freedoms became part of the personal mission undertaken by former First Lady Eleanor Roosevelt in 1948. She helped inspire the United Nations Declaration of Human Rights, General Assembly Resolution 217A. Indeed, these Four Freedoms were explicitly incorporated into the preamble to the Universal Declaration of Human Rights, which reads: "Whereas disregard and contempt for human rights have resulted in barbarous acts which have outraged the conscience of mankind, and the advent of a world in which human beings shall enjoy the freedom of speech and belief and freedom from fear and want has been proclaimed the highest aspiration of the common people."

Disarmament
FDR called for "a world-wide reduction of armaments" as a goal for "the future days, which we seek to make secure" but one that was "attainable in our own time and generation." More immediately, though, he called for a massive build-up of U.S. arms production:

"Every realist knows that the democratic way of life is at this moment being directly assailed in every part of the world ... The need of the moment is that our actions and our policy should be devoted primarily—almost exclusively—to meeting this foreign peril. ... [T]he immediate need is a swift and driving increase in our armament production. ... I also ask this Congress for authority and for funds sufficient to manufacture additional munitions and war supplies of many kinds, to be turned over to those nations which are now in actual war with aggressor nations."

Violation
In a 1942 radio address, President Roosevelt declared the Four Freedoms embodied "rights of men of every creed and every race, wherever they live." On February 19, 1942, he authorized Japanese American internment with Executive Order 9066. It allowed local military commanders to designate "military areas" as "exclusion zones", from which "any or all persons may be excluded". This power was used to declare that all people of Japanese ancestry were excluded from the entire Pacific coast, including all of California and much of Oregon, Washington, and Arizona, except for those in internment camps. By 1946, the United States had incarcerated 120,000 individuals of Japanese descent, of whom about 80,000 had been born in the United States.

Franklin D. Roosevelt Four Freedoms Park
The Franklin D. Roosevelt Four Freedoms Park is a park designed by the architect Louis Kahn for the south point of Roosevelt Island. The park celebrates the famous speech, and text from the speech is inscribed on a granite wall in the final design of the park.

Awards
The Roosevelt Institute honors outstanding individuals who have demonstrated a lifelong commitment to these ideals. The Four Freedoms Award medals are awarded at ceremonies at Hyde Park, New York and Middelburg, Netherlands during alternate years. The awards were first presented in 1982 on the centenary of President Roosevelt's birth as well as the bicentenary of diplomatic relations between the United States and the Netherlands.

Among the laureates have been:

 * William Brennan
 * H.M. Juan Carlos of Spain
 * Jimmy Carter
 * Bill Clinton
 * The Dalai Lama
 * Mikhail Gorbachev
 * Averell Harriman
 * Václav Havel
 * H.R.H. Princess Juliana of the Netherlands
 * John F. Kennedy
 * Mike Mansfield
 * Paul Newman
 * Tip O'Neill
 * Shimon Peres
 * Coretta Scott King
 * Brent Scowcroft
 * Harry S. Truman
 * Liv Ullmann
 * Elie Wiesel
 * Joanne Woodward

In popular culture

 * John Crowley's novel Four Freedoms (2009) is largely based on the themes of Roosevelt's speech.
 * FDR commissioned sculptor Walter Russell to design a monument to be dedicated to the first hero of the war. The Four Freedoms Monument was created in 1941 and dedicated at Madison Square Garden, in New York City, in 1943.
 * Artist Kindred McLeary painted America the Mighty (1941), also known as Defense of Human Freedoms, in the State Department's Harry S. Truman Building.
 * Artist Hugo Ballin painted The Four Freedoms mural (1942) in the Council Chamber of the City Hall of Burbank, California.
 * New Jersey muralist Michael Lenson (1903–1972) painted The Four Freedoms mural (1943) for the Fourteenth Street School in Newark, New Jersey.
 * Muralist Anton Refregier painted the History of San Francisco murals (completed 1948) in the Rincon Center in San Francisco, California; panel 27 depicts the four freedoms.
 * Artist Mildred Nungester Wolfe painted a four-panel Four Freedoms mural (complete 1959) depicting the four freedoms for a country store in Richton, Mississippi. Those panels now hang in the Mississippi Museum of Art.
 * Allyn Cox painted four Four Freedoms murals (completed 1982) that hang in the Great Experiment Hall in the United States House of Representatives; each of the four panels depicts allegorical figures representing the four freedoms.
 * Since 1986, the fictional Four Freedoms Plaza has served as the headquarters for Marvel Comics superhero team Fantastic Four.
 * In the early 1990s, artist David McDonald reproduced Rockwell's Four Freedoms paintings as four large murals on the side of an old grocery building in downtown Silverton, Oregon.
 * In 2008, Florida International University's Wolfsonian museum hosted the Thoughts on Democracy exhibition that displayed posters created by 60 leading contemporary artists and designers, invited to create a new graphic design inspired by American illustrator Norman Rockwell's Four Freedoms posters.
 * Four Freedoms is the adopted title of a bottom-shelf bourbon whiskey brand.

Norman Rockwell's paintings
Roosevelt's speech inspired a set of four paintings by Norman Rockwell.

Paintings
The members of the set, known collectively as The Four Freedoms, were published in four consecutive issues of The Saturday Evening Post. The four paintings subsequently were displayed around the US by the United States Department of the Treasury.

Essays
Each painting was published with a matching essay on that particular "Freedom":
 * Freedom of Speech, by Booth Tarkington (February 20, 1943).
 * Freedom of Worship, by Will Durant (February 27, 1943).
 * Freedom from Want, by Carlos Bulosan (March 6, 1943).
 * Freedom from Fear, by Stephen Vincent Benét (March 13, 1943; the date of Benét's death).

Postage stamps
Rockwell's Four Freedoms paintings were reproduced as postage stamps by the United States Post Office in 1943, in 1946, and in 1994, the centenary of Rockwell's birth.

Rockwell's icons

 * Kimble, James J. "The illustrated four freedoms: FDR, Rockwell, and the margins of the rhetorical presidency." Presidential Studies Quarterly 45.1 (2015): 46–69.
 * Lynch III, Sylvio. Morality and Aspiration: Some Conditions of Norman Rockwell's Four Freedoms (PhD Diss. Bowling Green State University, 2020) online
 * Murray, Stuart, James McCabe, and John Frohnmayer. Norman Rockwell's Four Freedoms: Images that Inspire a Nation (Berkshire House, 1993) online.
 * Olson, Lester G. "Portraits in praise of a people: A rhetorical analysis of Norman Rockwell's icons in Franklin D. Roosevelt's “four freedoms” campaign." Quarterly Journal of Speech 69.1 (1983): 15–24.

license: Creative Commons - Attribution Share-Alike - https://creativecommons.org/licenses/by-sa/4.0/

title: Four Freedoms


text:
First-order logic

First-order logic—also called predicate logic, predicate calculus, quantificational logic—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable. This distinguishes it from propositional logic, which does not use quantifiers or relations; in this sense, propositional logic is the foundation of first-order logic.

A theory about a topic, such as set theory, a theory for groups, or a formal theory of arithmetic, is usually a first-order logic together with a specified domain of discourse (over which the quantified variables range), finitely many functions from that domain to itself, finitely many predicates defined on that domain, and a set of axioms believed to hold about them. "Theory" is sometimes understood in a more formal sense as just a set of sentences in first-order logic.

The term "first-order" distinguishes first-order logic from higher-order logic, in which there are predicates having predicates or functions as arguments, or in which quantification over predicates, functions, or both, are permitted. In first-order theories, predicates are often associated with sets. In interpreted higher-order theories, predicates may be interpreted as sets of sets.

There are many deductive systems for first-order logic which are both sound, i.e. all provable statements are true in all models, and complete, i.e. all statements which are true in all models are provable. Although the logical consequence relation is only semidecidable, much progress has been made in automated theorem proving in first-order logic. First-order logic also satisfies several metalogical theorems that make it amenable to analysis in proof theory, such as the Löwenheim–Skolem theorem and the compactness theorem.

First-order logic is the standard for the formalization of mathematics into axioms, and is studied in the foundations of mathematics. Peano arithmetic and Zermelo–Fraenkel set theory are axiomatizations of number theory and set theory, respectively, into first-order logic. No first-order theory, however, has the strength to uniquely describe a structure with an infinite domain, such as the natural numbers or the real line. Axiom systems that do fully describe these two structures, i.e. categorical axiom systems, can be obtained in stronger logics such as second-order logic.

The foundations of first-order logic were developed independently by Gottlob Frege and Charles Sanders Peirce. For a history of first-order logic and how it came to dominate formal logic, see José Ferreirós (2001).

Introduction
While propositional logic deals with simple declarative propositions, first-order logic additionally covers predicates and quantification. A predicate evaluates to true or false for an entity or entities in the domain of discourse.

Consider the two sentences "Socrates is a philosopher" and "Plato is a philosopher". In propositional logic, these sentences themselves are viewed as the individuals of study, and might be denoted, for example, by variables such as p and q. They are not viewed as an application of a predicate, such as $$\text{isPhil}$$, to any particular objects in the domain of discourse, instead viewing them as purely an utterance which is either true or false. However, in first-order logic, these two sentences may be couched as statements that a certain individual or non-logical object has a property. In this example, both sentences happen to have the common form $$\text{isPhil}(x)$$ for some individual $$x$$, in the first sentence the value of the variable x is "Socrates", and in the second sentence it is "Plato". Due to the ability to speak about non-logical individuals along with the original logical connectives, first-order logic includes propositional logic.

The truth of a formula such as "x is a philosopher" depends on which object is denoted by x and on the interpretation of the predicate "is a philosopher". Consequently, "x is a philosopher" alone does not have a definite truth value of true or false, and is akin to a sentence fragment. Relationships between predicates can be stated using logical connectives. For example, the first-order formula "if x is a philosopher, then x is a scholar", is a conditional statement with "x is a philosopher" as its hypothesis, and "x is a scholar" as its conclusion, which again needs specification of x in order to have a definite truth value.

Quantifiers can be applied to variables in a formula. The variable x in the previous formula can be universally quantified, for instance, with the first-order sentence "For every x, if x is a philosopher, then x is a scholar". The universal quantifier "for every" in this sentence expresses the idea that the claim "if x is a philosopher, then x is a scholar" holds for all choices of x.

The negation of the sentence "For every x, if x is a philosopher, then x is a scholar" is logically equivalent to the sentence "There exists x such that x is a philosopher and x is not a scholar". The existential quantifier "there exists" expresses the idea that the claim "x is a philosopher and x is not a scholar" holds for some choice of x.

The predicates "is a philosopher" and "is a scholar" each take a single variable. In general, predicates can take several variables. In the first-order sentence "Socrates is the teacher of Plato", the predicate "is the teacher of" takes two variables.

An interpretation (or model) of a first-order formula specifies what each predicate means, and the entities that can instantiate the variables. These entities form the domain of discourse or universe, which is usually required to be a nonempty set. For example, in an interpretation with the domain of discourse consisting of all human beings and the predicate "is a philosopher" understood as "was the author of the Republic", the sentence "There exists x such that x is a philosopher" is seen as being true, as witnessed by Plato.

There are two key parts of first-order logic. The syntax determines which finite sequences of symbols are well-formed expressions in first-order logic, while the semantics determines the meanings behind these expressions.

Syntax
Unlike natural languages, such as English, the language of first-order logic is completely formal, so that it can be mechanically determined whether a given expression is well formed. There are two key types of well-formed expressions: terms, which intuitively represent objects, and formulas, which intuitively express statements that can be true or false. The terms and formulas of first-order logic are strings of symbols, where all the symbols together form the alphabet of the language.

Alphabet
As with all formal languages, the nature of the symbols themselves is outside the scope of formal logic; they are often regarded simply as letters and punctuation symbols.

It is common to divide the symbols of the alphabet into logical symbols, which always have the same meaning, and non-logical symbols, whose meaning varies by interpretation. For example, the logical symbol $$\land$$ always represents "and"; it is never interpreted as "or", which is represented by the logical symbol $$\lor$$. However, a non-logical predicate symbol such as Phil(x) could be interpreted to mean "x is a philosopher", "x is a man named Philip", or any other unary predicate depending on the interpretation at hand.

Logical symbols
Logical symbols are a set of characters that vary by author, but usually include the following:
 * Quantifier symbols: $∀$ for universal quantification, and $∃$ for existential quantification
 * Logical connectives: $∧$ for conjunction, $∨$ for disjunction, $→$ for implication, $↔$ for biconditional, $¬$ for negation. Some authors use Cpq instead of $→$ and Epq instead of $↔$, especially in contexts where → is used for other purposes. Moreover, the horseshoe $⊃$ may replace $→$; the triple-bar $≡$ may replace $↔$; a tilde ($~$), Np, or Fp may replace $¬$; a double bar $$\|$$, $$+$$, or Apq may replace $∨$; and an ampersand $&$, Kpq, or the middle dot $⋅$ may replace $∧$, especially if these symbols are not available for technical reasons. (The aforementioned symbols Cpq, Epq, Np, Apq, and Kpq are used in Polish notation.)
 * Parentheses, brackets, and other punctuation symbols. The choice of such symbols varies depending on context.
 * An infinite set of variables, often denoted by lowercase letters at the end of the alphabet x, y, z, ... . Subscripts are often used to distinguish variables: $x_{0}, x_{1}, x_{2}, ....$
 * An equality symbol (sometimes, identity symbol) $=$ (see below).

Not all of these symbols are required in first-order logic. Either one of the quantifiers along with negation, conjunction (or disjunction), variables, brackets, and equality suffices.

Other logical symbols include the following:
 * Truth constants: T, V, or $⊤$ for "true" and F, O, or $⊥$ for "false" (V and O are from Polish notation). Without any such logical operators of valence 0, these two constants can only be expressed using quantifiers.
 * Additional logical connectives such as the Sheffer stroke, Dpq (NAND), and exclusive or, Jpq.

Non-logical symbols
Non-logical symbols represent predicates (relations), functions and constants. It used to be standard practice to use a fixed, infinite set of non-logical symbols for all purposes:

 * For every integer n ≥ 0, there is a collection of n-ary, or n-place, predicate symbols. Because they represent relations between n elements, they are also called relation symbols. For each arity n, there is an infinite supply of them:
 * Pn0, Pn1, Pn2, Pn3, ...
 * For every integer n ≥ 0, there are infinitely many n-ary function symbols:
 * fn0, fn1, fn2, fn3, ...

When the arity of a predicate symbol or function symbol is clear from context, the superscript n is often omitted.

In this traditional approach, there is only one language of first-order logic. This approach is still common, especially in philosophically oriented books.

A more recent practice is to use different non-logical symbols according to the application one has in mind. Therefore, it has become necessary to name the set of all non-logical symbols used in a particular application. This choice is made via a signature.

Typical signatures in mathematics are {1, ×} or just {×} for groups, or {0, 1, +, ×, <} for ordered fields. There are no restrictions on the number of non-logical symbols. The signature can be empty, finite, or infinite, even uncountable. Uncountable signatures occur for example in modern proofs of the Löwenheim–Skolem theorem.

Though signatures might in some cases imply how non-logical symbols are to be interpreted, interpretation of the non-logical symbols in the signature is separate (and not necessarily fixed). Signatures concern syntax rather than semantics.

In this approach, every non-logical symbol is of one of the following types:

 * A predicate symbol (or relation symbol) with some valence (or arity, number of arguments) greater than or equal to 0. These are often denoted by uppercase letters such as P, Q and R. Examples:
 * In P(x), P is a predicate symbol of valence 1. One possible interpretation is "x is a man".
 * In Q(x,y), Q is a predicate symbol of valence 2. Possible interpretations include "x is greater than y" and "x is the father of y".
 * Relations of valence 0 can be identified with propositional variables, which can stand for any statement. One possible interpretation of R is "Socrates is a man".
 * A function symbol, with some valence greater than or equal to 0. These are often denoted by lowercase roman letters such as f, g and h. Examples:
 * f(x) may be interpreted as "the father of x". In arithmetic, it may stand for "-x". In set theory, it may stand for "the power set of x".
 * In arithmetic, g(x,y) may stand for "x+y". In set theory, it may stand for "the union of x and y".
 * Function symbols of valence 0 are called constant symbols, and are often denoted by lowercase letters at the beginning of the alphabet such as a, b and c. The symbol a may stand for Socrates. In arithmetic, it may stand for 0. In set theory, it may stand for the empty set.

The traditional approach can be recovered in the modern approach, by simply specifying the "custom" signature to consist of the traditional sequences of non-logical symbols.

Formation rules
The formation rules define the terms and formulas of first-order logic. When terms and formulas are represented as strings of symbols, these rules can be used to write a formal grammar for terms and formulas. These rules are generally context-free (each production has a single symbol on the left side), except that the set of symbols may be allowed to be infinite and there may be many start symbols, for example the variables in the case of terms.

Terms
The set of terms is inductively defined by the following rules: Only expressions which can be obtained by finitely many applications of rules 1 and 2 are terms. For example, no expression involving a predicate symbol is a term.
 * Variables. Any variable symbol is a term.
 * Functions. If f is an n-ary function symbol, and t1, ..., tn are terms, then f(t1,...,tn) is a term. In particular, symbols denoting individual constants are nullary function symbols, and thus are terms.

Formulas
The set of formulas (also called well-formed formulas or WFFs) is inductively defined by the following rules: Only expressions which can be obtained by finitely many applications of rules 1–5 are formulas. The formulas obtained from the first two rules are said to be atomic formulas.
 * 1) Predicate symbols. If P is an n-ary predicate symbol and t1, ..., tn are terms then P(t1,...,tn) is a formula.
 * 2) Equality. If the equality symbol is considered part of logic, and t1 and t2 are terms, then t1 = t2 is a formula.
 * 3) Negation. If $$\varphi$$ is a formula, then $$\lnot\varphi$$ is a formula.
 * 4) Binary connectives. If $\varphi$ and $\psi$ are formulas, then ($$\varphi\rightarrow\psi$$) is a formula. Similar rules apply to other binary logical connectives.
 * 5) Quantifiers. If $$\varphi$$  is a formula and x is a variable, then $$\forall x \varphi$$ (for all x, $$\varphi$$ holds) and $$\exists x \varphi$$ (there exists x such that $$\varphi$$) are formulas.

For example:
 * $$\forall x \forall y (P(f(x)) \rightarrow\neg (P(x) \rightarrow Q(f(y),x,z)))$$

is a formula, if f is a unary function symbol, P a unary predicate symbol, and Q a ternary predicate symbol. However, $$\forall x\, x \rightarrow$$ is not a formula, although it is a string of symbols from the alphabet.

The role of the parentheses in the definition is to ensure that any formula can only be obtained in one way—by following the inductive definition (i.e., there is a unique parse tree for each formula). This property is known as unique readability of formulas. There are many conventions for where parentheses are used in formulas. For example, some authors use colons or full stops instead of parentheses, or change the places in which parentheses are inserted. Each author's particular definition must be accompanied by a proof of unique readability.

Notational conventions
For convenience, conventions have been developed about the precedence of the logical operators, to avoid the need to write parentheses in some cases. These rules are similar to the order of operations in arithmetic. A common convention is: Moreover, extra punctuation not required by the definition may be inserted—to make formulas easier to read. Thus the formula:
 * $$\lnot$$ is evaluated first
 * $$\land$$ and $$\lor$$ are evaluated next
 * Quantifiers are evaluated next
 * $$\to$$ is evaluated last.
 * $$\lnot \forall x P(x) \to \exists x \lnot P(x)$$

might be written as:
 * $$(\lnot [\forall x P(x)]) \to \exists x [\lnot P(x)].$$

In some fields, it is common to use infix notation for binary relations and functions, instead of the prefix notation defined above. For example, in arithmetic, one typically writes "2 + 2 = 4" instead of "=(+(2,2),4)". It is common to regard formulas in infix notation as abbreviations for the corresponding formulas in prefix notation, cf. also term structure vs. representation.

The definitions above use infix notation for binary connectives such as $$\to$$. A less common convention is Polish notation, in which one writes $$\rightarrow$$, $$\wedge$$ and so on in front of their arguments rather than between them. This convention is advantageous in that it allows all punctuation symbols to be discarded. As such, Polish notation is compact and elegant, but rarely used in practice because it is hard for humans to read. In Polish notation, the formula:
 * $$\forall x \forall y (P(f(x)) \rightarrow\neg (P(x) \rightarrow Q(f(y),x,z)))$$

becomes "∀x∀y→Pfx¬→ PxQfyxz".

Free and bound variables
In a formula, a variable may occur free or bound (or both). One formalization of this notion is due to Quine, first the concept of a variable occurrence is defined, then whether a variable occurrence is free or bound, then whether a variable symbol overall is free or bound. In order to distinguish different occurrences of the identical symbol x, each occurrence of a variable symbol x in a formula φ is identified with the initial substring of φ up to the point at which said instance of the symbol x appears. p.297 Then, an occurrence of x is said to be bound if that occurrence of x lies within the scope of at least one of either $$\exists x$$ or $$\forall x$$. Finally, x is bound in φ if all occurrences of x in φ are bound. pp.142--143

Intuitively, a variable symbol is free in a formula if at no point is it quantified: pp.142--143 in $∀y P(x, y)$, the sole occurrence of variable x is free while that of y is bound. The free and bound variable occurrences in a formula are defined inductively as follows.
 * Atomic formulas : If φ is an atomic formula, then x occurs free in φ if and only if x occurs in φ. Moreover, there are no bound variables in any atomic formula.
 * Negation : x occurs free in ¬φ if and only if x occurs free in φ. x occurs bound in ¬φ if and only if x occurs bound in φ
 * Binary connectives : x occurs free in (φ → ψ) if and only if x occurs free in either φ or ψ. x occurs bound in (φ → ψ) if and only if x occurs bound in either φ or ψ. The same rule applies to any other binary connective in place of →.
 * Quantifiers : x occurs free in $∀y φ$, if and only if x occurs free in φ and x is a different symbol from y. Also, x occurs bound in $∀y φ$, if and only if x is y or x occurs bound in φ. The same rule holds with $∃$ in place of $∀$.

For example, in $∀x ∀y (P(x) → Q(x,f(x),z))$, x and y occur only bound, z occurs only free, and w is neither because it does not occur in the formula.

Free and bound variables of a formula need not be disjoint sets: in the formula $P(x) → ∀x Q(x)$, the first occurrence of x, as argument of P, is free while the second one, as argument of Q, is bound.

A formula in first-order logic with no free variable occurrences is called a first-order sentence. These are the formulas that will have well-defined truth values under an interpretation. For example, whether a formula such as Phil(x) is true must depend on what x represents. But the sentence $∃x Phil(x)$ will be either true or false in a given interpretation.

Example: ordered abelian groups
In mathematics, the language of ordered abelian groups has one constant symbol 0, one unary function symbol −, one binary function symbol +, and one binary relation symbol ≤. Then:
 * The expressions +(x, y) and +(x, +(y, −(z))) are terms. These are usually written as x + y and x + y − z.
 * The expressions +(x, y) = 0 and ≤(+(x, +(y, −(z))), +(x, y)) are atomic formulas. These are usually written as x + y = 0 and x + y − z ≤  x + y.
 * The expression $$(\forall x \forall y \, [\mathop{\leq}(\mathop{+}(x, y), z) \to \forall x\, \forall y\, \mathop{+}(x, y) = 0)]$$ is a formula, which is usually written as $$\forall x \forall y ( x + y \leq z) \to \forall x \forall y (x+y = 0).$$ This formula has one free variable, z.

The axioms for ordered abelian groups can be expressed as a set of sentences in the language. For example, the axiom stating that the group is commutative is usually written $$(\forall x)(\forall y)[x+ y = y + x].$$

Semantics
An interpretation of a first-order language assigns a denotation to each non-logical symbol (predicate symbol, function symbol, or constant symbol) in that language. It also determines a domain of discourse that specifies the range of the quantifiers. The result is that each term is assigned an object that it represents, each predicate is assigned a property of objects, and each sentence is assigned a truth value. In this way, an interpretation provides semantic meaning to the terms, predicates, and formulas of the language. The study of the interpretations of formal languages is called formal semantics. What follows is a description of the standard or Tarskian semantics for first-order logic. (It is also possible to define game semantics for first-order logic, but aside from requiring the axiom of choice, game semantics agree with Tarskian semantics for first-order logic, so game semantics will not be elaborated herein.)

First-order structures
The most common way of specifying an interpretation (especially in mathematics) is to specify a structure (also called a model; see below). The structure consists of a domain of discourse D and an interpretation function $I$ mapping non-logical symbols to predicates, functions, and constants.

The domain of discourse D is a nonempty set of "objects" of some kind. Intuitively, given an interpretation, a first-order formula becomes a statement about these objects; for example, $$\exists x P(x)$$ states the existence of some object in D for which the predicate P is true (or, more precisely, for which the predicate assigned to the predicate symbol P by the interpretation is true). For example, one can take D to be the set of integers.

Non-logical symbols are interpreted as follows:

 * The interpretation of an n-ary function symbol is a function from Dn to D. For example, if the domain of discourse is the set of integers, a function symbol f of arity 2 can be interpreted as the function that gives the sum of its arguments. In other words, the symbol f is associated with the function $I(f)$ which, in this interpretation, is addition.

 * The interpretation of a constant symbol (a function symbol of arity 0) is a function from D0 (a set whose only member is the empty tuple) to D, which can be simply identified with an object in D. For example, an interpretation may assign the value $$I(c)=10$$ to the constant symbol $$c$$.

 * The interpretation of an n-ary predicate symbol is a set of n-tuples of elements of D, giving the arguments for which the predicate is true. For example, an interpretation $$I(P)$$ of a binary predicate symbol P may be the set of pairs of integers such that the first one is less than the second. According to this interpretation, the predicate P would be true if its first argument is less than its second argument. Equivalently, predicate symbols may be assigned Boolean-valued functions from Dn to $$\{\mathrm{true, false}\}$$.

Evaluation of truth values
A formula evaluates to true or false given an interpretation and a variable assignment μ that associates an element of the domain of discourse with each variable. The reason that a variable assignment is required is to give meanings to formulas with free variables, such as $$y = x$$. The truth value of this formula changes depending on the values that x and y denote.

First, the variable assignment μ can be extended to all terms of the language, with the result that each term maps to a single element of the domain of discourse. The following rules are used to make this assignment:
 * Variables. Each variable x evaluates to μ(x)
 * Functions. Given terms $$t_1, \ldots, t_n$$ that have been evaluated to elements $$d_1, \ldots, d_n$$ of the domain of discourse, and a n-ary function symbol f, the term $$f(t_1, \ldots, t_n)$$ evaluates to $$(I(f))(d_1,\ldots,d_n)$$.

Next, each formula is assigned a truth value. The inductive definition used to make this assignment is called the T-schema. \psi$$, etc. is evaluated according to the truth table for the connective in question, as in propositional logic.
 * Atomic formulas (1). A formula $$P(t_1,\ldots,t_n)$$ is associated the value true or false depending on whether $$\langle v_1,\ldots,v_n \rangle \in I(P)$$, where $$v_1,\ldots,v_n$$ are the evaluation of the terms $$t_1,\ldots,t_n$$ and $$I(P)$$ is the interpretation of $$P$$, which by assumption is a subset of $$D^n$$.
 * Atomic formulas (2). A formula $$t_1 = t_2$$ is assigned true if $$t_1$$ and $$t_2$$ evaluate to the same object of the domain of discourse (see the section on equality below).
 * Logical connectives. A formula in the form $$\neg \varphi$$, $$\varphi \rightarrow
 * Existential quantifiers. A formula $$\exists x \varphi(x)$$ is true according to M and $$\mu$$ if there exists an evaluation $$\mu'$$ of the variables that differs from $$\mu$$ at most regarding the evaluation of x and such that φ is true according to the interpretation M and the variable assignment $$\mu'$$. This formal definition captures the idea that $$\exists x \varphi(x)$$ is true if and only if there is a way to choose a value for x such that φ(x) is satisfied.
 * Universal quantifiers. A formula $$\forall x \varphi(x)$$ is true according to M and $$\mu$$ if φ(x) is true for every pair composed by the interpretation M and some variable assignment $$\mu'$$ that differs from $$\mu$$ at most on the value of x. This captures the idea that $$\forall x \varphi(x)$$ is true if every possible choice of a value for x causes φ(x) to be true.

If a formula does not contain free variables, and so is a sentence, then the initial variable assignment does not affect its truth value. In other words, a sentence is true according to M and $$\mu$$ if and only if it is true according to M and every other variable assignment $$\mu'$$.

There is a second common approach to defining truth values that does not rely on variable assignment functions. Instead, given an interpretation M, one first adds to the signature a collection of constant symbols, one for each element of the domain of discourse in M; say that for each d in the domain the constant symbol cd is fixed. The interpretation is extended so that each new constant symbol is assigned to its corresponding element of the domain. One now defines truth for quantified formulas syntactically, as follows: This alternate approach gives exactly the same truth values to all sentences as the approach via variable assignments.
 * Existential quantifiers (alternate). A formula $$\exists x \varphi(x)$$ is true according to M if there is some d in the domain of discourse such that $$\varphi(c_d)$$ holds. Here $$\varphi(c_d)$$ is the result of substituting cd for every free occurrence of x in φ.
 * Universal quantifiers (alternate). A formula $$\forall x \varphi(x)$$ is true according to M if, for every d in the domain of discourse, $$\varphi(c_d)$$ is true according to M.

Validity, satisfiability, and logical consequence
If a sentence φ evaluates to true under a given interpretation M, one says that M satisfies φ; this is denoted $$M \vDash \varphi$$. A sentence is satisfiable if there is some interpretation under which it is true. This is a bit different from the symbol $$\vDash$$ from model theory, where $$M\vDash\phi$$ denotes satisfiability in a model, i.e. "there is a suitable assignment of values in $$M$$'s domain to variable symbols of $$\phi$$".

Satisfiability of formulas with free variables is more complicated, because an interpretation on its own does not determine the truth value of such a formula. The most common convention is that a formula φ with free variables $$x_1$$, ..., $$x_n$$ is said to be satisfied by an interpretation if the formula φ remains true regardless which individuals from the domain of discourse are assigned to its free variables $$x_1$$, ..., $$x_n$$. This has the same effect as saying that a formula φ is satisfied if and only if its universal closure $$\forall x_1 \dots \forall x_n \phi (x_1, \dots, x_n)$$ is satisfied.

A formula is logically valid (or simply valid) if it is true in every interpretation. These formulas play a role similar to tautologies in propositional logic.

A formula φ is a logical consequence of a formula ψ if every interpretation that makes ψ true also makes φ true. In this case one says that φ is logically implied by ψ.

Algebraizations
An alternate approach to the semantics of first-order logic proceeds via abstract algebra. This approach generalizes the Lindenbaum–Tarski algebras of propositional logic. There are three ways of eliminating quantified variables from first-order logic that do not involve replacing quantifiers with other variable binding term operators: These algebras are all lattices that properly extend the two-element Boolean algebra.
 * Cylindric algebra, by Alfred Tarski and colleagues;
 * Polyadic algebra, by Paul Halmos;
 * Predicate functor logic, mainly due to Willard Quine.

Tarski and Givant (1987) showed that the fragment of first-order logic that has no atomic sentence lying in the scope of more than three quantifiers has the same expressive power as relation algebra. This fragment is of great interest because it suffices for Peano arithmetic and most axiomatic set theory, including the canonical ZFC. They also prove that first-order logic with a primitive ordered pair is equivalent to a relation algebra with two ordered pair projection functions.

First-order theories, models, and elementary classes
A first-order theory of a particular signature is a set of axioms, which are sentences consisting of symbols from that signature. The set of axioms is often finite or recursively enumerable, in which case the theory is called effective. Some authors require theories to also include all logical consequences of the axioms. The axioms are considered to hold within the theory and from them other sentences that hold within the theory can be derived.

A first-order structure that satisfies all sentences in a given theory is said to be a model of the theory. An elementary class is the set of all structures satisfying a particular theory. These classes are a main subject of study in model theory.

Many theories have an intended interpretation, a certain model that is kept in mind when studying the theory. For example, the intended interpretation of Peano arithmetic consists of the usual natural numbers with their usual operations. However, the Löwenheim–Skolem theorem shows that most first-order theories will also have other, nonstandard models.

A theory is consistent if it is not possible to prove a contradiction from the axioms of the theory. A theory is complete if, for every formula in its signature, either that formula or its negation is a logical consequence of the axioms of the theory. Gödel's incompleteness theorem shows that effective first-order theories that include a sufficient portion of the theory of the natural numbers can never be both consistent and complete.

Empty domains
The definition above requires that the domain of discourse of any interpretation must be nonempty. There are settings, such as inclusive logic, where empty domains are permitted. Moreover, if a class of algebraic structures includes an empty structure (for example, there is an empty poset), that class can only be an elementary class in first-order logic if empty domains are permitted or the empty structure is removed from the class.

There are several difficulties with empty domains, however: Thus, when the empty domain is permitted, it must often be treated as a special case. Most authors, however, simply exclude the empty domain by definition.
 * Many common rules of inference are valid only when the domain of discourse is required to be nonempty. One example is the rule stating that $$\varphi \lor \exists x \psi$$ implies $$\exists x (\varphi \lor \psi)$$ when x is not a free variable in $$\varphi$$. This rule, which is used to put formulas into prenex normal form, is sound in nonempty domains, but unsound if the empty domain is permitted.
 * The definition of truth in an interpretation that uses a variable assignment function cannot work with empty domains, because there are no variable assignment functions whose range is empty. (Similarly, one cannot assign interpretations to constant symbols.) This truth definition requires that one must select a variable assignment function (μ above) before truth values for even atomic formulas can be defined. Then the truth value of a sentence is defined to be its truth value under any variable assignment, and it is proved that this truth value does not depend on which assignment is chosen. This technique does not work if there are no assignment functions at all; it must be changed to accommodate empty domains.

Deductive systems
A deductive system is used to demonstrate, on a purely syntactic basis, that one formula is a logical consequence of another formula. There are many such systems for first-order logic, including Hilbert-style deductive systems, natural deduction, the sequent calculus, the tableaux method, and resolution. These share the common property that a deduction is a finite syntactic object; the format of this object, and the way it is constructed, vary widely. These finite deductions themselves are often called derivations in proof theory. They are also often called proofs but are completely formalized unlike natural-language mathematical proofs.

A deductive system is sound if any formula that can be derived in the system is logically valid. Conversely, a deductive system is complete if every logically valid formula is derivable. All of the systems discussed in this article are both sound and complete. They also share the property that it is possible to effectively verify that a purportedly valid deduction is actually a deduction; such deduction systems are called effective.

A key property of deductive systems is that they are purely syntactic, so that derivations can be verified without considering any interpretation. Thus, a sound argument is correct in every possible interpretation of the language, regardless of whether that interpretation is about mathematics, economics, or some other area.

In general, logical consequence in first-order logic is only semidecidable: if a sentence A logically implies a sentence B then this can be discovered (for example, by searching for a proof until one is found, using some effective, sound, complete proof system). However, if A does not logically imply B, this does not mean that A logically implies the negation of B. There is no effective procedure that, given formulas A and B, always correctly decides whether A logically implies B.

Rules of inference
A rule of inference states that, given a particular formula (or set of formulas) with a certain property as a hypothesis, another specific formula (or set of formulas) can be derived as a conclusion. The rule is sound (or truth-preserving) if it preserves validity in the sense that whenever any interpretation satisfies the hypothesis, that interpretation also satisfies the conclusion.

For example, one common rule of inference is the rule of substitution. If t is a term and φ is a formula possibly containing the variable x, then φ[t/x] is the result of replacing all free instances of x by t in φ. The substitution rule states that for any φ and any term t, one can conclude φ[t/x] from φ provided that no free variable of t becomes bound during the substitution process. (If some free variable of t becomes bound, then to substitute t for x it is first necessary to change the bound variables of φ to differ from the free variables of t.)

To see why the restriction on bound variables is necessary, consider the logically valid formula φ given by $$\exists x (x = y)$$, in the signature of (0,1,+,×,=) of arithmetic. If t is the term "x + 1", the formula φ[t/y] is $$\exists x ( x = x+1)$$, which will be false in many interpretations. The problem is that the free variable x of t became bound during the substitution. The intended replacement can be obtained by renaming the bound variable x of φ to something else, say z, so that the formula after substitution is $$\exists z ( z = x+1)$$, which is again logically valid.

The substitution rule demonstrates several common aspects of rules of inference. It is entirely syntactical; one can tell whether it was correctly applied without appeal to any interpretation. It has (syntactically defined) limitations on when it can be applied, which must be respected to preserve the correctness of derivations. Moreover, as is often the case, these limitations are necessary because of interactions between free and bound variables that occur during syntactic manipulations of the formulas involved in the inference rule.

Hilbert-style systems and natural deduction
A deduction in a Hilbert-style deductive system is a list of formulas, each of which is a logical axiom, a hypothesis that has been assumed for the derivation at hand or follows from previous formulas via a rule of inference. The logical axioms consist of several axiom schemas of logically valid formulas; these encompass a significant amount of propositional logic. The rules of inference enable the manipulation of quantifiers. Typical Hilbert-style systems have a small number of rules of inference, along with several infinite schemas of logical axioms. It is common to have only modus ponens and universal generalization as rules of inference.

Natural deduction systems resemble Hilbert-style systems in that a deduction is a finite list of formulas. However, natural deduction systems have no logical axioms; they compensate by adding additional rules of inference that can be used to manipulate the logical connectives in formulas in the proof.

Sequent calculus
The sequent calculus was developed to study the properties of natural deduction systems. Instead of working with one formula at a time, it uses sequents, which are expressions of the form:
 * $$A_1, \ldots, A_n \vdash B_1, \ldots, B_k,$$

where A1, ..., An, B1, ..., Bk are formulas and the turnstile symbol $$\vdash$$ is used as punctuation to separate the two halves. Intuitively, a sequent expresses the idea that $$(A_1 \land \cdots\land A_n)$$ implies $$(B_1\lor\cdots\lor B_k)$$.

Tableaux method

Unlike the methods just described the derivations in the tableaux method are not lists of formulas. Instead, a derivation is a tree of formulas. To show that a formula A is provable, the tableaux method attempts to demonstrate that the negation of A is unsatisfiable. The tree of the derivation has $$\lnot A$$ at its root; the tree branches in a way that reflects the structure of the formula. For example, to show that $$C \lor D$$ is unsatisfiable requires showing that C and D are each unsatisfiable; this corresponds to a branching point in the tree with parent $$C \lor D$$ and children C and D.

Resolution
The resolution rule is a single rule of inference that, together with unification, is sound and complete for first-order logic. As with the tableaux method, a formula is proved by showing that the negation of the formula is unsatisfiable. Resolution is commonly used in automated theorem proving.

The resolution method works only with formulas that are disjunctions of atomic formulas; arbitrary formulas must first be converted to this form through Skolemization. The resolution rule states that from the hypotheses $$A_1 \lor\cdots\lor A_k \lor C$$ and $$B_1\lor\cdots\lor B_l\lor\lnot C$$, the conclusion $$A_1\lor\cdots\lor A_k\lor B_1\lor\cdots\lor B_l$$ can be obtained.

Provable identities
Many identities can be proved, which establish equivalences between particular formulas. These identities allow for rearranging formulas by moving quantifiers across other connectives and are useful for putting formulas in prenex normal form. Some provable identities include:
 * $$\lnot \forall x \, P(x) \Leftrightarrow \exists x \, \lnot P(x)$$
 * $$\lnot \exists x \, P(x) \Leftrightarrow \forall x \, \lnot P(x)$$
 * $$\forall x \, \forall y \, P(x,y) \Leftrightarrow \forall y \, \forall x \, P(x,y)$$
 * $$\exists x \, \exists y \, P(x,y) \Leftrightarrow \exists y \, \exists x \, P(x,y)$$
 * $$\forall x \, P(x) \land \forall x \, Q(x) \Leftrightarrow \forall x \, (P(x) \land Q(x)) $$
 * $$\exists x \, P(x) \lor \exists x \, Q(x) \Leftrightarrow \exists x \, (P(x) \lor Q(x)) $$
 * $$P \land \exists x \, Q(x) \Leftrightarrow \exists x \, (P \land Q(x)) $$ (where $$x$$ must not occur free in $$P$$)
 * $$P \lor \forall x \, Q(x) \Leftrightarrow \forall x \, (P \lor Q(x)) $$ (where $$x$$ must not occur free in $$P$$)

Equality and its axioms
There are several different conventions for using equality (or identity) in first-order logic. The most common convention, known as first-order logic with equality, includes the equality symbol as a primitive logical symbol which is always interpreted as the real equality relation between members of the domain of discourse, such that the "two" given members are the same member. This approach also adds certain axioms about equality to the deductive system employed. These equality axioms are:
 * Reflexivity. For each variable x, x = x.
 * Substitution for functions. For all variables x and y, and any function symbol f,
 * x = y → f(..., x, ...) = f(..., y, ...).
 * Substitution for formulas. For any variables x and y and any formula φ(x), if φ' is obtained by replacing any number of free occurrences of x in φ with y, such that these remain free occurrences of y, then:
 * x = y → (φ → φ').

These are axiom schemas, each of which specifies an infinite set of axioms. The third schema is known as Leibniz's law, "the principle of substitutivity", "the indiscernibility of identicals", or "the replacement property". The second schema, involving the function symbol f, is (equivalent to) a special case of the third schema, using the formula:
 * x = y → (f(..., x, ...) = z → f(..., y, ...) = z).

Many other properties of equality are consequences of the axioms above, for example:
 * Symmetry. If x = y then y = x.
 * Transitivity. If x = y and y = z then x = z.

First-order logic without equality
An alternate approach considers the equality relation to be a non-logical symbol. This convention is known as first-order logic without equality. If an equality relation is included in the signature, the axioms of equality must now be added to the theories under consideration, if desired, instead of being considered rules of logic. The main difference between this method and first-order logic with equality is that an interpretation may now interpret two distinct individuals as "equal" (although, by Leibniz's law, these will satisfy exactly the same formulas under any interpretation). That is, the equality relation may now be interpreted by an arbitrary equivalence relation on the domain of discourse that is congruent with respect to the functions and relations of the interpretation.

When this second convention is followed, the term normal model is used to refer to an interpretation where no distinct individuals a and b satisfy a = b. In first-order logic with equality, only normal models are considered, and so there is no term for a model other than a normal model. When first-order logic without equality is studied, it is necessary to amend the statements of results such as the Löwenheim–Skolem theorem so that only normal models are considered.

First-order logic without equality is often employed in the context of second-order arithmetic and other higher-order theories of arithmetic, where the equality relation between sets of natural numbers is usually omitted.

Defining equality within a theory
If a theory has a binary formula A(x,y) which satisfies reflexivity and Leibniz's law, the theory is said to have equality, or to be a theory with equality. The theory may not have all instances of the above schemas as axioms, but rather as derivable theorems. For example, in theories with no function symbols and a finite number of relations, it is possible to define equality in terms of the relations, by defining the two terms s and t to be equal if any relation is unchanged by changing s to t in any argument.

Some theories allow other ad hoc definitions of equality:
 * In the theory of partial orders with one relation symbol ≤, one could define s = t to be an abbreviation for s ≤ t ∧ t ≤ s.
 * In set theory with one relation ∈, one may define s = t to be an abbreviation for $∀x (s ∈ x ↔ t ∈ x) ∧ ∀x (x ∈ s ↔ x ∈ t)$. This definition of equality then automatically satisfies the axioms for equality. In this case, one should replace the usual axiom of extensionality, which can be stated as $$\forall x \forall y [ \forall z (z \in x \Leftrightarrow z \in y) \Rightarrow x = y]$$, with an alternative formulation $$\forall x \forall y [ \forall z (z \in x \Leftrightarrow z \in y) \Rightarrow \forall z (x \in z \Leftrightarrow y \in z) ]$$, which says that if sets x and y have the same elements, then they also belong to the same sets.

Metalogical properties
One motivation for the use of first-order logic, rather than higher-order logic, is that first-order logic has many metalogical properties that stronger logics do not have. These results concern general properties of first-order logic itself, rather than properties of individual theories. They provide fundamental tools for the construction of models of first-order theories.

Completeness and undecidability
Gödel's completeness theorem, proved by Kurt Gödel in 1929, establishes that there are sound, complete, effective deductive systems for first-order logic, and thus the first-order logical consequence relation is captured by finite provability. Naively, the statement that a formula φ logically implies a formula ψ depends on every model of φ; these models will in general be of arbitrarily large cardinality, and so logical consequence cannot be effectively verified by checking every model. However, it is possible to enumerate all finite derivations and search for a derivation of ψ from φ. If ψ is logically implied by φ, such a derivation will eventually be found. Thus first-order logical consequence is semidecidable: it is possible to make an effective enumeration of all pairs of sentences (φ,ψ) such that ψ is a logical consequence of φ.

Unlike propositional logic, first-order logic is undecidable (although semidecidable), provided that the language has at least one predicate of arity at least 2 (other than equality). This means that there is no decision procedure that determines whether arbitrary formulas are logically valid. This result was established independently by Alonzo Church and Alan Turing in 1936 and 1937, respectively, giving a negative answer to the Entscheidungsproblem posed by David Hilbert and Wilhelm Ackermann in 1928. Their proofs demonstrate a connection between the unsolvability of the decision problem for first-order logic and the unsolvability of the halting problem.

There are systems weaker than full first-order logic for which the logical consequence relation is decidable. These include propositional logic and monadic predicate logic, which is first-order logic restricted to unary predicate symbols and no function symbols. Other logics with no function symbols which are decidable are the guarded fragment of first-order logic, as well as two-variable logic. The Bernays–Schönfinkel class of first-order formulas is also decidable. Decidable subsets of first-order logic are also studied in the framework of description logics.

The Löwenheim–Skolem theorem
The Löwenheim–Skolem theorem shows that if a first-order theory of cardinality λ has an infinite model, then it has models of every infinite cardinality greater than or equal to λ. One of the earliest results in model theory, it implies that it is not possible to characterize countability or uncountability in a first-order language with a countable signature. That is, there is no first-order formula φ(x) such that an arbitrary structure M satisfies φ if and only if the domain of discourse of M is countable (or, in the second case, uncountable).

The Löwenheim–Skolem theorem implies that infinite structures cannot be categorically axiomatized in first-order logic. For example, there is no first-order theory whose only model is the real line: any first-order theory with an infinite model also has a model of cardinality larger than the continuum. Since the real line is infinite, any theory satisfied by the real line is also satisfied by some nonstandard models. When the Löwenheim–Skolem theorem is applied to first-order set theories, the nonintuitive consequences are known as Skolem's paradox.

The compactness theorem
The compactness theorem states that a set of first-order sentences has a model if and only if every finite subset of it has a model. This implies that if a formula is a logical consequence of an infinite set of first-order axioms, then it is a logical consequence of some finite number of those axioms. This theorem was proved first by Kurt Gödel as a consequence of the completeness theorem, but many additional proofs have been obtained over time. It is a central tool in model theory, providing a fundamental method for constructing models.

The compactness theorem has a limiting effect on which collections of first-order structures are elementary classes. For example, the compactness theorem implies that any theory that has arbitrarily large finite models has an infinite model. Thus, the class of all finite graphs is not an elementary class (the same holds for many other algebraic structures).

There are also more subtle limitations of first-order logic that are implied by the compactness theorem. For example, in computer science, many situations can be modeled as a directed graph of states (nodes) and connections (directed edges). Validating such a system may require showing that no "bad" state can be reached from any "good" state. Thus, one seeks to determine if the good and bad states are in different connected components of the graph. However, the compactness theorem can be used to show that connected graphs are not an elementary class in first-order logic, and there is no formula φ(x,y) of first-order logic, in the logic of graphs, that expresses the idea that there is a path from x to y. Connectedness can be expressed in second-order logic, however, but not with only existential set quantifiers, as $$\Sigma_1^1$$ also enjoys compactness.

Lindström's theorem
Per Lindström showed that the metalogical properties just discussed actually characterize first-order logic in the sense that no stronger logic can also have those properties (Ebbinghaus and Flum 1994, Chapter XIII). Lindström defined a class of abstract logical systems, and a rigorous definition of the relative strength of a member of this class. He established two theorems for systems of this type:
 * A logical system satisfying Lindström's definition that contains first-order logic and satisfies both the Löwenheim–Skolem theorem and the compactness theorem must be equivalent to first-order logic.
 * A logical system satisfying Lindström's definition that has a semidecidable logical consequence relation and satisfies the Löwenheim–Skolem theorem must be equivalent to first-order logic.

Limitations
Although first-order logic is sufficient for formalizing much of mathematics and is commonly used in computer science and other fields, it has certain limitations. These include limitations on its expressiveness and limitations of the fragments of natural languages that it can describe.

For instance, first-order logic is undecidable, meaning a sound, complete and terminating decision algorithm for provability is impossible. This has led to the study of interesting decidable fragments, such as C2: first-order logic with two variables and the counting quantifiers $$\exists^{\ge n}$$ and $$\exists^{\le n}$$.

Expressiveness
The Löwenheim–Skolem theorem shows that if a first-order theory has any infinite model, then it has infinite models of every cardinality. In particular, no first-order theory with an infinite model can be categorical. Thus, there is no first-order theory whose only model has the set of natural numbers as its domain, or whose only model has the set of real numbers as its domain. Many extensions of first-order logic, including infinitary logics and higher-order logics, are more expressive in the sense that they do permit categorical axiomatizations of the natural numbers or real numbers. This expressiveness comes at a metalogical cost, however: by Lindström's theorem, the compactness theorem and the downward Löwenheim–Skolem theorem cannot hold in any logic stronger than first-order.

Formalizing natural languages
First-order logic is able to formalize many simple quantifier constructions in natural language, such as "every person who lives in Perth lives in Australia". Hence, first-order logic is used as a basis for knowledge representation languages, such as FO(.).

Still, there are complicated features of natural language that cannot be expressed in first-order logic. "Any logical system which is appropriate as an instrument for the analysis of natural language needs a much richer structure than first-order predicate logic".

Restrictions, extensions, and variations
There are many variations of first-order logic. Some of these are inessential in the sense that they merely change notation without affecting the semantics. Others change the expressive power more significantly, by extending the semantics through additional quantifiers or other new logical symbols. For example, infinitary logics permit formulas of infinite size, and modal logics add symbols for possibility and necessity.

Restricted languages
First-order logic can be studied in languages with fewer logical symbols than were described above:
 * Because $$\exists x \varphi(x)$$ can be expressed as $$\neg \forall x \neg \varphi(x)$$, and $$\forall x \varphi(x)$$ can be expressed as $$\neg \exists x \neg \varphi(x)$$, either of the two quantifiers $$\exists$$ and $$\forall$$ can be dropped.
 * Since $$\varphi \lor \psi$$ can be expressed as $$\lnot (\lnot \varphi \land \lnot \psi)$$ and $$\varphi \land \psi$$ can be expressed as $$\lnot(\lnot \varphi \lor \lnot \psi)$$, either $$\vee$$ or $$\wedge$$ can be dropped. In other words, it is sufficient to have $$\neg$$ and $$\vee$$, or $$\neg$$ and $$\wedge$$, as the only logical connectives.
 * Similarly, it is sufficient to have only $$\neg$$ and $$\rightarrow$$ as logical connectives, or to have only the Sheffer stroke (NAND) or the Peirce arrow (NOR) operator.
 * It is possible to entirely avoid function symbols and constant symbols, rewriting them via predicate symbols in an appropriate way. For example, instead of using a constant symbol $$ \; 0 $$ one may use a predicate  $$ \; 0(x) $$  (interpreted as $$ \; x=0 $$ ) and replace every predicate such as $$\; P(0,y) $$ with $$ \forall x \;(0(x) \rightarrow P(x,y)) $$. A function such as $$ f(x_1,x_2,...,x_n) $$ will similarly be replaced by a predicate  $$ F(x_1,x_2,...,x_n,y) $$ interpreted as $$ y = f(x_1,x_2,...,x_n) $$. This change requires adding additional axioms to the theory at hand, so that interpretations of the predicate symbols used have the correct semantics.

Restrictions such as these are useful as a technique to reduce the number of inference rules or axiom schemas in deductive systems, which leads to shorter proofs of metalogical results. The cost of the restrictions is that it becomes more difficult to express natural-language statements in the formal system at hand, because the logical connectives used in the natural language statements must be replaced by their (longer) definitions in terms of the restricted collection of logical connectives. Similarly, derivations in the limited systems may be longer than derivations in systems that include additional connectives. There is thus a trade-off between the ease of working within the formal system and the ease of proving results about the formal system.

It is also possible to restrict the arities of function symbols and predicate symbols, in sufficiently expressive theories. One can in principle dispense entirely with functions of arity greater than 2 and predicates of arity greater than 1 in theories that include a pairing function. This is a function of arity 2 that takes pairs of elements of the domain and returns an ordered pair containing them. It is also sufficient to have two predicate symbols of arity 2 that define projection functions from an ordered pair to its components. In either case it is necessary that the natural axioms for a pairing function and its projections are satisfied.

Many-sorted logic
Ordinary first-order interpretations have a single domain of discourse over which all quantifiers range. Many-sorted first-order logic allows variables to have different sorts, which have different domains. This is also called typed first-order logic, and the sorts called types (as in data type), but it is not the same as first-order type theory. Many-sorted first-order logic is often used in the study of second-order arithmetic.

When there are only finitely many sorts in a theory, many-sorted first-order logic can be reduced to single-sorted first-order logic. One introduces into the single-sorted theory a unary predicate symbol for each sort in the many-sorted theory and adds an axiom saying that these unary predicates partition the domain of discourse. For example, if there are two sorts, one adds predicate symbols $$P_1(x)$$ and $$P_2(x)$$ and the axiom:
 * $$\forall x ( P_1(x) \lor P_2(x)) \land \lnot \exists x (P_1(x) \land P_2(x))$$.

Then the elements satisfying $$P_1$$ are thought of as elements of the first sort, and elements satisfying $$P_2$$ as elements of the second sort. One can quantify over each sort by using the corresponding predicate symbol to limit the range of quantification. For example, to say there is an element of the first sort satisfying formula φ(x), one writes:
 * $$\exists x (P_1(x) \land \varphi(x))$$.

Additional quantifiers
Additional quantifiers can be added to first-order logic.
 * Sometimes it is useful to say that "$P(x)$ holds for exactly one x", which can be expressed as $∃!x P(x)$. This notation, called uniqueness quantification, may be taken to abbreviate a formula such as $∃x (P(x) ∧∀y (P(y) → (x = y)))$.
 * First-order logic with extra quantifiers has new quantifiers Qx,..., with meanings such as "there are many x such that ...". Also see branching quantifiers and the plural quantifiers of George Boolos and others.
 * Bounded quantifiers are often used in the study of set theory or arithmetic.

Infinitary logics
Infinitary logic allows infinitely long sentences. For example, one may allow a conjunction or disjunction of infinitely many formulas, or quantification over infinitely many variables. Infinitely long sentences arise in areas of mathematics including topology and model theory.

Infinitary logic generalizes first-order logic to allow formulas of infinite length. The most common way in which formulas can become infinite is through infinite conjunctions and disjunctions. However, it is also possible to admit generalized signatures in which function and relation symbols are allowed to have infinite arities, or in which quantifiers can bind infinitely many variables. Because an infinite formula cannot be represented by a finite string, it is necessary to choose some other representation of formulas; the usual representation in this context is a tree. Thus, formulas are, essentially, identified with their parse trees, rather than with the strings being parsed.

The most commonly studied infinitary logics are denoted Lαβ, where α and β are each either cardinal numbers or the symbol ∞. In this notation, ordinary first-order logic is Lωω. In the logic L∞ω, arbitrary conjunctions or disjunctions are allowed when building formulas, and there is an unlimited supply of variables. More generally, the logic that permits conjunctions or disjunctions with less than κ constituents is known as Lκω. For example, Lω 1ω permits countable conjunctions and disjunctions.

The set of free variables in a formula of Lκω can have any cardinality strictly less than κ, yet only finitely many of them can be in the scope of any quantifier when a formula appears as a subformula of another. In other infinitary logics, a subformula may be in the scope of infinitely many quantifiers. For example, in Lκ∞, a single universal or existential quantifier may bind arbitrarily many variables simultaneously. Similarly, the logic Lκλ permits simultaneous quantification over fewer than λ variables, as well as conjunctions and disjunctions of size less than κ.

Non-classical and modal logics

 * Intuitionistic first-order logic uses intuitionistic rather than classical reasoning; for example, ¬¬φ need not be equivalent to φ and ¬ ∀x.φ is in general not equivalent to ∃ x.¬φ.
 * First-order modal logic allows one to describe other possible worlds as well as this contingently true world which we inhabit. In some versions, the set of possible worlds varies depending on which possible world one inhabits. Modal logic has extra modal operators with meanings which can be characterized informally as, for example "it is necessary that φ" (true in all possible worlds) and "it is possible that φ" (true in some possible world). With standard first-order logic we have a single domain, and each predicate is assigned one extension. With first-order modal logic we have a domain function that assigns each possible world its own domain, so that each predicate gets an extension only relative to these possible worlds. This allows us to model cases where, for example, Alex is a philosopher, but might have been a mathematician, and might not have existed at all. In the first possible world P(a) is true, in the second P(a) is false, and in the third possible world there is no a in the domain at all.
 * First-order fuzzy logics are first-order extensions of propositional fuzzy logics rather than classical propositional calculus.

Fixpoint logic
Fixpoint logic extends first-order logic by adding the closure under the least fixed points of positive operators.

Higher-order logics
The characteristic feature of first-order logic is that individuals can be quantified, but not predicates. Thus
 * $$\exists a ( \text{Phil}(a))$$

is a legal first-order formula, but
 * $$\exists \text{Phil} ( \text{Phil}(a))$$

is not, in most formalizations of first-order logic. Second-order logic extends first-order logic by adding the latter type of quantification. Other higher-order logics allow quantification over even higher types than second-order logic permits. These higher types include relations between relations, functions from relations to relations between relations, and other higher-type objects. Thus the "first" in first-order logic describes the type of objects that can be quantified.

Unlike first-order logic, for which only one semantics is studied, there are several possible semantics for second-order logic. The most commonly employed semantics for second-order and higher-order logic is known as full semantics. The combination of additional quantifiers and the full semantics for these quantifiers makes higher-order logic stronger than first-order logic. In particular, the (semantic) logical consequence relation for second-order and higher-order logic is not semidecidable; there is no effective deduction system for second-order logic that is sound and complete under full semantics.

Second-order logic with full semantics is more expressive than first-order logic. For example, it is possible to create axiom systems in second-order logic that uniquely characterize the natural numbers and the real line. The cost of this expressiveness is that second-order and higher-order logics have fewer attractive metalogical properties than first-order logic. For example, the Löwenheim–Skolem theorem and compactness theorem of first-order logic become false when generalized to higher-order logics with full semantics.

Automated theorem proving and formal methods
Automated theorem proving refers to the development of computer programs that search and find derivations (formal proofs) of mathematical theorems. Finding derivations is a difficult task because the search space can be very large; an exhaustive search of every possible derivation is theoretically possible but computationally infeasible for many systems of interest in mathematics. Thus complicated heuristic functions are developed to attempt to find a derivation in less time than a blind search.

The related area of automated proof verification uses computer programs to check that human-created proofs are correct. Unlike complicated automated theorem provers, verification systems may be small enough that their correctness can be checked both by hand and through automated software verification. This validation of the proof verifier is needed to give confidence that any derivation labeled as "correct" is actually correct.

Some proof verifiers, such as Metamath, insist on having a complete derivation as input. Others, such as Mizar and Isabelle, take a well-formatted proof sketch (which may still be very long and detailed) and fill in the missing pieces by doing simple proof searches or applying known decision procedures: the resulting derivation is then verified by a small core "kernel". Many such systems are primarily intended for interactive use by human mathematicians: these are known as proof assistants. They may also use formal logics that are stronger than first-order logic, such as type theory. Because a full derivation of any nontrivial result in a first-order deductive system will be extremely long for a human to write, results are often formalized as a series of lemmas, for which derivations can be constructed separately.

Automated theorem provers are also used to implement formal verification in computer science. In this setting, theorem provers are used to verify the correctness of programs and of hardware such as processors with respect to a formal specification. Because such analysis is time-consuming and thus expensive, it is usually reserved for projects in which a malfunction would have grave human or financial consequences.

For the problem of model checking, efficient algorithms are known to decide whether an input finite structure satisfies a first-order formula, in addition to computational complexity bounds: see.

title: First-order logic


text:
Talk:Fusion

Nuclear fusion talk
I have moved the entire previous content (concerning solely nuclear fusion) on this talk page Talk:Fusion to Talk:Nuclear fusion. --Jerzy(t) 03:10, 2004 Mar 7 (UTC) The reference to Dragonball Z rather brings down the tone of the page.

Layout and headings
I feel the layout is unnecessarily complex. I'd like to move all the examples where fusion is used by definition to the top, as nuclear fusion and jazz fusion are the most common disambiguation links. All the names can be grouped lower in simpler categories. --Knulclunk 03:57, 13 May 2007 (UTC)
 * I agree. most people mean Jazz Fusion by fusion, which you can not find on the list, only on the fusion music list. —Preceding unsigned comment added by 91.139.27.23 (talk) 14:22, 8 November 2008 (UTC)

Maintenance
I moved the non-navigable-link and dictionary entries from the page to the list below. Please be sure a blue-linkable wikipedia article exists for an entry before restoring it. Robsavoie (talk) 21:42, 3 July 2010 (UTC)

Business: Computers: Entertainment:
 * Fusion, an oil company that contributes to the economy of Penn Island
 * Fusion RTOS, an embedded or real-time operating system
 * Fusion WebPilot browser, an embedded web browser
 * Microcode Solutions Fusion, a popular Macintosh Emulator for Amiga computers
 * Fusion, a combat technique in Dragon Ball that merges two or more people into a single, more powerful individual
 * Fusion Radio Chicago, a top rated Internet radio dance music station broadcasting from Chicago, IL
 * Fusion Radio, an Internet radio station broadcasting from the University of Toronto
 * Fusion (Sven Väth album), a 1998 album by Sven Väth

title: Talk:Fusion


text:
Functor

In mathematics, specifically category theory, a functor is a mapping between categories. Functors were first considered in algebraic topology, where algebraic objects (such as the fundamental group) are associated to topological spaces, and maps between these algebraic objects are associated to continuous maps between spaces. Nowadays, functors are used throughout modern mathematics to relate various categories. Thus, functors are important in all areas within mathematics to which category theory is applied.

The words category and functor were borrowed by mathematicians from the philosophers Aristotle and Rudolf Carnap, respectively. The latter used functor in a linguistic context; see function word.

Definition
Let C and D be categories. A functor F from C to D is a mapping that
 * associates each object $$X$$ in C to an object $$F(X)$$ in D,
 * associates each morphism $$f \colon X \to Y$$ in C to a morphism $$F(f) \colon F(X) \to F(Y)$$ in D such that the following two conditions hold:
 * $$F(\mathrm{id}_{X}) = \mathrm{id}_{F(X)}\,\!$$ for every object $$X$$ in C,
 * $$F(g \circ f) = F(g) \circ F(f)$$ for all morphisms $$f \colon X \to Y\,\!$$ and $$g \colon Y\to Z$$ in C.

That is, functors must preserve identity morphisms and composition of morphisms.

Covariance and contravariance
There are many constructions in mathematics that would be functors but for the fact that they "turn morphisms around" and "reverse composition". We then define a contravariant functor F from C to D as a mapping that
 * associates each object $$X$$ in C with an object $$F(X)$$ in D,
 * associates each morphism $$f \colon X\to Y$$ in C with a morphism $$F(f) \colon F(Y) \to F(X)$$ in D such that the following two conditions hold:
 * $$F(\mathrm{id}_X) = \mathrm{id}_{F(X)}\,\!$$ for every object $$X$$ in C,
 * $$F(g \circ f) = F(f) \circ F(g)$$ for all morphisms $$f \colon X\to Y$$ and $$g \colon Y\to Z$$ in C.

Note that contravariant functors reverse the direction of composition.

Ordinary functors are also called covariant functors in order to distinguish them from contravariant ones. Note that one can also define a contravariant functor as a covariant functor on the opposite category $$C^\mathrm{op}$$. Some authors prefer to write all expressions covariantly. That is, instead of saying $$F \colon C\to D$$ is a contravariant functor, they simply write $$F \colon C^{\mathrm{op}} \to D$$ (or sometimes $$F \colon C \to D^{\mathrm{op}}$$) and call it a functor.

Contravariant functors are also occasionally called cofunctors.

There is a convention which refers to "vectors"—i.e., vector fields, elements of the space of sections $$\Gamma(TM)$$ of a tangent bundle $$TM$$—as "contravariant" and to "covectors"—i.e., 1-forms, elements of the space of sections $$\Gamma\mathord\left(T^*M\right)$$ of a cotangent bundle $$T^*M$$—as "covariant". This terminology originates in physics, and its rationale has to do with the position of the indices ("upstairs" and "downstairs") in expressions such as $${x'}^{\,i} = \Lambda^i_j x^j$$ for $$\mathbf{x}' = \boldsymbol{\Lambda}\mathbf{x}$$ or $$\omega'_i = \Lambda^j_i \omega_j$$ for $$\boldsymbol{\omega}' = \boldsymbol{\omega}\boldsymbol{\Lambda}^\textsf{T}.$$ In this formalism it is observed that the coordinate transformation symbol $$\Lambda^j_i$$ (representing the matrix $$\boldsymbol{\Lambda}^\textsf{T}$$) acts on the "covector coordinates" "in the same way" as on the basis vectors: $$\mathbf{e}_i = \Lambda^j_i\mathbf{e}_j$$—whereas it acts "in the opposite way" on the "vector coordinates" (but "in the same way" as on the basis covectors: $$\mathbf{e}^i = \Lambda^i_j \mathbf{e}^j$$). This terminology is contrary to the one used in category theory because it is the covectors that have pullbacks in general and are thus contravariant, whereas vectors in general are covariant since they can be pushed forward. See also Covariance and contravariance of vectors.

Opposite functor
Every functor $$F \colon C\to D$$ induces the opposite functor $$F^\mathrm{op} \colon  C^\mathrm{op}\to D^\mathrm{op}$$, where $$C^\mathrm{op}$$ and $$D^\mathrm{op}$$ are the opposite categories to $$C$$ and $$D$$. By definition, $$F^\mathrm{op}$$ maps objects and morphisms in the identical way as does $$F$$. Since $$C^\mathrm{op}$$ does not coincide with $$C$$ as a category, and similarly for $$D$$, $$F^\mathrm{op}$$ is distinguished from $$F$$. For example, when composing $$F \colon C_0\to C_1$$ with $$G \colon  C_1^\mathrm{op}\to C_2$$, one should use either $$G\circ F^\mathrm{op}$$ or $$G^\mathrm{op}\circ F$$. Note that, following the property of opposite category, $$\left(F^\mathrm{op}\right)^\mathrm{op} = F$$.

Bifunctors and multifunctors
A bifunctor (also known as a binary functor) is a functor whose domain is a product category. For example, the Hom functor is of the type Cop × C → Set. It can be seen as a functor in two arguments. The Hom functor is a natural example; it is contravariant in one argument, covariant in the other.

A multifunctor is a generalization of the functor concept to n variables. So, for example, a bifunctor is a multifunctor with n = 2.

Properties
Two important consequences of the functor axioms are:
 * F transforms each commutative diagram in C into a commutative diagram in D;
 * if f is an isomorphism in C, then F(f) is an isomorphism in D.

One can compose functors, i.e. if F is a functor from A to B and G is a functor from B to C then one can form the composite functor G ∘ F from A to C. Composition of functors is associative where defined. Identity of composition of functors is the identity functor. This shows that functors can be considered as morphisms in categories of categories, for example in the category of small categories.

A small category with a single object is the same thing as a monoid: the morphisms of a one-object category can be thought of as elements of the monoid, and composition in the category is thought of as the monoid operation. Functors between one-object categories correspond to monoid homomorphisms. So in a sense, functors between arbitrary categories are a kind of generalization of monoid homomorphisms to categories with more than one object.

Examples
\{0\} \mapsto f(\{0\})  = \{f(0)\}       = \{\{\}\},\ $$ $$ \{1\} \mapsto f(\{1\})  = \{f(1)\}       = \{X\},\ $$ $$ \{0,1\} \mapsto f(\{0,1\}) = \{f(0), f(1)\} = \{\{\}, X\}. $$ Note that $$f(\{0, 1\})$$ consequently generates the trivial topology on $$X$$. Also note that although the function $$f$$ in this example mapped to the power set of $$X$$, that need not be the case in general.
 * Diagram: For categories C and J, a diagram of type J in C is a covariant functor $$D \colon J\to C$$.
 * (Category theoretical) presheaf:For categories C and J, a J-presheaf on C is a contravariant functor $$D \colon C\to J$$.In the special case when J is Set, the category of sets and functions, D is called a presheaf on C.
 * Presheaves (over a topological space): If X is a topological space, then the open sets in X form a partially ordered set Open(X) under inclusion. Like every partially ordered set, Open(X) forms a small category by adding a single arrow U → V if and only if $$U \subseteq V$$. Contravariant functors on Open(X) are called presheaves on X. For instance, by assigning to every open set U the associative algebra of real-valued continuous functions on U, one obtains a presheaf of algebras on X.
 * Constant functor: The functor C → D which maps every object of C to a fixed object X in D and every morphism in C to the identity morphism on X. Such a functor is called a constant or selection functor.
 * Endofunctor:: A functor that maps a category to that same category; e.g., polynomial functor.
 * Identity functor:: In category C, written 1C or idC, maps an object to itself and a morphism to itself. The identity functor is an endofunctor.
 * Diagonal functor: The diagonal functor is defined as the functor from D to the functor category DC which sends each object in D to the constant functor at that object.
 * Limit functor: For a fixed index category J, if every functor J → C has a limit (for instance if C is complete), then the limit functor CJ → C assigns to each functor its limit. The existence of this functor can be proved by realizing that it is the right-adjoint to the diagonal functor and invoking the Freyd adjoint functor theorem. This requires a suitable version of the axiom of choice. Similar remarks apply to the colimit functor (which assigns to every functor its colimit, and is covariant).
 * Power sets functor: The power set functor P : Set → Set maps each set to its power set and each function $$ f \colon X \to Y$$ to the map which sends $$U \in \mathcal{P}(X)$$ to its image $$f(U) \in \mathcal{P}(Y)$$. One can also consider the contravariant power set functor which sends $$ f \colon X \to Y $$ to the map which sends $$V \subseteq Y$$ to its inverse image $$f^{-1}(V) \subseteq X.$$ For example, if $$X = \{0,1\}$$ then $$F(X) = \mathcal{P}(X) = \{\{\}, \{0\}, \{1\}, X\}$$. Suppose $$f(0) = \{\}$$ and $$f(1) = X$$. Then $$F(f)$$ is the function which sends any subset $$U$$ of $$X$$ to its image $$f(U)$$, which in this case means $$\{\} \mapsto f(\{\}) = \{\}$$, where $$\mapsto$$ denotes the mapping under $$F(f)$$, so this could also be written as $$(F(f))(\{\})= \{\}$$. For the other values,$$
 * : The map which assigns to every vector space its dual space and to every linear map its dual or transpose is a contravariant functor from the category of all vector spaces over a fixed field to itself.
 * Fundamental group: Consider the category of pointed topological spaces, i.e. topological spaces with distinguished points. The objects are pairs (X, x0), where X is a topological space and x0 is a point in X. A morphism from (X, x0) to (Y, y0) is given by a continuous map f : X → Y with f(x0) = y0. To every topological space X with distinguished point x0, one can define the fundamental group based at x0, denoted π1(X, x0). This is the group of homotopy classes of loops based at x0, with the group operation of concatenation. If f : X → Y is a morphism of pointed spaces, then every loop in X with base point x0 can be composed with f to yield a loop in Y with base point y0. This operation is compatible with the homotopy equivalence relation and the composition of loops, and we get a group homomorphism from π(X, x0) to π(Y, y0). We thus obtain a functor from the category of pointed topological spaces to the category of groups. In the category of topological spaces (without distinguished point), one considers homotopy classes of generic curves, but they cannot be composed unless they share an endpoint. Thus one has the fundamental groupoid instead of the fundamental group, and this construction is functorial.
 * Algebra of continuous functions: A contravariant functor from the category of topological spaces (with continuous maps as morphisms) to the category of real associative algebras is given by assigning to every topological space X the algebra C(X) of all real-valued continuous functions on that space. Every continuous map f : X → Y induces an algebra homomorphism C(f) : C(Y) → C(X) by the rule C(f)(φ) = φ ∘ f for every φ in C(Y).
 * Tangent and cotangent bundles: The map which sends every differentiable manifold to its tangent bundle and every smooth map to its derivative is a covariant functor from the category of differentiable manifolds to the category of vector bundles. Doing this constructions pointwise gives the tangent space, a covariant functor from the category of pointed differentiable manifolds to the category of real vector spaces. Likewise, cotangent space is a contravariant functor, essentially the composition of the tangent space with the dual space above.
 * Group actions/representations: Every group G can be considered as a category with a single object whose morphisms are the elements of G. A functor from G to Set is then nothing but a group action of G on a particular set, i.e. a G-set. Likewise, a functor from G to the category of vector spaces, VectK, is a linear representation of G. In general, a functor G → C can be considered as an "action" of G on an object in the category C. If C is a group, then this action is a group homomorphism.
 * Lie algebras: Assigning to every real (complex) Lie group its real (complex) Lie algebra defines a functor.
 * Tensor products: If C denotes the category of vector spaces over a fixed field, with linear maps as morphisms, then the tensor product $$V \otimes W$$ defines a functor C × C → C which is covariant in both arguments.
 * Forgetful functors: The functor U : Grp → Set which maps a group to its underlying set and a group homomorphism to its underlying function of sets is a functor. Functors like these, which "forget" some structure, are termed forgetful functors. Another example is the functor Rng → Ab which maps a ring to its underlying additive abelian group. Morphisms in Rng (ring homomorphisms) become morphisms in Ab (abelian group homomorphisms).
 * Free functors: Going in the opposite direction of forgetful functors are free functors. The free functor F : Set → Grp sends every set X to the free group generated by X. Functions get mapped to group homomorphisms between free groups. Free constructions exist for many categories based on structured sets. See free object.
 * Homomorphism groups: To every pair A, B of abelian groups one can assign the abelian group Hom(A, B) consisting of all group homomorphisms from A to B. This is a functor which is contravariant in the first and covariant in the second argument, i.e. it is a functor Abop × Ab → Ab (where Ab denotes the category of abelian groups with group homomorphisms). If f : A1 → A2 and g : B1 → B2 are morphisms in Ab, then the group homomorphism Hom(f, g): Hom(A2, B1) → Hom(A1, B2) is given by φ ↦ g ∘ φ ∘ f. See Hom functor.
 * Representable functors: We can generalize the previous example to any category C. To every pair X, Y of objects in C one can assign the set Hom(X, Y) of morphisms from X to Y. This defines a functor to Set which is contravariant in the first argument and covariant in the second, i.e. it is a functor Cop × C → Set. If f : X1 → X2 and g : Y1 → Y2 are morphisms in C, then the map Hom(f, g) : Hom(X2, Y1) → Hom(X1, Y2) is given by φ ↦ g ∘ φ ∘ f. Functors like these are called representable functors. An important goal in many settings is to determine whether a given functor is representable.

Relation to other categorical concepts
Let C and D be categories. The collection of all functors from C to D forms the objects of a category: the functor category. Morphisms in this category are natural transformations between functors.

Functors are often defined by universal properties; examples are the tensor product, the direct sum and direct product of groups or vector spaces, construction of free groups and modules, direct and inverse limits. The concepts of limit and colimit generalize several of the above.

Universal constructions often give rise to pairs of adjoint functors.

Computer implementations
Functors sometimes appear in functional programming. For instance, the programming language Haskell has a class  where   is a polytypic function used to map functions (morphisms on Hask, the category of Haskell types) between existing types to functions between some new types.

title: Functor