Nuprl Lemma : K_uforces_connect_lemma
∀v,u,knd,K:Top.
(K-uforces(K;mFOconnect(knd;u;v)) ~ if knd =a "and" then λi,a. ((K-uforces(K;u) i a) ∧ (K-uforces(K;v) i a))
if knd =a "or" then λi,a. ((K-uforces(K;u) i a) ∨ (K-uforces(K;v) i a))
else λi,a. ∀[j:World]. (K-uforces(K;u) j a) ⇒ (K-uforces(K;v) j a) supposing i ≤ j
fi )
Proof
Definitions occuring in Statement :
K-uforces: K-uforces(K;fmla),
K-le: i ≤ j,
K-world: World,
mFOconnect: mFOconnect(knd;left;right),
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
top: Top,
all: ∀x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
apply: f a,
lambda: λx.A[x],
token: "$token",
sqequal: s ~ t
Definitions unfolded in proof :
all: ∀x:A. B[x],
K-uforces: K-uforces(K;fmla),
mFOconnect: mFOconnect(knd;left;right),
mFOL_ind: mFOL_ind,
member: t ∈ T
Lemmas referenced :
istype-top
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
sqequalRule,
inhabitedIsType,
hypothesisEquality,
cut,
introduction,
extract_by_obid,
hypothesis
Latex:
\mforall{}v,u,knd,K:Top.
(K-uforces(K;mFOconnect(knd;u;v)) \msim{} if knd =a "and"
then \mlambda{}i,a. ((K-uforces(K;u) i a) \mwedge{} (K-uforces(K;v) i a))
if knd =a "or" then \mlambda{}i,a. ((K-uforces(K;u) i a) \mvee{} (K-uforces(K;v) i a))
else \mlambda{}i,a. \mforall{}[j:World]. (K-uforces(K;u) j a) {}\mRightarrow{} (K-uforces(K;v) j a) supposing i \mleq{} j
fi )
Date html generated:
2019_10_16-AM-11_45_32
Last ObjectModification:
2018_10_16-AM-11_00_04
Theory : minimal-first-order-logic
Home
Index