The Theory log
Parents
min
Children
init
Constants
T
 BOOL
$∀
 ('a → BOOL) → BOOL
$∃
 ('a → BOOL) → BOOL
F
 BOOL
$¬
 BOOL → BOOL
$∧
 BOOL → BOOL → BOOL
$∨
 BOOL → BOOL → BOOL
OneOne
 ('a → 'b) → BOOL
Onto
 ('a → 'b) → BOOL
TypeDefn
 ('b → BOOL) → ('a → 'b) → BOOL
Fixity
Binder: ∀ ∃
Right Infix 30:
∨
Right Infix 40:
∧
Prefix 50: ¬
Terminators
∀ ∃ ¬ ∧ ∨
Definitions
T
t_def
 ⊢ T ⇔ (λ x• x) = (λ x• x)
∀
∀_def
 ⊢ $∀ = (λ P• P = (λ x• T))
∃
∃_def
 ⊢ $∃ = (λ P• P ($ε P))
F
f_def
 ⊢ F ⇔ (∀ b• b)
¬
¬_def
 ⊢ $¬ = (λ b• b ⇒ F)
∧
∧_def
 ⊢ $∧ = (λ b1 b2• ∀ b• (b1 ⇒ b2 ⇒ b) ⇒ b)
∨
∨_def
 ⊢ $∨ = (λ b1 b2• ∀ b• (b1 ⇒ b) ⇒ (b2 ⇒ b) ⇒ b)
OneOne
one_one_def
 ⊢ OneOne = (λ f• ∀ x1 x2• f x1 = f x2 ⇒ x1 = x2)
Onto
onto_def
 ⊢ Onto = (λ f• ∀ y• ∃ x• y = f x)
TypeDefn
type_defn_def
⊢ TypeDefn
fill= (λ P rep
fill• OneOne rep ∧ (∀ x• P x ⇔ (∃ y• x = rep y)))

up quick index

privacy policy

Created:

V