Nuprl - Kleene

Origin Definitions Sections ClassicalProps(jlc) Doc

KleeneNuprl Section: Kleene - Kleene 3-valued truth connectives.

Selected Objects
`def`	`K_imp`	`p q == case p: 3 3; 3 case q: 3 3; 3 3; 3 3;; 3 q;`
`def`	`K_not`	`p == case p: 3 3; 3 3; 3 3;`
`def`	`K_and`	`p q == case p: 3 3; 3 case q: 3 3; 3 3; 3 3;; 3 q;`
`def`	`K_or`	`p q == case p: 3 q; 3 case q: 3 3; 3 3; 3 3;; 3 3;`
`THM`	`K_and_equal_Three_2`	`x,y:. x y = 3 x = 3 & y = 3`
`THM`	`K_or_equal_Three_2`	`x,y:. x y = 3 x = 3 y = 3`

Origin Definitions Sections ClassicalProps(jlc) Doc