∀A∀a(a∈A∈Univ ⇒ a∈Univ)
∀A∀B∀a∀b((A,B∈Univ ∧ a∈A ∧ b∈B) ⇒ (a,b)∈Univ)
∀A∀a(a∈A∈Univ ⇒ a∈Univ)
∀A∀B∀a∀b((A,B∈Univ ∧ a∈A ∧ b∈B) ⇒ (a,b)∈Univ)
場の量子化の手順
量子場とは何か
場の量子化の手順
量子場とは何か
Natは自然数全体
Mat(R):=Map*(Nat×Nat,R):={ A | A∈Map(Nat×Nat,R) ∧ card({ (i,j) | (i,j)∈Nat×Nat ∧ A(i,j)≠0 })∈Nat }
A,B∈Map(Nat×Nat,R), i,j∈Nat
(A+B)(i,j):=A(i,j)+B(i,j)
O:={ ((i,j),0) | (i,j)∈Nat×Nat }
a∈R
(a・A)(i,j):=a×A(i,j)
(Map(Nat×Nat,R),+,・)はR上加群
(Map*(Nat×Nat,R),+,・)もR上加群
Natは自然数全体
Mat(R):=Map*(Nat×Nat,R):={ A | A∈Map(Nat×Nat,R) ∧ card({ (i,j) | (i,j)∈Nat×Nat ∧ A(i,j)≠0 })∈Nat }
A,B∈Map(Nat×Nat,R), i,j∈Nat
(A+B)(i,j):=A(i,j)+B(i,j)
O:={ ((i,j),0) | (i,j)∈Nat×Nat }
a∈R
(a・A)(i,j):=a×A(i,j)
(Map(Nat×Nat,R),+,・)はR上加群
(Map*(Nat×Nat,R),+,・)もR上加群
指数が変数のとき、f(x)=a^xは指数関数
ベースが変数のとき、f(x)=x^aはベキ関数
exp(a)(x):=a^x
pow(a)(x):=x^a
n∈Nat
Seg(n):={ k | k∈Nat ∧ k<n }
φ∈Map(Seg(suc(n)),Real)
x∈Real
k∈Seg(card(φ))
mono(φ,k)(x):=mul(φ(k),pow(k)(x))
poly(φ)(x):=Σ{ (k,mono(φ,k)(x)) | k∈Seg(card(φ)) }
指数が変数のとき、f(x)=a^xは指数関数
ベースが変数のとき、f(x)=x^aはベキ関数
exp(a)(x):=a^x
pow(a)(x):=x^a
n∈Nat
Seg(n):={ k | k∈Nat ∧ k<n }
φ∈Map(Seg(suc(n)),Real)
x∈Real
k∈Seg(card(φ))
mono(φ,k)(x):=mul(φ(k),pow(k)(x))
poly(φ)(x):=Σ{ (k,mono(φ,k)(x)) | k∈Seg(card(φ)) }
群論・環論も公理から入るのに、なぜホモロジー論ではそうはならないんだろう。
群論・環論も公理から入るのに、なぜホモロジー論ではそうはならないんだろう。
f,g∈CMap(X,Y)
I:=[0,1]
f,gはホモトピック :⇔ ∃F(F∈Map(I,CMap(X,Y)) ∧ F(0)=f ∧ F(1)=g ∧ { ((t,x),F(t)(x)) | t∈I ∧ x∈X }∈CMap(I×X,Y))
f,g∈CMap(X,Y)
I:=[0,1]
f,gはホモトピック :⇔ ∃F(F∈Map(I,CMap(X,Y)) ∧ F(0)=f ∧ F(1)=g ∧ { ((t,x),F(t)(x)) | t∈I ∧ x∈X }∈CMap(I×X,Y))
Countable(x):=Intersect({ A | x∈A ∧ ∀y(y∈A ⇒ Suc(y)∈A) })
Countable(∅)は最小の無限集合
Countable(Countable(∅))はまだ順序数ではない
Cup(Countable(∅),Countable(Countable(∅)))は順序数
xは順序数 ⇒ Cup(x,Countable(x))は順序数
LimOn:=Intersect({ A | ∅∈A ∧ ∀x(x∈A ⇒ Cup(x,Countable(x))∈A) })
LimOnは極限順序数全体
Countable(x):=Intersect({ A | x∈A ∧ ∀y(y∈A ⇒ Suc(y)∈A) })
Countable(∅)は最小の無限集合
Countable(Countable(∅))はまだ順序数ではない
Cup(Countable(∅),Countable(Countable(∅)))は順序数
xは順序数 ⇒ Cup(x,Countable(x))は順序数
LimOn:=Intersect({ A | ∅∈A ∧ ∀x(x∈A ⇒ Cup(x,Countable(x))∈A) })
LimOnは極限順序数全体
(G,*)は群、eは(G,*)の単位元、(R,+,×)は環、0は(R,+)の単位元、1は(R,×)の単位元、・:R×G→Rはスカラー積
Map*(G,R):={ φ | φ∈Map(G,R) ∧ card({ σ | σ∈G ∧ φ(σ)≠0 })∈Nat }
F:={ (φ,Σ{ (σ,φ(σ)・σ) | σ∈G }) | φ∈Map*(G,R) }
R[G]:={ F(φ) | φ∈Map*(G,R) }
F(φ)+F(ψ):=F(φ+ψ)
0:={ (σ,0) | σ∈G }
(G,*)は群、eは(G,*)の単位元、(R,+,×)は環、0は(R,+)の単位元、1は(R,×)の単位元、・:R×G→Rはスカラー積
Map*(G,R):={ φ | φ∈Map(G,R) ∧ card({ σ | σ∈G ∧ φ(σ)≠0 })∈Nat }
F:={ (φ,Σ{ (σ,φ(σ)・σ) | σ∈G }) | φ∈Map*(G,R) }
R[G]:={ F(φ) | φ∈Map*(G,R) }
F(φ)+F(ψ):=F(φ+ψ)
0:={ (σ,0) | σ∈G }
LはKの(外側)拡大 :⇔ ∃σ(σ∈Map(K,L) ∧ σは体準同型 ∧ σは単射)
LはKの(内部)拡大 :⇔ (K⊂L ∧ KはLの部分体)
(LはKの外側拡大 ∧ σはその体準同型) ⇒ Lはσ(K)の内部拡大
LはKの内部拡大 ⇒ Lは恒等写像を体準同型とするKの外側拡大
LはKの(外側)拡大 :⇔ ∃σ(σ∈Map(K,L) ∧ σは体準同型 ∧ σは単射)
LはKの(内部)拡大 :⇔ (K⊂L ∧ KはLの部分体)
(LはKの外側拡大 ∧ σはその体準同型) ⇒ Lはσ(K)の内部拡大
LはKの内部拡大 ⇒ Lは恒等写像を体準同型とするKの外側拡大
A:=Complex\{1}
f(n,x):=pow(1/n,x)
g(n,x):=1/(1 - pow(1/n,x))
φ:={ (m,n) | nはm番目の素数 }
(A,f,g,φ)∈S
A:=Complex\{1}
f(n,x):=pow(1/n,x)
g(n,x):=1/(1 - pow(1/n,x))
φ:={ (m,n) | nはm番目の素数 }
(A,f,g,φ)∈S
fは連続写像 ⇔ f={ (x,y) | x∈X ∧ y∈Y ∧ ∀φ((φ∈Map(Nat,X\{x}) ∧ limX(φ)=x) ⇒ limY(com(φ,f))=y) }
fはxで連続 ⇔ ∃y(y∈Y ∧ ∀φ((φ∈Map(Nat,X\{x}) ∧ limX(φ)=x) ⇒ limY(com(φ,f))=y))
fは連続写像 ⇔ f={ (x,y) | x∈X ∧ y∈Y ∧ ∀φ((φ∈Map(Nat,X\{x}) ∧ limX(φ)=x) ⇒ limY(com(φ,f))=y) }
fはxで連続 ⇔ ∃y(y∈Y ∧ ∀φ((φ∈Map(Nat,X\{x}) ∧ limX(φ)=x) ⇒ limY(com(φ,f))=y))
slope(f,φ)(n) := (f(φ(n)) - f(limX(φ))) / (φ(n) - limX(φ))
f∈Map(X,Y)に対し、
A:=Dom(D(f))はXの開集合で、D(f)はAからYへの連続写像ならば、fは可微分
slope(f,φ)(n) := (f(φ(n)) - f(limX(φ))) / (φ(n) - limX(φ))
f∈Map(X,Y)に対し、
A:=Dom(D(f))はXの開集合で、D(f)はAからYへの連続写像ならば、fは可微分
xとyが変数 ⇒ (x∈y)、(x=Y)は論理式
φが論理式 ⇒ ¬φは論理式
(φとψが論理式 ∧ φとψの束縛変数は重ならない) ⇒ (φ∧ψ)は論理式
(φは論理式 ∧ xはφに含まれる自由変数) ⇒ ∃xφは論理式
これらの有限回のステップで得られるものだけが論理式
∃xφのような形式に括り出された変数は束縛変数と呼び、そうでない変数は自由変数と呼ぶ
xとyが変数 ⇒ (x∈y)、(x=Y)は論理式
φが論理式 ⇒ ¬φは論理式
(φとψが論理式 ∧ φとψの束縛変数は重ならない) ⇒ (φ∧ψ)は論理式
(φは論理式 ∧ xはφに含まれる自由変数) ⇒ ∃xφは論理式
これらの有限回のステップで得られるものだけが論理式
∃xφのような形式に括り出された変数は束縛変数と呼び、そうでない変数は自由変数と呼ぶ
ベースの集合Xには、全順序構造が入っている。
Aは区間 :⇔ (A⊂X ∧ ∃a∃b(a,b∈X ∧ A={x | a<x≦b}))
(A_i | 1≦i≦n)は分割 :⇔ (∀i(A_iは区間) ∧ ∀i∀j(i≠j ⇒ Cap(A_i,A_j)=∅) ∧ Union({A_i | 1≦i≦n})は区間)
(A_i | 1≦i≦n)はBの分割 :⇔ ((A_i | 1≦i≦n)は分割 ∧ Union({A_i | 1≦i≦n})=B)
ベースの集合Xには、全順序構造が入っている。
Aは区間 :⇔ (A⊂X ∧ ∃a∃b(a,b∈X ∧ A={x | a<x≦b}))
(A_i | 1≦i≦n)は分割 :⇔ (∀i(A_iは区間) ∧ ∀i∀j(i≠j ⇒ Cap(A_i,A_j)=∅) ∧ Union({A_i | 1≦i≦n})は区間)
(A_i | 1≦i≦n)はBの分割 :⇔ ((A_i | 1≦i≦n)は分割 ∧ Union({A_i | 1≦i≦n})=B)
実解析
関数解析
複素解析
確率解析
調和解析
実解析
関数解析
複素解析
確率解析
調和解析
Φ:={x|∀y(¬(y∈x))}
{∅}⊂Cap(Φ,M)
Ω:={x|∅∈x ∧ ∀y∀z((y∈x ∧ (y,z)∈Suc) ⇒ z∈x)}
ω:=Intersect(Ω)
{ω}⊂Cap(Ω,M)
となっていないといけない
{∅}:=Φ
集合論的な等号'='が有効な下では、Φには要素はただ一つしかなく、それを∅としている(空集合記号の定義)
Onは順序数全体
Cap(Ω,On)=On
Union(Cap(On,M))∈On
モデルには天井が必要?
到達不能基数?
Φ:={x|∀y(¬(y∈x))}
{∅}⊂Cap(Φ,M)
Ω:={x|∅∈x ∧ ∀y∀z((y∈x ∧ (y,z)∈Suc) ⇒ z∈x)}
ω:=Intersect(Ω)
{ω}⊂Cap(Ω,M)
となっていないといけない
{∅}:=Φ
集合論的な等号'='が有効な下では、Φには要素はただ一つしかなく、それを∅としている(空集合記号の定義)
Onは順序数全体
Cap(Ω,On)=On
Union(Cap(On,M))∈On
モデルには天井が必要?
到達不能基数?
∃x∀y(¬(y∈x))
無限集合の公理
∃x(∅∈x ∧ ∀y∀z((y∈x ∧ ∀u(u∈z ⇔ (u∈y ∨ u=y))) ⇒ z∈x))
ベキ集合の公理
∀x∃y∀u(u∈y ⇔ ∀v(v∈u ⇒ v∈x))
和集合の公理
∀x∃y∀u(u∈y ⇔ ∃v(u∈v ∧ v∈x))
対集合の公理
∀x∀y∃z∀u(u∈z ⇔ (u=x ∨ u=y))
置換公理
∀x(∀u(u∈x ⇒ ∃!v(P[u,v])) ⇒ ∃y∀v(v∈y ⇔ ∃u(u∈x ∧ P[u,v])))
∃x∀y(¬(y∈x))
無限集合の公理
∃x(∅∈x ∧ ∀y∀z((y∈x ∧ ∀u(u∈z ⇔ (u∈y ∨ u=y))) ⇒ z∈x))
ベキ集合の公理
∀x∃y∀u(u∈y ⇔ ∀v(v∈u ⇒ v∈x))
和集合の公理
∀x∃y∀u(u∈y ⇔ ∃v(u∈v ∧ v∈x))
対集合の公理
∀x∀y∃z∀u(u∈z ⇔ (u=x ∨ u=y))
置換公理
∀x(∀u(u∈x ⇒ ∃!v(P[u,v])) ⇒ ∃y∀v(v∈y ⇔ ∃u(u∈x ∧ P[u,v])))
Union := { (x,y) | ∀u(u∈y ⇔ ∃v(u∈v ∧ v∈x)) }
Intersect := { (x,y) | ∀u(u∈y ⇔ (∃v(u∈v ∧ v∈x) ∧ ∀v(v∈x ⇒ u∈v))) }
Pair := { ((x,y),z) | ∀u(u∈z ⇔ (u=x ∨ u=y)) }
Union := { (x,y) | ∀u(u∈y ⇔ ∃v(u∈v ∧ v∈x)) }
Intersect := { (x,y) | ∀u(u∈y ⇔ (∃v(u∈v ∧ v∈x) ∧ ∀v(v∈x ⇒ u∈v))) }
Pair := { ((x,y),z) | ∀u(u∈z ⇔ (u=x ∨ u=y)) }
∀x∀y(¬P[x,y]) ⇒ ∀x∀y∀z((P[x,y] ∧ P[x,z]) ⇒ y=z)
が成立
{ (x,y) | P[x,y] }=∅ ⇒ ∀x∀y∀z((P[x,y] ∧ P[x,z]) ⇒ y=z)
{ (x,y) | P[x,y] }=∅ ⇒ { (x,y) | P[x,y] }は写像
∅は写像
が成立
∀x∀y(¬P[x,y]) ⇒ ∀x∀y∀z((P[x,y] ∧ P[x,z]) ⇒ y=z)
が成立
{ (x,y) | P[x,y] }=∅ ⇒ ∀x∀y∀z((P[x,y] ∧ P[x,z]) ⇒ y=z)
{ (x,y) | P[x,y] }=∅ ⇒ { (x,y) | P[x,y] }は写像
∅は写像
が成立
Ran := { (f,y) | ∀v(v∈y ⇔ ∃u((u,v)∈f)) }
Prod := { ((x,y),z) | ∀u∀v((u,v)∈z ⇔ (u∈x ∧ v∈y)) }
∃!x(P[x]) :⇔ (∃x(P[x]) ∧ ∀u∀v((P[u] ∧ P[v]) ⇒ u=v))
Ran := { (f,y) | ∀v(v∈y ⇔ ∃u((u,v)∈f)) }
Prod := { ((x,y),z) | ∀u∀v((u,v)∈z ⇔ (u∈x ∧ v∈y)) }
∃!x(P[x]) :⇔ (∃x(P[x]) ∧ ∀u∀v((P[u] ∧ P[v]) ⇒ u=v))