The Theory si
Parents
hol
Constants
i
IND
$∈i
IND → IND → BOOL
suci
IND → IND
Aliases
i : IND
$∈i : IND → IND → BOOL
suc
suci : IND → IND
Fixity
Right Infix 240:
i
Axioms
strong_infinity_axiom
⊢ ∃ qqml.gifmk_var("∈i", qqco.gif(IND → IND → BOOL)⌝)⌝
fill• ∀ p
fill• ∃ q
fill• p ∈i q
fill∧ (∀ x
fill• x ∈i q
fill⇒ (∃ y
fill• y ∈i q
fill∧ (∀ Z
fill• ∃ z
fill• z ∈i y
fill∧ (∀ v
fill• v ∈i z ⇔ v ∈i x ∧ Z v)))
fill∧ (∀ f
fill• (∀ u• u ∈i x ⇒ f u ∈i q)
fill⇒ (∃ y
fill• y ∈i q
fill∧ (∀ u• u ∈i x ⇒ f u ∈i y))))
Definitions
i
⊢ T
i
⊢ ∀ p
fill• ∃ q
fill• p ∈ q
fill∧ (∀ x
fill• x ∈ q
fill⇒ (∃ y
fill• y ∈ q
fill∧ (∀ Z
fill• ∃ z
fill• z ∈ y
fill∧ (∀ v• v ∈ z ⇔ v ∈ x ∧ Z v)))
fill∧ (∀ f
fill• (∀ u• u ∈ x ⇒ f u ∈ q)
fill⇒ (∃ y
fill• y ∈ q ∧ (∀ u• u ∈ x ⇒ f u ∈ y))))
suci
⊢ ∀ or
fill• suc or = (ε or'• ∀ x• x ∈ or ∨ x = or ⇔ x ∈ or')

up quick index

privacy policy

Created:

V