一つだけの公理を用いる論理体系

gistfile1.txt

公理X: ((a -> b -> a) -> ((c -> d -> e) -> (c -> d) -> c -> e) -> (f -> g -> f) -> h) -> hとおく。

定理P: α -> β -> γ -> β
a' -> b' -> a' : (a -> b -> a) -> ((c -> d -> e) -> (c -> d) -> c -> e) -> (f -> g -> f) -> h
a' : a -> b -> a
b' : (c -> d -> e) -> (c -> d) -> c -> e
a' : (f -> g -> f) -> h
→ b' -> a'
→ b' -> a -> b -> a
→ α -> β -> γ -> β

定理K: α -> β -> α
P.α: ((a -> b -> a) -> ((c -> d -> e) -> (c -> d) -> c -> e) -> (f -> g -> f) -> h) -> h
→ P.β -> P.γ -> P.β
→ α -> β -> α

定理S: (α -> β -> γ) -> (α -> β) -> α -> γ
P.α: X.a -> X.b -> X.a
P.β: (X.c -> X.d -> X.e) -> (X.c -> X.d) -> X.c -> X.e
P.γ: X.f -> X.g -> X.f
P.β: X.h
→ X.h
→ (α -> β -> γ) -> (α -> β) -> α -> γ

定理I: α -> α

S.α: K.α
S.β: K.β
S.γ: K.α
→ I' : (α -> β) -> α -> α

I'.α : K.α
I'.β : K.β -> K.α
→ I : α -> α