人気ブログランキング |

「数学ガール ゲーデルの不完全性定理」の10章「冬」の単元で定義される関数、述語の一覧表 14

定義-27 substAtWith(x,n,c)
xのn番目の要素をcで置き換えたもの

定義-28 freepos(k,v,n)
xでk+1番目の、自由であるvの場所

定義-29 freenum(v,x)
xでvが自由である場所の総数

定義-30 subsuSome(k,x,v,c)
xの自由であるvの出てくる場所のうち、k個をcで置き換えた論理式

定義-31 subst(a,v,c)
aの自由であるvをすべてcで置換した論理式

定義32
implies(a,b) a→b
and(a,b) a∧b
equiv(a,b) a↔︎b
exisits(x,a) ∃x(a)

定義-33 typelift(n,x)
xをnだけ型持ち上げしたもの

定義-34 IsAxiomI(x)
xは公理Iから得られる論理式

定義-35 IsSchemaII(n,x)
xは公理II-nから得られる論理式

定義-36 IsAxiomII(x)
xは公理IIから得られる論理式

定義-37 IsNotBoundIn(z,y,v)
zはyの中でvが自由な範囲に束縛された変数を持たない

定義-38 IsSchemaIII(1,x)
xは公理III-1から得られる論理式

定義-39 IsSchemaIII(2,x)
xは公理III-2から得られる論理式

定義-40 IsAxiomIV(x)
xは公理IVから得られる論理式

定義-41 IsAxiomV(x)
xは公理Vから得られる論理式

定義-42 IsAxiom(x)
xは公理である

定義-43 IsConseq(x,a,b)
xはaとbの直接の帰結である

定義-44 IsProof(x)
xは形式的証明である

IsAxiomAt(x,n)
xのn番目の要素は公理である

ConseqAt(x,n)
0より大きく、n未満のp,qが存在して、x[n]はx[p]とx[q]の直接の帰結である

定義-45 Provs(p,x)
pはxの形式的証明である

定義-46 IsProvable(x)
xには形式的証明が存在する
by tomoarrow | 2016-03-22 07:00 | モチーフについて | Comments(0)