The Theory init
Parents
log
Children
misc
Axioms
bool_cases_axiom
⊢ ∀ b• (b ⇔ T) ∨ (b ⇔ F)
⇒_antisym_axiom
⊢ ∀ b1 b2• (b1 ⇒ b2) ⇒ (b2 ⇒ b1) ⇒ (b1 ⇔ b2)
η_axiom
⊢ ∀ f• (λ x• f x) = f
ε_axiom
⊢ ∀ P x• P x ⇒ P ($ε P)
infinity_axiom
⊢ ∃ f• OneOne f ∧ ¬ Onto f

up quick index

privacy policy

Created:

V