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