Nuprl Lemma : K_uforces_quant_lemma
∀body,z,isall,K:Top.
(K-uforces(K;mFOquant(isall;z;body)) ~ if isall
then λi,a. ∀[j:World]. ∀v:Dom(j). (K-uforces(K;body) j a[z := v]) supposing i ≤ j
else λi,a. ∃v:Dom(i). (K-uforces(K;body) i a[z := v])
fi )
Proof
Definitions occuring in Statement :
K-uforces: K-uforces(K;fmla),
K-dom: Dom(i),
K-le: i ≤ j,
K-world: World,
mFOquant: mFOquant(isall;var;body),
update-assignment: a[x := v],
ifthenelse: if b then t else f fi ,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
top: Top,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
apply: f a,
lambda: λx.A[x],
sqequal: s ~ t
Definitions unfolded in proof :
all: ∀x:A. B[x],
K-uforces: K-uforces(K;fmla),
mFOquant: mFOquant(isall;var;body),
mFOL_ind: mFOL_ind,
member: t ∈ T
Lemmas referenced :
istype-top
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
cut,
sqequalRule,
hypothesis,
inhabitedIsType,
hypothesisEquality,
introduction,
extract_by_obid
Latex:
\mforall{}body,z,isall,K:Top.
(K-uforces(K;mFOquant(isall;z;body)) \msim{} if isall
then \mlambda{}i,a. \mforall{}[j:World]. \mforall{}v:Dom(j). (K-uforces(K;body) j a[z := v]) supposing i \mleq{} j
else \mlambda{}i,a. \mexists{}v:Dom(i). (K-uforces(K;body) i a[z := v])
fi )
Date html generated:
2019_10_16-AM-11_45_37
Last ObjectModification:
2018_10_16-AM-10_52_49
Theory : minimal-first-order-logic
Home
Index