Nuprl Theory zeno

(only non hidden objects are presented)

COMzeno_comThis theory formalizes famous Zeno paradox
COMzeno_authorPavel Naumov
COMzeno_dateJanuary - February 1996
COMzeno_local~pavel/Nuprl/zeno.thy
COMzeno_webhttp://www.cs.cornell.edu/Info/People/pavel/Nuprl/lib/zeno
COMzeno_reqRequires only Nuprl4.2 standard libraries
COMzeno_end_com----------------------------------
THMphole_auxn:{1...}. f:(n + 1) n. i:(n + 1). j:{(i + 1)..(n + 1)}. f i = f j
THMphole_aux_ezn:{1...}. f:(n + 1) n. i:(n + 1). j:{(i + 1)..(n + 1)}. f i = f j
DISPsignature_dfSignature{<i:level>}(<E:E:*><T:T:*><L:L:*>)== Signature(<E><T><L>) Signature(<E:E:*><T:T:*><L:L:*>)== Signature(<E><T><L>)
ABSsignatureSignature(E;T;L) == e_rel:(E E ) t_rel:(T T ) l_rel:(L L ) inst_e:(E ) time:(E T) d:(T L) t0:T t1:T def_t:(T ) (L )
THMsignature_wfE,T,L:. Signature(E;T;L) '
DISPsign_e_rel_df<s:sign:E>.e_rel== < < == <
ABSsign_e_rel< == s.1
THMsign_e_rel_wfE,T,L:. s:Signature(E;T;L). < E E
DISPsign_t_rel_df<s:sign:E>.t_rel== < <== <
ABSsign_t_rel< == s.2.1
THMsign_t_rel_wfE,T,L:. s:Signature(E;T;L). < T T
DISPsign_l_rel_df<s:sign:E>.l_rel== < <== <
ABSsign_l_rel< == s.2.2.1
THMsign_l_rel_wfE,T,L:. s:Signature(E;T;L). < L L
DISPsign_inst_e_df<s:sign:E>.inst_e== I I== I
ABSsign_inst_eI == s.2.2.2.1
THMsign_inst_e_wfE,T,L:. s:Signature(E;T;L). I E
DISPsign_time_df<s:sign:E>.time== time time== time
ABSsign_timetime == s.2.2.2.2.1
THMsign_time_wfE,T,L:. s:Signature(E;T;L). time E T
DISPsign_d_df<s:sign:E>.d== <s>.d
ABSsign_ds.d == s.2.2.2.2.2.1
THMsign_d_wfE,T,L:. s:Signature(E;T;L). s.d T L
DISPsign_t0_df<s:sign:E>.t0== t0 t0== t0
ABSsign_t0t0 == s.2.2.2.2.2.2.1
THMsign_t0_wfE,T,L:. s:Signature(E;T;L). t0 T
DISPsign_t1_df<s:sign:E>.t1== <s>.t1
ABSsign_t1s.t1 == s.2.2.2.2.2.2.2.1
THMsign_t1_wfE,T,L:. s:Signature(E;T;L). s.t1 T
DISPsign_def_t_df<s:sign:E>.def_t== Def Def== Def
ABSsign_def_tDef == s.2.2.2.2.2.2.2.2.1
THMsign_def_t_wfE,T,L:. s:Signature(E;T;L). Def T
DISPsign_def_l_df<s:sign:E>.def_l== Def Def== Def
ABSsign_def_lDef == s.2.2.2.2.2.2.2.2.2
THMsign_def_l_wfE,T,L:. s:Signature(E;T;L). Def L
MLcreate_signatureClass Declaration for: s Signature(E;T;L) Long Name: signature Short Name: sign Parameters: E : T : L : Fields: (< ) e_rel : E E (<) t_rel : T T (sign_x_rel(s)) l_rel : L L (I) inst_e : E (time) time : E T (s.d) d : T L (t0) t0 : T (s.t1) t1 : T (Def) def_t : T (Def) def_l : L Universe: '
DISPsign_t_ref_rel_dfsign_t_ref_rel(<T:T:*><s:s:*>)== ==
ABSsign_t_ref_rel == x,y.x < y x = y
THMsign_t_ref_rel_wfE,T,X:. S:Signature(E;T;X). T T
DISPsign_l_ref_rel_dfsign_l_ref_rel(<L:L:*><S:S:*>)== ==
ABSsign_l_ref_rel == x,y.x < y x = y
THMsign_l_ref_rel_wfE,T,L:. S:Signature(E;T;L). L L
COMzeno_vs_jackson=== stuff that Paul Jackson forgot to put into theory gen_algebra_1 == =
DISPir_connex_dfIrConnex(<T:T:*><x:var>,<y:var>.<R:R:*>)== IrConnex(<T><x>,<y>.<R>)
ABSir_connexIrConnex(T;x,y.R[x; y]) == x,y:T. R[x; y] x = y R[x; y]
THMir_connex_wfT:. R:T T . IrConnex(T;x,y.R[x;y])
DISPir_order_dfIrOrder(<T:T:*><x:var>,<y:var>.<R:R:*>)== IrOrder(<T><x>,<y>.<R>)
ABSir_orderIrOrder(T;x,y.R[x; y]) == Irrefl(T;x,y.R[x; y]) Trans(T;x,y.R[x; y])
THMir_order_wfT:. R:T T . IrOrder(T;x,y.R[x;y])
DISPir_linorder_dfIrLinorder(<T:T:*><x:var>,<y:var>.<R:R:*>) == IrLinorder(<T><x>,<y>.<R>)
ABSir_linorderIrLinorder(T;x,y.R[x; y]) == IrConnex(T;x,y.R[x; y]) IrOrder(T;x,y.R[x; y])
THMir_linorder_wfT:. R:T T . IrLinorder(T;x,y.R[x;y])
COMback2zeno=== now back to zeno ===
DISPrun_dfRun(<E:E:*><T:T:*><L:L:*><S:S:*>)== Run(<E><T><L><S>)
ABSrunRun(E;T;L;S) == Order(E;e,f.e < f) IrLinorder(T;t,u.t < u) IrLinorder(L;x,y.x < y) t0 < S.t1 (r,u:T. t0 r r < u u S.t1 (S.d r) < (S.d u)) (e,f:E. I e I f (e < f (time e) < (time f))) (e:E. n:. w:{f:E| f < e} n. Inj({f:E| f < e} ;n;w)) Def t0 (r:T. t0 r r S.t1 Def r Def (S.d r))
THMrun_wfE,T,X:. S:Signature(E;T;X). Run(E;T;X;S)
DISPconcurrent_dfconcurrent{<i:level>}(<E:E:*><T:T:*><L:L:*><S1:S1:*><S2:S2:*>) == <S1> || <S2> <S1:S1:*> || <S2:S2:*>== <S1> || <S2>
ABSconcurrentS1 || S2 == < = < < = < < = < I = I time = time Def = Def Def = Def
THMconcurrent_wfE,T,L:. S1,S2:Signature(E;T;L). S1 || S2 '
DISPrace_dfrace{<i:level>}(<E:E:*><T:T:*><L:L:*><Ach:Ach:*><Tor:Tor:*>) == <Ach> <Tor> <Ach:Ach:*> <Tor:Tor:*>== <Ach> <Tor>
ABSraceAch Tor == Ach || Tor t0 = t0 (Tor.t1 < Ach.t1 (t:T (t0 < t t Ach.t1 Ach.d t = Tor.d t (s:T. t0 s s < t (Ach.d s) < (Tor.d s))) Def t))
THMrace_wfE,T,X:. Ach,Tor:Signature(E;T;X). Ach Tor '
DISPivp_dfIVP(<T:T:*><L:L:*><S:S:*>)== IVP(<S>) IVP(<S:S:*>)== IVP(<S>)
ABSivpIVP(S) == b,e:T. a:L. t0 b b < e e S.t1 (S.d b) < a a < (S.d e) Def b Def a Def e (t:T. b < t t < e S.d t = a Def t)
THMivp_wfE,T,L:. S:Signature(E;T;L). IVP(S)
THMsuccessorE,T,L:. Ach,Tor:Signature(E;T;L). u,w:T. Run(E;T;L;Ach) Run(E;T;L;Tor) Ach Tor IVP(Ach) Ach.d w = Tor.d w t0 u u < w (w Ach.t1 w Tor.t1) (Ach.d u) < (Tor.d u) Def u Def w (v:T. u < v v < w Def v)
THMsuccessor_ezE,T,L:. Ach,Tor:Signature(E;T;L). u,w:T. Run(E;T;L;Ach) Run(E;T;L;Tor) Ach Tor IVP(Ach) Ach.d w = Tor.d w t0 u u < w (w Ach.t1 w Tor.t1) (Ach.d u) < (Tor.d u) Def u Def w (v:T. u < v v < w Def v)
THMsequenceE,T,L:. Ach,Tor:Signature(E;T;L). w:T. Run(E;T;L;Ach) Run(E;T;L;Tor) Ach Tor IVP(Ach) Ach.d w = Tor.d w t0 < w (w Ach.t1 w Tor.t1) (s:T. t0 s s < w (Ach.d s) < (Tor.d s)) Def w (n: v:n T t0 = v 0 (i:(n - 1). (v i) < (v (i + 1))) (i:n. (v i) < w Def (v i) t0 (v i)))
THMsequence_ezE,T,L:. Ach,Tor:Signature(E;T;L). w:T. Run(E;T;L;Ach) Run(E;T;L;Tor) Ach Tor IVP(Ach) Ach.d w = Tor.d w t0 < w (w Ach.t1 w Tor.t1) (s:T. t0 s s < w (Ach.d s) < (Tor.d s)) Def w (n: v:n T t0 = v 0 (i:(n - 1). (v i) < (v (i + 1))) (i:n. (v i) < w Def (v i) t0 (v i)))
THMmult_transT:. R:T T . n:{2...}. v:n T. Trans(T;x,y.x R y) (i:(n - 1). (v i) R (v (i + 1))) (v 0) R (v (n - 1))
THMmult_trans_ezT:. R:T T . n:{2...}. v:n T. Trans(T;x,y.x R y) (i:(n - 1). (v i) R (v (i + 1))) (v 0) R (v (n - 1))
DISPtep_dfTEP(<E:E:*><T:T:*><S:S:*>)== TEP TEP== TEP
ABStepTEP == t:T. e:E. Def t I e t = time e
THMtep_wfE,T,L:. S:Signature(E;T;L). TEP
THMsign_t_ref_rel_transE,T,L:. S:Signature(E;T;L). u,v,w:T. Run(E;T;L;S) u v v w u w
THMsign_t_ref_rel_trans_ezE,T,L:. S:Signature(E;T;L). u,v,w:T. Run(E;T;L;S) u v v w u w
THMparadoxE,T,L:. Ach,Tor:Signature(E;T;L). (Run(E;T;L;Ach) Run(E;T;L;Tor)) Ach Tor Ach.t1 Tor.t1 IVP(Ach) TEP
THMparadox_ezE,T,L:. Ach,Tor:Signature(E;T;L). (Run(E;T;L;Ach) Run(E;T;L;Tor)) Ach Tor Ach.t1 Tor.t1 IVP(Ach) TEP

the other theories