Nuprl - Some Definitions

Thms sequent falsification Sections ClassicalProps(jlc) Doc

Assignment	`Def Assignment == Var` `Thm* Assignment Type`
Sequent	`Def Sequent == (Formula List)(Formula List)` `Thm* Sequent Type`
decidable	`Def Dec(P) == P P` `Thm* A:Prop. Dec(A) Prop`
sequent_falsifiable	`Def a \| S == FS.H.a \|= F & FS.C.a \| F` `Thm* a:Assignment, S:Sequent. a \| S Type`
formula_falsifiable	`Def a \| F == (F under a) = 3` `Thm* a:Assignment, F:Formula. a \| F Type`
formula_sat	`Def a \|= F == (F under a) = 3` `Thm* a:Assignment, F:Formula. a \|= F Type`
Three	`Def == Unit+Unit+Unit` `Thm* Type`
Formula	`Def Formula == rec(formula.Var+formula+(formulaformula)+(formulaformula)+(formulaformula))` `Thm* Formula Type`
Var	`Def Var == Atom` `Thm* Var Type`
not	`Def A == A False` `Thm* A:Prop. (A) Prop`
C	`Def s.C == s.2` `Thm* s:Sequent. s.C Formula List`
list_all	`Def xL.P(x) == (letrec list_all L = (Case of L; nil True ; h.t P(h) & list_all(t)) ) (L) Thm* T:Type, P:(TProp), L:T List. xL.P(x) Type` `Thm* T:Type, P:(TType). xnil.P(x) Type`
H	`Def s.H == s.1` `Thm* s:Sequent. s.H Formula List`
valuation	`Def (F under a) == (letrec val f = case f: x (a(x)); p val(p); pq val(p) val(q); pq val(p) val(q); pq val(p) val(q); ) (F)` `Thm* a:Assignment, F:Formula. (F under a)`
K_and	`Def p q == case p: 3 3; 3 case q: 3 3; 3 3; 3 3;; 3 q;` `Thm* p,q:. p q`
K_not	`Def p == case p: 3 3; 3 3; 3 3;` `Thm* p:. p`
Three_0	`Def 3 == inl()` `Thm* 3`
letrec_body	`Def = b == b`
letrec_arg	`Def x b(x) (x) == b(x)`
letrec	`Def (letrec f b(f)) == b((letrec f b(f)) ) (recursive)`
K_imp	`Def p q == case p: 3 3; 3 case q: 3 3; 3 3; 3 3;; 3 q;` `Thm* p,q:. p q`
K_or	`Def p q == case p: 3 q; 3 case q: 3 3; 3 3; 3 3;; 3 3;` `Thm* p,q:. p q`
Three_2	`Def 3 == inr(inr())` `Thm* 3`
formula_case	`Def case F: x varC(x); p1 notC(p1); p2p3 andC(p2;p3); p4p5 orC(p4;p5); p6p7 impC(p6;p7); == InjCase(F; x. varC(x); F. InjCase(F; p1. notC(p1); F. InjCase(F; x. x/p2,p3.andC(p2;p3); F. InjCase(F; x. x/p4,p5.orC(p4;p5), x/p6,p7.impC(p6;p7)))))`
Three_1	`Def 3 == inr(inl())` `Thm* 3`
Three_case	`Def case x: 3 case0; 3 case1; 3 case2; == InjCase(x; zero. case0; one_or_two. InjCase(one_or_two; one. case1; two. case2)) Thm* t:Type{i}, t':Type{j}, t'':Type{k}, c:t, c':t', c'':t''. case 3: 3 c; 3 c'; 3 c''; t Thm* t:Type{i}, t':Type{j}, t'':Type{k}, c:t, c':t', c'':t''. case 3: 3 c'; 3 c''; 3 c; t''` `Thm* t:Type{i}, t':Type{j}, t'':Type{k}, c:t, c':t', c'':t''. case 3: 3 c; 3 c'; 3 c''; t''`

About: