Monday, September 10, 2007

Proof theory

Proof theory

From Wikipedia, the free encyclopedia

Jump to: navigation, search

Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed according to the axioms and rules of inference of the logical system. As such, proof theory is syntactic in nature, in contrast to model theory, which is semantic in nature. Together with model theory, axiomatic set theory, and recursion theory, proof theory is one of the so-called four pillars of the foundations of mathematics.[1] Proof theory can also be considered a branch of philosophical logic, where the primary interest is in the idea of a proof-theoretic semantics, an idea which depends upon technical ideas in structural proof theory to be feasible.

Contents

[hide]

[edit] History

Although the formalisation of logic was much advanced by the work of such figures as Gottlob Frege, Giuseppe Peano, Bertrand Russell, and Richard Dedekind, the story of modern proof theory is often seen as being established by David Hilbert, who initiated what is called Hilbert's program in the foundations of mathematics. Kurt Gödel's seminal work on proof theory first advanced, then refuted this program: his completeness theorem initially seemed to bode well for Hilbert's aim of reducing all mathematics to a finitist formal system; then his incompleteness theorems showed that this is unattainable. All of this work was carried out with the proof calculi called the Hilbert systems.

In parallel with the proof theoretic work of Gödel, Gerhard Gentzen was laying the foundations of what is now known as structural proof theory. In a few short years, Gentzen introduced the core formalisms of natural deduction (simultaneously with and independently of Jaskowski) and the sequent calculus, made fundamental advances in the formalisation of intuitionistic logic, introduced the important idea of analytic proof, and provided the first combinatorial proof of the consistency of Peano arithmetic.

[edit] Formal and informal proof

The informal proofs of everyday mathematical practice are unlike the formal proofs of proof theory. They are rather like high-level sketches that would allow an expert to reconstruct a formal proof at least in principle, given enough time and patience. For most mathematicians, writing a fully formal proof would have all the drawbacks of programming in machine code.

Formal proofs are constructed with the help of computers in automated theorem proving. Significantly, these proofs can be checked automatically, also by computer. (Checking formal proofs is usually trivial, whereas finding proofs is typically quite hard.) An informal proof in the mathematics literature, by contrast, requires weeks of peer review to be checked, and may still contain errors.

[edit] Kinds of proof calculi

The three most well-known styles of proof calculi are:

Each of these can give a complete and axiomatic formalization of propositional or predicate logic of either the classical or intuitionistic flavour, almost any modal logic, and many substructural logics, such as relevance logic or linear logic. Indeed it is unusual to find a logic that resists being represented in one of these calculi.

[edit] Consistency proofs

Main article: Consistency proof

As previously mentioned, the spur for the mathematical investigation of proofs in formal theories was Hilbert's program. The central idea of this program was that if we could give finitary proofs of consistency for all the sophisticated formal theories needed by mathematicians, then we could ground these theories by means of a metamathematical argument, which shows that all of their purely universal assertions (more technically their provable Π01 sentences) are finitarily true; once so grounded we do not care about the non-finitary meaning of their existential theorems, regarding these as pseudo-meaningful stipulations of the existence of ideal entities.

The failure of the program was induced by Kurt Gödel's incompleteness theorems, which showed that any ω-consistent theory that is sufficiently strong to express certain simple arithmetic truths, cannot prove its own consistency, which on Gödel's formulation is a \Pi^0_1 sentence.

Much investigation has been carried out on this topic since, which has in particular led to:

  • Refinement of Gödel's result, particularly J. Barkley Rosser's refinement, weakening the above requirement of ω-consistency to simple consistency;
  • Axiomatisation of the core of Gödel's result in terms of a modal language, provability logic;
  • Transfinite iteration of theories, due to Alan Turing and Solomon Feferman;
  • The recent discovery of self-verifying theories, systems strong enough to talk about themselves, but too weak to carry out the diagonal argument that is the key to Gödel's unprovability argument.

[edit] Structural proof theory

Structural proof theory is the subdiscipline of proof theory that studies proof calculi that support a notion of analytic proof. The notion of analytic proof was introduced by Gentzen for the sequent calculus; there the analytic proofs are those that are cut-free. His natural deduction calculus also supports a notion of analytic proof, as shown by Dag Prawitz. The definition is slightly more complex: we say the analytic proofs are the normal forms, which are related to the notion of normal form in term rewriting. More exotic proof calculi such as Jean-Yves Girard's proof nets also support a notion of analytic proof.

Structural proof theory is connected to type theory by means of the Curry-Howard correspondence, which observes a structural analogy between the process of normalisation in the natural deduction calculus and beta reduction in the typed lambda calculus. This provides the foundation for the intuitionistic type theory developed by Per Martin-Löf, and is often extended to a three way correspondence, the third leg of which are the cartesian closed categories.

In linguistics, type-logical grammar, categorial grammar and Montague grammar apply formalisms based on structural proof theory to give a formal natural language semantics.

[edit] Tableau systems

Tableau systems apply the central idea of analytic proof from structural proof theory to provide decision procedures and semi-decision procedures for a wide range of logics.

[edit] Ordinal analysis

Main article: Ordinal analysis

Ordinal analysis is a powerful technique for providing combinatorial consistency proofs for theories formalising arithmetic and analysis.

[edit] Substructural logics

Main article: Substructural logic

[edit] See also

[edit] References

  1. ^ Wang, Hao (1981). Popular Lectures on Mathematical Logic. Van Nostrand Reinhold Company, 3–4. ISBN 0442231091.


Recursion

Recursion

From Wikipedia, the free encyclopedia

Jump to: navigation, search
A visual form of recursion known as the Droste effect.
A visual form of recursion known as the Droste effect.

Recursion, in mathematics and computer science, is a method of defining functions in which the function being defined is applied within its own definition. The term is also used more generally to describe a process of repeating objects in a self-similar way. For instance, when the surfaces of two mirrors are almost parallel with each other the nested images that occur are a form of recursion.

Contents

[hide]

[edit] Formal definitions of recursion

See recursion

In mathematics and computer science, recursion specifies (or constructs) a class of objects or methods (or an object from a certain class) by defining a few very simple base cases or methods (often just one), and then defining rules to break down complex cases into simpler cases.

For example, the following is a recursive definition of person's ancestors:

  • One's parents are one's ancestors (base case);
  • The parents of any ancestor are also ancestors of the person under consideration (recursion step).

It is convenient to think that a recursive definition defines objects in terms of "previously defined" objects of the class to define.

Definitions such as these are often found in mathematics. For example, the formal definition of natural numbers in set theory is: 0 is a natural number, and each natural number has a successor, which is also a natural number.

Here is another, perhaps simpler way to understand recursive processes:

  1. Are we done yet? If so, return the results. Without such a termination condition a recursion would go on forever.
  2. If not, simplify the problem, solve the simpler problem(s), and assemble the results into a solution for the original problem. Then return that solution.

A more humorous illustration goes: "In order to understand recursion, one must first understand recursion." Or perhaps more accurate is the following, from Andrew Plotkin: "If you already know what recursion is, just remember the answer. Otherwise, find someone who is standing closer to Douglas Hofstadter than you are; then ask him or her what recursion is."

Examples of mathematical objects often defined recursively are functions, sets, and especially fractals.

[edit] Recursion in language

The use of recursion in linguistics, and the use of recursion in general, dates back to the ancient Indian linguist Pāṇini in the 5th century BC, who made use of recursion in his grammar rules of Sanskrit.

Linguist Noam Chomsky theorizes that unlimited extension of a language such as English is possible only by the recursive device of embedding sentences in sentences. Thus, a chatty little girl may say, "Dorothy, who met the wicked Witch of the West in Munchkin Land where her wicked Witch sister was killed, liquidated her with a pail of water." Clearly, two simple sentences — "Dorothy met the Wicked Witch of the West in Munchkin Land" and "Her sister was killed in Munchkin Land" — can be embedded in a third sentence, "Dorothy liquidated her with a pail of water," to obtain a very verbose sentence.

However, if "Dorothy met the Wicked Witch" can be analyzed as a simple sentence, then the recursive sentence "He lived in the house Jack built" could be analyzed that way too, if "Jack built" is analyzed as an adjective, "Jack-built", that applies to the house in the same way "Wicked" applies to the Witch. "He lived in the Jack-built house" is unusual, perhaps poetic sounding, but it is not clearly wrong.

The idea that recursion is necessary for the unlimited extension of a language is challenged by linguist Daniel Everett in his work Cultural Constraints on Grammar and Cognition in Pirahã: Another Look at the Design Features of Human Language in which he hypothesizes that cultural factors made recursion unnecessary in the development of the Pirahã language. This concept challenges Chomsky's idea and accepted linguistic doctrine that recursion is the only trait which differentiates human and animal communication and is currently under intense debate.

[edit] Recursion in plain English

Recursion is the process a procedure goes through when one of the steps of the procedure involves rerunning the entire same procedure. A procedure that goes through recursion is said to be recursive. Something is also said to be recursive when it is the result of a recursive procedure.

To understand recursion, one must recognize the distinction between a procedure and the running of a procedure. A procedure is a set of steps that are to be taken based on a set of rules. The running of a procedure involves actually following the rules and performing the steps. An analogy might be that a procedure is like a menu in that it is the possible steps, while running a procedure is actually choosing the courses for the meal from the menu.

A procedure is recursive if one of the steps that makes up the procedure calls for a new running of the procedure. Therefore a recursive four course meal would be a meal in which one of the choices of appetizer, salad, entrée, or dessert was an entire meal unto itself. So a recursive meal might be potato skins, baby greens salad, chicken parmesan, and for dessert, a four course meal, consisting of crab cakes, Caesar salad, for an entrée, a four course meal, and chocolate cake for dessert, so on until each of the meals within the meals is completed.

A recursive procedure must complete every one of its steps. Even if a new running is called in one of its steps, each running must run through the remaining steps. What this means is that even if the salad is an entire four course meal unto itself, you still have to eat your entrée and dessert.

[edit] Recursive humor

A common geeky joke (for example recursion in the Jargon File) is the following "definition" of recursion.

Recursion
See "Recursion".

Another example occurs in Kernighan and Ritchie's "The C Programming Language." The following index entry is found on page 269:

recursion 86, 139, 141, 182, 202, 269

This is a parody on references in dictionaries, which in some careless cases may lead to circular definitions. Jokes often have an element of wisdom, and also an element of misunderstanding. This one is also the second-shortest possible example of an erroneous recursive definition of an object, the error being the absence of the termination condition (or lack of the initial state, if looked at from an opposite point of view). Newcomers to recursion are often bewildered by its apparent circularity, until they learn to appreciate that a termination condition is key. A variation is:

Recursion
If you still don't get it, See: "Recursion".

which actually does terminate, as soon as the reader "gets it".

Other examples are recursive acronyms, such as GNU, PHP or TTP (Dilbert; "The TTP Project").

[edit] Recursion in mathematics

A Sierpinski triangle—a confined recursion of triangles to form a geometric lattice.
A Sierpinski triangle—a confined recursion of triangles to form a geometric lattice.

[edit] Recursively defined sets

  • Example: the natural numbers

The canonical example of a recursively defined set is given by the natural numbers:

1 is in N
if n is in N, then n + 1 is in N
The set of natural numbers is the smallest set of real numbers satisfying the previous two properties.
  • Example: The set of true reachable propositions

Another interesting example is the set of all true "reachable" propositions in an axiomatic system.

  • if a proposition is an axiom, it is a true reachable proposition.
  • if a proposition can be obtained from true reachable propositions by means of inference rules, it is a true reachable proposition.
  • The set of true reachable propositions is the smallest set of reachable propositions satisfying these conditions.

This set is called 'true reachable propositions' because: in non-constructive approaches to the foundations of mathematics, the set of true propositions is larger than the set recursively constructed from the axioms and rules of inference. See also Gödel's incompleteness theorems.

(Note that determining whether a certain object is in a recursively defined set is not an algorithmic task.)

[edit] Functional recursion

A function may be partly defined in terms of itself. A familiar example is the Fibonacci number sequence: F(n) = F(n − 1) + F(n − 2). For such a definition to be useful, it must lead to values which are non-recursively defined, in this case F(0) = 0 and F(1) = 1.

A famous recursive function is the Ackermann function which, unlike the Fibonacci sequence, cannot be expressed without recursion.

[edit] Recursive proofs

The standard way to define new systems of mathematics or logic is to define objects (such as "true" and "false", or "all natural numbers"), then define operations on these. These are the base cases. After this, all valid computations in the system are defined with rules for assembling these. In this way, if the base cases and rules are all proven to be calculable, then any formula in the mathematical system will also be calculable.

This sounds unexciting, but this type of proof is the normal way to prove that a calculation is impossible. This can often save a lot of time. For example, this type of proof was used to prove that the area of a circle is not a simple ratio of its diameter, and that no angle can be trisected with compass and straightedge -- both puzzles that fascinated the ancients.

[edit] Recursive optimization

Dynamic programming is an approach to optimization which restates a multiperiod or multistep optimization problem in recursive form. The key result in dynamic programming is the Bellman equation, which writes the value of the optimization problem at an earlier time (or earlier step) in terms of its value at a later time (or later step).

[edit] Recursion in computer science

A common method of simplification is to divide a problem into subproblems of the same type. As a computer programming technique, this is called divide and conquer and is key to the design of many important algorithms, as well as being a fundamental part of dynamic programming.

Recursion in computer programming is exemplified when a function is defined in terms of itself. One example application of recursion is in parsers for programming languages. The great advantage of recursion is that an infinite set of possible sentences, designs or other data can be defined, parsed or produced by a finite computer program.

Recurrence relations are equations to define one or more sequences recursively. Some specific kinds of recurrence relation can be "solved" to obtain a non-recursive definition.

A classic example of recursion is the definition of the factorial function, given here in C code:

unsigned int factorial(unsigned int n) {
if (n <= 1) return 1;
return n * factorial(n-1);
}

The function calls itself recursively on a smaller version of the input (n - 1) and multiplies the result of the recursive call by n, until reaching the base case, analogously to the mathematical definition of factorial.

Use of recursion in an algorithm has both advantages and disadvantages. The main advantage is usually simplicity. The main disadvantage is often that the algorithm may require large amounts of memory if the depth of the recursion is very large. It has been claimed that recursive algorithms are easier to understand because they do not contain the clutter (e.g., extra variables) associated with looping algorithms. There is no experimental evidence for this claim.

It is often possible to replace a recursive call with a simple loop, as the following example of factorial shows:

unsigned int factorial(unsigned int n) {
unsigned int result = 1;
if (n <= 1) return 1;
while (n--) result *= n;
return result;
}

An example of recursive algorithm is procedure that processes (does something with) all the nodes of a tree data structure:

void ProcessTree(node x) {
unsigned int i = 0;
while (i < x.count) {
ProcessTree(x.children[i]);
i++;
}
ProcessNode(x); // now perform the operation with the node itself
}

To process the whole tree, procedure is called with root node representing the tree as an initial parameter. The procedure calls itself recursively on all child nodes of the given node (i.e. sub-trees of the given tree), until reaching the base case that is node with no child nodes (i.e. tree having no branches usually called "leaf").

Tree data structure itself can be defined recursively (and so predestinated for recursive processing) like this:

typedef struct {
unsigned int count;
node* children;
} node

[edit] The recursion theorem

In set theory, this is a theorem guaranteeing that recursively defined functions exist. Given a set X, an element a of X and a function f: X \rightarrow X, the theorem states that there is a unique function F: N \rightarrow X (where N denotes the set of natural numbers) such that

F(0) = a
F(n + 1) = f(F(n))

for any natural number n.

[edit] Proof of uniqueness

Take two functions f and g of domain N and codomain A such that:

f(0) = a
g(0) = a
f(n + 1) = F(f(n))
g(n + 1) = F(g(n))

where a is an element of A. We want to prove that f = g. Two functions are equal if they:

i. have equal domains/codomains;
ii. have the same graphic.
i. :ii. Mathematical induction: for all n in N, f(n) = g(n)? (We shall call this condition, say, Eq(n)):
1.Eq(0) if and only if f(0) = g(0) if and only if a = a.
2.Let n be an element of N. Assuming that Eq(n) holds, we want to show that Eq(n + 1) holds as well, which is easy because: f(n + 1) = F(f(n)) = F(g(n)) = g(n + 1).

you should consider N union {0} as a domain of F.


[edit] Proof of existence

  • See Hungerford, "Algebra", first chapter on set theory.

Some common recurrence relations are:

[edit] See also

[edit] References

  • Johnsonbaugh, Richard (2004). Discrete Mathematics. Prentice Hall. ISBN 0-13-117686-2.
  • Hofstadter, Douglas (1999). Gödel, Escher, Bach: an Eternal Golden Braid. Basic Books. ISBN 0-465-02656-7.
  • Shoenfield, Joseph R. (2000). Recursion Theory. A K Peters Ltd. ISBN 1-56881-149-7.
  • Causey, Robert L. (2001). Logic, Sets, and Recursion. Jones & Bartlett. ISBN 0-7637-1695-2.
  • Cori, Rene; Lascar, Daniel; Pelletier, Donald H. (2001). Recursion Theory, Godel's Theorems, Set Theory, Model Theory. Oxford University Press. ISBN 0-19-850050-5.
  • Barwise, Jon; Moss, Lawrence S. (1996). Vicious Circles. Stanford Univ Center for the Study of Language and Information. ISBN 0-19-850050-5. - offers a treatment of corecursion.
  • Rosen, Kenneth H. (2002). Discrete Mathematics and Its Applications. McGraw-Hill College. ISBN 0-07-293033-0.
  • Cormen, Thomas H., Charles E. Leiserson, Ronald L. Rivest, Clifford Stein (2001). Introduction to Algorithms. Mit Pr. ISBN 0-262-03293-7.
  • Kernighan, B.; Ritchie, D. (1988). The C programming Language. Prentice Hall. ISBN 0-13-110362-8.
  • Stokey, Nancy,; Robert Lucas; Edward Prescott (1989). Recursive Methods in Economic Dynamics. Harvard University Press. ISBN 0674750969.

[edit] External links

Look up recursion, recursivity in Wiktionary, the free dictionary.

Mathematical induction

Mathematical induction

From Wikipedia, the free encyclopedia

Jump to: navigation, search

Mathematical induction is a method of mathematical proof typically used to establish that a given statement is true of all natural numbers. It is done by

  • proving that the first statement in the infinite sequence of statements is true, and then
  • proving that if any one statement in the infinite sequence of statements is true, then so is the next one

The method can be extended to prove statements about more general well-founded structures, such as trees; this generalization, known as structural induction, is used in mathematical logic and computer science. Indeed, the validity of mathematical induction is logically equivalent to the well-ordering principle.

Mathematical induction should not be misconstrued as a form of inductive reasoning, which is considered non-rigorous in mathematics. (See Problem of induction.) In fact, mathematical induction is a form of deductive reasoning and is fully rigorous.

Contents

[hide]

[edit] History

The earliest traces of mathematical induction can be found in Euclid's proof that the number of primes is infinite and in Bhaskara II's "cyclic method".[1] A form of proof by mathematical induction appears in a book written by Al-Karaji around 1000AD, who used it to prove the binomial theorem, Pascal's triangle, and the sum of integral cubes.[2][3] Shortly afterwards, Ibn al-Haytham (Alhazen) used the inductive method to prove the sum of fourth powers, and by extension, the sum of any integral powers, which was an important result in integral calculus.[4][5] He only stated it for particular integers, but his proof for those integers was by induction and generalizable.[4]

None of these ancient mathematicians explicitly gave the inductive hypothesis. The first rigorous exposition of the principle of induction was given by Francesco Maurolico, in his Arithmeticorum libri duo (1575), who used the technique to prove that the sum of the first n odd integers is n2. Induction was also discovered independently by the Swiss Jakob Bernoulli, and the Frenchmen Pascal and Fermat.[1]

[edit] Description

The simplest and most common form of mathematical induction proves that a statement holds for all natural numbers n and consists of two steps:

  1. The basis: showing that the statement holds when n = 0.
  2. The inductive step: showing that if the statement holds for n = m, then the same statement also holds for n = m + 1.

The proposition following the word "if" in the inductive step is called the induction hypothesis (or inductive hypothesis). To perform the inductive step, one assumes the induction hypothesis (that the statement is true for n = m) and then uses this assumption to prove the statement for n = m + 1.

A formal description of mathematical induction can be illustrated by reference to the sequential effect of falling dominoes.
A formal description of mathematical induction can be illustrated by reference to the sequential effect of falling dominoes.

This method works by first proving the statement is true for a starting value, and then proving that the process used to go from one value to the next is valid. If these are both proven, then any value can be obtained by performing the process repeatedly. It may be helpful to think of the domino effect; if you have a long row of dominoes standing on end, and you can be sure that:

  1. The first domino will fall
  2. Whenever a domino falls, its next neighbor will also fall,

then you can conclude that all of the dominoes will fall, and this fact is inevitable.

Another analogy can be to consider an infinite set of identical lily pads, all equally spaced on a pond. If a frog wishes to traverse the pond, he must:

  1. Determine if the first lily pad will hold his weight.
  2. Prove that he can jump from one lily pad to another.

Thus, he can conclude that he can jump to all of the lily pads.

[edit] Axiom of Induction

The basic assumption or axiom of induction (accepted not proved) is, in logical symbols,

\forall \mbox{ predicates }P,\, (P(0) \land \forall k [P(k) \Rightarrow P(k+1)]) \Rightarrow \forall n P(n)

where P is the proposition in question and n is a natural number.

Step 1. prove P(0) - the formula holds for integer 0.
Step 2. prove that for all (or any) natural number k, P(k) implies P(k + 1). To do this one assumes P(k) and shows that it implies P(k + 1). This does not mean substituting (k + 1) into P(k) - this is a very common mistake, which consists in assuming what is to be proved. Together 1 and 2 imply that P(n) holds for all n greater than or equal to 0.

[edit] Example

Suppose we wish to prove the statement:

1 + 2 + 3 + \cdots + n = \frac{n(n + 1)}{2}

for all natural numbers n; call this statement P(n). (This is a special case of Faulhaber's formula.) This is a simple formula for the sum of the positive natural numbers less than or equal to number n. The proof that the statement is true for all natural numbers n proceeds as follows.

Check if it is true for n = 1. The sum of 1 and no other number is simply 1. And 1(1 + 1) / 2 = 1. So the statement is true for n = 1. Thus we have that P(1) holds.

Now we have to show that if the statement holds when n = m, then it also holds when n = m + 1. This can be done as follows.

Assume the statement is true for n = m, i.e.,

1 + 2 + \cdots + m = \frac{m(m + 1)}{2}.

Adding m + 1 (which is clearly the left-hand side's next term) to both sides does not change the equality:

1 + 2 + \cdots + m + (m + 1) = \frac{m(m + 1)}{2} + (m+ 1)

By algebraic manipulation we have for the right-hand side

= \frac{m(m + 1)}{2} + \frac{2(m + 1)}{2} = \frac{(m + 2)(m + 1)}{2} = \frac{(m + 1)(m + 2)}{2} = \frac{(m + 1)((m + 1) + 1)}{2}.

Thus we have

1 + 2 + \cdots + (m + 1) = \frac{(m + 1)((m + 1) + 1)}{2}

Notice that this is equivalent to the assertion made by P(m + 1). This proof is conditional: we made the assumption that P(m) is true, and from that we derived P(m + 1). Thus, if P(m) is true, P(m + 1) must also be true. Symbolically, we have shown that

P(m) \Rightarrow P(m + 1).\,

Now, to finish, we use the process of mathematical induction:

  1. We know P(1) is true by substituting in 1 for n.
  2. Since P(1) implies P(1 + 1), we get P(2).
  3. Similarly, since P(2) implies P(2 + 1), we get P(3).
  4. With P(3), P(4) follows.
  5. From P(4), we get P(5).
  6. Etc. (Here is where the axiom of mathematical induction comes in.)
  7. We may conclude that P(n) holds for any natural number n. Q.E.D.


About Me