Nuprl Lemma : K_forces_connect_lemma
∀u,v,knd,K:Top.
(K-forces(K;mFOconnect(knd;u;v)) ~ if knd =a "and" then λi,a. ((K-forces(K;u) i a) ∧ (K-forces(K;v) i a))
if knd =a "or" then λi,a. ((K-forces(K;u) i a) ∨ (K-forces(K;v) i a))
else λi,a. ∀j:{j:World| i ≤ j} . ((K-forces(K;u) j a) ⇒ (K-forces(K;v) j a))
fi )
Proof
Definitions occuring in Statement :
K-forces: K-forces(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,
top: Top,
all: ∀x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
lambda: λx.A[x],
token: "$token",
sqequal: s ~ t
Definitions unfolded in proof :
all: ∀x:A. B[x],
K-forces: K-forces(K;fmla),
mFOconnect: mFOconnect(knd;left;right),
mFOL_ind: mFOL_ind,
member: t ∈ T
Lemmas referenced :
top_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
sqequalRule,
inhabitedIsType,
hypothesisEquality,
universeIsType,
cut,
introduction,
extract_by_obid,
hypothesis
Latex:
\mforall{}u,v,knd,K:Top.
(K-forces(K;mFOconnect(knd;u;v)) \msim{} if knd =a "and"
then \mlambda{}i,a. ((K-forces(K;u) i a) \mwedge{} (K-forces(K;v) i a))
if knd =a "or" then \mlambda{}i,a. ((K-forces(K;u) i a) \mvee{} (K-forces(K;v) i a))
else \mlambda{}i,a. \mforall{}j:\{j:World| i \mleq{} j\} . ((K-forces(K;u) j a) {}\mRightarrow{} (K-forces(K;v) j a))
fi )
Date html generated:
2019_10_16-AM-11_45_07
Last ObjectModification:
2018_10_15-PM-06_44_02
Theory : minimal-first-order-logic
Home
Index