Nuprl Lemma : mFOL-sequent-evidence_transitivity1
From uniform evidence that hyps ⇒ x and uniform evidence that x ⇒ y
we construct uniform evidence that hyps ⇒ y.⋅
∀[hyps:mFOL() List]. ∀[x,y:mFOL()].
((∀[Dom:Type]. ∀[S:FOStruct(Dom)].
∀a:FOAssignment(Dom). (Dom,S,a |= mFOL-abstract(x) ⇒ Dom,S,a |= mFOL-abstract(y)))
⇒ mFOL-sequent-evidence(<hyps, x>)
⇒ mFOL-sequent-evidence(<hyps, y>))
Proof
Definitions occuring in Statement :
mFOL-sequent-evidence: mFOL-sequent-evidence(s),
mFOL-abstract: mFOL-abstract(fmla),
mFOL: mFOL(),
FOSatWith: Dom,S,a |= fmla,
FOStruct: FOStruct(Dom),
FOAssignment: FOAssignment(Dom),
list: T List,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
pair: <a, b>,
universe: Type
Lemmas :
tuple-type_wf,
map_wf,
mFOL_wf,
FOSatWith_wf,
mFOL-abstract_wf,
FOAssignment_wf,
FOStruct_wf,
mFOL-sequent-evidence_wf,
list_wf,
uall_wf,
all_wf
\mforall{}[hyps:mFOL() List]. \mforall{}[x,y:mFOL()].
((\mforall{}[Dom:Type]. \mforall{}[S:FOStruct(Dom)].
\mforall{}a:FOAssignment(Dom). (Dom,S,a |= mFOL-abstract(x) {}\mRightarrow{} Dom,S,a |= mFOL-abstract(y)))
{}\mRightarrow{} mFOL-sequent-evidence(<hyps, x>)
{}\mRightarrow{} mFOL-sequent-evidence(<hyps, y>))
Date html generated:
2015_07_17-AM-07_56_37
Last ObjectModification:
2015_01_27-AM-10_05_19
Home
Index