| dbpprop:abstract
|
- Herbrand's theorem is a fundamental result of mathematical logic obtained by Jacques Herbrand (1930). It essentially allows a certain kind of reduction of first-order logic to propositional logic. Although Herbrand originally proved his theorem for arbitrary formulas of first-order logic, the simpler version shown here, restricted to formulas in prenex form containing only existential quantifiers became more popular. Let <math>(\exists y_1,\ldots,y_n)F(y_1,\ldots,y_n)</math> be a formula of first-order logic with <math>F(y_1,\ldots,y_n)</math> quantifier-free. Then <math>(\exists y_1,\ldots,y_n)F(y_1,\ldots,y_n)</math> is valid if and only if there exists a finite sequence of terms <math>t_{ij}</math>, with <math>1 \le i \le k</math> and <math>1 \le j \le n</math>, such that <math>F(t_{11},\ldots,t_{1n}) \vee \ldots \vee F(t_{k1},\ldots,t_{kn})</math> is valid. If it is valid, <math>F(t_{11},\ldots,t_{1n}) \vee \ldots \vee F(t_{k1},\ldots,t_{kn})</math> is called a Herbrand disjunction for <math>(\exists y_1,\ldots,y_n)F(y_1,\ldots,y_n)</math>. Informally: a formula <math>A</math> in prenex form containing existential quantifiers only is provable (valid) in first-order logic if and only if a disjunction comprising of substitution instances of the quantifier-free subformula of <math>A</math> is a tautology (propositionally derivable). The restriction to formulas in prenex form containing only existential quantifiers does not limit the generality of the theorem, because formulas can be converted to prenex form and their universal quantifiers can be removed by Herbrandization. Conversion to prenex form can be avoided, if structural Herbrandization is performed. Herbrandization can be avoided by imposing additional restrictions on the variable dependencies allowed in the Herbrand disjunction.
- Der nach Jacques Herbrand, einem französischen Logiker, benannte Satz von Herbrand (engl. Herbrand's theorem, was gelegentlich nicht ganz korrekt als Herbrand-Theorie übersetzt wird) in der Prädikatenlogik lautet: Sei F eine geschlossene Formel in Skolemform, F ist genau dann unerfüllbar, wenn es eine endliche Teilmenge der Herbrand-Expansion E(F) gibt, die - im aussagenlogischen Sinn - unerfüllbar ist.
- En logique, le théorème de Herbrand établit un lien entre calcul des prédicats et calcul des propositions. Alors qu'il est possible de déterminer de manière certaine si une proposition du calcul des propositions est démontrable ou pas, la question équivalente pour une formule du calcul des prédicats est plus délicate. Le théorème de Herbrand répond partiellement à cette question, bien qu'on sache depuis les travaux de Gödel, Tarski, Church, Turing et autres, qu'il n'existe pas d'algorithme permettant de décider si une formule générale du calcul des prédicats est prouvable ou non.
- Twierdzenie Herbranda to jedno z najważniejszych twierdzeń konstruktywnych logiki pierwszego rzędu: Formuła jest tautologią wtedy i tylko wtedy gdy tautologią jest pewne rozwinięcie Herbranda tej formuły. Ponieważ każde rozwinięcie jest właściwie skończoną formułą rachunku zdań, a więc da się rozstrzygnąć w czasie skończonym (wykładniczym), ilość rozwinięć Herbranda dla formuły natomast jest zbiorem przeliczalnym, umożliwia to udowodnienie każdej tautologii logiki pierwszego rzędu, chociaż może to zająć nieograniczoną ilość czasu.
- Em lógica matemática, o teorema de Herbrand é um resultado básico de Jacques Herbrand. Ele essencialmente declara que na lógica de primeira ordem formal, toda regra para os quantificadores (<math>\forall/\exists</math>) podem ser permutada até o início de uma demonstração. Formalmente: Numa lógica predicada sem igualdade, uma formula <math>A</math> na forma prenex (todos os quantificadores antes da formula) é apta a demonstração se e somente se uma sequência <math>S</math> abrangendo as instancias substituidas das meta-formulas de <math>A</math> livres de quantificadores é proposicionalmente derivavel, e <math>A</math> só pode ser obtida de S por regras estruturais e regras de quantificadores.
- 在逻辑学中，埃尔布朗定理(Herbrand's theorem)建立了命题逻辑计算和谓词逻辑计算之间的关系，因此埃尔布朗定理可能是一种已知的确定手段来判断一个命题的命题逻辑计算是否是有限的，对于一个含有复杂谓词的公式，它的谓词逻辑计算也起到同样的判断。通过对埃尔布朗定理的应用，部分解决回答了上述问题。但是虽然有Gödel(哥德尔)，Tarski(塔尔斯基)，Church(邱奇)，Turing(图灵)和其他科学家在逻辑学领域中卓越的研究成果，但是至今不存在一个算法，能够决定一个普遍公式的谓词逻辑计算是否是可计算的这样一个问题，我们不知道这个算法是否是可以被证明的。
|
| rdfs:comment
|
- Herbrand's theorem is a fundamental result of mathematical logic obtained by Jacques Herbrand (1930). It essentially allows a certain kind of reduction of first-order logic to propositional logic. Although Herbrand originally proved his theorem for arbitrary formulas of first-order logic, the simpler version shown here, restricted to formulas in prenex form containing only existential quantifiers became more popular.
- Der nach Jacques Herbrand, einem französischen Logiker, benannte Satz von Herbrand (engl. Herbrand's theorem, was gelegentlich nicht ganz korrekt als Herbrand-Theorie übersetzt wird) in der Prädikatenlogik lautet: Sei F eine geschlossene Formel in Skolemform, F ist genau dann unerfüllbar, wenn es eine endliche Teilmenge der Herbrand-Expansion E(F) gibt, die - im aussagenlogischen Sinn - unerfüllbar ist.
- En logique, le théorème de Herbrand établit un lien entre calcul des prédicats et calcul des propositions. Alors qu'il est possible de déterminer de manière certaine si une proposition du calcul des propositions est démontrable ou pas, la question équivalente pour une formule du calcul des prédicats est plus délicate.
- Twierdzenie Herbranda to jedno z najważniejszych twierdzeń konstruktywnych logiki pierwszego rzędu: Formuła jest tautologią wtedy i tylko wtedy gdy tautologią jest pewne rozwinięcie Herbranda tej formuły.
- Em lógica matemática, o teorema de Herbrand é um resultado básico de Jacques Herbrand. Ele essencialmente declara que na lógica de primeira ordem formal, toda regra para os quantificadores (<math>\forall/\exists</math>) podem ser permutada até o início de uma demonstração.
|
![[RDF Data]](/statics/sw-cube.png)
