翻訳と辞書 Words near each other ・ Herculean Effort Productions ・ Herculean Sarcophagus of Genzano ・ Hercules ・ Hercules & Xena Roleplaying Game ・ Herboso ・ Herbow ・ Herbrand Award ・ Herbrand interpretation ・ Herbrand Lavik ・ Herbrand Lofthus ・ Herbrand quotient ・ Herbrand Russell, 11th Duke of Bedford ・ Herbrand Sackville, 9th Earl De La Warr ・ Herbrand structure ・ Herbrand's theorem ・ Herbrandization ・ Herbrandston ・ Herbrand–Ribet theorem ・ Herbrechtingen ・ Herbringhauser Bach ・ Herbs (band) ・ Herbs and Apples ・ Herbs de Majorca ・ Herbs in Polish mythology ・ Herbsaint ・ Herbsheim ・ Herbsleben ・ Herbst ・ Herbst Glacier ・ Herbst in Peking Dictionary Lists mini英和辞書 mini和英辞書 Webster 1913 Latin-English FOLDOC Wikipedia English ウィキペディア

翻訳と辞書　辞書検索 [ 開発暫定版 ] スポンサード リンク Herbrandization ： ウィキペディア英語版 Herbrandization The Herbrandization of a logical formula (named after Jacques Herbrand) is a construction that is dual to the Skolemization of a formula. Thoralf Skolem had considered the Skolemizations of formulas in prenex form as part of his proof of the Löwenheim-Skolem theorem (Skolem 1920). Herbrand worked with this dual notion of Herbrandization, generalized to apply to non-prenex formulas as well, in order to prove Herbrand's theorem (Herbrand 1930). The resulting formula is not necessarily equivalent to the original one. As with Skolemization which only preserves satisfiability, Herbrandization being Skolemization's dual preserves validity: the resulting formula is valid if and only if the original one is. Let $F$ be a formula in the language of first-order logic. We may assume that $F$ contains no variable that is bound by two different quantifier occurrences, and that no variable occurs both bound and free. (That is, $F$ could be relettered to ensure these conditions, in such a way that the result is an equivalent formula). The ''Herbrandization'' of $F$ is then obtained as follows: * First, replace any free variables in $F$ by constant symbols. * Second, delete all quantifiers on variables that are either (1) universally quantified and within an even number of negation signs, or (2) existentially quantified and within an odd number of negation signs. * Finally, replace each such variable $v$ with a function symbol $f\_v(x\_1,\backslash dots,x\_k)$, where $x\_1,\backslash dots,x\_k$ are the variables that are still quantified, and whose quantifiers govern $v$. For instance, consider the formula $F\; :=\; \backslash forall\; y\; \backslash exists\; x\; (\backslash wedge\; \backslash neg\backslash exists\; z\; S(x,z))$. There are no free variables to replace. The variables $y,z$ are the kind we consider for the second step, so we delete the quantifiers $\backslash forall\; y$ and $\backslash exists\; z$. Finally, we then replace $y$ with a constant $c\_y$ (since there were no other quantifiers governing $y$), and we replace $z$ with a function symbol $f\_z(x)$: : $F^H\; =\; \backslash exists\; x\; (\backslash wedge\; \backslash neg\; S(x,f\_z(x))).$ The ''Skolemization'' of a formula is obtained similarly, except that in the second step above, we would delete quantifiers on variables that are either (1) existentially quantified and within an even number of negations, or (2) universally quantified and within an odd number of negations. Thus, considering the same $F$ from above, its Skolemization would be: : $F^S\; =\; \backslash forall\; y\; (\backslash wedge\; \backslash neg\backslash exists\; z\; S(f\_x(y),z)).$ To understand the significance of these constructions, see Herbrand's theorem or the Löwenheim-Skolem theorem. == See also == * Predicate functor logic 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Herbrandization」の詳細全文を読む スポンサード リンク 翻訳と辞書 : 翻訳のためのインターネットリソース Copyright(C) kotoba.ne.jp 1997-2016. All Rights Reserved.