祖先関係
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/06/10 03:00 UTC 版)
「系列の一般理論の若干のトピックス」という題名の第3章の主要な成果は,今日,祖先関係と呼ばれるものに関連している。フレーゲは,xに手続きfを適用した結果がyであることを, ⊢ f ( x , y ) {\displaystyle \vdash f(x,y)} と表す（この記事では,現代記法で,xfy と書く）。また,フレーゲは,「xが性質Fを持ち,かつ,xに手続きfを適用した結果もつねに性質Fを持つ」とき,「性質Fはf系列において遺伝的である」（この記事では,Her(F)と書く）と言う。 ∀ x ( F x → ∀ y ( x f y → F y ) ) ≡ H e r ( F ) {\displaystyle \forall x(Fx\to \forall y(xfy\to Fy))\equiv Her(F)} である。また,この記事では,「f系列でのxのすべての子ども（xに手続きfを適用した結果のすべて）が性質Fを持つ」ことをIn(x,F)と書く。すなわち, ∀ a ( x f a → F a ) ≡ I n ( x , F ) {\displaystyle \forall a(xfa\to Fa)\equiv In(x,F)} である。フレーゲは命題76で,xに手続きfを適用した結果のすべてが持つあらゆる遺伝的性質を,yが持つとき,「xはyの祖先である」あるいは「yはxの子孫である」（xf*yと書く）と定義した。 76: ⊩ ∀ F [ H e r ( F ) → ( I n ( x , F ) → F y ) ] ≡ x f ∗ y {\displaystyle \Vdash \forall F[Her(F)\to (In(x,F)\to Fy)]\equiv xf^{*}y} . 命題81から, ⊢ F x → [ H e r ( F ) → x f ∗ y ∨ y = x → F y ) ] {\displaystyle \vdash Fx\to [Her(F)\to xf^{*}y\vee y=x\to Fy)]} . が得られるが,これは数学的帰納法の原理を与えるものである。 命題98は,祖先関係が推移的であることを示す。 98: ⊢ x f ∗ y → ( y f ∗ z → x f ∗ z ) {\displaystyle \vdash xf^{*}y\to (yf^{*}z\to xf^{*}z)} . 命題99は,「zは,xで始まるf系列に属する」（この記事では,xf*=z と書く）とは,「zは,xであるか,または,xの子孫である」ことと定義している。 99: ⊩ x f ∗ z ∨ z = x ≡ x f ∗ = z {\displaystyle \Vdash xf^{*}z\vee z=x\equiv xf^{*}=z} 命題115は,「fは関数的な（多対一の,一意的な）手続きである」（この記事ではFN(f)と書く）とは,yがxへの手続きfの適用結果であり,手続きfをxへ適用した結果がすべてyと同じであること,と定義している。 115: ⊩ ∀ y ∀ x [ x f y → ∀ z ( x f z → y = z ) ] ≡ F N ( f ) {\displaystyle \Vdash \forall y\forall x[xfy\to \forall z(xfz\to y=z)]\equiv FN(f)} . 最後の命題133は,手続きfが関数的で,mとyがf系列でxの子孫であるとき,yはmの祖先であるか,またはmで始まるf系列に属することを示す。 133: ⊢ F N ( f ) → [ x f ∗ m → ( x f ∗ y → y f ∗ m ∨ m f ∗ = y ) {\displaystyle \vdash FN(f)\to [xf^{*}m\to (xf^{*}y\to yf^{*}m\vee mf^{*}=y)} . フレーゲは,祖先関係の成果を含む『概念記法』の成果を,後の仕事『算術の基礎』に適用した。
※この「祖先関係」の解説は、「概念記法」の解説の一部です。
「祖先関係」を含む「概念記法」の記事については、「概念記法」の概要を参照ください。
- 祖先関係のページへのリンク
