Analytic proof
Encyclopedia
In mathematical analysis
, an analytical proof is a proof of a theorem in analysis that only makes use of methods from analysis, and which does not make use of results from geometry. The term was first used by Bernard Bolzano
, who first provided a non-analytic proof of his intermediate value theorem
and then, several years later provided proof of the theorem which was free from intuitions concerning lines crossing each other at a point and so he felt happy calling analytic (Bolzano 1817).
Bolzano's philosophical work encouraged a more abstract reading of when a demonstration could be regarded as analytic, where a proof is analytic if it does not go beyond its subject matter (Sebastik 2007). In proof theory
, an analytical proof has come to mean a proof whose structure is simple in a special way, due to conditions on the kind of inferences that ensure none of them go beyond what is contained in the assumptions and what is demonstrated.
, so defining the subfield of structural proof theory
. There is no uncontroversial general definition of analytic proof, but for several proof calculi there is an accepted notion. For example:
However, it is possible to extend the inference rules of both calculi so that there are proofs that satisfy the condition but are not analytic. For example, a particularly tricky example of this is the analytic cut rule, used widely in the tableau method, which is a special case of the cut rule where the cut formula is a subformula of side formulae of the cut rule: a proof that contains an analytic cut is by virtue of that rule not analytic.
Furthermore, structural proof theories that are not analogous to Gentzen's theories have other notions of analytic proof. For example, the calculus of structures
organises its inference rules into pairs, called the up fragment and the down fragment, and an analytic proof is one that only contains the down fragment.
Mathematical analysis
Mathematical analysis, which mathematicians refer to simply as analysis, has its beginnings in the rigorous formulation of infinitesimal calculus. It is a branch of pure mathematics that includes the theories of differentiation, integration and measure, limits, infinite series, and analytic functions...
, an analytical proof is a proof of a theorem in analysis that only makes use of methods from analysis, and which does not make use of results from geometry. The term was first used by Bernard Bolzano
Bernard Bolzano
Bernhard Placidus Johann Nepomuk Bolzano , Bernard Bolzano in English, was a Bohemian mathematician, logician, philosopher, theologian, Catholic priest and antimilitarist of German mother tongue.-Family:Bolzano was the son of two pious Catholics...
, who first provided a non-analytic proof of his intermediate value theorem
Intermediate value theorem
In mathematical analysis, the intermediate value theorem states that for each value between the least upper bound and greatest lower bound of the image of a continuous function there is at least one point in its domain that the function maps to that value....
and then, several years later provided proof of the theorem which was free from intuitions concerning lines crossing each other at a point and so he felt happy calling analytic (Bolzano 1817).
Bolzano's philosophical work encouraged a more abstract reading of when a demonstration could be regarded as analytic, where a proof is analytic if it does not go beyond its subject matter (Sebastik 2007). In proof theory
Proof theory
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...
, an analytical proof has come to mean a proof whose structure is simple in a special way, due to conditions on the kind of inferences that ensure none of them go beyond what is contained in the assumptions and what is demonstrated.
Structural proof theory
In proof theory, the notion of analytic proof provides the fundamental concept that brings out the similarities between a number of essentially distinct proof calculiProof calculus
In mathematical logic, a proof calculus corresponds to a family of formal systems that use a common style of formal inference for its inference rules...
, so defining the subfield of structural proof theory
Structural proof theory
In mathematical logic, structural proof theory is the subdiscipline of proof theory that studies proof calculi that support a notion of analytic proof.-Analytic proof:...
. There is no uncontroversial general definition of analytic proof, but for several proof calculi there is an accepted notion. For example:
- In Gerhard GentzenGerhard GentzenGerhard Karl Erich Gentzen was a German mathematician and logician. He had his major contributions in the foundations of mathematics, proof theory, especially on natural deduction and sequent calculus...
's natural deduction calculus the analytic proofs are those in normal form; that is, no formula occurrence is both the principal premise of an elimination rule and the conclusion of an introduction rule; - In Gentzen's sequent calculusSequent calculusIn proof theory and mathematical logic, sequent calculus is a family of formal systems sharing a certain style of inference and certain formal properties. The first sequent calculi, systems LK and LJ, were introduced by Gerhard Gentzen in 1934 as a tool for studying natural deduction in...
the analytic proofs are those that do not use the cut rule.
However, it is possible to extend the inference rules of both calculi so that there are proofs that satisfy the condition but are not analytic. For example, a particularly tricky example of this is the analytic cut rule, used widely in the tableau method, which is a special case of the cut rule where the cut formula is a subformula of side formulae of the cut rule: a proof that contains an analytic cut is by virtue of that rule not analytic.
Furthermore, structural proof theories that are not analogous to Gentzen's theories have other notions of analytic proof. For example, the calculus of structures
Calculus of structures
The calculus of structures is a proof calculus with deep inference for studying the structural proof theory of noncommutative logic. The calculus has since been applied to study linear logic, classical logic, modal logic, and process calculi, and many benefits are claimed to follow in these...
organises its inference rules into pairs, called the up fragment and the down fragment, and an analytic proof is one that only contains the down fragment.