Search engine for discovering works of Art, research articles, and books related to Art and Culture
Javascript must be enabled to continue!
Herbrand’s theorem
View through CrossRef
According to Herbrand’s theorem, each formula F of quantification theory can be associated with a sequence F1, F2, F3,… of quantifier-free formulas such that F is provable just in case Fn is truth-functionally valid for some n. This theorem was the centrepiece of Herbrand’s dissertation, written in 1929 as a contribution to Hilbert’s programme. It provides a finitistically meaningful interpretation of quantification over an infinite domain. Furthermore, it can be applied to yield various consistency and decidability results for formal systems. Herbrand was the first to exploit it in this way, and his work has influenced subsequent research in these areas. While Herbrand’s approach to proof theory has perhaps been overshadowed by the tradition which derives from Gentzen, recent work on automated reasoning continues to draw on his ideas.
Title: Herbrand’s theorem
Description:
According to Herbrand’s theorem, each formula F of quantification theory can be associated with a sequence F1, F2, F3,… of quantifier-free formulas such that F is provable just in case Fn is truth-functionally valid for some n.
This theorem was the centrepiece of Herbrand’s dissertation, written in 1929 as a contribution to Hilbert’s programme.
It provides a finitistically meaningful interpretation of quantification over an infinite domain.
Furthermore, it can be applied to yield various consistency and decidability results for formal systems.
Herbrand was the first to exploit it in this way, and his work has influenced subsequent research in these areas.
While Herbrand’s approach to proof theory has perhaps been overshadowed by the tradition which derives from Gentzen, recent work on automated reasoning continues to draw on his ideas.
Related Results
Herbrand's Theorem in Inductive Proofs
Herbrand's Theorem in Inductive Proofs
An inductive proof can be represented as a proof schema, i.e. as a parameterized sequence of proofs defined in a primitive recursive way. A corresponding cut-elimination method, ca...
Extracting Herbrand systems from refutation schemata
Extracting Herbrand systems from refutation schemata
Abstract
An inductive proof can be represented as a proof schema, i.e. as a parameterized sequence of proofs defined in a primitive recursive way. A corresponding cu...
An abstract form of the first epsilon theorem
An abstract form of the first epsilon theorem
Abstract
We present a new method of computing Herbrand disjunctions. The up-to-date most direct approach to calculate Herbrand disjunctions is based on Hilbert’s eps...
ON SKOLEMIZATION AND PROOF COMPLEXITY
ON SKOLEMIZATION AND PROOF COMPLEXITY
The impact of Skolemization on the complexity of proofs in the sequent calculus is investigated. It is shown that prefix Skolemization may result in a nonelementary increase of Her...
Fermat's Last Theorem: A Proof by Contradiction
Fermat's Last Theorem: A Proof by Contradiction
In this paper I offer an algebraic proof by contradiction of Fermat’s Last Theorem. Using an alternative to the standard binomial expansion, (a+b) n = a n + b Pn i=1 a n−i (a + b) ...
The Gauss–Bonnet theorem
The Gauss–Bonnet theorem
The Gauss–Bonnet theorem is a crowning result of surface theory that gives a fundamental connection between geometry and topology. Roughly speaking, geometry refers to the “local” ...
A Fundamental Study of Composite Numbers as a Different Perspective on Problems Related to Prime Numbers
A Fundamental Study of Composite Numbers as a Different Perspective on Problems Related to Prime Numbers
Prime number-related issues can be viewed from drastically different perspectives by examining the close connections between prime numbers and composite numbers. We think that mult...
Can a computer proof be elegant?
Can a computer proof be elegant?
In computer science, proofs about computer algorithms are par for the course. Proofs
by
computer algorithms, on the other hand, are not so readily accepted....