text:
Natural deduction

In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use axioms as much as possible to express the logical laws of deductive reasoning.

History
Natural deduction grew out of a context of dissatisfaction with the axiomatizations of deductive reasoning common to the systems of Hilbert, Frege, and Russell (see, e.g., Hilbert system). Such axiomatizations were most famously used by Russell and Whitehead in their mathematical treatise Principia Mathematica. Spurred on by a series of seminars in Poland in 1926 by Łukasiewicz that advocated a more natural treatment of logic, Jaśkowski made the earliest attempts at defining a more natural deduction, first in 1929 using a diagrammatic notation, and later updating his proposal in a sequence of papers in 1934 and 1935. His proposals led to different notations such as Fitch-style calculus (or Fitch's diagrams) or Suppes' method for which Lemmon gave a variant now known as Suppes–Lemmon notation.

Natural deduction in its modern form was independently proposed by the German mathematician Gerhard Gentzen in 1933, in a dissertation delivered to the faculty of mathematical sciences of the University of Göttingen. The term natural deduction (or rather, its German equivalent natürliches Schließen) was coined in that paper:

Gentzen was motivated by a desire to establish the consistency of number theory. He was unable to prove the main result required for the consistency result, the cut elimination theorem—the Hauptsatz—directly for natural deduction. For this reason he introduced his alternative system, the sequent calculus, for which he proved the Hauptsatz both for classical and intuitionistic logic. In a series of seminars in 1961 and 1962 Prawitz gave a comprehensive summary of natural deduction calculi, and transported much of Gentzen's work with sequent calculi into the natural deduction framework. His 1965 monograph Natural deduction: a proof-theoretical study was to become a reference work on natural deduction, and included applications for modal and second-order logic.

In natural deduction, a proposition is deduced from a collection of premises by applying inference rules repeatedly. The system presented in this article is a minor variation of Gentzen's or Prawitz's formulation, but with a closer adherence to Martin-Löf's description of logical judgments and connectives.

History of notation styles
Natural deduction has had a large variety of notation styles, which can make it difficult to recognize a proof if you're not familiar with one of them. To help with this situation, this article has a section explaining how to read all the notation that it will actually use. This section just explains the historical evolution of notation styles, most of which cannot be shown because there are no illustrations available under a public copyright license – the reader is pointed to the SEP and IEP for pictures.
 * Gentzen invented natural deduction using tree-shaped proofs – see for details.
 * Jaśkowski changed this to a notation that used various nested boxes.
 * Fitch changed Jaśkowski method of drawing the boxes, creating Fitch notation.
 * 1940: In a textbook, Quine indicated antecedent dependencies by line numbers in square brackets, anticipating Suppes' 1957 line-number notation.
 * 1950: In a textbook, demonstrated a method of using one or more asterisks to the left of each line of proof to indicate dependencies. This is equivalent to Kleene's vertical bars. (It is not totally clear if Quine's asterisk notation appeared in the original 1950 edition or was added in a later edition.)
 * 1957: An introduction to practical logic theorem proving in a textbook by . This indicated dependencies (i.e. antecedent propositions) by line numbers at the left of each line.
 * 1963: uses sets of line numbers to indicate antecedent dependencies of the lines of sequential logical arguments based on natural deduction inference rules.
 * 1965: The entire textbook by is an introduction to logic proofs using a method based on that of Suppes, what is now known as Suppes–Lemmon notation.
 * 1967: In a textbook, briefly demonstrated two kinds of practical logic proofs, one system using explicit quotations of antecedent propositions on the left of each line, the other system using vertical bar-lines on the left to indicate dependencies.

Notation
The reader should be familiar with common symbols for logical connectives. Here is a table with the most common notational variants.

Gentzen's tree notation
Gentzen, who invented natural deduction, had his own notation style for arguments. This will be exemplified by a simple argument below. Let's say we have a simple example argument in propositional logic, such as, "if it's raining then it's cloudly; it is raining; therefore it's cloudy". (This is in modus ponens.) Representing this as a list of propositions, as is common, we would have:

 * $$1) ~ P \to Q$$
 * $$2) ~ P$$
 * $$\therefore ~ Q$$

In Gentzen's notation, this would be written like this:

 * $$\frac{P \to Q, P}{Q}$$

The premises are shown above a line, called the inference line, separated by a comma, which indicates combination of premises. The conclusion is written below the inference line. The inference line represents syntactic consequence, sometimes called deductive consequence, which is also symbolized with ⊢. So the above can also be written in one line as $$P \to Q, P \vdash Q$$. (The turnstile, for syntactic consequence, is of lower precedence than the comma, which represents premise combination, which in turn is of lower precedence than the arrow, used for material implication; so no parentheses are needed to interpret this formula.)

Syntactic consequence is contrasted with semantic consequence, which is symbolized with ⊧. In this case, the conclusion follows syntactically because natural deduction is a syntactic proof system, which assumes inference rules as primitives.

Gentzen's style will be used in much of this article. Gentzen's discharging annotations used to internalise hypothetical judgments can be avoided by representing proofs as a tree of sequents Γ ⊢A instead of a tree of judgments that A (is true).

Suppes–Lemmon notation
Many textbooks use Suppes–Lemmon notation, so this article will also give that – although as of now, this is only included for propositional logic, and the rest of the coverage is given only in Gentzen style. A proof, laid out in accordance with the Suppes–Lemmon notation style, is a sequence of lines containing sentences, where each sentence is either an assumption, or the result of applying a rule of proof to earlier sentences in the sequence. Each line of proof is made up of a sentence of proof, together with its annotation, its assumption set, and the current line number. The assumption set lists the assumptions on which the given sentence of proof depends, which are referenced by the line numbers. The annotation specifies which rule of proof was applied, and to which earlier lines, to yield the current sentence. Here's an example proof: This proof will become clearer when the inference rules and their appropriate annotations are specified – see.

Propositional language syntax
This section defines the formal syntax for a propositional logic language, contrasting the common ways of doing so with a Gentzen-style way of doing so.

Common definition styles
The formal language $$\mathcal{L}$$ of a propositional calculus is usually defined by a recursive definition, such as this one, from Bostock:

There are other ways of doing it, such as the BNF grammar $$\phi ::= a_1, a_2, \ldots ~ | ~  \neg\phi  ~ | ~  \phi ~ \& ~ \psi  ~ | ~  \phi \vee \psi  ~ | ~  \phi \rightarrow \psi  ~ | ~  \phi \leftrightarrow \psi$$.
 * 1) Each sentence-letter is a formula.
 * 2) "$$\top$$" and "$$\bot$$" are formulae.
 * 3) If $$\varphi$$ is a formula, so is $$\neg\varphi$$.
 * 4) If $$\varphi$$ and $$\psi$$ are formulae, so are $$(\varphi \land \psi)$$, $$(\varphi \lor \psi)$$, $$(\varphi \to \psi)$$, $$(\varphi \leftrightarrow \psi)$$.
 * 5) Nothing else is a formula.

Gentzen-style definition
A syntax definition can also be given using, by writing well-formed formulas below the inference line and any schematic variables used by those formulas above it. For instance, the equivalent of rules 3 and 4, from Bostock's definition above, is written as follows:

 * $$\frac{\varphi}{(\neg \varphi)} \quad \frac{\varphi \quad \psi}{(\varphi \lor \psi)} \quad \frac{\varphi \quad \psi}{(\varphi \land \psi)} \quad \frac{\varphi \quad \psi}{(\varphi \rightarrow \psi)} \quad \frac{\varphi \quad \psi}{(\varphi \leftrightarrow \psi)}$$.

A different notational convention sees the language's syntax as a categorial grammar with the single category "formula", denoted by the symbol $$\mathcal{F}$$. So any elements of the syntax are introduced by categorizations, for which the notation is $$\varphi : \mathcal{F}$$, meaning "$$\varphi$$ is an expression for an object in the category $$\mathcal{F}$$." The sentence-letters, then, are introduced by categorizations such as $$P : \mathcal{F}$$, $$Q : \mathcal{F}$$, $$R : \mathcal{F}$$, and so on; the connectives, in turn, are defined by statements similar to the above, but using categorization notation, as seen below: In the rest of this article, the $$\varphi : \mathcal{F}$$ categorization notation will be used for any Gentzen-notation statements defining the language's grammar; any other statements in Gentzen notation will be inferences, asserting that a sequent follows rather than that an expression is a well-formed formula.

Gentzen-style inference rules
The following is a complete list of primitive inference rules for natural deduction in classical propositional logic:

This table follows the custom of using Greek letters as schemata, which may range over any formulas, rather than only over atomic propositions. The name of a rule is given to the right of its formula tree. For instance, the first introduction rule is named $$\wedge_i$$, which is short for "conjunction introduction".

Gentzen-style example proofs
As an example of the use of inference rules, consider commutativity of conjunction. If A ∧ B, then B ∧ A; this derivation can be drawn by composing inference rules in such a fashion that premises of a lower inference match the conclusion of the next higher inference.

$$ \cfrac{\cfrac{A \wedge B}{B\hbox{ }}\ \wedge_{E2} \qquad \cfrac{A \wedge B}{A}\ \wedge_{E1}} {B \wedge A}\ \wedge_I $$

As a second example, consider the derivation of "A ⊃ (B ⊃ (A ∧ B))": $$ \cfrac{\cfrac{\cfrac{}{A}\ u \quad \cfrac{}{B}\ w}{A \wedge B}\ \wedge_I}{ \cfrac{B \supset \left ( A \wedge B \right )}{ A \supset \left ( B \supset \left ( A \wedge B \right ) \right ) }\ \supset_{I^u} }\ \supset_{I^w} $$ This full derivation has no unsatisfied premises; however, sub-derivations are hypothetical. For instance, the derivation of "B ⊃ (A ∧ B)" is hypothetical with antecedent "A" (named u).

Suppes–Lemmon-style inference rules
Natural deduction inference rules, due ultimately to Gentzen, are given below. There are ten primitive rules of proof, which are the rule assumption, plus four pairs of introduction and elimination rules for the binary connectives, and the rule reductio ad adbsurdum. Disjunctive Syllogism can be used as an easier alternative to the proper ∨-elimination, and MTT and DN are commonly given rules, although they are not primitive.

Suppes–Lemmon-style example proof
Recall that an example proof was already given when introducing. This is a second example.

Consistency, completeness, and normal forms
A theory is said to be consistent if falsehood is not provable (from no assumptions) and is complete if every theorem or its negation is provable using the inference rules of the logic. These are statements about the entire logic, and are usually tied to some notion of a model. However, there are local notions of consistency and completeness that are purely syntactic checks on the inference rules, and require no appeals to models. The first of these is local consistency, also known as local reducibility, which says that any derivation containing an introduction of a connective followed immediately by its elimination can be turned into an equivalent derivation without this detour. It is a check on the strength of elimination rules: they must not be so strong that they include knowledge not already contained in their premises. As an example, consider conjunctions.
 * $$\begin{aligned}\cfrac{\cfrac{\cfrac{}{A\ }u\qquad\cfrac{}{B\ }w}{A \wedge B\ }\wedge_I}{A\ }\wedge_{E1}\end{aligned}\quad\Rightarrow\quad\cfrac{}{A\ }u$$

Dually, local completeness says that the elimination rules are strong enough to decompose a connective into the forms suitable for its introduction rule. Again for conjunctions:
 * $$\cfrac{}{A \wedge B\ }u \quad \Rightarrow \quad \begin{aligned}\cfrac{\cfrac{\cfrac{}{A \wedge B\ }u}{A\ }\wedge_{E1} \qquad \cfrac{\cfrac{}{A \wedge B\ }u}{B\ }\wedge_{E2}}{A \wedge B\ }\wedge_I\end{aligned}$$

These notions correspond exactly to β-reduction (beta reduction) and η-conversion (eta conversion) in the lambda calculus, using the Curry–Howard isomorphism. By local completeness, we see that every derivation can be converted to an equivalent derivation where the principal connective is introduced. In fact, if the entire derivation obeys this ordering of eliminations followed by introductions, then it is said to be normal. In a normal derivation all eliminations happen above introductions. In most logics, every derivation has an equivalent normal derivation, called a normal form. The existence of normal forms is generally hard to prove using natural deduction alone, though such accounts do exist in the literature, most notably by Dag Prawitz in 1961. It is much easier to show this indirectly by means of a cut-free sequent calculus presentation.

First and higher-order extensions

The logic of the earlier section is an example of a single-sorted logic, i.e., a logic with a single kind of object: propositions. Many extensions of this simple framework have been proposed; in this section we will extend it with a second sort of individuals or terms. More precisely, we will add a new category, "term", denoted $$\mathcal{T}$$. We shall fix a countable set $$V$$ of variables, another countable set $$F$$ of function symbols, and construct terms with the following formation rules:

\frac{v\in V}{v : \mathcal{T}} \hbox{ var}_F $$

and

\frac{f\in F\qquad t_1 : \mathcal{T}\qquad  t_2 : \mathcal{T}\qquad \cdots \qquad t_n : \mathcal{T}}{f(t_1, t_2,\cdots,t_n) : \mathcal{T}} \hbox{ app}_F $$

For propositions, we consider a third countable set P of predicates, and define atomic predicates over terms with the following formation rule:

\frac{\phi\in P\qquad t_1 : \mathcal{T}\qquad  t_2 : \mathcal{T}\qquad \cdots \qquad t_n : \mathcal{T}}{\phi(t_1, t_2,\cdots,t_n) : \mathcal{F}} \hbox{ pred}_F $$

The first two rules of formation provide a definition of a term that is effectively the same as that defined in term algebra and model theory, although the focus of those fields of study is quite different from natural deduction. The third rule of formation effectively defines an atomic formula, as in first-order logic, and again in model theory.

To these are added a pair of formation rules, defining the notation for quantified propositions; one for universal (∀) and existential (∃) quantification:

\frac{x\in V \qquad A : \mathcal{F}}{\forall x.A : \mathcal{F}} \;\forall_F \qquad\qquad \frac{x\in V \qquad A : \mathcal{F}}{\exists x.A : \mathcal{F}} \;\exists_F $$

The universal quantifier has the introduction and elimination rules:

\cfrac{ \begin{array}{c} \cfrac{}{a : \mathcal{T}}\text{ u} \\ \vdots \\{}[a/x]A \end{array} }{\forall x.A }\;\forall_{I^{u,a}} \qquad \qquad \frac{\forall x.A \qquad t : \mathcal{T}}{[t/x]A}\;\forall_{E} $$

The existential quantifier has the introduction and elimination rules:

\frac{[t/x]A }{\exists x.A}\;\exists_{I} \qquad\qquad \cfrac{ \begin{array}{cc} & \underbrace{\,\cfrac{}{a : \mathcal{T}}\hbox{ u} \quad \cfrac{}{[a/x]A }\hbox{ v}\,}\\ & \vdots \\ \exists x.A \quad & C \\ \end{array} } {C }\exists_{E^{a,u,v}} $$

In these rules, the notation [t/x] A stands for the substitution of t for every (visible) instance of x in A, avoiding capture. As before the superscripts on the name stand for the components that are discharged: the term a cannot occur in the conclusion of ∀I (such terms are known as eigenvariables or parameters), and the hypotheses named u and v in ∃E are localised to the second premise in a hypothetical derivation. Although the propositional logic of earlier sections was decidable, adding the quantifiers makes the logic undecidable.

So far, the quantified extensions are first-order: they distinguish propositions from the kinds of objects quantified over. Higher-order logic takes a different approach and has only a single sort of propositions. The quantifiers have as the domain of quantification the very same sort of propositions, as reflected in the formation rules:

\cfrac{ \begin{matrix} \cfrac{}{p : \mathcal{F}}\hbox{ u} \\ \vdots \\ A: \mathcal{F} \\ \end{matrix}} {\forall p.A : \mathcal{F}} \;\forall_{F^u} \qquad\qquad

\cfrac{ \begin{matrix} \cfrac{}{p : \mathcal{F}}\hbox{ u} \\ \vdots \\ A: \mathcal{F} \\ \end{matrix}} {\exists p.A : \mathcal{F}} \;\exists_{F^u} $$

A discussion of the introduction and elimination forms for higher-order logic is beyond the scope of this article. It is possible to be in-between first-order and higher-order logics. For example, second-order logic has two kinds of propositions, one kind quantifying over terms, and the second kind quantifying over propositions of the first kind.

Proofs and type theory
The presentation of natural deduction so far has concentrated on the nature of propositions without giving a formal definition of a proof. To formalise the notion of proof, we alter the presentation of hypothetical derivations slightly. We label the antecedents with proof variables (from some countable set V of variables), and decorate the succedent with the actual proof. The antecedents or hypotheses are separated from the succedent by means of a turnstile (⊢). This modification sometimes goes under the name of localised hypotheses. The following diagram summarises the change. The collection of hypotheses will be written as Γ when their exact composition is not relevant. To make proofs explicit, we move from the proof-less judgment "A" to a judgment: "π is a proof of (A)", which is written symbolically as "π : A". Following the standard approach, proofs are specified with their own formation rules for the judgment "π proof". The simplest possible proof is the use of a labelled hypothesis; in this case the evidence is the label itself. Let us re-examine some of the connectives with explicit proofs. For conjunction, we look at the introduction rule ∧I to discover the form of proofs of conjunction: they must be a pair of proofs of the two conjuncts. Thus: The elimination rules ∧E1 and ∧E2 select either the left or the right conjunct; thus the proofs are a pair of projections—first (fst) and second (snd). For implication, the introduction form localises or binds the hypothesis, written using a λ; this corresponds to the discharged label. In the rule, "Γ, u:A" stands for the collection of hypotheses Γ, together with the additional hypothesis u. With proofs available explicitly, one can manipulate and reason about proofs. The key operation on proofs is the substitution of one proof for an assumption used in another proof. This is commonly known as a substitution theorem, and can be proved by induction on the depth (or structure) of the second judgment.

Substitution theorem

 * If Γ ⊢ π1 : A and Γ, u:A ⊢ π2 : B, then Γ ⊢ [π1/u] π2 : B.

So far the judgment "Γ ⊢ π : A" has had a purely logical interpretation. In type theory, the logical view is exchanged for a more computational view of objects. Propositions in the logical interpretation are now viewed as types, and proofs as programs in the lambda calculus. Thus the interpretation of "π : A" is "the program π has type A". The logical connectives are also given a different reading: conjunction is viewed as product (×), implication as the function arrow (→), etc. The differences are only cosmetic, however. Type theory has a natural deduction presentation in terms of formation, introduction and elimination rules; in fact, the reader can easily reconstruct what is known as simple type theory from the previous sections.

The difference between logic and type theory is primarily a shift of focus from the types (propositions) to the programs (proofs). Type theory is chiefly interested in the convertibility or reducibility of programs. For every type, there are canonical programs of that type which are irreducible; these are known as canonical forms or values. If every program can be reduced to a canonical form, then the type theory is said to be normalising (or weakly normalising). If the canonical form is unique, then the theory is said to be strongly normalising. Normalisability is a rare feature of most non-trivial type theories, which is a big departure from the logical world. (Recall that almost every logical derivation has an equivalent normal derivation.) To sketch the reason: in type theories that admit recursive definitions, it is possible to write programs that never reduce to a value; such looping programs can generally be given any type. In particular, the looping program has type ⊥, although there is no logical proof of "⊥". For this reason, the propositions as types; proofs as programs paradigm only works in one direction, if at all: interpreting a type theory as a logic generally gives an inconsistent logic.

Example: Dependent Type Theory
Like logic, type theory has many extensions and variants, including first-order and higher-order versions. One branch, known as dependent type theory, is used in a number of computer-assisted proof systems. Dependent type theory allows quantifiers to range over programs themselves. These quantified types are written as Π and Σ instead of ∀ and ∃, and have the following formation rules: These types are generalisations of the arrow and product types, respectively, as witnessed by their introduction and elimination rules. Dependent type theory in full generality is very powerful: it is able to express almost any conceivable property of programs directly in the types of the program. This generality comes at a steep price — either typechecking is undecidable (extensional type theory), or extensional reasoning is more difficult (intensional type theory). For this reason, some dependent type theories do not allow quantification over arbitrary programs, but rather restrict to programs of a given decidable index domain, for example integers, strings, or linear programs.

Since dependent type theories allow types to depend on programs, a natural question to ask is whether it is possible for programs to depend on types, or any other combination. There are many kinds of answers to such questions. A popular approach in type theory is to allow programs to be quantified over types, also known as parametric polymorphism; of this there are two main kinds: if types and programs are kept separate, then one obtains a somewhat more well-behaved system called predicative polymorphism; if the distinction between program and type is blurred, one obtains the type-theoretic analogue of higher-order logic, also known as impredicative polymorphism. Various combinations of dependency and polymorphism have been considered in the literature, the most famous being the lambda cube of Henk Barendregt.

The intersection of logic and type theory is a vast and active research area. New logics are usually formalised in a general type theoretic setting, known as a logical framework. Popular modern logical frameworks such as the calculus of constructions and LF are based on higher-order dependent type theory, with various trade-offs in terms of decidability and expressive power. These logical frameworks are themselves always specified as natural deduction systems, which is a testament to the versatility of the natural deduction approach.

Classical and modal logics
For simplicity, the logics presented so far have been intuitionistic. Classical logic extends intuitionistic logic with an additional axiom or principle of excluded middle:

 * For any proposition p, the proposition p ∨ ¬p is true.

This statement is not obviously either an introduction or an elimination; indeed, it involves two distinct connectives. Gentzen's original treatment of excluded middle prescribed one of the following three (equivalent) formulations, which were already present in analogous forms in the systems of Hilbert and Heyting:

(XM3 is merely XM2 expressed in terms of E.) This treatment of excluded middle, in addition to being objectionable from a purist's standpoint, introduces additional complications in the definition of normal forms.

A comparatively more satisfactory treatment of classical natural deduction in terms of introduction and elimination rules alone was first proposed by Parigot in 1992 in the form of a classical lambda calculus called λμ. The key insight of his approach was to replace a truth-centric judgment A with a more classical notion, reminiscent of the sequent calculus: in localised form, instead of Γ ⊢ A, he used Γ ⊢ Δ, with Δ a collection of propositions similar to Γ. Γ was treated as a conjunction, and Δ as a disjunction. This structure is essentially lifted directly from classical sequent calculi, but the innovation in λμ was to give a computational meaning to classical natural deduction proofs in terms of a callcc or a throw/catch mechanism seen in LISP and its descendants. (See also: first class control.)

Another important extension was for modal and other logics that need more than just the basic judgment of truth. These were first described, for the alethic modal logics S4 and S5, in a natural deduction style by Prawitz in 1965, and have since accumulated a large body of related work. To give a simple example, the modal logic S4 requires one new judgment, "A valid", that is categorical with respect to truth:

 * If "A" (is true) under no assumption that "B" (is true), then "A valid".

This categorical judgment is internalised as a unary connective ◻A (read "necessarily A") with the following introduction and elimination rules:

Note that the premise "A valid" has no defining rules; instead, the categorical definition of validity is used in its place. This mode becomes clearer in the localised form when the hypotheses are explicit. We write "Ω;Γ ⊢ A" where Γ contains the true hypotheses as before, and Ω contains valid hypotheses. On the right there is just a single judgment "A"; validity is not needed here since "Ω ⊢ A valid" is by definition the same as "Ω;⋅ ⊢ A". The introduction and elimination forms are then:

The modal hypotheses have their own version of the hypothesis rule and substitution theorem.

Modal substitution theorem

 * : If Ω;⋅ ⊢ π1 : A and Ω, u: (A valid) ; Γ ⊢ π2 : C, then Ω;Γ ⊢ [π1/u] π2 : C.

This framework of separating judgments into distinct collections of hypotheses, also known as multi-zoned or polyadic contexts, is very powerful and extensible; it has been applied for many different modal logics, and also for linear and other substructural logics, to give a few examples. However, relatively few systems of modal logic can be formalised directly in natural deduction. To give proof-theoretic characterisations of these systems, extensions such as labelling or systems of deep inference.

The addition of labels to formulae permits much finer control of the conditions under which rules apply, allowing the more flexible techniques of analytic tableaux to be applied, as has been done in the case of labelled deduction. Labels also allow the naming of worlds in Kripke semantics; presents an influential technique for converting frame conditions of modal logics in Kripke semantics into inference rules in a natural deduction formalisation of hybrid logic. surveys the application of many proof theories, such as Avron and Pottinger's hypersequents and Belnap's display logic to such modal logics as S5 and B.

Comparison with sequent calculus
The sequent calculus is the chief alternative to natural deduction as a foundation of mathematical logic. In natural deduction the flow of information is bi-directional: elimination rules flow information downwards by deconstruction, and introduction rules flow information upwards by assembly. Thus, a natural deduction proof does not have a purely bottom-up or top-down reading, making it unsuitable for automation in proof search. To address this fact, Gentzen in 1935 proposed his sequent calculus, though he initially intended it as a technical device for clarifying the consistency of predicate logic. Kleene, in his seminal 1952 book Introduction to Metamathematics, gave the first formulation of the sequent calculus in the modern style.

In the sequent calculus all inference rules have a purely bottom-up reading. Inference rules can apply to elements on both sides of the turnstile. (To differentiate from natural deduction, this article uses a double arrow ⇒ instead of the right tack ⊢ for sequents.) The introduction rules of natural deduction are viewed as right rules in the sequent calculus, and are structurally very similar. The elimination rules on the other hand turn into left rules in the sequent calculus. To give an example, consider disjunction; the right rules are familiar: On the left: Recall the ∨E rule of natural deduction in localised form: The proposition A ∨ B, which is the succedent of a premise in ∨E, turns into a hypothesis of the conclusion in the left rule ∨L. Thus, left rules can be seen as a sort of inverted elimination rule. This observation can be illustrated as follows: In the sequent calculus, the left and right rules are performed in lock-step until one reaches the initial sequent, which corresponds to the meeting point of elimination and introduction rules in natural deduction. These initial rules are superficially similar to the hypothesis rule of natural deduction, but in the sequent calculus they describe a transposition or a handshake of a left and a right proposition: The correspondence between the sequent calculus and natural deduction is a pair of soundness and completeness theorems, which are both provable by means of an inductive argument.

 * Soundness of ⇒ wrt. ⊢ : If Γ ⇒ A, then Γ ⊢ A.
 * Completeness of ⇒ wrt. ⊢ : If Γ ⊢ A, then Γ ⇒ A.

It is clear by these theorems that the sequent calculus does not change the notion of truth, because the same collection of propositions remain true. Thus, one can use the same proof objects as before in sequent calculus derivations. As an example, consider the conjunctions. The right rule is virtually identical to the introduction rule The left rule, however, performs some additional substitutions that are not performed in the corresponding elimination rules.

The kinds of proofs generated in the sequent calculus are therefore rather different from those of natural deduction. The sequent calculus produces proofs in what is known as the β-normal η-long form, which corresponds to a canonical representation of the normal form of the natural deduction proof. If one attempts to describe these proofs using natural deduction itself, one obtains what is called the intercalation calculus (first described by John Byrnes), which can be used to formally define the notion of a normal form for natural deduction.

The substitution theorem of natural deduction takes the form of a structural rule or structural theorem known as cut in the sequent calculus.

Cut (substitution)

 * If Γ ⇒ π1 : A and Γ, u:A ⇒ π2 : C, then Γ ⇒ [π1/u] π2 : C.

In most well behaved logics, cut is unnecessary as an inference rule, though it remains provable as a meta-theorem; the superfluousness of the cut rule is usually presented as a computational process, known as cut elimination. This has an interesting application for natural deduction; usually it is extremely tedious to prove certain properties directly in natural deduction because of an unbounded number of cases. For example, consider showing that a given proposition is not provable in natural deduction. A simple inductive argument fails because of rules like ∨E or E which can introduce arbitrary propositions. However, we know that the sequent calculus is complete with respect to natural deduction, so it is enough to show this unprovability in the sequent calculus. Now, if cut is not available as an inference rule, then all sequent rules either introduce a connective on the right or the left, so the depth of a sequent derivation is fully bounded by the connectives in the final conclusion. Thus, showing unprovability is much easier, because there are only a finite number of cases to consider, and each case is composed entirely of sub-propositions of the conclusion. A simple instance of this is the global consistency theorem: "⋅ ⊢ ⊥" is not provable. In the sequent calculus version, this is manifestly true because there is no rule that can have "⋅ ⇒ ⊥" as a conclusion! Proof theorists often prefer to work on cut-free sequent calculus formulations because of such properties.

General references

 * (English translation Investigations into Logical Deduction in M. E. Szabo. The Collected Works of Gerhard Gentzen. North-Holland Publishing Company, 1969.)
 * Translated and with appendices by Paul Taylor and Yves Lafont.
 * Reprinted in Polish logic 1920–39, ed. Storrs McCall.
 * Lecture notes to a short course at Università degli Studi di Siena, April 1983.
 * PhD thesis.
 * MSc thesis.
 * Lecture notes to a short course at Università degli Studi di Siena, April 1983.
 * PhD thesis.
 * MSc thesis.
 * Lecture notes to a short course at Università degli Studi di Siena, April 1983.
 * PhD thesis.
 * MSc thesis.
 * PhD thesis.
 * MSc thesis.
 * PhD thesis.
 * MSc thesis.
 * PhD thesis.
 * MSc thesis.
 * MSc thesis.

title: Natural deduction


text:
Peter Kropotkin

Pyotr Alexeyevich Kropotkin (9 December 1842 – 8 February 1921) was a Russian anarchist and geographer known as a proponent of anarchist communism.

Born into an aristocratic land-owning family, Kropotkin attended Page Corps and later served as an officer in Siberia, where he participated in several geological expeditions. He was imprisoned for his activism in 1874 and managed to escape two years later. He spent the next 41 years in exile in Switzerland, France (where he was imprisoned for almost four years) and England. While in exile, he gave lectures and published widely on anarchism and geography. Kropotkin returned to Russia after the Russian Revolution in 1917, but he was disappointed by the Bolshevik state.

Kropotkin was a proponent of a decentralized communist society free from central government and based on voluntary associations of self-governing communities and worker-run enterprises. He wrote many books, pamphlets and articles, the most prominent being The Conquest of Bread and Fields, Factories, and Workshops, with Mutual Aid: A Factor of Evolution being his principal scientific offering. He contributed the article on anarchism to the Encyclopædia Britannica Eleventh Edition and left an unfinished work on anarchist ethical philosophy.

Early life
Kropotkin was born in Moscow on 9 December 1842, in the Konyushennaya ("Equerries") district. His father, Alexander, was a typical royal officer who owned serfs in three provinces and whose family descended from the Grand Princes of Smolensk. His mother, Ekatarina Sulima, was the daughter of General Nikolai Sulima and a descendant of a Zaporozhian Cossacks leader. Peter, the youngest of her four children, was three years old when she died of tuberculosis. Kropotkin's father remarried two years later. This stepmother was indifferent towards the Kropotkin children and had a streak of jealous vindictiveness, going through great lengths to remove the memory of Kropotkin's mother.

With his father mostly absent, Kropotkin and his older brother, Alexander, were raised by their German nurse. Kropotkin developed an enduring compassion for the estate's servants and serfs who cared for him and relayed stories of his mother's kindness. He was raised in the family's Moscow mansion and an estate in Nikolskoye, Kaluga Oblast, outside Moscow.

At the age of eight, Kropotkin attended Tsar Nicholas I's Royal Ball. Commending the child's costume, the tsar chose Kropotkin for his Page Corps, an elite school in St. Petersburg that combined military and court education and produced the tsar's imperial attendants. Kropotkin joined the Page Corps as a teenager and began a 14-year epistolary relationship with his brother that charts his intellectual and emotional development. By the time of his arrival, Kropotkin had already shown a populist position towards the emancipation of serfs and a nature of revolt against his father and the school's hazing. Kropotkin began his first underground revolutionary writings at the school, where he advocated for a Russian constitution. He developed an interest in science, reading, and opera. As a top student, Kropotkin became a sergeant-major in 1861 and was thrust into court life, serving as the emperor's personal Page de Chambre. His views of the tsar and court life soured as imperial policy changed over the next year. Privately he was preoccupied with the need to live a societally useful life.

Siberia
For his tour of service, in 1862 he chose the Amur Cossacks in east Siberia, an undesirable post that would let him study the technical mathematics of artillery, travel, life in nature and financial independence from his father. He developed a firm worldview of compassion for the poor and contrasted the pride and dignity of the yeoman peasant farmers against the indignities of serfdom. He wrote approvingly of the cultivated Transbaikalia governor-general Boleslav Kukel, to whom Kropotkin reported. Kukel engaged Kropotkin in prison reform and city self-governance projects that the central government ultimately denied. The exiled poet and political prisoner Mikhail Larionovitch Mikhailov introduced Kropotkin to anarchism by recommending he read an essay by Pierre-Joseph Proudhon. Kropotkin's brother came to live with him in Irkutsk.

After Kukel's ouster in early 1863, Kropotkin found solace in geographical work. He led a disguised reconnaissance expedition to find a direct route through Manchuria from Chita to Vladivostok the next year. He explored the East Siberian Mountains in the north the year after. The mountain measurements from his 1866 Olekminsk-Vitimsk expedition confirmed his Manchurian hypothesis that the Siberian area from the Ural Mountains to the Pacific Ocean was a plateau and not a plain. This discovery of the Patom and Vitim Plateaus won him a gold medal from the Russian Geographical Society and led to the commercialization of the Lena gold fields. A range of mountains in this region was later named for him.

Kropotkin covered Siberia for St. Petersburg newspapers since his arrival, including the condition of the Polish political exiles who participated in the unsuccessful 1866 Baikal Insurrection. Kropotkin secured a promise from the governor-general to suspend the prisoners' death sentences, which was reneged. Disillusioned, Kropotkin and his brother resolved to leave the military. His time in Siberia taught him to appreciate peasant social organization and convinced him that administrative reform was an ineffectual means to improve social conditions.

After five years in Siberia, Kropotkin and his brother moved to St. Petersburg, where they continued their schooling and academic work. Kropotkin took a position with the Russian interior ministry with no duties. He studied physics, math, and geography at the university. After presenting his Vitim expedition findings, Kropotkin accepted the Russian Geographical Society's part-time offer of its Physical Geography section Secretaryship. Kropotkin translated Herbert Spencer for additional income. He continued to develop a theory, which he considered his best scientific contribution, that the East Siberian mountains were part of a large plateau and not independent ridges. Kropotkin participated in an 1870 polar expedition plan that postulated the existence of what was later discovered as the Franz Josef Land Arctic archipelago.

In early 1871, he was commissioned to study the Ice Age in Scandinavian geography, in which Kropotkin developed theories of the glaciation of Europe and the glacial lakes of its northeast. His father died later that year and Kropotkin inherited a wealthy estate in Tambov. Kropotkin turned down the Geographical Society's offer of its general secretary position, instead choosing work on his Ice Age data and interest in bettering the lives of peasants.

Anarchism

While Kropotkin became increasingly revolutionary in his writings, he was not known for activism. He was spurred by the 1871 Paris Commune and trial of Sergey Nechayev. He and his brother attended meetings on the Franco-Prussian War and revolutionism. Likely at the encouragement of a Swiss extended family member and his own desire to see the socialist worker's movement, Kropotkin set out to see Switzerland and Western Europe in February 1872. Over three months, he met Mikhail Sazhin in Zurich, worked and fell out with Nikolai Utin's Marxist group in Geneva, and was introduced to the Jura Federation's James Guillaume and Adhémar Schwitzguébel. The Jura were the main internal opposition to the Marxist-controlled First International, as followers of Mikhail Bakunin. Kropotkin was quickly impressed and was instantly converted to anarchism by the group's egalitarianism and independence of expression, but narrowly missed meeting the leading anarchist, Bakunin, while there. Kropotkin visited Belgium's movement before returning to Russia in May with contraband literature.

Back in St. Petersburg, Kropotkin joined the Chaikovsky Circle, a group of revolutionaries that Kropotkin considered more educational than revolutionary in their activities. Kropotkin believed in the inevitability of social revolution and the need for stateless social organization. His populist revolutionary program for the group focused on urban workers and peasants whereas the group's moderates focused on students. Partially for this reason, he declined to contribute his personal wealth to the group. He viewed professionals as unlikely to forgo their privileges and judged them to not live societally useful lives. His program emphasized federated agrarian communes and a revolutionary party. While he could speak powerfully, Kropotkin was not a successful organizer.

Kropotkin's first political memo in November 1873 covered his basic plan for stateless social reconstruction including common property, worker control of factories, shared physical labor towards societal need, and labor vouchers in lieu of money. He emphasized living among commoners and using propaganda to focus mass dissatisfaction. He rejected the Nechayev conspiracy model. Members of the circle began to be arrested in late 1873 and the Third Section secret police came for Kropotkin in March 1874.

His arrest for agitation, as a former page de chambre and officer, was scandalous. Kropotkin had just filed his Ice Age report and had been recently elected president of the Geographical Society's Physical and Mathematical Department. At the society's request the tsar granted Kropotkin books to finish his glaciation report. Kropotkin was held in the Peter and Paul Fortress. His brother, who had also radicalized as a follower of Lavrov, was also arrested and exiled in Siberia, where he committed suicide about a decade later.

Kropotkin was moved to the House of Detention prison military hospital in St. Petersburg for poor health, with the help of his sister. With assistance from friends, he escaped from the minimal-security prison in June 1876. By way of Scandinavia and England, Kropotkin arrived in Switzerland by the end of the year, where he met Italian anarchists Carlo Cafiero and Errico Malatesta. He visited Belgium and Zurich, where he met French geographer Élisée Reclus, who became a close friend.

Exile
Kropotkin associated with the Jura Federation and began editing its publication. He met and married his wife, a Russian Jewish student, in 1878. In 1879, he started Le Révolté, a revolutionary fortnightly, in Geneva that published his personal articulation of anarchist communism, the idea of distributing work product communally based on need rather than by work. He became the philosophy's most prominent proponent, despite not creating it. The philosophy became part of the Jura program in 1880 at Kropotkin's advocacy. Le Révolté also published Kropotkin's best known pamphlet, "An Appeal to the Young," in 1880.

Switzerland expelled Kropotkin at Russia's behest after the assassination of Alexander II in early 1881. He moved to Thonon-les-Bains, France, near Geneva, so that his wife could finish her Swiss education. Upon learning that the Holy League, a tsarist group, intended to kill him for his alleged association with the assassination, he moved to London, but could only bear to live there for a year. Upon his return in late 1882, the French arrested him for agitation, partly to appease Russia. He was sentenced to five years in Lyons. In early 1883, he was transferred to the Clairvaux Prison, where he continued his academic work. A public campaign of intellectuals and French legislators called for his release. Reclus published Words of a Rebel, a compilation of Kropotkin's Révolté writings while he was in prison, which became a main source of Kropotkin's thoughts on revolution. As Kropotkin's health worsened from scurvy and malaria, France released him in early 1886. He would stay in England through 1917, settling in Harrow, London, apart from brief trips to other European countries.

In London in late 1886, he co-founded Freedom, an anarchist monthly and the first English anarchist periodical, which he continued to support for almost three decades. His first and only child was born the next year. He published multiple books over the next coming years including In Russian and French Prisons and The Conquest of Bread. His intellectual circle in London included William Morris and W. B. Yeats as well as old Russian friends Sergey Stepnyak-Kravchinsky and Nikolai Tchaikovsky. Kropotkin contributed to the Geographical Journal and Nature.

After 1890, according to biographers George Woodcock and Ivan Avakumović, Kropotkin became more of a scholarly recluse and less of a propagandist. His works' revolutionary zeal subsided as he turned to social, ethical, and scientific questions. He joined the British Association for the Advancement of Science. He continued to contribute to Freedom but was no longer an editor.

Several of Kropotkin's books began as journal articles. His writings on anarchist communist social life were printed in the French successor to Le Révolté and later revised into The Conquest of Bread in 1892. Kropotkin's writings on decentralizing production and industry against the countervailing trend of centralized industrialization were compiled into his Fields, Factories, and Workshops in 1899. His research throughout the 1890s on the animal instinct for cooperation as a counterpoint to Darwinism became a series of articles in Nineteenth Century and, later, the book Mutual Aid: A Factor of Evolution, which was widely translated.

Following a scientific congress in Toronto in 1897, Kropotkin toured Canada. His experience there led him to advise the Russian Doukhobors who sought to immigrate there. He helped facilitate their emigration in 1899. Kropotkin entered the United States and met John Most, Emma Goldman, and Benjamin Tucker. American publishers published his Memoirs of a Revolutionist and Fields, Factories, and Workshops by the end of the decade. He visited the United States again in 1901 at the invitation of the Lowell Institute to give lectures on Russian literature that were later published. He published The Great French Revolution (1909), The Terror in Russia (1909), and Modern Science and Anarchism (1913). His 70th birthday in 1912 had celebratory gatherings in London and Paris.

Kropotkin's support for Western entry into World War I, siding with England and France, divided the anarchist movement, which had been anti-war, and damaged his esteem as a luminary of socialism. He exacerbated this by insisting, with returning to Russia, that Russians support the war as well.

Return to Russia

With the outbreak of the Russian Revolution, Kropotkin returned to Russia in June 1917. He refused the Petrograd Provisional Government's offer of a cabinet seat. In August, he advocated for defending Russia and the revolution at the National State Conference. Kropotkin applied for a residence in Moscow in 1918, which was personally approved by Vladimir Lenin, head of the Soviet government. Months later, finding life in Moscow difficult in his old age, Kropotkin moved with his family to a friend's home in the nearby town of Dmitrov. In 1919, Emma Goldman visited his family there. Kropotkin met with Lenin in Moscow and corresponded by mail to discuss political questions of the day. He advocated for workers' cooperatives and argued against the Bolsheviks' hostage policy and centralization of authority while simultaneously encouraging Western comrades to stop their governments' military interventions in Russia. Kropotkin ultimately had little impact on the Russian revolution, but his advocacy work for political and anarchist prisoners in Russia and for the Russian revolution, during the last four years of his life replenished some of the goodwill he had lost from his support for Western powers in World War I.

Kropotkin died of pneumonia on 8 February 1921. His family refused an offer of a state funeral. With his Moscow funeral, the Bolsheviks permitted the diminished Russian anarchist movement an official, restrained occasion to memorialize their figurehead. It was the last major anarchist demonstration of the period in Russia, as the movement and Kropotkin's writings would be fully suppressed later that year.

Critique of capitalism
Kropotkin critiqued what he considered to be the fallacies of the economic systems of feudalism and capitalism. He believed they create poverty and artificial scarcity and promote privilege. Alternatively, he proposed a more decentralized economic system based on mutual aid and voluntary cooperation. He argued that the tendencies for this kind of organization already exist, both in evolution and in human society.

Kropotkin disagreed in part with the Marxist critique of capitalism, including the labor theory of value, believing there was no necessary link between work performed and the values of commodities. His attack on the institution of wage labor was based more on the power employers exerted over employees, and not only on the extraction of surplus value from their labor. Kropotkin claimed this power was made possible by the state's protection of private ownership of productive resources. However, Kropotkin believed the possibility of surplus value was itself the problem, holding that a society would still be unjust if the workers of a particular industry kept their surplus to themselves, rather than redistributing it for the common good.

Critique of state socialism
Kropotkin believed that a communist society could be established only by a social revolution, which he described as, "... the taking possession by the people of all social wealth. It is the abolition of all the forces which have so long hampered the development of Humanity". However, he criticized forms of revolutionary methods (like those proposed by Marxism and Blanquism) that retained the use of state power, arguing that any central authority was incompatible with the dramatic changes needed by a social revolution. Kropotkin believed that the mechanisms of the state were deeply rooted in maintaining the power of one class over another, and thus could not be used to emancipate the working class. Instead, Kropotkin insisted that both private property and the state needed to be abolished together. "The economic change which will result from the Social Revolution will be so immense and so profound, it must so change all the relations based today on property and exchange, that it is impossible for one or any individual to elaborate the different social forms, which must spring up in the society of the future. [...] Any authority external to it will only be an obstacle, only a trammel on the organic labor which must be accomplished, and beside that a source of discord and hatred."Kropotkin believed that any post-revolutionary government would lack the local knowledge to organize a diverse population. Their vision of society would be limited by their own vindictive, self-serving, or narrow ideals. To ensure order, preserve authority, and organize production the state would need to use violence and coercion to suppress further revolution, and control workers. The workers would be reliant on the state bureaucracy to organize them, so they would never develop the initiative to self-organize as they needed. This would lead to the re-creation of classes, an oppressed workforce, and eventually another revolution. Thus, Kropotkin wrote that maintaining the state would paralyze any true social revolution, making the idea of a "revolutionary government" a contradiction in terms:"We know that Revolution and Government are incompatible; one must destroy the other, no matter what name is given to government, whether dictator, royalty, or parliament. We know that what makes the strength and the truth of our party is contained in this fundamental formula — 'Nothing good or durable can be done except by the free initiative of the people, and every government tends to destroy it;' and so the very best among us, if their ideas had not to pass through the crucible of the popular mind, before being put into execution, and if they should become masters of that formidable machine — the government — and could thus act as they chose, would become in a week fit only for the gallows. We know whither every dictator leads, even the best intentioned, — namely to the death of all revolutionary movement."Rather than a centralized approach, Kropotkin stressed the need for decentralized organization. He believed that dissolving the state would cripple counter-revolution without reverting to authoritarian methods of control, writing, "In order to conquer, something more than guillotines are required. It is the revolutionary idea, the truly wide revolutionary conception, which reduces its enemies to impotence by paralyzing all the instruments by which they have governed hitherto." He believed this was possible only through a widespread "Boldness of thought, a distinct and wide conception of all that is desired, constructive force arising from the people in proportion as the negation of authority dawns; and finally -- the initiative of all in the work of reconstruction -- this will give to the revolution the Power required to conquer."

Kropotkin applied this criticism to the Bolsheviks' rule following the October Revolution. Kropotkin summarized his thoughts in a 1919 letter to the workers of Western Europe, promoting the possibility of revolution, but also warning against the centralized control in Russia, which he believed had condemned them to failure. Kropotkin wrote to Lenin in 1920, describing the desperate conditions that he believed to be the result of bureaucratic organization, and urging Lenin to allow for local and decentralized institutions. Following an announcement of executions later that year, Kropotkin sent Lenin another furious letter, admonishing the terror which Kropotkin saw as needlessly destructive.

Cooperation and competition
In 1902, Kropotkin published his book Mutual Aid: A Factor of Evolution, which gave an alternative view of animal and human survival. At the time, some proponents of "Social Darwinism" such as Francis Galton proffered a theory of interpersonal competition and natural hierarchy. Instead, Kropotkin argued that "it was an evolutionary emphasis on cooperation instead of competition in the Darwinian sense that made for the success of species, including the human". In the last chapter, he wrote: "In the animal world we have seen that the vast majority of species live in societies, and that they find in association the best arms for the struggle for life: understood, of course, in its wide Darwinian sense – not as a struggle for the sheer means of existence, but as a struggle against all natural conditions unfavourable to the species. The animal species [...] in which individual struggle has been reduced to its narrowest limits [...] and the practice of mutual aid has attained the greatest development [...] are invariably the most numerous, the most prosperous, and the most open to further progress. The mutual protection which is obtained in this case, the possibility of attaining old age and of accumulating experience, the higher intellectual development, and the further growth of sociable habits, secure the maintenance of the species, its extension, and its further progressive evolution. The unsociable species, on the contrary, are doomed to decay."

Kropotkin did not deny the presence of competitive urges in humans, but did not consider them the driving force of human history. He believed that seeking out conflict proved to be socially beneficial only in attempts to destroy injustice, as well as authoritarian institutions such as the state or the Russian Orthodox Church, which he saw as stifling human creativity and impeding human instinctual drive towards cooperation.

Kropotkin claimed that the benefits arising from mutual organization incentivizes humans more than mutual strife. His hope was that in the long run, mutual organization would drive individuals to produce. Anarcho-primitivists and anarcho-communists believe that a gift economy can break the cycle of poverty. They rely on Kropotkin, who believed that the hunter-gatherers he had visited implemented mutual aid.

Mutual aid
In his 1892 book The Conquest of Bread, Kropotkin proposed a system of economics based on mutual exchanges made in a system of voluntary cooperation. He believed that in a society that is socially, culturally, and industrially developed enough to produce all the goods and services it needs, there would be no obstacle, such as preferential distribution, pricing or monetary exchange, to prevent everyone to take what they need from the social product. He supported the eventual abolition of money or tokens of exchange for goods and services.

Kropotkin believed that Mikhail Bakunin's collectivist economic model was just a wage system by a different name and that such a system would breed the same type of centralization and inequality as a capitalist wage system. He stated that it is impossible to determine the value of an individual's contributions to the products of labor and thought that anyone who was placed in a position of trying to make such determinations would wield authority over those whose wages they determined.

According to Kirkpatrick Sale, "[w]ith Mutual Aid especially, and later with Fields, Factories, and Workshops, Kropotkin was able to move away from the absurdist limitations of individual anarchism and no-laws anarchism that had flourished during this period and provide instead a vision of communal anarchism, following the models of independent cooperative communities he discovered while developing his theory of mutual aid. It was an anarchism that opposed centralized government and state-level laws as traditional anarchism did, but understood that at a certain small scale, communities and communes and co-ops could flourish and provide humans with a rich material life and wide areas of liberty without centralized control."

Self-sufficiency
Kropotkin's focus on local production led to his view that a country should strive for self-sufficiency by manufacturing its own goods and growing its own food, thus lessening the need to rely on imports. To these ends, he advocated irrigation and greenhouses to boost local food production.

Personal life
Kropotkin married Sofia, a Russian Jewish student, in Switzerland in October 1878. She was over a decade younger than Kropotkin. Kropotkin references her as a primary source of criticism and feedback. Her published story, "The Wife of Number 4,237", was based on her own experience with her husband at Clairvaux prison. She created an archive in Moscow dedicated to his works before her death in 1941. Their only child, Alexandra, was born in London in 1887. Kropotkin was reserved about his private life.

As an individual, Kropotkin was known for having exceptional integrity and moral character that matched his beliefs. Henry Hyndman, an ideological adversary, recalled Kropotkin's charm and sincerity. These traits, wrote Stepnyak-Kravchinsky, contributed to Kropotkin's power as a public speaker. As a thinker, Kropotkin focused more acutely on issues of morality than of economics or politics and carried himself by his own principles without imposition on others. In practice, this made him more of a "revolutionary humanitarian" than a revolutionist by deed. He was also known for being exceptionally kind and for forgoing material comforts to live a revolutionary, principled life by example. Gerald Runkle wrote that "Kropotkin with his scholarly and saintly ways ... almost brought respectability to the movement."

Legacy

As the anarchists' leading theorist in his lifetime, Kropotkin wrote their most systematic doctrine and in an accessible way; and led the development of anarchist-communist social doctrine. His works, inventive and pragmatic, were the most read anarchist books and pamphlets, with translations into major European and Eastern languages that influenced revolutionaries (e.g., Nestor Makhno and Emiliano Zapata) and non-anarchist reformers alike (e.g., Patrick Geddes, Ebenezer Howard), as well as a wide range of intellectuals (including the writers Ba Jin and James Joyce). Much of Kropotkin's impact was in his intellectual writings prior to 1914. He had little influence on the Russian revolution, despite returning for it.

Emma Goldman regarded Kropotkin as her "great teacher" and as among the greatest minds and personalities of the 19th century.

After Kropotkin's 1921 death, the Bolsheviks permitted Kropotkin's Moscow house to become a Kropotkin Museum. This closed in 1938 with his wife's death.

Kropotkin is the namesake for multiple regional entities. The Konyushennaya district in Moscow, where Kropotkin was born, is now known by his name, as the Kropotkinsky district, including the Kropotkinskaya metro station. He is the namesake for a large town in the North Caucasus (southwest Russia) and a small town in Siberia. The Kropotkin Range he was first to cross in the Siberian Patom Highlands was named for him, as was a peak in East Antarctica.

Books

 * In Russian and French Prisons, London: Ward and Downey; 1887.
 * The Conquest of Bread (Paris, 1892) Project Gutenberg e-text, Project LibriVox audiobook
 * The Great French Revolution, 1789–1793 (French original: Paris, 1893; English translation: London, 1909). e-text (in French), Anarchist Library e-text (in English)
 * The Terror in Russia, 1909, RevoltLib e-text
 * Words of a Rebel, 1885,
 * Fields, Factories, and Workshops (London and New York, 1898).
 * Memoirs of a Revolutionist, London: Smith, Elder; 1899. Anarchist Library e-text, Anarchy Archives e-text
 * Mutual Aid: A Factor of Evolution (London, 1902) Project Gutenberg e-text, Project LibriVox audiobook
 * Modern Science and Anarchism, 1903, *
 * Russian Literature: Ideals and Realities (New York: A. A. Knopf, 1905). Anarchy Archives e-text
 * The State: Its Historic Role, published 1946,
 * Ethics: Origin and Development (unfinished). Included as first part of Origen y evolución de la moral (Spanish e-text)

Pamphlets

 * An Appeal to the Young (1880)
 * Communism and Anarchy (1901)
 * Anarchist Communism: Its Basis and Principles (1887)
 * The Industrial Village of the Future (1884)
 * Law and Authority (1886)
 * The Coming Anarchy (1887)
 * The Place of Anarchy in Socialist Evolution (1886)
 * The Wage System (1920)
 * The Commune of Paris (1880)
 * Anarchist Morality (1898)
 * Expropriation
 * The Great French Revolution and Its Lesson (1909)
 * Process Under Socialism (1887)
 * Are Prisons Necessary? Chapter X from "In Russian and French Prisons" (1887)
 * The Coming War (1913)
 * Wars and Capitalism (1914)
 * Revolutionary Government (1892)
 * The Scientific Basis of Anarchy (1887)
 * The Fortress Prison of St. Petersburg (1883)
 * Advice to Those About to Emigrate (1893)
 * Some of the Resources of Canada (1898)
 * Anarchism: Its Philosophy and Ideal (1896)
 * Revolutionary Studies (1892)
 * Direct Action of Environment and Evolution (1920)
 * The Present Crisis in Russia (1901)
 * The Spirit of Revolt (1880)
 * The State: Its Historic Role (1897)
 * On Economics Selected Passages from his Writings (1898–1913)
 * On the Teaching of Physiography (1893)
 * War! (1914)

Articles

 * "The Constitutional Agitation in Russia," 1905.
 * "Brain Work and Manual Work," 1890.
 * "Manifesto of the Sixteen," 1916.
 * "Organized Vengeance Called 'Justice.'"
 * "A Proposed Communist Settlement: A New Colony for Tyneside or Wearside."
 * "What Geography Ought to Be," 1885.
 * "On Order"
 * "Maxím Górky," 1904
 * "Research on the Ice age", Notices of the Imperial Russian Geographical Society, 1876.
 * "Baron Toll", The Geographical Journal, Vol. 23, No. 6. (Jun. 1904), pp. 770–772, JSTOR
 * "The population of Russia", The Geographical Journal, Vol. 10, No. 2. (Aug. 1897), pp. 196–202, JSTOR
 * "The old beds of the Amu-Daria", The Geographical Journal, Vol. 12, No. 3. (Sep. 1898), pp. 306–310, JSTOR
 * "Russian Schools and the Holy Synod," 1902
 * Mr. Mackinder; Mr. Ravenstein; Dr. Herbertson; Prince Kropotkin; Mr. Andrews; Cobden Sanderson; Elisée Reclus, "On Spherical Maps and Reliefs: Discussion", The Geographical Journal, Vol. 22, No. 3. (Sep. 1903), pp. 294–299, JSTOR
 * "The desiccation of Eur-Asia", Geographical Journal, 23 (1904), 722–41.
 * "Finland" in Encyclopædia Britannica (11th ed.), 1911 (in part; with Joseph R. Fisher and John Scott Keltie)
 * "Finland: A Rising Nationality," Nineteenth Century, 1885
 * "Anarchism" in Encyclopædia Britannica (11th ed.), 1911
 * "Anti-militarism. Was it properly understood?", Freedom, vol.XXVIII, no. 307 (November 1914), pp. 82–83.
 * "An open letter of Peter Kropotkin to the Western workingmen", The Railway Review (29 June 1917), p. 4.

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

title: Peter Kropotkin


text:
Thalidomide

Thalidomide, sold under the brand names Contergan and Thalomid among others, is an oral medication used to treat a number of cancers (e.g., multiple myeloma), graft-versus-host disease, and many skin disorders (e.g., complications of leprosy such as skin lesions). Thalidomide has been used to treat conditions associated with HIV: aphthous ulcers, HIV-associated wasting syndrome, diarrhea, and Kaposi's sarcoma, but increases in HIV viral load have been reported.

Common side effects include sleepiness, rash, and dizziness. Severe side effects include tumor lysis syndrome, blood clots, and peripheral neuropathy. Thalidomide is a known human teratogen and carries an extremely high risk of severe, life-threatening birth defects if administered during pregnancy. It causes skeletal deformities such as amelia (absence of legs and/or arms), absence of bones, and phocomelia (malformation of the limbs). A single dose of thalidomide, regardless of dosage, is enough to cause teratogenic effects.

Thalidomide was first marketed in 1957 in West Germany, where it was available over the counter. When first released, thalidomide was promoted for anxiety, trouble sleeping, "tension", and morning sickness. While it was initially thought to be safe in pregnancy, concerns regarding birth defects arose, resulting in its removal from the market in Europe in 1961. The total number of infants severely harmed by thalidomide use during pregnancy is estimated at over 10,000, possibly 20,000, of whom about 40% died around the time of birth. Those who survived had limb, eye, urinary tract, and heart problems. Its initial entry into the US market was prevented by Frances Kelsey, a reviewer at the FDA. The birth defects caused by thalidomide led to the development of greater drug regulation and monitoring in many countries.

It was approved in the United States in 1998 for use as a treatment for cancer. It is on the World Health Organization's List of Essential Medicines. It is available as a generic medication.

Medical uses

Thalidomide is used as a first-line treatment for multiple myeloma in combination with dexamethasone or with melphalan and prednisone to treat acute episodes of erythema nodosum leprosum, as well as for maintenance therapy.

The bacterium that causes tuberculosis (TB) is related to leprosy. Thalidomide may be helpful in some cases where standard TB drugs and corticosteroids are not sufficient to resolve severe inflammation in the brain.

It is used as a second-line treatment to manage graft-versus-host disease and aphthous stomatitis in children and has been prescribed for other conditions in children, including actinic prurigo and epidermolysis bullosa; the evidence for these uses is weak. It is recommended only as a third line treatment in graft-versus-host-disease in adults because of lack of efficacy and side effects observed in clinical trials.

Contraindications
Prescriptions of thalidomide are accompanied by strict measures to avoid any possibility of use during pregnancy, and thalidomide should be avoided in men wanting to conceive. In the United States, the prescribing doctor is required to ensure that contraception is being used, and that regular pregnancy tests are taken.

Adverse effects
Thalidomide causes birth defects. The U.S. Food and Drug Administration (FDA) and other regulatory agencies have approved marketing of the drug only with an auditable risk evaluation and mitigation strategy that ensures that people using the drug are aware of the risks and avoid pregnancy; this applies to both men and women, as the drug can be transmitted in semen.

There is a high risk that thalidomide can cause excessive blood clots. There is also a high risk that thalidomide can interfere with production of several types of new blood cells, creating a risk of infection via neutropenia, leukopenia, and lymphopenia, and risks that blood will not clot via thrombocytopenia. There is also a risk of anemia via lack of red blood cells. The drug can also damage nerves, causing potentially irreversible peripheral neuropathy.

Thalidomide has several adverse cardiovascular effects, including risk of heart attacks, pulmonary hypertension, and changes in heart rhythm, such as syncope, bradycardia, and atrioventricular block.

Thalidomide can cause liver damage and severe skin reactions like Stevens–Johnson syndrome. It tends to make people sleepy, which creates risk when driving and operating other machinery. As it kills cancer cells, it can cause tumor lysis syndrome. Thalidomide can prevent menstruation.

In addition, very common (reported in more than 10% of people) adverse effects include tremor, dizziness, tingling, numbness, constipation, and peripheral edema.

Common adverse effects (reported by 1–10% of people) include confusion, depressed mood, reduced coordination, heart failure, difficulty breathing, interstitial lung disease, lung inflammation, vomiting, dry mouth, rashes, dry skin, fever, weakness, and a sense of unwellness.

Interactions
There are no expected pharmacokinetic interactions between thalidomide and other medicines due to its neutral effects on P-glycoprotein and the cytochrome P450 family. It may interact with sedatives due to its sedative action and bradycardic agents, like beta-blockers, due to its bradycardia-inducing effects. Risk of peripheral neuropathy may be increased by concomitant treatment of thalidomide with other agents known to cause peripheral neuropathy. The risk of venous thromboembolisms with thalidomide seems to be increased when patients are treated with oral contraceptives or other cytotoxic agents (including doxorubicin and melphalan) concurrently. Thalidomide may interfere with various contraceptives, and hence it is advised that women of reproductive age use at least two different means of contraception to ensure that no child will be conceived while they are taking thalidomide.

Overdose
As of 2013, eighteen cases of overdoses had been reported with doses of up to 14.4 grams, none of them fatal. No specific antidote for overdose exists and treatment is purely supportive.

Pharmacology
The precise mechanism of action for thalidomide was not known until the twenty-first century, although efforts to identify thalidomide's teratogenic action generated more than 2,000 research papers and the proposal of 15 or 16 plausible mechanisms by 2000. The primary mechanism of action of thalidomide and its analogs in both their anti-cancer and teratogenic effects is now known to be as cereblon E3 ligase modulators.

Thalidomide also binds to and acts as an antagonist of the androgen receptor and hence is a nonsteroidal antiandrogen of some capacity. In accordance, it can produce gynecomastia and sexual dysfunction as side effects in men.

Chirality and biological activity
Thalidomide is provided as a racemic mixture of two enantiomers; while there are reports that only one of the enantiomers may cause birth defects, the body converts each enantiomer into the other through mechanisms that are not well understood. The (R)-enantiomer has the desired sedative effect while the (S)-enantiomer harbors embryo-toxic and teratogenic effect. Attempting to extract solely R-thalidomide does not remove the risk of birth defects, as it was demonstrated that the "safe" R-thalidomide undergoes an in vivo chiral inversion to the "teratogenic" S-thalidomide. Under biological conditions, the enantiomers interconvert (bidirectional chiral inversion – (R)- to (S)- and vice versa).

Chemistry

Thalidomide is racemic; while S-thalidomide is the bioactive form of the molecule, the individual enantiomers can racemize to each other due to the acidic hydrogen at the chiral centre, which is the carbon of the glutarimide ring bonded to the phthalimide substituent. The racemization process can occur in vivo. The process of conversion of one enantiomer to its mirror-image version with no other change in the molecule is called chiral inversion.

Celgene Corporation originally synthesized thalidomide using a three-step sequence starting with L -glutamic acid treatment, but this has since been reformed by the use of  L -glutamine. As shown in the image below, N-carbethoxyphthalimide (1) can react with L -glutamine to yield N-phthaloyl- L -glutamine (2). Cyclization of N-phthaloyl- L -glutamine occurs using carbonyldiimidazole, which then yields thalidomide (3). Celgene Corporation's original method resulted in a 31% yield of S-thalidomide, whereas the two-step synthesis yields 85–93% product that is 99% pure.

In 2023, it is reported that phthalic anhydride and L -glutamine under suitable conditions can react directly to form thalidomide. In the procedure, phthalic anhydride and L -glutamine are grounded and added into toluene solvent. The solution, along with triethylamine and acetic anhydride, is refluxed at ~110°C for 9 hours; after that the solution goes though a simple vacuum filtration procedure to obtain the product.

History
In 1952, thalidomide was synthesised by Chemical Industry Basel, but was found "to have no effect on animals" and was discarded on that basis. In 1957, it was acquired by Chemie Grünenthal in Germany. The German company had been established as a soap maker after World War II ended, to address the urgent market need for antibiotics. Heinrich Mückter was appointed to head the discovery program based on his experience working with the German army's antiviral research. While preparing reagents for the work, Mueckter's assistant Wilhelm Kunz isolated a by-product that was recognized by pharmacologist Herbert Keller as an analog of glutethimide, a sedative. The medicinal chemistry work turned to improving the lead compound into a suitable drug: the result was thalidomide. The toxicity was examined in several animals, and the drug was introduced in 1956 as a sedative, but it was never tested on pregnant women.

Researchers at Chemie Grünenthal found that thalidomide was a particularly effective antiemetic that had an inhibitory effect on morning sickness. On 1 October 1957, the company launched thalidomide and began marketing it under the trade name Contergan. It was proclaimed a "wonder drug" for insomnia, coughs, colds and headaches.

During that period, the use of medications during pregnancy was not strictly controlled, and drugs were not thoroughly tested for potential harm to the fetus. Thousands of pregnant women took the drug to relieve their symptoms. At the time of the drug's development, scientists did not believe any drug taken by a pregnant woman could pass across the placental barrier and harm the developing fetus. There soon appeared reports of abnormalities in children being born to mothers using thalidomide. In late 1959, it was noticed that peripheral neuritis developed in patients who took the drug over a period of time, and it was only after this point that thalidomide ceased to be provided over the counter.

While initially considered safe, the drug was responsible for teratogenic deformities in children born after their mothers used it during pregnancies, prior to the third trimester. In November 1961, thalidomide was taken off the market due to massive pressure from the press and public. Experts estimate that thalidomide led to the death of approximately 2,000 children and serious birth defects in more than 10,000 children, with over half of them in West Germany. The regulatory authorities in East Germany never approved thalidomide. One reason for the initially unobserved side effects of the drug and the subsequent approval in West Germany was that at that time drugs did not have to be tested for teratogenic effects. They were tested for toxicity on rodents only, as was usual at the time.

In the UK, the British pharmaceutical company The Distillers Company (Biochemicals) Ltd, a subsidiary of Distillers Co. Ltd (now part of Diageo plc), marketed thalidomide throughout the UK, Australia and New Zealand, under the brand name Distaval, as a remedy for morning sickness. Their advertisement claimed that "Distaval can be given with complete safety to pregnant women and nursing mothers without adverse effect on mother or child ... Outstandingly safe Distaval has been prescribed for nearly three years in this country." Globally, more pharmaceutical companies started to produce and market the drug under license from Chemie Grünenthal. By the mid-1950s, 14 pharmaceutical companies were marketing thalidomide in 46 countries under at least 37 different trade names.

In the US, representatives from Chemie Grünenthal approached Smith, Kline & French (SKF), now GlaxoSmithKline, with a request to market and distribute the drug in North America. A memorandum, rediscovered in 2010 in the archives of the FDA, shows that in 1956–57, as part of its in-licensing approach, Smith, Kline and French conducted animal tests and ran a clinical trial of the drug in the US involving 875 people, including pregnant women. In 1956, researchers involved in clinical trials at SKF noted that, even when used in very high doses, thalidomide could not induce sleep in mice. When administered at doses 50 to 650 times larger than that claimed by Chemie Grünenthal to be "sleep inducing", the researchers could still not achieve the hypnotic effect in animals that it had on humans. After completion of the trial, and based on reasons kept hidden for decades, SKF declined to commercialize the drug. In 1958, Chemie Grünenthal reached an agreement with the William S. Merrell Company in Cincinnati, Ohio (later Richardson-Merrell, now part of Sanofi), to market and distribute thalidomide throughout the US.

The US FDA refused to approve thalidomide for marketing and distribution. However, the drug was distributed in large quantities for testing purposes, after the American distributor and manufacturer Richardson-Merrell had applied for its approval in September 1960. The official in charge of the FDA review, Frances Oldham Kelsey, did not rely on information from the company, which did not include any test results. Richardson-Merrell was called on to perform tests and report the results. The company demanded approval six times, and was refused each time. The distribution for "testing" resulted in 17 children born in the US with thalidomide-induced malformations. Oldham Kelsey was awarded the President's Award for Distinguished Federal Civilian Service by President Kennedy in 1962 for not allowing thalidomide to be approved for sale in the US. She was also inducted into the National Women's Hall of Fame in 2000.

Canada's Food and Drug Directorate approved the sale of thalidomide by prescription in November, 1960. There were many different forms sold: Kevadon, produced by the William S. Merrell Company seeking approval for its thalidomide product, was released on the market in April 1961, and the most common variant (Horner's Talimol) was put on the market on October 23 of the same year. Two months after Talimol went on sale, pharmaceutical companies sent physicians letters warning about the risk of birth defects. It was not until March 1962 that both drugs were banned from the Canadian market by the directorate, and soon afterward physicians were warned to destroy their supplies.

Leprosy treatment
In 1964, Israeli physician Jacob Sheskin administered thalidomide to a patient critically ill with leprosy. The patient exhibited erythema nodosum leprosum (ENL), a painful skin condition, one of the complications of leprosy. The treatment was attempted despite the ban on thalidomide's use, and results were favourable: the patient slept for hours and was able to get out of bed without aid upon awakening. A clinical trial studying the use of thalidomide in leprosy soon followed.

Thalidomide has been used by Brazilian physicians as the drug of choice for the treatment of severe ENL since 1965, and by 1996, at least 33 cases of thalidomide embryopathy were recorded in people born in Brazil after 1965. Since 1994, the production, dispensing, and prescription of thalidomide have been strictly controlled, requiring women to use two forms of birth control and submit to regular pregnancy tests. Despite this, cases of thalidomide embryopathy continue, with at least 100 cases identified in Brazil between 2005 and 2010. 5.8 million thalidomide pills were distributed throughout Brazil in this time period, largely to poor Brazilians in areas with little access to healthcare, and these cases have occurred despite the controls.

In 1998, the FDA approved the drug's use in the treatment of ENL. Because of thalidomide's potential for causing birth defects, the drug may be distributed only under tightly controlled conditions. The FDA required that Celgene Corporation, which planned to market thalidomide under the brand name Thalomid, establish a system for thalidomide education and prescribing safety (STEPS) oversight program. The conditions required under the program include limiting prescription and dispensing rights to authorized prescribers and pharmacies only, keeping a registry of all patients prescribed thalidomide, providing extensive patient education about the risks associated with the drug, and providing periodic pregnancy tests for women who take the drug.

In 2010, the World Health Organization stated that it did not recommend thalidomide for leprosy due to the difficulty of adequately controlling its use, and due to the availability of clofazimine.

Cancer treatment
Shortly after the teratogenic properties of thalidomide were recognized in the mid-1960s, its anti-cancer potential was explored and two clinical trials were conducted in people with advanced cancer, including some people with multiple myeloma; the trials were inconclusive.

Little further work was done with thalidomide in cancer until the 1990s.

Judah Folkman pioneered studies into the role of angiogenesis (the proliferation and growth of blood vessels) in the development of cancer, and in the early 1970s had shown that solid tumors could not expand without it. In 1993 he surprised the scientific world by hypothesizing the same was true of blood cancers, and the next year he published work showing that a biomarker of angiogenesis was higher in all people with cancer, but especially high in people with blood cancers, and other evidence emerged as well. Meanwhile, a member of his lab, Robert D'Amato, who was looking for angiogenesis inhibitors, discovered in 1994 that thalidomide inhibited angiogenesis and was effective in suppressing tumor growth in rabbits. Around that time, the wife of a man who was dying of multiple myeloma and whom standard treatments had failed, called Folkman asking him about his anti-angiogenesis ideas. Folkman persuaded the patient's doctor to try thalidomide, and that doctor conducted a clinical trial of thalidomide for people with multiple myeloma in which about a third of the subjects responded to the treatment. The results of that trial were published in the New England Journal of Medicine in 1999.

After further work was done by Celgene and others, in 2006 the US Food and Drug Administration granted accelerated approval for thalidomide in combination with dexamethasone for the treatment of newly diagnosed multiple myeloma patients.

It was also evaluated whether thalidomide can be combined with melphalan and prednisone for patients with multiple myeloma. This combination of drugs probably results in an increase of the overall survival.

Birth defect crisis
In the late 1950s and early 1960s, more than 10,000 children in 46 countries were born with deformities, such as phocomelia, as a consequence of thalidomide use. The severity and location of the deformities depended on how many days into the pregnancy the mother was before beginning treatment, with the time-sensitive window occurring approximately between day 20 and day 36 post-fertilisation. Thalidomide taken on the 20th day of pregnancy caused central brain damage, day 21 would damage the eyes, day 22 the ears and face, day 24 the arms, and leg damage would occur if taken up to day 28.

It is not known exactly how many worldwide victims of the drug there have been, although estimates range from 10,000 to 20,000. Despite the side effects, thalidomide was sold in pharmacies in Canada until 1962.

Notable cases

 * Lorraine Mercer MBE  of the United Kingdom, born with phocomelia of both arms and legs, is the only thalidomide survivor to carry the Olympic Torch.
 * Thomas Quasthoff, an internationally acclaimed bass-baritone, who describes himself: "1.34 meters tall, short arms, seven fingers — four right, three left — large, relatively well-formed head, brown eyes, distinctive lips; profession: singer".
 * Niko von Glasow produced a documentary called NoBody's Perfect, based on the lives of 12 people affected by the drug, which was released in 2008.
 * Mercédes Benegbi, born with phocomelia of both arms, drove the successful campaign for compensation from her government for Canadians who were affected by thalidomide.
 * Mat Fraser, born with phocomelia of both arms, is an English rock musician, actor, writer and performance artist. He produced a 2002 television documentary "Born Freak", which looked at this historical tradition and its relevance to modern disabled performers. This work has become the subject of academic analysis in the field of disability studies.
 * Sue Kent, born in 1963 with phocomelia of both arms, eight inches long, no thumbs, and seven fingers – three on one hand, four on the other - has appeared as a presenter on the BBC TV show Gardener's World since 2020, demonstrating her ability to garden using her feet and toes where others would use their hands.
 * Christian Lohr, born in 1962 with phocomelia of both arms and both legs, is a Swiss politician who served for 14 years in the legislature in the Canton Thurgau including 2 years as its president and has been a member of the national legislature since 2011.

Change in drug regulations
The disaster prompted many countries to introduce tougher rules for the testing and licensing of drugs, such as the 1962 Kefauver Harris Amendment (US), 1965 Directive 65/65/EEC1 (EU), and the Medicines Act 1968 (UK). In the United States, the new regulations strengthened the FDA, among other ways, by requiring applicants to prove efficacy and to disclose all side effects encountered in testing. The FDA subsequently initiated the Drug Efficacy Study Implementation to reclassify drugs already on the market.

Impact on research involving women
In 1977 the US Federal Drug Administration published a clinical trial guideline that excluded women of "childbearing potential" from the early phases of most clinical trials, which in practice led to their exclusion from later trial phases as well. This 1977 FDA guideline was implemented in response to a protectionist climate caused by the thalidomide tragedy. In the 1980s, a US task force on women's health concluded that a lack of women's health research (in part due to the FDA guideline) had compromised the amount and quality of information available about diseases and treatments affecting women. This led to the National Institute of Health policy that women should, when beneficial, be included in clinical trials.

Quality of life
In the 1960s, thalidomide was successfully marketed as a safer alternative to barbiturates. Due to a successful marketing campaign, thalidomide was widely used by pregnant women during the first trimester of pregnancy. However, thalidomide is a teratogenic substance, and a proportion of children born during the 1960s had thalidomide embryopathy (TE). Of these babies born with TE, "about 40% of them died before their first birthday". The surviving individuals are now middle-aged and they report experiencing challenges (physical, psychological, and socioeconomic) related to TE.

Individuals born with TE frequently experience a wide variety of health problems secondary to their TE. These health conditions include both physical and psychological conditions. When compared to individuals of similar demographic profiles, those born with TE report less satisfaction with their quality of life and their overall health. Access to health care services can also be a challenge for these people, and women in particular have experienced difficulty in locating healthcare professionals who can understand and embrace their needs.

Brand names
Brand names include Contergan, Thalomid, Talidex, Talizer, Neurosedyn, Distaval and many others.

Research
Research efforts have been focused on determining how thalidomide causes birth defects and its other activities in the human body, efforts to develop safer analogs, and efforts to find further uses for thalidomide.

Thalidomide analogs
The exploration of the antiangiogenic and immunomodulatory activities of thalidomide has led to the study and creation of thalidomide analogs. Celgene has sponsored numerous clinical trials with analogues to thalidomide, such as lenalidomide, that are substantially more powerful and have fewer side effects — except for greater myelosuppression. In 2005, Celgene received FDA approval for lenalidomide (Revlimid) as the first commercially useful derivative. Revlimid is available only in a restricted distribution setting to avoid its use during pregnancy. Further studies are being conducted to find safer compounds with useful qualities. Another more potent analog, pomalidomide, is now FDA approved. Additionally, apremilast was approved by the FDA in March 2014. These thalidomide analogs can be used to treat different diseases, or used in a regimen to fight two conditions.

Interest turned to pomalidomide, a derivative of thalidomide marketed by Celgene. It is a very active anti-angiogenic agent and also acts as an immunomodulator. Pomalidomide was approved in February 2013 by the FDA as a treatment for relapsed and refractory multiple myeloma. It received a similar approval from the European Commission in August 2013, and is expected to be marketed in Europe under the brand name Imnovid.

Clinical research
There is no conclusive evidence that thalidomide or lenalidomide is useful to bring about or maintain remission in Crohn's disease.

Thalidomide was studied in a Phase II trial for Kaposi's sarcoma, a rare soft-tissue cancer most commonly seen in the immunocompromised, that is caused by the Kaposi's sarcoma-associated herpesvirus (KSHV).

 * AIDS wasting syndrome, associated diarrhea
 * Renal cell carcinoma (RCC)
 * Glioblastoma multiforme
 * Prostate cancer
 * Melanoma
 * Colorectal cancer
 * Crohn's disease
 * Rheumatoid arthritis
 * Behcet's syndrome
 * Breast cancer
 * Head and neck cancer
 * Ovarian cancer
 * Chronic heart failure
 * Graft-versus-host disease
 * Tuberculous meningitis

title: Thalidomide