Theory: bool

Parents

• min

Type constants

Term constants

• ?:('a -> bool) -> bool {fixity = Binder}
• T:bool {fixity = Prefix}
• !:('a -> bool) -> bool {fixity = Binder}
• /\:bool -> bool -> bool {fixity = Infix 400}
• \/:bool -> bool -> bool {fixity = Infix 300}
• F:bool {fixity = Prefix}
• ~:bool -> bool {fixity = Prefix}
• ?!:('a -> bool) -> bool {fixity = Binder}
• LET:('a -> 'b) -> 'a -> 'b {fixity = Prefix}
• COND:bool -> 'a -> 'a -> 'a {fixity = Prefix}
• ONE_ONE:('a -> 'b) -> bool {fixity = Prefix}
• ONTO:('a -> 'b) -> bool {fixity = Prefix}
• TYPE_DEFINITION:('a -> bool) -> ('b -> 'a) -> bool {fixity = Prefix}

Axioms

BOOL_CASES_AX

|- !t. (t = T) \/ (t = F)

IMP_ANTISYM_AX

|- !t1 t2. (t1 ==> t2) ==> (t2 ==> t1) ==> (t1 = t2)

ETA_AX

|- !t. (\x. t x) = t

SELECT_AX

|- !P x. P x ==> P ($@ P)

INFINITY_AX

|- ?f. ONE_ONE f /\ ~(ONTO f)

Definitions

EXISTS_DEF

|- $? = (\P. P ($@ P))

TRUTH

|- T = (\x. x) = (\x. x)

FORALL_DEF

|- $! = (\P. P = (\x. T))

AND_DEF

|- $/\ = (\t1 t2. !t. (t1 ==> t2 ==> t) ==> t)

OR_DEF

|- $\/ = (\t1 t2. !t. (t1 ==> t) ==> (t2 ==> t) ==> t)

F_DEF

|- F = (!t. t)

NOT_DEF

|- ~ = (\t. t ==> F)

EXISTS_UNIQUE_DEF

|- $?! = (\P. $? P /\ (!x y. P x /\ P y ==> (x = y)))

LET_DEF

|- LET = (\f x. f x)

COND_DEF

|- COND = (\t t1 t2. @x. ((t = T) ==> (x = t1)) /\ ((t = F) ==> (x = t2)))

ONE_ONE_DEF

|- !f. ONE_ONE f = (!x1 x2. (f x1 = f x2) ==> (x1 = x2))

ONTO_DEF

|- !f. ONTO f = (!y. ?x. y = f x)

TYPE_DEFINITION

|- !P rep.
     TYPE_DEFINITION P rep =
     (!x' x''. (rep x' = rep x'') ==> (x' = x'')) /\
     (!x. P x = (?x'. x = rep x'))

Theorems