The Theory gst-ax
Parents
wf_relp basic_hol
Constants
$∈g
GS → GS → BOOL
$⊆g
GS → GS → BOOL
ManyOne
('a → 'b → BOOL) → BOOL
g
GS → GS
g
GS → GS
RelIm
(GS → GS → BOOL) → GS → GS
Sep
GS → (GS → BOOL) → GS
galaxy
GS → BOOL
Gx
GS → GS
transitive
GS → BOOL
g
GS
Imagep
(GS → GS) → GS → GS
Pairg
GS → GS → GS
Unit
GS → GS
$∪g
GS → GS → GS
g
GS → GS
$∩g
GS → GS → GS
Types
GS
Fixity
Right Infix 230:
g g
Right Infix 240:
g g
Axioms
gs_ext_axiom
⊢ ∀ s t• s = t ⇔ (∀ e• e ∈g s ⇔ e ∈g t)
gs_wf_axiom
⊢ well_founded $∈g
Ontology_axiom
⊢ ∀ s
fill• ∃ g
fill• s ∈g g
fill∧ (∀ t
fill• t ∈g g
fill⇒ t ⊆g g
fill∧ (∃ p
fill• (∀ v• v ∈g p ⇔ v ⊆g t) ∧ p ∈g g)
fill∧ (∃ u
fill• (∀ v
fill• v ∈g u ⇔ (∃ w• v ∈g w ∧ w ∈g t))
fill∧ u ∈g g)
fill∧ (∀ rel
fill• ManyOne rel
fill⇒ (∃ r
fill• (∀ v
fill• v ∈g r
fill⇔ (∃ w• w ∈g t ∧ rel w v))
fill∧ (r ⊆g g ⇒ r ∈g g))))
Definitions
g
⊢ ∀ s t• s ⊆g t ⇔ (∀ e• e ∈g s ⇒ e ∈g t)
ManyOne
⊢ ∀ r• ManyOne r ⇔ (∀ x y z• r x y ∧ r x z ⇒ y = z)
g
⊢ ∀ s t• t ∈gg s ⇔ t ⊆g s
g
⊢ ∀ s t• t ∈gg s ⇔ (∃ e• t ∈g e ∧ e ∈g s)
RelIm
⊢ ∀ rel s t
fill• ManyOne rel
fill⇒ (t ∈g RelIm rel s ⇔ (∃ e• e ∈g s ∧ rel e t))
Sep
⊢ ∀ s p e• e ∈g Sep s p ⇔ e ∈g s ∧ p e
galaxy
⊢ ∀ s
fill• galaxy s
fill⇔ (∃ x• x ∈g s)
fill∧ (∀ t
fill• t ∈g s
fill⇒ t ⊆g s
fill∧ ℘g t ∈g s
fill∧ ⋃g t ∈g s
fill∧ (∀ rel
fill• ManyOne rel
fill⇒ RelIm rel t ⊆g s
fill⇒ RelIm rel t ∈g s))
Gx
⊢ ∀ s t
fill• t ∈g Gx s ⇔ (∀ g• galaxy g ∧ s ∈g g ⇒ t ∈g g)
transitive
⊢ ∀ s• transitive s ⇔ (∀ e• e ∈g s ⇒ e ⊆g s)
g
⊢ ∀ s• ¬ s ∈gg
Imagep
⊢ ∀ f s x• x ∈g Imagep f s ⇔ (∃ e• e ∈g s ∧ x = f e)
Pairg
⊢ ∀ s t e• e ∈g Pairg s t ⇔ e = s ∨ e = t
Unit
⊢ ∀ s• Unit s = Pairg s s
g
⊢ ∀ s t e• e ∈g s ∪g t ⇔ e ∈g s ∨ e ∈g t
g
⊢ ∀ s
fill• ⋂g s = Sep (⋃g s) (λ x• ∀ t• t ∈g s ⇒ x ∈g t)
g
⊢ ∀ s t• s ∩g t = Sep s (λ x• x ∈g t)
Theorems
gs_wf_min_thm
⊢ ∀ x
fill• (∃ y• y ∈g x)
fill⇒ (∃ z• z ∈g x ∧ ¬ (∃ v• v ∈g z ∧ v ∈g x))
gs_wf_ind_thm
⊢ ∀ s• (∀ x• (∀ y• y ∈g x ⇒ s y) ⇒ s x) ⇒ (∀ x• s x)
g_eq_thm
⊢ ∀ A B• A = B ⇔ A ⊆g B ∧ B ⊆g A
g_refl_thm
⊢ ∀ A• A ⊆g A
gg_thm
⊢ ∀ e A B• e ∈g A ∧ A ⊆g B ⇒ e ∈g B
g_trans_thm
⊢ ∀ A B C• A ⊆g B ∧ B ⊆g C ⇒ A ⊆g C
gg_thm
⊢ ∀ s t• t ∈g s ⇒ t ⊆gg s
galaxies_∃_thm
⊢ ∀ s• ∃ g• s ∈g g ∧ galaxy g
t_in_Gx_t_thm
⊢ ∀ t• t ∈g Gx t
Gx_⊆g_galaxy
⊢ ∀ s g• galaxy g ∧ s ∈g g ⇒ Gx s ⊆g g
galaxy_Gx
⊢ ∀ s• galaxy (Gx s)
GalaxiesTransitive_thm
⊢ ∀ s• galaxy s ⇒ transitive s
GCloseSep
⊢ ∀ g• galaxy g ⇒ (∀ s• s ∈g g ⇒ (∀ p• Sep s p ∈g g))
Gx_transitive_thm
⊢ ∀ s• transitive (Gx s)
Gx_mono_thm
⊢ ∀ s t• s ⊆g t ⇒ Gx s ⊆g Gx t
Gx_mono_thm2
⊢ ∀ s t• s ∈g t ⇒ Gx s ⊆g Gx t
t_sub_Gx_t_thm
⊢ ∀ t• t ⊆g Gx t
Gx_mono_thm3
⊢ ∀ s t• s ⊆g t ⇒ s ⊆g Gx t
Gx_trans_thm2
⊢ ∀ s t• s ∈g t ⇒ s ∈g Gx t
Gx_trans_thm3
⊢ ∀ s t u• s ∈g t ∧ t ∈g Gx u ⇒ s ∈g Gx u
G∅gC
⊢ ∀ g• galaxy g ⇒ ∅gg g
gg_thm
⊢ ∀ s• ∅gg t
gg_thm
⊢ ⋃gg = ∅g
GImagepC
⊢ ∀ g
fill• galaxy g
fill⇒ (∀ s
fill• s ∈g g
fill⇒ (∀ f• Imagep f s ⊆g g ⇒ Imagep f s ∈g g))
Pairg_eq_thm
⊢ ∀ s t u v
fill• Pairg s t = Pairg u v
fill⇔ s = u ∧ t = v ∨ s = v ∧ t = u
GClosePairg
⊢ ∀ g
fill• galaxy g
fill⇒ (∀ s t• s ∈g g ∧ t ∈g g ⇒ Pairg s t ∈g g)
GCloseUnit
⊢ ∀ g• galaxy g ⇒ (∀ s• s ∈g g ⇒ Unit s ∈g g)
gg_thm
⊢ ∀ A B• A ⊆g A ∪g B ∧ B ⊆g A ∪g B
gg_thm1
⊢ ∀ A B C• A ⊆g C ∧ B ⊆g C ⇒ A ∪g B ⊆g C
gg_thm2
⊢ ∀ A B C D• A ⊆g C ∧ B ⊆g D ⇒ A ∪g B ⊆g C ∪g D
gg_clauses
⊢ ∀ A• A ∪gg = A ∧ ∅gg A = A
GClose∪g
⊢ ∀ g
fill• galaxy g
fill⇒ (∀ s t• s ∈g g ∧ t ∈g g ⇒ s ∪g t ∈g g)
g_thm
⊢ ∀ x s e
fill• x ∈g s ⇒ (e ∈gg s ⇔ (∀ y• y ∈g s ⇒ e ∈g y))
gg_thm
⊢ ∀ s t• s ∈g t ⇒ ⋂g t ⊆g s
gg_thm
⊢ ∀ A B
fill• A ∈g B
fill⇒ (∀ C• (∀ D• D ∈g B ⇒ C ⊆g D) ⇒ C ⊆gg B)
gg_thm
⊢ ⋂gg = ∅g
GClose⋂g
⊢ ∀ g• galaxy g ⇒ (∀ s• s ∈g g ⇒ ⋂g s ∈g g)
GClose∩g
⊢ ∀ g
fill• galaxy g
fill⇒ (∀ s t• s ∈g g ∧ t ∈g g ⇒ s ∩g t ∈g g)
g_thm
⊢ ∀ s t e• e ∈g s ∩g t ⇔ e ∈g s ∧ e ∈g t
gg_thm
⊢ ∀ A B• A ∩g B ⊆g A ∧ A ∩g B ⊆g B
gg_thm1
⊢ ∀ A B C• A ⊆g C ∧ B ⊆g C ⇒ A ∩g B ⊆g C
gg_thm2
⊢ ∀ A B C D• A ⊆g C ∧ B ⊆g D ⇒ A ∩g B ⊆g C ∩g D
gg_thm3
⊢ ∀ A B C• C ⊆g A ∧ C ⊆g B ⇒ C ⊆g A ∩g B
gst_opext_clauses
⊢ ∀ s t x f u v e p
fill• ¬ s ∈gg
fill∧ (t ∈gg s ⇔ t ⊆g s)
fill∧ (t ∈gg s ⇔ (∃ e• t ∈g e ∧ e ∈g s))
fill∧ (x ∈g Imagep f s ⇔ (∃ e• e ∈g s ∧ x = f e))
fill∧ (Pairg s t = Pairg u v
fill⇔ s = u ∧ t = v ∨ s = v ∧ t = u)
fill∧ (e ∈g Pairg s t ⇔ e = s ∨ e = t)
fill∧ (Unit s = Unit t ⇔ s = t)
fill∧ (e ∈g Unit s ⇔ e = s)
fill∧ (Pairg s t = Unit u ⇔ s = u ∧ t = u)
fill∧ (Unit s = Pairg t u ⇔ s = t ∧ s = u)
fill∧ (e ∈g Sep s p ⇔ e ∈g s ∧ p e)
fill∧ (e ∈g s ∪g t ⇔ e ∈g s ∨ e ∈g t)
fill∧ (e ∈g s ∩g t ⇔ e ∈g s ∧ e ∈g t)
gst_relext_clauses
⊢ ∀ s t
fill• (s = t ⇔ (∀ e• e ∈g s ⇔ e ∈g t))
fill∧ (s ⊆g t ⇔ (∀ e• e ∈g s ⇒ e ∈g t))

up quick index

privacy policy

Created:

V