text:
Intuitionistic logic

Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems of intuitionistic logic do not assume the law of the excluded middle and double negation elimination, which are fundamental inference rules in classical logic.

Formalized intuitionistic logic was originally developed by Arend Heyting to provide a formal basis for L. E. J. Brouwer's programme of intuitionism. From a proof-theoretic perspective, Heyting’s calculus is a restriction of classical logic in which the law of excluded middle and double negation elimination have been removed. Excluded middle and double negation elimination can still be proved for some propositions on a case by case basis, however, but do not hold universally as they do with classical logic. The standard explanation of intuitionistic logic is the BHK interpretation.

Several systems of semantics for intuitionistic logic have been studied. One of these semantics mirrors classical Boolean-valued semantics but uses Heyting algebras in place of Boolean algebras. Another semantics uses Kripke models. These, however, are technical means for studying Heyting’s deductive system rather than formalizations of Brouwer’s original informal semantic intuitions. Semantical systems claiming to capture such intuitions, due to offering meaningful concepts of “constructive truth” (rather than merely validity or provability), are Kurt Gödel’s dialectica interpretation, Stephen Cole Kleene’s realizability, Yurii Medvedev’s logic of finite problems, or Giorgi Japaridze’s computability logic. Yet such semantics persistently induce logics properly stronger than Heyting’s logic. Some authors have argued that this might be an indication of inadequacy of Heyting’s calculus itself, deeming the latter incomplete as a constructive logic.

Mathematical constructivism
In the semantics of classical logic, propositional formulae are assigned truth values from the two-element set $$\{\top, \bot\}$$ ("true" and "false" respectively), regardless of whether we have direct evidence for either case. This is referred to as the 'law of excluded middle', because it excludes the possibility of any truth value besides 'true' or 'false'. In contrast, propositional formulae in intuitionistic logic are not assigned a definite truth value and are only considered "true" when we have direct evidence, hence proof. (We can also say, instead of the propositional formula being "true" due to direct evidence, that it is inhabited by a proof in the Curry–Howard sense.) Operations in intuitionistic logic therefore preserve justification, with respect to evidence and provability, rather than truth-valuation.

Intuitionistic logic is a commonly-used tool in developing approaches to constructivism in mathematics. The use of constructivist logics in general has been a controversial topic among mathematicians and philosophers (see, for example, the Brouwer–Hilbert controversy). A common objection to their use is the above-cited lack of two central rules of classical logic, the law of excluded middle and double negation elimination. David Hilbert considered them to be so important to the practice of mathematics that he wrote:
 * "Taking the principle of excluded middle from the mathematician would be the same, say, as proscribing the telescope to the astronomer or to the boxer the use of his fists. To prohibit existence statements and the principle of excluded middle is tantamount to relinquishing the science of mathematics altogether."

Intuitionistic logic has found practical use in mathematics despite the challenges presented by the inability to utilize these rules. One reason for this is that its restrictions produce proofs that have the existence property, making it also suitable for other forms of mathematical constructivism. Informally, this means that if there is a constructive proof that an object exists, that constructive proof may be used as an algorithm for generating an example of that object, a principle known as the Curry–Howard correspondence between proofs and algorithms. One reason that this particular aspect of intuitionistic logic is so valuable is that it enables practitioners to utilize a wide range of computerized tools, known as proof assistants. These tools assist their users in the generation and verification of large-scale proofs, whose size usually precludes the usual human-based checking that goes into publishing and reviewing a mathematical proof. As such, the use of proof assistants (such as Agda or Coq) is enabling modern mathematicians and logicians to develop and prove extremely complex systems, beyond those that are feasible to create and check solely by hand. One example of a proof that was impossible to satisfactorily verify without formal verification is the famous proof of the four color theorem. This theorem stumped mathematicians for more than a hundred years, until a proof was developed that ruled out large classes of possible counterexamples, yet still left open enough possibilities that a computer program was needed to finish the proof. That proof was controversial for some time, but, later, it was verified using Coq.

Syntax
The syntax of formulas of intuitionistic logic is similar to propositional logic or first-order logic. However, intuitionistic connectives are not definable in terms of each other in the same way as in classical logic, hence their choice matters. In intuitionistic propositional logic (IPL) it is customary to use →, ∧, ∨, ⊥ as the basic connectives, treating ¬A as an abbreviation for (A → ⊥). In intuitionistic first-order logic both quantifiers ∃, ∀ are needed.

Hilbert-style calculus
Intuitionistic logic can be defined using the following Hilbert-style calculus. This is similar to a way of axiomatizing classical propositional logic.

In propositional logic, the inference rule is modus ponens and the axioms are To make this a system of first-order predicate logic, the generalization rules are added, along with the axioms
 * MP: from $$\phi \to \psi$$ and $$\phi$$ infer $$\psi$$
 * THEN-1: $$\psi \to (\phi \to \psi )$$
 * THEN-2: $$\big(\chi \to (\phi \to \psi )\big) \to \big((\chi \to \phi) \to (\chi \to \psi )\big)$$
 * AND-1: $$\phi \land \chi \to \phi $$
 * AND-2: $$\phi \land \chi \to \chi $$
 * AND-3: $$\phi \to \big(\chi \to (\phi \land \chi )\big)$$
 * OR-1: $$\phi \to \phi \lor \chi $$
 * OR-2: $$\chi \to \phi \lor \chi $$
 * OR-3: $$(\phi \to \psi ) \to \Big((\chi \to \psi ) \to \big((\phi \lor \chi) \to \psi )\Big)$$
 * FALSE: $$\bot \to \phi $$
 * $$\forall $$-GEN: from $$\psi \to \phi $$ infer $$\psi \to (\forall x \ \phi )$$, if $$x$$ is not free in $$\psi $$
 * $$\exists $$-GEN: from $$\phi \to \psi $$ infer $$(\exists x \ \phi ) \to \psi $$, if $$x$$ is not free in $$\psi $$
 * PRED-1: $$(\forall x \ \phi (x)) \to \phi (t)$$, if the term $$t$$ is free for substitution for the variable $$x$$ in $$\phi$$ (i.e., if no occurrence of any variable in $$t$$ becomes bound in $$\phi (t)$$)
 * PRED-2: $$\phi (t) \to (\exists x \ \phi (x))$$, with the same restriction as for PRED-1

Negation
If one wishes to include a connective $$\neg$$ for negation rather than consider it an abbreviation for $$\phi \to \bot $$, it is enough to add:
 * NOT-1': $$(\phi \to \bot ) \to \neg \phi $$
 * NOT-2': $$\neg \phi \to (\phi \to \bot )$$

There are a number of alternatives available if one wishes to omit the connective $$\bot $$ (false). For example, one may replace the three axioms FALSE, NOT-1', and NOT-2' with the two axioms as at. Alternatives to NOT-1 are $$(\phi \to \neg \chi ) \to (\chi \to \neg \phi )$$ or $$(\phi \to \neg \phi ) \to \neg \phi $$.
 * NOT-1: $$(\phi \to \chi ) \to \big((\phi \to \neg \chi ) \to \neg \phi \big)$$
 * NOT-2: $$\chi \to (\neg \chi \to \psi)$$

Equivalence
The connective $$\leftrightarrow $$ for equivalence may be treated as an abbreviation, with $$\phi \leftrightarrow \chi $$ standing for $$(\phi \to \chi ) \land (\chi \to \phi )$$. Alternatively, one may add the axioms

 * IFF-1: $$(\phi \leftrightarrow \chi ) \to (\phi \to \chi )$$
 * IFF-2: $$(\phi \leftrightarrow \chi ) \to (\chi \to \phi )$$
 * IFF-3: $$(\phi \to \chi ) \to ((\chi \to \phi ) \to (\phi \leftrightarrow \chi ))$$

IFF-1 and IFF-2 can, if desired, be combined into a single axiom $$(\phi \leftrightarrow \chi ) \to ((\phi \to \chi ) \land (\chi \to \phi ))$$ using conjunction.

Sequent calculus
Gerhard Gentzen discovered that a simple restriction of his system LK (his sequent calculus for classical logic) results in a system that is sound and complete with respect to intuitionistic logic. He called this system LJ. In LK any number of formulas is allowed to appear on the conclusion side of a sequent; in contrast LJ allows at most one formula in this position.

Other derivatives of LK are limited to intuitionistic derivations but still allow multiple conclusions in a sequent. LJ' is one example.

Theorems
The theorems of the pure logic are the statements provable from the axioms and inference rules. For example, using THEN-1 in THEN-2 reduces it to $$\big(\chi \to (\phi \to \psi )\big) \to \big(\phi \to (\chi \to \psi )\big)$$. A formal proof of the latter using the Hilbert system is given on that page. With $$\bot$$ for $$\psi$$, this in turn implies $$(\chi \to \neg\phi) \to (\phi \to \neg\chi)$$. In words: "If $$\chi$$ being the case implies that $$\phi$$ is absurd, then if $$\phi$$ does hold, one has that $$\chi$$ is not the case." Due to the symmetry of the statement, one in fact obtained
 * $$(\chi \to \neg\phi) \leftrightarrow (\phi \to \neg\chi)$$

When explaining the theorems of intuitionistic logic in terms of classical logic, it can be understood as a weakening thereof: It is more conservative in what it allows a reasoner to infer, while not permitting any new inferences that could not be made under classical logic. Each theorem of intuitionistic logic is a theorem in classical logic, but not conversely. Many tautologies in classical logic are not theorems in intuitionistic logic – in particular, as said above, one of intuitionistic logic's chief aims is to not affirm the law of the excluded middle so as to vitiate the use of non-constructive proof by contradiction, which can be used to furnish existence claims without providing explicit examples of the objects that it proves exist.

Double negations
It does merely "not affirm" the law of the excluded middle because while it is not necessarily the case that the law is upheld in any context, no counterexample can be given either. Such a counterexample would be an inference (inferring the negation of the law for a certain proposition) disallowed under classical logic and thus is not allowed in a strict weakening like intuitionistic logic. Formally, it is a simple theorem that $$\big((\psi\lor(\psi\to\varphi))\to\varphi\big) \leftrightarrow \varphi$$ for any two propositions. By considering any $$\varphi$$ established to be false this indeed shows that the double negation of the law $$\neg\neg(\psi\lor\neg\psi)$$ is retained as a tautology already in minimal logic. So the propositional calculus is always compatible with classical logic. When assuming the law implies a proposition, then by applying contraposition twice and using the double-negated excluded middle, one may prove double-negated variants of various strictly classical tautologies. The situation is more intricate for predicate logic formulas, when some quantified expressions are being negated.

Double negation and implication
Akin to the above, from modus ponens in the form $$\psi\to((\psi\to\varphi)\to\varphi)$$ follows $$\psi\to\neg\neg\psi$$. The relation between them may always be used to obtain new formulas: A weakened premise makes for a strong implication, and vice versa. For example, note that if $$(\neg\neg \psi) \to \phi$$ holds, then so does $$\psi \to \phi$$, but the schema in the other direction would imply the double-negation elimination principle. Propositions for which double-negation elimination is possible are also called stable. Intuitionistic logic proves stability only for restricted types of propositions. A formula for which excluded middle holds can be proven stable using the disjunctive syllogism, which is discussed more thoroughly below. The converse does however not hold in general, unless the excluded middle statement at hand is stable itself.

An implication $$\psi \to \neg\phi$$ can be proven to be equivalent to $$\neg\neg\psi \to \neg\phi$$, whatever the propositions. As a special case, it follows that propositions of negated form ($$\psi=\neg\phi$$ here) are stable, i.e. $$\neg\neg\neg\phi \to \neg\phi$$ is always valid.

In general, $$\neg\neg \psi \to \phi$$ is stronger than $$\psi \to \phi$$, which is stronger than $$\neg\neg (\psi \to \phi)$$, which itself implies the three equivalent statements $$\psi \to (\neg\neg \phi)$$, $$(\neg\neg \psi) \to (\neg\neg \phi)$$ and $$\neg\phi\to\neg\psi$$. Using the disjunctive syllogism, the previous four are indeed equivalent. This also gives an intuitionistically valid derivation of $$\neg\neg(\neg\neg\phi\to\phi)$$, as it is thus equivalent to an identity.

When $$\psi$$ expresses a claim, then its double-negation $$\neg\neg\psi$$ merely expresses the claim that a refutation of $$\psi$$ would be inconsistent. Having proven such a mere double-negation also still aids in negating other statements through negation introduction, as then $$(\phi\to\neg\psi)\to\neg\phi$$. A double-negated existential statement does not denote existence of an entity with a property, but rather the absurdity of assumed non-existence of any such entity. Also all the principles in the next section involving quantifiers explain use of implications with hypothetical existence as premise.

Formula translation
Weakening statements by adding two negations before existential quantifiers (and atoms) is also the core step in the double-negation translation. It constitutes an embedding of classical first-order logic into intuitionistic logic: a first-order formula is provable in classical logic if and only if its Gödel–Gentzen translation is provable intuitionistically. For example, any theorem of classical propositional logic of the form $$\psi\to\phi$$ has a proof consisting of an intuitionistic proof of $$\psi\to\neg\neg\phi$$ followed by one application of double-negation elimination. Intuitionistic logic can thus be seen as a means of extending classical logic with constructive semantics.

Non-interdefinability of operators
Already minimal logic easily proves the following theorems, relating conjunction resp. disjunction to the implication using negation:
 * $$(\phi \lor \psi) \to \neg (\neg \phi \land \neg \psi)$$
 * $$(\phi \lor \psi) \to (\neg \phi \to \neg \neg \psi)$$, a weakened variant of the disjunctive syllogism

resp.
 * $$(\phi \land \psi) \to \neg (\neg \phi \lor \neg \psi)$$
 * $$(\phi \land \psi) \to \neg (\phi \to \neg \psi)$$ and similarly $$(\phi \to \psi) \to \neg (\phi \land \neg\psi)$$

Indeed, stronger variants of these still do hold - for example the antecedents may be double-negated, as noted, or all $$\psi$$ may be replaced by $$\neg\neg\psi$$ on the antecedent sides, as will be discussed. However, neither of these five implications can be reversed without immediately implying excluded middle (consider $$\neg \psi$$ for $$\phi$$) resp. double-negation elimination (consider true $$\phi$$). Hence, the left hand sides do not constitute a possible definition of the right hand sides.

In contrast, in classical propositional logic it is possible to take one of those three connectives plus negation as primitive and define the other two in terms of it, in this way. Such is done, for example, in Łukasiewicz's three axioms of propositional logic. It is even possible to define all in terms of a sole sufficient operator such as the Peirce arrow (NOR) or Sheffer stroke (NAND). Similarly, in classical first-order logic, one of the quantifiers can be defined in terms of the other and negation. These are fundamentally consequences of the law of bivalence, which makes all such connectives merely Boolean functions. The law of bivalence is not required to hold in intuitionistic logic. As a result, none of the basic connectives can be dispensed with, and the above axioms are all necessary. So most of the classical identities between connectives and quantifiers are only theorems of intuitionistic logic in one direction. Some of the theorems go in both directions, i.e. are equivalences, as subsequently discussed.

Existential vs. universal quantification
Firstly, when $$x$$ is not free in the proposition $$\varphi$$, then
 * $$\big(\exists x\, (\phi(x)\to \varphi)\big)\,\,\to\,\,\Big(\big(\forall x \ \phi(x)\big)\to\varphi\Big)$$

When the domain of discourse is empty, then by the principle of explosion, an existential statement implies anything. When the domain contains at least one term, then assuming excluded middle for $$\forall x \, \phi(x)$$, the inverse of the above implication becomes provably too, meaning the two sides become equivalent. This inverse direction is equivalent to the drinker's paradox (DP). Moreover, an existential and dual variant of it is given by the independence of premise principle (IP). Classically, the statement above is moreover equivalent to a more disjunctive form discussed further below. Constructively, existence claims are however generally harder to come by.

If the domain of discourse is not empty and $$\phi$$ is moreover independent of $$x$$, such principles are equivalent to formulas in the propositional calculus. Here, the formula then just expresses the identity $$(\phi\to\varphi)\to(\phi\to\varphi)$$. This is the curried form of modus ponens $$((\phi\to\varphi)\land\phi)\to\varphi$$, which in the special the case with $$\varphi$$ as a false proposition results in the law of non-contradiction principle $$\neg(\phi\land\neg\phi)$$. Considering a false proposition $$\varphi$$ for the original implication results in the important In words: "If there exists an entity $$x$$ that does not have the property $$\phi$$, then the following is refuted: Each entity has the property $$\phi$$."
 * $$(\exists x \ \neg \phi(x)) \to \neg (\forall x \ \phi(x))$$

The quantifier formula with negations also immediately follows from the non-contradiction principle derived above, each instance of which itself already follows from the more particular $$\neg(\neg\neg\phi\land\neg\phi)$$. To derive a contradiction given $$\neg\phi$$, it suffices to establish its negation $$\neg\neg\phi$$ (as opposed to the stronger $$\phi$$) and this makes proving double-negations valuable also. By the same token, the original quantifier formula in fact still holds with $$\forall x \ \phi(x)$$ weakened to $$\forall x \big((\phi(x)\to\varphi)\to\varphi\big)$$. And so, in fact, a stronger theorem holds:
 * $$(\exists x \ \neg \phi(x)) \to \neg (\forall x \, \neg\neg\phi(x))$$

In words: "If there exists an entity $$x$$ that does not have the property $$\phi$$, then the following is refuted: For each entity, one is not able to prove that it does not have the property $$\phi$$".

Secondly,
 * $$\big(\forall x \, (\phi(x)\to \varphi)\big)\,\,\leftrightarrow\,\,\big((\exists x \ \phi(x))\to\varphi\big)$$

where similar considerations apply. Here the existential part is always a hypothesis and this is an equivalence. Considering the special case again, The proven conversion $$(\chi\to\neg \phi)\leftrightarrow(\phi\to\neg \chi)$$ can be used to obtain two further implications:
 * $$(\forall x \ \neg \phi(x)) \leftrightarrow \neg (\exists x \ \phi(x))$$
 * $$(\forall x \ \phi(x)) \to \neg (\exists x \ \neg \phi(x))$$
 * $$(\exists x \ \phi(x)) \to \neg (\forall x \ \neg \phi(x))$$

Of course, variants of such formulas can also be derived that have the double-negations in the antecedent. A special case of the first formula here is $$(\forall x \, \neg\phi(x)) \to \neg (\exists x \, \neg \neg \phi(x))$$ and this is indeed stronger than the $$\to$$-direction of the equivalence bullet point listed above. For simplicity of the discussion here and below, the formulas are generally presented in weakened forms without all possible insertions of double-negations in the antecedents.

More general variants hold. Incorporating the predicate $$\psi$$ and currying, the following generalization also entails the relation between implication and conjunction in the predicate calculus, discussed below.
 * $$\big(\forall x \ \phi(x)\to (\psi(x)\to\varphi)\big)\,\,\leftrightarrow\,\,\Big(\big(\exists x \ \phi(x)\land \psi(x)\big)\to\varphi\Big)$$

If the predicate $$\psi$$ is decidedly false for all $$x$$, then this equivalence is trivial. If $$\psi$$ is decidedly true for all $$x$$, the schema simply reduces to the previously stated equivalence. In the language of classes, $$A=\{x\mid\phi(x)\}$$ and $$B=\{x\mid\psi(x)\}$$, the special case of this equivalence with false $$\varphi$$ equates two characterizations of disjointness $$A\cap B=\emptyset$$:
 * $$\forall(x\in A).x\notin B\,\,\leftrightarrow\,\,\neg\exists(x\in A).x\in B$$

Disjunction vs. conjunction
There are finite variations of the quantifier formulas, with just two propositions: The first principle cannot be reversed: Considering $$\neg \psi$$ for $$\phi$$ would imply the weak excluded middle, i.e. the statement $$\neg \psi \lor \neg \neg \psi$$. But intuitionistic logic alone does not even prove $$\neg \psi \lor \neg \neg \psi\lor (\neg \neg \psi\to \psi)$$. So in particular, there is no distributivity principle for negations deriving the claim $$\neg \phi \lor \neg \psi$$ from $$\neg(\phi \land \psi)$$. For an informal example of the constructive reading, consider the following: From conclusive evidence it not to be the case that both Alice and Bob showed up to their date, one cannot derive conclusive evidence, tied to either of the two persons, that this person did not show up. Negated propositions are comparably weak, in that the classically valid De Morgan's law, granting a disjunction from a single negative hypothetical, does not automatically hold constructively. The intuitionistic propositional calculus and some of its extensions exhibit the disjunction property instead, implying one of the disjuncts of any disjunction individually would have to be derivable as well.
 * $$(\neg \phi \lor \neg \psi) \to \neg (\phi \land \psi)$$
 * $$(\neg \phi \land \neg \psi) \leftrightarrow \neg (\phi \lor \psi)$$

The converse variants of those two, and the equivalent variants with double-negated antecedents, had already been mentioned above. Implications towards the negation of a conjunction can often be proven directly from the non-contradiction principle. In this way one may alos obtain the mixed form of the implications, e.g. $$(\neg \phi \lor \psi) \to \neg (\phi \land \neg \psi)$$. Concatenating the theorems, we also find The reverse cannot be provable, as it would prove weak excluded middle.
 * $$(\neg \neg \phi \lor \neg \neg \psi) \to \neg \neg (\phi \lor \psi)$$

In predicate logic, the constant domain principle is not valid: $$\forall x \big(\varphi \lor \psi(x)\big)$$ does not imply the stronger $$\varphi\lor \forall x\,\psi(x)$$. The distributive properties does however hold for any finite number of propositions. For a variant of the De Morgan law concerning two existentially closed decidable predicates, see LLPO.

Conjunction vs. implication
From the general equivalence also follows import-export, expressing incompatibility of two predicates using two different connectives: Due to the symmetry of the conjunction connective, this again implies the already established $$(\phi \to \neg \psi) \leftrightarrow (\psi \to \neg \phi) $$. The equivalence formula for the negated conjunction may be understood as a special case of currying and uncurrying. Many more considerations regarding double-negations again apply. And both non-reversible theorems relating conjunction and implication mentioned in the introduction follow from this equivalence. One is a converse, and $$(\phi \to \psi) \to \neg (\phi \land \neg\psi)$$ holds simply because $$\phi \to \psi$$ is stronger than $$\phi \to \neg\neg\psi$$.
 * $$(\phi \to \neg \psi) \leftrightarrow \neg (\phi \land \psi)$$

Now when using the principle in the next section, the following variant of the latter, with more negations on the left, also holds: A consequence is that
 * $$\neg (\phi \to \psi) \leftrightarrow (\neg \neg \phi \land \neg \psi) $$
 * $$\neg \neg (\phi \land \psi) \leftrightarrow (\neg \neg \phi \land \neg \neg \psi) $$

Disjunction vs. implication
Already minimal logic proves excluded middle equivalent to consequentia mirabilis, an instance of Peirce's law. Now akin to modus ponens, clearly $$(\phi \lor \psi)\to((\phi\to\psi)\to \psi)$$ already in minimal logic, which is a theorem that does not even involve negations. In classical logic, this implication is in fact an equivalence. With taking $$\phi$$ to be of the form $$\psi\to\varphi$$, excluded middle together with explosion is seen to entail Peirce's law.

In intuitionistic logic, one obtains variants of the stated theorem involving $$\bot$$, as follows. Firstly, note that two different formulas for $$\neg (\phi \land \psi)$$ mentioned above can be used to imply $$(\neg \phi \vee \neg \psi) \to (\phi \to \neg \psi)$$. The latter are forms of the disjunctive syllogism for negated propositions, $$\neg\psi$$. A strengthened form still holds in intuitionistic logic: As in previous sections, the positions of $$\neg \phi $$ and $$\phi $$ may be switched, giving a stronger principle than the one mentioned in the introduction. So, for example, intuitionistically "Either $$P$$ or $$Q$$" is a stronger propositional formula than "If not $$P$$, then $$Q$$", whereas these are classically interchangeable. The implication cannot generally be reversed, as that immediately implies excluded middle.
 * $$(\neg \phi \lor \psi) \to (\phi \to \psi)$$

Non-contradiction and explosion together also prove the stronger variant $$(\neg \phi \lor \psi) \to (\neg\neg\phi \to \psi)$$. And this shows how excluded middle for $$\psi$$ implies double-negation elimination for it. For a fixed $$\psi$$, this implication cannot generally be reversed. (However, as $$\neg\neg(\psi\lor\neg \psi)$$ is always constructively valid, it follows that assuming double-negation elimination for all such disjunctions implies classical logic also.)

Of course the formulas established here may be combined to obtain yet more variations. For example, the disjunctive syllogism as presented generalizes to
 * $$\Big(\big(\exists x \ \neg\phi(x)\big)\lor\varphi\Big)\,\,\to\,\,\Big(\big(\forall x \ \phi(x)\big)\to\varphi\Big)$$

If some term exists at all, the antecedent here even implies $$\exists x \big(\phi(x)\to\varphi\big)$$, which in turn itself also implies the conclusion here (this is again the very first formula mentioned in this section).

The bulk of the discussion in these sections applies just as well to just minimal logic. But as for the disjunctive syllogism with general $$\psi$$, minimal logic can at most prove $$(\neg\phi \lor \psi) \to (\neg\neg \phi \to \psi')$$ where $$\psi'$$ denotes $$\neg\neg\psi\land(\psi\lor\neg\psi)$$. The conclusion here can only be simplified to $$\psi$$ using explosion.

Equivalences
The above lists also contain equivalences. The equivalence involving a conjunction and a disjunction stems from $$(P\lor Q)\to R$$ actually being stronger than $$P\to R$$. Both sides of the equivalence can be understood as conjunctions of independent implications. Above, absurdity $$\bot$$ is used for $$R$$. In functional interpretations, it corresponds to if-clause constructions. So e.g. "Not ($$P$$ or $$Q$$)" is equivalent to "Not $$P$$, and also not $$Q$$".

An equivalence itself is generally defined as, and then equivalent to, a conjunction ($$\land$$) of implications ($$\to$$), as follows: With it, such connectives become in turn definable from it:
 * $$(\phi\leftrightarrow \psi) \leftrightarrow \big((\phi \to \psi)\land(\psi\to\phi)\big)$$
 * $$(\phi\to\psi) \leftrightarrow ((\phi\lor\psi) \leftrightarrow \psi)$$
 * $$(\phi\to\psi) \leftrightarrow ((\phi\land\psi) \leftrightarrow \phi)$$
 * $$(\phi\land\psi) \leftrightarrow ((\phi\to\psi)\leftrightarrow\phi)$$
 * $$(\phi\land\psi) \leftrightarrow (((\phi\lor\psi)\leftrightarrow\psi)\leftrightarrow\phi)$$

In turn, $$\{\lor, \leftrightarrow, \bot\}$$ and $$\{\land, \leftrightarrow, \neg\}$$ are complete bases of intuitionistic connectives, for example.

Functionally complete connectives
As shown by Alexander V. Kuznetsov, either of the following connectives – the first one ternary, the second one quinary – is by itself functionally complete: either one can serve the role of a sole sufficient operator for intuitionistic propositional logic, thus forming an analog of the Sheffer stroke from classical propositional logic:
 * $$\big((P\lor Q)\land\neg R\big)\lor\big(\neg P\land(Q\leftrightarrow R)\big)$$
 * $$P\to\big(Q\land\neg R\land(S\lor T)\big)$$

Semantics
The semantics are rather more complicated than for the classical case. A model theory can be given by Heyting algebras or, equivalently, by Kripke semantics. Recently, a Tarski-like model theory was proved complete by Bob Constable, but with a different notion of completeness than classically.

Unproved statements in intuitionistic logic are not given an intermediate truth value (as is sometimes mistakenly asserted). One can prove that such statements have no third truth value, a result dating back to Glivenko in 1928. Instead they remain of unknown truth value, until they are either proved or disproved. Statements are disproved by deducing a contradiction from them.

A consequence of this point of view is that intuitionistic logic has no interpretation as a two-valued logic, nor even as a finite-valued logic, in the familiar sense. Although intuitionistic logic retains the trivial propositions $$\{\top, \bot\}$$ from classical logic, each proof of a propositional formula is considered a valid propositional value, thus by Heyting's notion of propositions-as-sets, propositional formulae are (potentially non-finite) sets of their proofs.

Heyting algebra semantics
In classical logic, we often discuss the truth values that a formula can take. The values are usually chosen as the members of a Boolean algebra. The meet and join operations in the Boolean algebra are identified with the ∧ and ∨ logical connectives, so that the value of a formula of the form A ∧ B is the meet of the value of A and the value of B in the Boolean algebra. Then we have the useful theorem that a formula is a valid proposition of classical logic if and only if its value is 1 for every valuation—that is, for any assignment of values to its variables.

A corresponding theorem is true for intuitionistic logic, but instead of assigning each formula a value from a Boolean algebra, one uses values from a Heyting algebra, of which Boolean algebras are a special case. A formula is valid in intuitionistic logic if and only if it receives the value of the top element for any valuation on any Heyting algebra.

It can be shown that to recognize valid formulas, it is sufficient to consider a single Heyting algebra whose elements are the open subsets of the real line R. In this algebra we have:

 * $$\begin{align}

\text{Value}[\bot] &=\emptyset \\ \text{Value}[\top] &= \mathbf{R} \\ \text{Value}[A \land B] &= \text{Value}[A] \cap \text{Value}[B] \\ \text{Value}[A \lor B] &= \text{Value}[A] \cup \text{Value}[B] \\ \text{Value}[A \to B] &= \text{int} \left ( \text{Value}[A]^\complement \cup \text{Value}[B] \right ) \end{align}$$

where int(X) is the interior of X and X∁ its complement.

The last identity concerning A → B allows us to calculate the value of ¬A:

 * $$\begin{align}

\text{Value}[\neg A] &= \text{Value}[A \to \bot] \\ &= \text{int} \left ( \text{Value}[A]^\complement \cup \text{Value}[\bot] \right ) \\ &= \text{int} \left ( \text{Value}[A]^\complement \cup \emptyset \right ) \\ &= \text{int} \left ( \text{Value}[A]^\complement \right ) \end{align}$$

With these assignments, intuitionistically valid formulas are precisely those that are assigned the value of the entire line. For example, the formula ¬(A ∧ ¬A) is valid, because no matter what set X is chosen as the value of the formula A, the value of ¬(A ∧ ¬A) can be shown to be the entire line:

 * $$\begin{align}

\text{Value}[\neg(A \land \neg A)] &= \text{int} \left ( \text{Value} [A \land \neg A]^\complement  \right )  && \text{Value}[\neg B] = \text{int}\left ( \text{Value}[B]^\complement \right) \\ &= \text{int} \left ( \left (\text{Value}[A] \cap \text{Value}[\neg A] \right )^\complement \right )\\ &= \text{int} \left ( \left (\text{Value}[A] \cap \text{int} \left (\text{Value}[A]^\complement \right ) \right )^\complement \right )  \\ &= \text{int} \left ( \left (X \cap \text{int} \left (X^\complement \right ) \right )^\complement \right ) \\ &= \text{int} \left (\emptyset^\complement \right ) && \text{int} \left (X^\complement \right ) \subseteq X^\complement \\ &= \text{int} (\mathbf{R}) \\ &= \mathbf{R} \end{align}$$

So the valuation of this formula is true, and indeed the formula is valid. But the law of the excluded middle, A ∨ ¬A, can be shown to be invalid by using a specific value of the set of positive real numbers for A:

 * $$\begin{align}

\text{Value}[A \lor \neg A] &= \text{Value}[A] \cup \text{Value}[\neg A] \\ &= \text{Value}[A] \cup \text{int} \left (  \text{Value}[A]^\complement \right) && \text{Value}[\neg B] = \text{int}\left ( \text{Value}[B]^\complement \right) \\ &= \{ x > 0\} \cup \text{int} \left (  \{x > 0\}^\complement \right ) \\ &= \{ x > 0\} \cup \text{int} \left ( \{x \leqslant 0 \} \right) \\ &= \{ x > 0\} \cup \{x < 0 \} \\ &=\{ x \neq 0 \} \\ &\neq \mathbf{R} \end{align}$$

The interpretation of any intuitionistically valid formula in the infinite Heyting algebra described above results in the top element, representing true, as the valuation of the formula, regardless of what values from the algebra are assigned to the variables of the formula. Conversely, for every invalid formula, there is an assignment of values to the variables that yields a valuation that differs from the top element. No finite Heyting algebra has the second of these two properties.

Kripke semantics
Building upon his work on semantics of modal logic, Saul Kripke created another semantics for intuitionistic logic, known as Kripke semantics or relational semantics.

Tarski-like semantics
It was discovered that Tarski-like semantics for intuitionistic logic were not possible to prove complete. However, Robert Constable has shown that a weaker notion of completeness still holds for intuitionistic logic under a Tarski-like model. In this notion of completeness we are concerned not with all of the statements that are true of every model, but with the statements that are true in the same way in every model. That is, a single proof that the model judges a formula to be true must be valid for every model. In this case, there is not only a proof of completeness, but one that is valid according to intuitionistic logic.

Admissible rules
In intuitionistic logic or a fixed theory using the logic, the situation can occur that an implication always hold metatheoretically, but not in the language. For example, in the pure propositional calculus, if $$(\neg A)\to(B\lor C)$$ is provable, then so is $$(\neg A\to B)\lor(\neg A\to C)$$. Another example is that $$(A\to B)\to(A\lor C)$$ being provable always also means that so is $$\big((A\to B)\to A\big)\lor\big((A\to B)\to C\big)$$. One says the system is closed under these implications as rules and they may be adopted.

Paraconsistent logic
Intuitionistic logic is related by duality to a paraconsistent logic known as Brazilian, anti-intuitionistic or dual-intuitionistic logic.

The subsystem of intuitionistic logic with the FALSE (resp. NOT-2) axiom removed is known as minimal logic and some differences have been elaborated on above.

Intermediate logics
In 1932, Kurt Gödel defined a system of logics intermediate between classical and intuitionistic logic. Indeed, any finite Heyting algebra that is not equivalent to a Boolean algebra defines (semantically) an intermediate logic. On the other hand, validity of formulae in pure intuitionistic logic is not tied to any individual Heyting algebra but relates to any and all Heyting algebras at the same time.

So for example, for a schema not involving negations, consider the classically valid $$(A\to B)\lor(B\to A)$$. Adopting this over intuitionistic logic gives the intermediate logic called Gödel-Dummett logic.

Relation to classical logic
The system of classical logic is obtained by adding any one of the following axioms:
 * $$\phi \lor \neg \phi$$ (Law of the excluded middle)
 * $$\neg \neg \phi \to \phi$$ (Double negation elimination)
 * $$(\neg \phi \to \phi) \to \phi$$ (Consequentia mirabilis, see also Peirce's law)

Various reformulations, or formulations as schemata in two variables (e.g. Peirce's law), also exist. One notable one is the (reverse) law of contraposition Such are detailed on the intermediate logics article.
 * $$(\neg \phi \to \neg \chi ) \to (\chi \to \phi)$$

In general, one may take as the extra axiom any classical tautology that is not valid in the two-element Kripke frame $$\circ{\longrightarrow}\circ$$ (in other words, that is not included in Smetanich's logic).

Many-valued logic
Kurt Gödel's work involving many-valued logic showed in 1932 that intuitionistic logic is not a finite-valued logic. (See the section titled Heyting algebra semantics above for an infinite-valued logic interpretation of intuitionistic logic.)

Modal logic
Any formula of the intuitionistic propositional logic (IPC) may be translated into the language of the normal modal logic S4 as follows:

 * $$\begin{align}

\bot^* &= \bot \\ A^* &= \Box A && \text{if } A \text{ is prime (a positive literal)} \\ (A \wedge B)^*&= A^* \wedge B^* \\ (A \vee B)^* &= A^* \vee B^* \\ (A \to B)^*&= \Box \left (A^* \to B^* \right ) \\ (\neg A)^*&= \Box(\neg (A^*)) && \neg A := A \to \bot \end{align}$$

and it has been demonstrated that the translated formula is valid in the propositional modal logic S4 if and only if the original formula is valid in IPC. The above set of formulae are called the Gödel–McKinsey–Tarski translation. There is also an intuitionistic version of modal logic S4 called Constructive Modal Logic CS4.

Lambda calculus
There is an extended Curry–Howard isomorphism between IPC and simply-typed lambda calculus.

title: Intuitionistic logic


text:
Talk:List of years in film

Untitled
UNITARY CONCEPT SCHEME/INDEX FOR LIST OF FILMS FOR EACH YEAR RE-WORK

WE NEED TO DEVELOP AN UNITARY SCHEME FOR EACH OF OUR "YEAR IN FILM" (LIKE IT IS DONE FROM 2002 IN FILM ONWARDS, BUT BETTER!).

WHAT     SHOULD BE DISPLAYED IN THE TABLE? (TITLE, PUBLISHING COMPANY, CAST ...) WHO      SHOULD BE INCLUDED IN THE LISTING OF THE CAST? (ALSO DIRECTORS, SCREENWRITERS ...) OR       SHOULD A NEW ROW BE CREATED? SHOULD   THE MAIN ACTORS BE "BOLDED"?

IN ADDITION WE NEED TO DEFINE THE GENRES, POSSIBLY UNITE THEM.

I WANT TO GRADUALLY PUT ALL THE "YEARSIN FILM" INTO THAT REGISTER SCHEME, SO IT HAS A UNITED LOOK AND STATISTICS CAN BE MADE EASIER! VÍS-A-VÍS

IN ORDER TO DISCUSS THIS I'D LIKE TO USE THIS PAGE; BUT WHEN IT IS TO START PROGRAMMING THE MODEL TABLE WE OUGHTA LAUNCH A PROJECT GROUP CONSISTING OF ME AND ANOTHER PROGRAMMER; AND VOLUNTEERS WHO HELP PUTTING THAT CONCEPT ON EVERY YEAR & FIND MISTAKES AND DISCUSS THE INFORMATION FROM THE CURRENT LISTS OF FILMS PER YEAR --134.109.116.45 (talk) 13:46, 15 October 2013 (UTC) Daniel Presberger

Narrow minded This list should be renamed "List of years in american film". Even then it would be very narrow minded. There is a strong commercial bias, Maya Deren is not even mentioned. Film is not only about making money.

Why are we including television here? If we're going to have this -- and if we do, it really should just be the important stuff -- Spongebob Squarepants really doesn't qualify. -- Zoe

Of course it qualifies Vera Cruz

 * There's going to be a separate set of pages for "years in television"... Was Spongebob in a movie? -Jazz77

 * You could always add what you think are important milestones in film and see if they stick. Just be sure to be concise and to the point. A list like this could go on forever if you were to take the completionist's route and include everything you could find (before the 1960s it's already starting to look like a mass of confusion). And make sure the entries are notable. The last thing we need is some dork listing his first baby video his dad shot with a Hi8. lol I think we probably need to work out a system of what to list and what's important. Maybe within each decade (or even year) listing separate them into singular moments, awards, events, and so on. But keep it a structured block of text or bullet points and layout. Like notable award winners worldwide, notable releases from their respective countries, etc. Just don't let the pendulum swing the complete opposite way just to avoid American made films. Gotta be fair here. And you can't be too esoteric and/or start listing experimental student films made in film schools that may never be seen again. We have to be reasonable here. --FazzMunkle (talk) 05:41, 28 January 2009 (UTC)

Could this list be changed to go forwards please? And I've moved "1800s in film" -- on Wikipedia, that is a decade not a century -- Tarquin 22:27 Jan 22, 2003 (UTC)

I removed from 1920 : - As radio is introduced, the popularity of silent films begins to decline

Seems a very dubious claim since silent films were still a growing industry and radio a curiosity still rare in homes at the time. -- Infrogmation 06:35 Feb 3, 2003 (UTC)

I shudder to think that Kangaroo Jack is the epitome of 2003 in films -- Zoe

 * Why delete future events? For example the following movie is scheduled for release in early December 2003.  The movie is in post-production and the studio has already committed to a Premier venue and date - publicly.

 * The Lord of the Rings: The Return of the King to be released in December. - kiwiinapanic 09:58 Feb 14, 2003 (UTC)

 * Because it hasn't happened yet. It may not happen.  A world war may stop anything from being released by the end of the year.  Peter Jackson may die in a car wreck and his work put on hold.  Why make predictions?  This is an encyclopedia, not a crystal ball.  -- Zoe

Most controversial film in history. - What makes it controversial? -- Zoe

 * It seems far too early to judge if Irreversible (movie) is the most controversial film in history. -- Infrogmation 02:13 Mar 16, 2003 (UTC)

I'm going to make some comments that apply to all the 'Years in Film pages'.

If you are going to put release dates on movies, please make them the first release in any country, not in the US. Second, please use a universally recognised date format. (12/1) is ambiguous.

The "Top Grossing" section has real problems. First it means "Top Grossing in the U.S." without saying so (I know this because the figures are copied from the IMDB). Second it needs to add the IMDB disclaimer, in case people think that the figures are the amounts taken in the year in question. Third, any movie which might still be shown in a theatre can have its grosses change, and thus the figures for 2002 might still be changing in 2003; it might be better simply to give links to the IMDB, like we do for 2003.

Please don't include movies that were released in the US in the year in question if they were released elsewhere earlier. If we gave a movie an entry in every year in which it was released in some country or other the lists would be very confusing.

DJ Clayworth 16:02, 29 Aug 2003 (UTC)

 * The Top Grossing sections are a mess. I just checked 1942 and removed 4 of the 5 listings. SOme of those on the list made only a tenth of the box office of the top movies. I used IMDB and Mchael Gelbert's The Encyclopedia of Movie Awards. Does anyone know what source was used to originally make the lists? The link to box office totals on this page is just as bad for instance for 1951 it lists On the Riveria as #4 when Gelbert makes it #20. Not an isolated difference - such are more common than not. Rmhermen 15:41, 8 Jun 2004 (UTC)
 * I did more checking and it appears that our lists are based on Worldboxoffice.com (link on this page) which at least currently says on its FAQ that the rankings should be ignored as there are so many missing movies from its database, especially old ones. I think we got duped. Rmhermen 16:49, 8 Jun 2004 (UTC)

2009

 * What happened to 2009 in film? -AMK152 02:37, 3 April 2006 (UTC)

Shift in importance of films?
I have made a thorough round through all the years, making for each a section "Films released in xxxx", in the place of "Other films" or other similar occasional headings, making sure each film mentioned in Awards and Top grossing was added to it's release year (as stated in the corresponding article, or the amg if without article). I have given a steady form to the year navigation (to the top right of each article) and fixed many links to point to the film articles (still, many remain linking to irrelevant articles). Also I have made an effort to keep the index box as uniform through the years as possible, turnung some subheadings to bold text.

In Awards I have reduced some subheaders to bold (like already done in some years, where "Academy Awards" had been turned to Awards and under it (in capitalized bold) "Academy Awards", "Golden Globe" (with inlined underlined bold sub-titles for 2 sub-types) and "BAFTA". My opinion is that "Directors Guild" is also important for their choice of director of the year. I also don't see why Cannes' "Palme d'Or" is not equally present, since they also accept english films for their awards and offer a more european art film view.

In the years of the 2000's surely the information on money, by being tabled over Awards, breaks the balance. Has there really been a shift in judging films by economical success over quality? If so, this issue is worth mentioning, in some relevant article. My view is that Awards should preceede Top grossing, all through the years, and that Academy Awards should be Awards with subsections as mentioned above. Technically I see no harm as it is, so long as there is an inclusive list (not table) for the films of each year, so that entries can be easilly added and crossed with other lists. As for encyclopedic presentation, I think a peer should tell us what is best. Hoverfish 10:47, 18 October 2006 (UTC)

Changing in 2006 and 2005
Jesus "Titties Fuckin'" Christ, who the fuck kept changing my movies that are the best ever to the movies I hate so much. Aargh,if it's some kunt or dick changing it, I'm callin' the fuckin' cops and endup in Juvie! —Preceding unsigned comment added by Danny66.6 (talk • contribs) 05:23, 1 September 2007 (UTC)

Criteria for film listed?
I have to ask, what exactly is the criteria for the films listed for each year? They come off as unnecessary, at least if they continue to be added without any point of reference citing why exactly they were important to their respective years. 131.247.37.177 (talk) —Preceding undated comment added 04:14, 2 May 2012 (UTC). \
 * The answer is quite obvious. If someone -- anyone -- has a favorite film, he or she adds it. No other criteria. (Please note: I'm not agreeing with this method, but that clearly is the method). Cresix (talk) 01:44, 11 October 2012 (UTC)

2014 through 2017
My two cents: 2014 through 2017 shpuld remain as separate articles, but not 2018. There have been two AfDs in recent months; see Articles for deletion/2018 in film (2nd nomination). I think we should hold off on re-creating the 2018 article until June 2014. Bearian (talk) 21:16, 18 November 2013 (UTC)

Discussion
People who edit this page may be intrested in this discussion about cutting down on excessive material. Thanks.  Lugnuts  Dick Laurent is dead 12:41, 29 April 2014 (UTC)

The Dark Knight Rises
The Dark Knight Rises should be add to 2012. Imean why would you have 2/3 of the trilogy listed? --TDKR Chicago 101 (talk) 02:19, 10 February 2015 (UTC)

We need a new system
It is obvious: we need to have a clear set of criteria for films to be included in this article. I'd say we should have a limit of films per year (I'd say eight) and sequels should be considered significant before inclusion (e.g. The Godfather Part II (won Academy Award for Best Picture) and Terminator 2 (for its groundbreaking effects) can be included, but not Iron Man 2 or Shrek 2). The last thing we need is a cluttered mess like List of unusual deaths once was. -24.18.128.102 (talk) 13:31, 1 December 2017 (UTC)
 * Until you have consensus STOP removing material from this article. You do not have consensus to delete information added by other editors...Modernist (talk) 20:22, 1 December 2017 (UTC)
 * More importantly, neither do YOU have consensus to keep all those films that were added there just today without consensus themselves. 24.18.128.102 (talk) 20:40, 1 December 2017 (UTC)
 * Instead of deleting material and complaining add your proposal for a clear system; and let other editors weigh in...Modernist (talk) 20:30, 1 December 2017 (UTC)

We should set a limit - something like, no more than six films per year, of which no more than three are English-language. Sheila1988 (talk) 20:41, 7 December 2020 (UTC)

Invitation to talk pages about the format of 2019 in film
Everyone seeing this is invited to the sections on WP:FILM and MOS:FILM about the format change on 2019 in film. BattleshipMan (talk) 21:37, 6 October 2019 (UTC)

Examples are terrible
The only examples are English language films with the exception of a few Japanese films and I am not sure why there are no examples of movies from other places like Africa Mexico or China etc — Preceding unsigned comment added by 71.173.64.11 (talk) 08:29, 12 May 2021 (UTC)

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

title: Talk:List of years in film


text:
Family tree

A family tree, also called a genealogy or a pedigree chart, is a chart representing family relationships in a conventional tree structure. More detailed family trees, used in medicine and social work, are known as genograms.

Representations of family history
Genealogical data can be represented in several formats, for example, as a pedigree or . Family trees are often presented with the oldest generations at the top of the tree and the younger generations at the bottom. An ancestry chart, which is a tree showing the ancestors of an individual and not all members of a family, will more closely resemble a tree in shape, being wider at the top than at the bottom. In some ancestry charts, an individual appears on the left and his or her ancestors appear to the right. Conversely, a descendant chart, which depicts all the descendants of an individual, will be narrowest at the top. Beyond these formats, some family trees might include all members of a particular surname (e.g., male-line descendants). Yet another approach is to include all holders of a certain office, such as the Kings of Germany, which represents the reliance on marriage to link dynasties together.

The passage of time can also be included to illustrate ancestry and descent. A time scale is often used, expanding radially across the center, divided into decades. Children of the parent form branches around the center and their names are plotted in their birth year on the time scale. Spouses' names join children's names and nuclear families of parents and children branch off to grandchildren, and so on. Great-grandparents are often in the center to portray four or five generations, which reflect the natural growth pattern of a tree as seen from the top but sometimes there can be great great grandparents or more. In a descendant tree, living relatives are common on the outer branches and contemporary cousins appear adjacent to each other. Privacy should be considered when preparing a living family tree.

The image of the tree probably originated with that of the Tree of Jesse in medieval art, used to illustrate the Genealogy of Christ in terms of a prophecy of Isaiah (Isaiah 11:1). Possibly the first non-biblical use, and the first to show full family relationships rather than a purely patrilineal scheme, was that involving family trees of the classical gods in Boccaccio's Genealogia Deorum Gentilium ("On the Genealogy of the Gods of the Gentiles"), whose first version dates to 1360.

Common formats
In addition to familiar representations of family history and genealogy as a tree structure, there are other notable systems used to illustrate and document ancestry and descent.

Ahnentafel

An Ahnentafel (German for "ancestor table") is a genealogical numbering system for listing a person's direct ancestors in a fixed sequence of ascent: and so on, back through the generations. Apart from the subject or proband, who can be male or female, all even-numbered persons are male, and all odd-numbered persons are female. In this scheme, the number of any person's father is double the person's number, and a person's mother is double the person's number plus one. This system can also be displayed as a tree:
 * 1) Subject (or proband)
 * 2) Father
 * 3) Mother
 * 4) Paternal grandfather
 * 5) Paternal grandmother
 * 6) Maternal grandfather
 * 7) Maternal grandmother

Fan chart
A fan chart features a half circle chart with concentric rings: the subject is the inner circle, the second circle is divided in two (each side is one parent), the third circle is divided in four, and so forth. Fan charts depict paternal and maternal ancestors.

Graph theory
While family trees are depicted as trees, family relations do not in general form a tree in the strict sense used in graph theory, since distant relatives can mate. Therefore, a person can have a common ancestor on both their mother's and father's side. However, because a parent must be born before their child, an individual cannot be their own ancestor, and thus there are no loops. In this regard, ancestry forms a directed acyclic graph. Nevertheless, graphs depicting matrilineal descent (mother-daughter relationships) and patrilineal descent (father-son relationships) do form trees. Assuming no common ancestor, an ancestry chart is a perfect binary tree, as each person has exactly one mother and one father; these thus have a regular structure. A Descendant chart, on the other hand, does not, in general, have a regular structure, as a person can have any number of children or none at all.

Notable examples
Family trees have been used to document family histories across time and cultures throughout the world.

Africa
In Africa, the ruling dynasty of Ethiopia claimed descent from King Solomon via the Queen of Sheba. Through this claim, the family traced their descent back to the House of David.

The genealogy of Ancient Egyptian ruling dynasties was recorded from the beginnings of the Pharaonic era c. 3000 BC to the end of the Ptolomaic Kingdom; although this is not a record of one continuously-linked family lineage, and surviving records are incomplete.

Elsewhere in Africa, oral traditions of genealogical recording predominate. Members of the Keita dynasty of Mali, for example, have had their pedigrees sung by griots during annual ceremonies since the 14th century. Meanwhile, in Nigeria, many ruling clans—most notably those descended from Oduduwa—claim descent from the legendary King Kisra. Here too, pedigrees are recited by griots attached to the royal courts.

The Americas
In some pre-contact Native American civilizations, genealogical records of ruling and priestly families were kept, some of which extended over several centuries or longer.

East Asia
There are extensive genealogies for the ruling dynasties of China, but these do not form a single, unified family tree. Additionally, it is unclear at which point(s) the most ancient historical figures named become mythological.

In Japan, the ancestry of the Imperial Family is traced back to the mythological origins of Japan. The connection to persons from the established historical record only begins in the mid-first millennium AD.

The longest family tree in the world is that of the Chinese philosopher and educator Confucius (551–479 BC), who is descended from King Tang (1675–1646 BC). The tree spans more than 80 generations from him and includes more than 2 million members. An international effort involving more than 450 branches around the world was started in 1998 to retrace and revise this family tree. A new edition of the Confucius genealogy was printed in September 2009 by the Confucius Genealogy Compilation Committee, to coincide with the 2560th anniversary of the birth of the Chinese thinker. This latest edition was expected to include some 1.3 million living members who are scattered around the world today.

Europe and West Asia
Before the Dark Ages, in the Greco-Roman world, some reliable pedigrees dated back perhaps at least as far as the first half of the first millennium BC; with claimed or mythological origins reaching back further. Roman clan and family lineages played an important part in the structure of their society and were the basis of their intricate system of personal names. However, there was a break in the continuity of record-keeping at the end of Classical Antiquity. Records of the lines of succession of the Popes and the Eastern Roman Emperors through this transitional period have survived, but these are not continuous genealogical histories of single families. Refer to descent from antiquity.

Many noble and aristocratic families of European and West Asian origin can reliably trace their ancestry back as far as the mid to late first millennium AD; some claiming undocumented descent from Classical Antiquity or mythological ancestors. In Europe, for example, the pedigree of Niall Noígíallach would be a contender for the longest, through Conn of the Hundred Battles (fl. 123 AD); in the legendary history of Ireland, he is further descended from Breogán, and ultimately from Adam, through the sons of Noah.

Another very old and extensive tree is that of the Lurie lineage—which includes Sigmund Freud and Martin Buber—and traces back to Lurie, a 13th-century rabbi in Brest-Litovsk, and from there to Rashi and purportedly back to the legendary King David, as documented by Neil Rosenstein in his book The Lurie Legacy. The 1999 edition of the Guinness Book of Records recorded the Lurie family in the "longest lineage" category as one of the oldest-known living families in the world today.

Family trees and representations of lineages are also important in religious traditions. The biblical genealogies of Jesus also claim descent from the House of David, covering a period of approximately 1000 years. In the Torah and Old Testament, genealogies are provided for many biblical persons, including a record of the descendants of Adam. Also according to the Torah, the Kohanim are descended from Aaron. Genetic testing performed at the Technion has shown that most modern Kohanim share common Y-chromosome origins, although there is no complete family tree of the Kohanim. In the Islamic world, claimed descent from Muhammad greatly enhanced the status of political and religious leaders; new dynasties often used claims of such descent to help establish their legitimacy.

Elsewhere
Elsewhere, in many human cultures, clan and tribal associations are based on claims of common ancestry, although detailed documentation of those origins is often very limited.

Global
Forms of family trees are also used in genetic genealogy. In 2022, scientists reported the largest detailed human genetic genealogy, that unifies human genomes from many sources for insights about human history, ancestry and evolution and demonstrates a novel computational method for estimating how human DNA is related via a series of 13 million linked trees along the genome, a tree-sequence, which has been described as the largest "human family tree".

Other uses
The author Pete Frame is notable for having produced "family trees" of rock bands. In this instance, the entries represent a membership of certain groups, and personnel changes within them, rather than family relationships. Several books have been produced with his family trees, which in turn have led to a BBC television series about them, including interviews from the bands depicted in the trees.

Another common use is in the creation of episcopal trees in Christian traditions that believe in apostolic succession. In this case, the connection is not made through blood, but through the order of succession of bishops.

title: Family tree


text:
Macrophage

Macrophages (abbreviated Mφ, MΦ or MP) are a type of white blood cell of the innate immune system that engulf and digest pathogens, such as cancer cells, microbes, cellular debris, and foreign substances, which do not have proteins that are specific to healthy body cells on their surface. This process is called phagocytosis, which acts to defend the host against infection and injury.

Macrophages are found in essentially all tissues, where they patrol for potential pathogens by amoeboid movement. They take various forms (with various names) throughout the body (e.g., histiocytes, Kupffer cells, alveolar macrophages, microglia, and others), but all are part of the mononuclear phagocyte system. Besides phagocytosis, they play a critical role in nonspecific defense (innate immunity) and also help initiate specific defense mechanisms (adaptive immunity) by recruiting other immune cells such as lymphocytes. For example, they are important as antigen presenters to T cells. In humans, dysfunctional macrophages cause severe diseases such as chronic granulomatous disease that result in frequent infections.

Beyond increasing inflammation and stimulating the immune system, macrophages also play an important anti-inflammatory role and can decrease immune reactions through the release of cytokines. Macrophages that encourage inflammation are called M1 macrophages, whereas those that decrease inflammation and encourage tissue repair are called M2 macrophages. This difference is reflected in their metabolism; M1 macrophages have the unique ability to metabolize arginine to the "killer" molecule nitric oxide, whereas M2 macrophages have the unique ability to metabolize arginine to the "repair" molecule ornithine. However, this dichotomy has been recently questioned as further complexity has been discovered.

Human macrophages are about 21 um in diameter and are produced by the differentiation of monocytes in tissues. They can be identified using flow cytometry or immunohistochemical staining by their specific expression of proteins such as CD14, CD40, CD11b, CD64, F4/80 (mice)/EMR1 (human), lysozyme M, MAC-1/MAC-3 and CD68.

Macrophages were first discovered and named by Élie Metchnikoff, a Russian Empire zoologist, in 1884.

Types

A majority of macrophages are stationed at strategic points where microbial invasion or accumulation of foreign particles is likely to occur. These cells together as a group are known as the mononuclear phagocyte system and were previously known as the reticuloendothelial system. Each type of macrophage, determined by its location, has a specific name:

Investigations concerning Kupffer cells are hampered because in humans, Kupffer cells are only accessible for immunohistochemical analysis from biopsies or autopsies. From rats and mice, they are difficult to isolate, and after purification, only approximately 5 million cells can be obtained from one mouse.

Macrophages can express paracrine functions within organs that are specific to the function of that organ. In the testis, for example, macrophages have been shown to be able to interact with Leydig cells by secreting 25-hydroxycholesterol, an oxysterol that can be converted to testosterone by neighbouring Leydig cells. Also, testicular macrophages may participate in creating an immune privileged environment in the testis, and in mediating infertility during inflammation of the testis.

Cardiac resident macrophages participate in electrical conduction via gap junction communication with cardiac myocytes.

Macrophages can be classified on basis of the fundamental function and activation. According to this grouping, there are classically activated (M1) macrophages, wound-healing macrophages (also known as alternatively-activated (M2) macrophages), and regulatory macrophages (Mregs).

Development
Macrophages that reside in adult healthy tissues either derive from circulating monocytes or are established before birth and then maintained during adult life independently of monocytes. By contrast, most of the macrophages that accumulate at diseased sites typically derive from circulating monocytes. Leukocyte extravasation describes monocyte entry into damaged tissue through the endothelium of blood vessels as they become macrophages. Monocytes are attracted to a damaged site by chemical substances through chemotaxis, triggered by a range of stimuli including damaged cells, pathogens and cytokines released by macrophages already at the site. At some sites such as the testis, macrophages have been shown to populate the organ through proliferation. Unlike short-lived neutrophils, macrophages survive longer in the body, up to several months.

Phagocytosis
Macrophages are professional phagocytes and are highly specialized in removal of dying or dead cells and cellular debris. This role is important in chronic inflammation, as the early stages of inflammation are dominated by neutrophils, which are ingested by macrophages if they come of age (see CD31 for a description of this process).

The neutrophils are at first attracted to a site, where they perform their function and die, before they or their neutrophil extracellular traps are phagocytized by the macrophages. When at the site, the first wave of neutrophils, after the process of aging and after the first 48 hours, stimulate the appearance of the macrophages whereby these macrophages will then ingest the aged neutrophils.

The removal of dying cells is, to a greater extent, handled by fixed macrophages, which will stay at strategic locations such as the lungs, liver, neural tissue, bone, spleen and connective tissue, ingesting foreign materials such as pathogens and recruiting additional macrophages if needed.

When a macrophage ingests a pathogen, the pathogen becomes trapped in a phagosome, which then fuses with a lysosome. Within the phagolysosome, enzymes and toxic peroxides digest the pathogen. However, some bacteria, such as Mycobacterium tuberculosis, have become resistant to these methods of digestion. Typhoidal Salmonellae induce their own phagocytosis by host macrophages in vivo, and inhibit digestion by lysosomal action, thereby using macrophages for their own replication and causing macrophage apoptosis. Macrophages can digest more than 100 bacteria before they finally die due to their own digestive compounds.

Role in innate immune response
When a pathogen invades, tissue resident macrophages are among the first cells to respond. Two of the main roles of the tissue resident macrophages are to phagocytose incoming antigen and to secrete proinflammatory cytokines that induce inflammation and recruit other immune cells to the site.

Phagocytosis of pathogens
Macrophages can internalize antigens through receptor-mediated phagocytosis. Macrophages have a wide variety of pattern recognition receptors (PRRs) that can recognize microbe-associated molecular patterns (MAMPs) from pathogens. Many PRRs, such as toll-like receptors (TLRs), scavenger receptors (SRs), C-type lectin receptors, among others, recognize pathogens for phagocytosis. Macrophages can also recognize pathogens for phagocytosis indirectly through opsonins, which are molecules that attach to pathogens and mark them for phagocytosis. Opsonins can cause a stronger adhesion between the macrophage and pathogen during phagocytosis, hence opsonins tend to enhance macrophages’ phagocytic activity. Both complement proteins and antibodies can bind to antigens and opsonize them. Macrophages have complement receptor 1 (CR1) and 3 (CR3) that recognize pathogen-bound complement proteins C3b and iC3b, respectively, as well as fragment crystallizable γ receptors (FcγRs) that recognize the fragment crystallizable (Fc) region of antigen-bound immunoglobulin G (IgG) antibodies. When phagocytosing and digesting pathogens, macrophages go through a respiratory burst where more oxygen is consumed to supply the energy required for producing reactive oxygen species (ROS) and other antimicrobial molecules that digest the consumed pathogens.

Cytokine secretion
Recognition of MAMPs by PRRs can activate tissue resident macrophages to secrete proinflammatory cytokines that recruit other immune cells. Among the PRRs, TLRs play a major role in signal transduction leading to cytokine production. The binding of MAMPs to TLR triggers a series of downstream events that eventually activates transcription factor NF-κB and results in transcription of the genes for several proinflammatory cytokines, including IL-1β, IL-6, TNF-α, IL-12B, and type I interferons such as IFN-α and IFN-β. Systemically, IL-1β, IL-6, and TNF-α induce fever and initiate the acute phase response in which the liver secretes acute phase proteins. Locally, IL-1β and TNF-α cause vasodilation, where the gaps between blood vessel epithelial cells widen, and upregulation of cell surface adhesion molecules on epithelial cells to induce leukocyte extravasation.

Neutrophils are among the first immune cells recruited by macrophages to exit the blood via extravasation and arrive at the infection site. Macrophages secrete many chemokines such as CXCL1, CXCL2, and CXCL8 (IL-8) that attract neutrophils to the site of infection. After neutrophils have finished phagocytosing and clearing the antigen at the end of the immune response, they undergo apoptosis, and macrophages are recruited from blood monocytes to help clear apoptotic debris.

Macrophages also recruit other immune cells such as monocytes, dendritic cells, natural killer cells, basophils, eosinophils, and T cells through chemokines such as CCL2, CCL4, CCL5, CXCL8, CXCL9, CXCL10, and CXCL11. Along with dendritic cells, macrophages help activate natural killer (NK) cells through secretion of type I interferons (IFN-α and IFN-β) and IL-12. IL-12 acts with IL-18 to stimulate the production of proinflammatory cytokine interferon gamma (IFN-γ) by NK cells, which serves as an important source of IFN-γ before the adaptive immune system is activated. IFN-γ enhances the innate immune response by inducing a more aggressive phenotype in macrophages, allowing macrophages to more efficiently kill pathogens.

Some of the T cell chemoattractants secreted by macrophages include CCL5, CXCL9, CXCL10, and CXCL11.

Interactions with CD4+ T Helper Cells
Macrophages are professional antigen presenting cells (APC), meaning they can present peptides from phagocytosed antigens on major histocompatibility complex (MHC) II molecules on their cell surface for T helper cells. Macrophages are not primary activators of naïve T helper cells that have never been previously activated since tissue resident macrophages do not travel to the lymph nodes where naïve T helper cells reside. Although macrophages are also found in secondary lymphoid organs like the lymph nodes, they do not reside in T cell zones and are not effective at activating naïve T helper cells. The macrophages in lymphoid tissues are more involved in ingesting antigens and preventing them from entering the blood, as well as taking up debris from apoptotic lymphocytes. Therefore, macrophages interact mostly with previously activated T helper cells that have left the lymph node and arrived at the site of infection or with tissue resident memory T cells.

Macrophages supply both signals required for T helper cell activation: 1) Macrophages present antigen peptide-bound MHC class II molecule to be recognized by the corresponding T cell receptor (TCR), and 2) recognition of pathogens by PRRs induce macrophages to upregulate the co-stimulatory molecules CD80 and CD86 (also known as B7) that binds to CD28 on T helper cells to supply the co-stimulatory signal. These interactions allow T helper cells to achieve full effector function and provide T helper cells with continued survival and differentiation signals preventing them from undergoing apoptosis due to lack of TCR signaling. For example, IL-2 signaling in T cells upregulates the expression of anti-apoptotic protein Bcl-2, but T cell production of IL-2 and the high-affinity IL-2 receptor IL-2RA both require continued signal from TCR recognition of MHC-bound antigen.

Activation
Macrophages can achieve different activation phenotypes through interactions with different subsets of T helper cells, such as TH1 and TH2. Although there is a broad spectrum of macrophage activation phenotypes, there are two major phenotypes that are commonly acknowledged. They are the classically activated macrophages, or M1 macrophages, and the alternatively activated macrophages, or M2 macrophages. M1 macrophages are proinflammatory, while M2 macrophages are mostly anti-inflammatory.

Classical
TH1 cells play an important role in classical macrophage activation as part of type 1 immune response against intracellular pathogens (such as intracellular bacteria) that can survive and replicate inside host cells, especially those pathogens that replicate even after being phagocytosed by macrophages. After the TCR of TH1 cells recognize specific antigen peptide-bound MHC class II molecules on macrophages, TH1 cells 1) secrete IFN-γ and 2) upregulate the expression of CD40 ligand (CD40L), which binds to CD40 on macrophages. These 2 signals activate the macrophages and enhance their ability to kill intracellular pathogens through increased production of antimicrobial molecules such as nitric oxide (NO) and superoxide (O2-). This enhancement of macrophages' antimicrobial ability by TH1 cells is known as classical macrophage activation, and the activated macrophages are known as classically activated macrophages, or M1 macrophages. The M1 macrophages in turn upregulates B7 molecules and antigen presentation through MHC class II molecules to provide signals that sustain T cell help. The activation of TH1 and M1 macrophage is a positive feedback loop, with IFN-γ from TH1 cells upregulating CD40 expression on macrophages; the interaction between CD40 on the macrophages and CD40L on T cells activate macrophages to secrete IL-12; and IL-12 promotes more IFN-γ secretion from TH1 cells. The initial contact between macrophage antigen-bound MHC II and TCR serves as the contact point between the two cells where most of the IFN-γ secretion and CD-40L on T cells concentrate to, so only macrophages directly interacting with TH1 cells are likely to be activated.

In addition to activating M1 macrophages, TH1 cells express Fas ligand (FasL) and lymphotoxin beta (LT-β) to help kill chronically infected macrophages that can no longer kill pathogens. The killing of chronically infected macrophages release pathogens to the extracellular space that can then be killed by other activated macrophages. TH1 cells also help recruit more monocytes, the precursor to macrophages, to the infection site. TH1 secretion TNF-α and LT-α to make blood vessels easier for monocytes to bind to and exit. TH1 secretion of CCL2 as a chemoattractant for monocytes. IL-3 and GM-CSF released by TH1 cells stimulate more monocyte production in the bone marrow.

When intracellular pathogens cannot be eliminated, such as in the case of Mycobacterium tuberculosis, the pathogen is contained through the formation of granuloma, an aggregation of infected macrophages surrounded by activated T cells. The macrophages bordering the activated lymphocytes often fuse to form multinucleated giant cells that appear to have increased antimicrobial ability due to their proximity to TH1 cells, but over time, the cells in the center start to die and form necrotic tissue.

Alternative
TH2 cells play an important role in alternative macrophage activation as part of type 2 immune response against large extracellular pathogens like helminths. TH2 cells secrete IL-4 and IL-13, which activate macrophages to become M2 macrophages, also known as alternatively activated macrophages. M2 macrophages express arginase-1, an enzyme that converts arginine to ornithine and urea. Ornithine help increase smooth muscle contraction to expel the worm and also participates in tissue and wound repair. Ornithine can be further metabolized to proline, which is essential for synthesizing collagen. M2 macrophages can also decrease inflammation by producing IL-1 receptor antagonist (IL-1RA) and IL-1 receptors that do not lead to downstream inflammatory signaling (IL-1RII).

Interactions with CD8+ cytotoxic t cells
Another part of the adaptive immunity activation involves stimulating CD8+ via cross presentation of antigens peptides on MHC class I molecules. Studies have shown that proinflammatory macrophages are capable of cross presentation of antigens on MHC class I molecules, but whether macrophage cross-presentation plays a role in naïve or memory CD8+ T cell activation is still unclear.

Interactions with B cells
Macrophages have been shown to secrete cytokines BAFF and APRIL, which are important for plasma cell isotype switching. APRIL and IL-6 secreted by macrophage precursors in the bone marrow help maintain survival of plasma cells homed to the bone marrow.

Subtypes
There are several activated forms of macrophages. In spite of a spectrum of ways to activate macrophages, there are two main groups designated M1 and M2. M1 macrophages: as mentioned earlier (previously referred to as classically activated macrophages), M1 "killer" macrophages are activated by LPS and IFN-gamma, and secrete high levels of IL-12 and low levels of IL-10. M1 macrophages have pro-inflammatory, bactericidal, and phagocytic functions. In contrast, the M2 "repair" designation (also referred to as alternatively activated macrophages) broadly refers to macrophages that function in constructive processes like wound healing and tissue repair, and those that turn off damaging immune system activation by producing anti-inflammatory cytokines like IL-10. M2 is the phenotype of resident tissue macrophages, and can be further elevated by IL-4. M2 macrophages produce high levels of IL-10, TGF-beta and low levels of IL-12. Tumor-associated macrophages are mainly of the M2 phenotype, and seem to actively promote tumor growth.

Macrophages exist in a variety of phenotypes which are determined by the role they play in wound maturation. Phenotypes can be predominantly separated into two major categories; M1 and M2. M1 macrophages are the dominating phenotype observed in the early stages of inflammation and are activated by four key mediators: interferon-γ (IFN-γ), tumor necrosis factor (TNF), and damage associated molecular patterns (DAMPs). These mediator molecules create a pro-inflammatory response that in return produce pro-inflammatory cytokines like Interleukin-6 and TNF. Unlike M1 macrophages, M2 macrophages secrete an anti-inflammatory response via the addition of Interleukin-4 or Interleukin-13. They also play a role in wound healing and are needed for revascularization and reepithelialization. M2 macrophages are divided into four major types based on their roles: M2a, M2b, M2c, and M2d. How M2 phenotypes are determined is still up for discussion but studies have shown that their environment allows them to adjust to whichever phenotype is most appropriate to efficiently heal the wound.

M2 macrophages are needed for vascular stability. They produce vascular endothelial growth factor-A and TGF-β1. There is a phenotype shift from M1 to M2 macrophages in acute wounds, however this shift is impaired for chronic wounds. This dysregulation results in insufficient M2 macrophages and its corresponding growth factors that aid in wound repair. With a lack of these growth factors/anti-inflammatory cytokines and an overabundance of pro-inflammatory cytokines from M1 macrophages chronic wounds are unable to heal in a timely manner. Normally, after neutrophils eat debris/pathogens they perform apoptosis and are removed. At this point, inflammation is not needed and M1 undergoes a switch to M2 (anti-inflammatory). However, dysregulation occurs as the M1 macrophages are unable/do not phagocytose neutrophils that have undergone apoptosis leading to increased macrophage migration and inflammation.

Both M1 and M2 macrophages play a role in promotion of atherosclerosis. M1 macrophages promote atherosclerosis by inflammation. M2 macrophages can remove cholesterol from blood vessels, but when the cholesterol is oxidized, the M2 macrophages become apoptotic foam cells contributing to the atheromatous plaque of atherosclerosis.

Role in muscle regeneration
The first step to understanding the importance of macrophages in muscle repair, growth, and regeneration is that there are two "waves" of macrophages with the onset of damageable muscle use– subpopulations that do and do not directly have an influence on repairing muscle. The initial wave is a phagocytic population that comes along during periods of increased muscle use that are sufficient to cause muscle membrane lysis and membrane inflammation, which can enter and degrade the contents of injured muscle fibers. These early-invading, phagocytic macrophages reach their highest concentration about 24 hours following the onset of some form of muscle cell injury or reloading. Their concentration rapidly declines after 48 hours. The second group is the non-phagocytic types that are distributed near regenerative fibers. These peak between two and four days and remain elevated for several days during while muscle tissue is rebuilding. The first subpopulation has no direct benefit to repairing muscle, while the second non-phagocytic group does.

It is thought that macrophages release soluble substances that influence the proliferation, differentiation, growth, repair, and regeneration of muscle, but at this time the factor that is produced to mediate these effects is unknown. It is known that macrophages' involvement in promoting tissue repair is not muscle specific; they accumulate in numerous tissues during the healing process phase following injury.

Role in wound healing
Macrophages are essential for wound healing. They replace polymorphonuclear neutrophils as the predominant cells in the wound by day two after injury. Attracted to the wound site by growth factors released by platelets and other cells, monocytes from the bloodstream enter the area through blood vessel walls. Numbers of monocytes in the wound peak one to one and a half days after the injury occurs. Once they are in the wound site, monocytes mature into macrophages. The spleen contains half the body's monocytes in reserve ready to be deployed to injured tissue.

The macrophage's main role is to phagocytize bacteria and damaged tissue, and they also debride damaged tissue by releasing proteases. Macrophages also secrete a number of factors such as growth factors and other cytokines, especially during the third and fourth post-wound days. These factors attract cells involved in the proliferation stage of healing to the area. Macrophages may also restrain the contraction phase. Macrophages are stimulated by the low oxygen content of their surroundings to produce factors that induce and speed angiogenesis and they also stimulate cells that re-epithelialize the wound, create granulation tissue, and lay down a new extracellular matrix. By secreting these factors, macrophages contribute to pushing the wound healing process into the next phase.

Role in limb regeneration
Scientists have elucidated that as well as eating up material debris, macrophages are involved in the typical limb regeneration in the salamander. They found that removing the macrophages from a salamander resulted in failure of limb regeneration and a scarring response.

Role in iron homeostasis
As described above, macrophages play a key role in removing dying or dead cells and cellular debris. Erythrocytes have a lifespan on average of 120 days and so are constantly being destroyed by macrophages in the spleen and liver. Macrophages will also engulf macromolecules, and so play a key role in the pharmacokinetics of parenteral irons.

The iron that is released from the haemoglobin is either stored internally in ferritin or is released into the circulation via ferroportin. In cases where systemic iron levels are raised, or where inflammation is present, raised levels of hepcidin act on macrophage ferroportin channels, leading to iron remaining within the macrophages.

Role in pigment retainment
Melanophages are a subset of tissue-resident macrophages able to absorb pigment, either native to the organism or exogenous (such as tattoos), from extracellular space. In contrast to dendritic juncional melanocytes, which synthesize melanosomes and contain various stages of their development, the melanophages only accumulate phagocytosed melanin in lysosome-like phagosomes. This occurs repeatedly as the pigment from dead dermal macrophages is phagocytosed by their successors, preserving the tattoo in the same place.

Role in tissue homeostasis
Every tissue harbors its own specialized population of resident macrophages, which entertain reciprocal interconnections with the stroma and functional tissue. These resident macrophages are sessile (non-migratory), provide essential growth factors to support the physiological function of the tissue (e.g. macrophage-neuronal crosstalk in the guts), and can actively protect the tissue from inflammatory damage.

Nerve-associated macrophages
Nerve-associated macrophages or NAMs are those tissue-resident macrophages that are associated with nerves. Some of them are known to have an elongated morphology of up to 200μm

Clinical significance
Due to their role in phagocytosis, macrophages are involved in many diseases of the immune system. For example, they participate in the formation of granulomas, inflammatory lesions that may be caused by a large number of diseases. Some disorders, mostly rare, of ineffective phagocytosis and macrophage function have been described, for example.

As a host for intracellular pathogens
In their role as a phagocytic immune cell macrophages are responsible for engulfing pathogens to destroy them. Some pathogens subvert this process and instead live inside the macrophage. This provides an environment in which the pathogen is hidden from the immune system and allows it to replicate.

Diseases with this type of behaviour include tuberculosis (caused by Mycobacterium tuberculosis) and leishmaniasis (caused by Leishmania species).

In order to minimize the possibility of becoming the host of an intracellular bacteria, macrophages have evolved defense mechanisms such as induction of nitric oxide and reactive oxygen intermediates, which are toxic to microbes. Macrophages have also evolved the ability to restrict the microbe's nutrient supply and induce autophagy.

Tuberculosis
Once engulfed by a macrophage, the causative agent of tuberculosis, Mycobacterium tuberculosis, avoids cellular defenses and uses the cell to replicate. Recent evidence suggests that in response to the pulmonary infection of Mycobacterium tuberculosis, the peripheral macrophages matures into M1 phenotype. Macrophage M1 phenotype is characterized by increased secretion of pro-inflammatory cytokines (IL-1β, TNF-α, and IL-6) and increased glycolytic activities essential for clearance of infection.

Leishmaniasis
Upon phagocytosis by a macrophage, the Leishmania parasite finds itself in a phagocytic vacuole. Under normal circumstances, this phagocytic vacuole would develop into a lysosome and its contents would be digested. Leishmania alter this process and avoid being destroyed; instead, they make a home inside the vacuole.

Chikungunya
Infection of macrophages in joints is associated with local inflammation during and after the acute phase of Chikungunya (caused by CHIKV or Chikungunya virus).

Others
Adenovirus (most common cause of pink eye) can remain latent in a host macrophage, with continued viral shedding 6–18 months after initial infection.

Brucella spp. can remain latent in a macrophage via inhibition of phagosome–lysosome fusion; causes brucellosis (undulant fever).

Legionella pneumophila, the causative agent of Legionnaires' disease, also establishes residence within macrophages.

Heart disease
Macrophages are the predominant cells involved in creating the progressive plaque lesions of atherosclerosis.

Focal recruitment of macrophages occurs after the onset of acute myocardial infarction. These macrophages function to remove debris, apoptotic cells and to prepare for tissue regeneration. Macrophages protect against ischemia-induced ventricular tachycardia in hypokalemic mice.

HIV infection
Macrophages also play a role in human immunodeficiency virus (HIV) infection. Like T cells, macrophages can be infected with HIV, and even become a reservoir of ongoing virus replication throughout the body. HIV can enter the macrophage through binding of gp120 to CD4 and second membrane receptor, CCR5 (a chemokine receptor). Both circulating monocytes and macrophages serve as a reservoir for the virus. Macrophages are better able to resist infection by HIV-1 than CD4+ T cells, although susceptibility to HIV infection differs among macrophage subtypes.

Cancer
Macrophages can contribute to tumor growth and progression by promoting tumor cell proliferation and invasion, fostering tumor angiogenesis and suppressing antitumor immune cells. Inflammatory compounds, such as tumor necrosis factor (TNF)-alpha released by the macrophages activate the gene switch nuclear factor-kappa B. NF-κB then enters the nucleus of a tumor cell and turns on production of proteins that stop apoptosis and promote cell proliferation and inflammation. Moreover, macrophages serve as a source for many pro-angiogenic factors including vascular endothelial factor (VEGF), tumor necrosis factor-alpha (TNF-alpha), macrophage colony-stimulating factor (M-CSF/CSF1) and IL-1 and IL-6, contributing further to the tumor growth.

Macrophages have been shown to infiltrate a number of tumors. Their number correlates with poor prognosis in certain cancers, including cancers of breast, cervix, bladder, brain and prostate. Some tumors can also produce factors, including M-CSF/CSF1, MCP-1/CCL2 and Angiotensin II, that trigger the amplification and mobilization of macrophages in tumors. Additionally, subcapsular sinus macrophages in tumor-draining lymph nodes can suppress cancer progression by containing the spread of tumor-derived materials.

Cancer therapy
Experimental studies indicate that macrophages can affect all therapeutic modalities, including surgery, chemotherapy, radiotherapy, immunotherapy and targeted therapy. Macrophages can influence treatment outcomes both positively and negatively. Macrophages can be protective in different ways: they can remove dead tumor cells (in a process called phagocytosis) following treatments that kill these cells; they can serve as drug depots for some anticancer drugs; they can also be activated by some therapies to promote antitumor immunity. Macrophages can also be deleterious in several ways: for example they can suppress various chemotherapies, radiotherapies  and immunotherapies. Because macrophages can regulate tumor progression, therapeutic strategies to reduce the number of these cells, or to manipulate their phenotypes, are currently being tested in cancer patients. However, macrophages are also involved in antibody mediated cytotoxicity (ADCC) and this mechanism has been proposed to be important for certain cancer immunotherapy antibodies.

Obesity
It has been observed that increased number of pro-inflammatory macrophages within obese adipose tissue contributes to obesity complications including insulin resistance and diabetes type 2.

The modulation of the inflammatory state of adipose tissue macrophages has therefore been considered a possible therapeutic target to treat obesity-related diseases. Although adipose tissue macrophages are subject to anti-inflammatory homeostatic control by sympathetic innervation, experiments using ADRB2 gene knockout mice indicate that this effect is indirectly exerted through the modulation of adipocyte function, and not through direct Beta-2 adrenergic receptor activation, suggesting that adrenergic stimulation of macrophages may be insufficient to impact adipose tissue inflammation or function in obesity.

Within the fat (adipose) tissue of CCR2 deficient mice, there is an increased number of eosinophils, greater alternative macrophage activation, and a propensity towards type 2 cytokine expression. Furthermore, this effect was exaggerated when the mice became obese from a high fat diet. This is partially caused by a phenotype switch of macrophages induced by necrosis of fat cells (adipocytes). In an obese individual some adipocytes burst and undergo necrotic death, which causes the residential M2 macrophages to switch to M1 phenotype. This is one of the causes of a low-grade systemic chronic inflammatory state associated with obesity.

Intestinal macrophages
Though very similar in structure to tissue macrophages, intestinal macrophages have evolved specific characteristics and functions given their natural environment, which is in the digestive tract. Macrophages and intestinal macrophages have high plasticity causing their phenotype to be altered by their environments. Like macrophages, intestinal macrophages are differentiated monocytes, though intestinal macrophages have to coexist with the microbiome in the intestines. This is a challenge considering the bacteria found in the gut are not recognized as "self" and could be potential targets for phagocytosis by the macrophage.

To prevent the destruction of the gut bacteria, intestinal macrophages have developed key differences compared to other macrophages. Primarily, intestinal macrophages do not induce inflammatory responses. Whereas tissue macrophages release various inflammatory cytokines, such as IL-1, IL-6 and TNF-α, intestinal macrophages do not produce or secrete inflammatory cytokines. This change is directly caused by the intestinal macrophages environment. Surrounding intestinal epithelial cells release TGF-β, which induces the change from proinflammatory macrophage to noninflammatory macrophage.

Even though the inflammatory response is downregulated in intestinal macrophages, phagocytosis is still carried out. There is no drop off in phagocytosis efficiency as intestinal macrophages are able to effectively phagocytize the bacteria,S. typhimurium and E. coli, but intestinal macrophages still do not release cytokines, even after phagocytosis. Also, intestinal macrophages do not express lipopolysaccharide (LPS), IgA, or IgG receptors. The lack of LPS receptors is important for the gut as the intestinal macrophages do not detect the microbe-associated molecular patterns (MAMPS/PAMPS) of the intestinal microbiome. Nor do they express IL-2 and IL-3 growth factor receptors.

Role in disease
Intestinal macrophages have been shown to play a role in inflammatory bowel disease (IBD), such as Crohn's disease (CD) and ulcerative colitis (UC). In a healthy gut, intestinal macrophages limit the inflammatory response in the gut, but in a disease-state, intestinal macrophage numbers and diversity are altered. This leads to inflammation of the gut and disease symptoms of IBD. Intestinal macrophages are critical in maintaining gut homeostasis. The presence of inflammation or pathogen alters this homeostasis, and concurrently alters the intestinal macrophages. There has yet to be a determined mechanism for the alteration of the intestinal macrophages by recruitment of new monocytes or changes in the already present intestinal macrophages.

Additionally, a new study reveals macrophages limit iron access to bacteria by releasing extracellular vesicles, improving sepsis outcomes.

History
Macrophages were first discovered late in the 19th century by Élie Metchnikoff. Élie Metchnikoff revolutionized the branch of macrophages by combining philosophical insights and the evolutionary study of life. Later on, Van Furth during the 1960s proposed the idea that circulating blood monocytes in adults allowed for the origin of all tissue macrophages. In recent years, publishing regarding macrophages has led people to believe that multiple resident tissue macrophages are independent of the blood monocytes as it is formed during the embryonic stage of development. Within the 21st century, all the ideas concerning the origin of macrophages (present in tissues) are compiled together to suggest that physiologically complex organisms, form macrophages independently by mechanisms that don't have to depend on the blood monocytes.

title: Macrophage