「数学ガール ゲーデルの不完全性定理」の10章「冬」の単元で定義される関数、述語の一覧表 14
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には形式的証明が存在する