### Nuprl Lemma : no-excluded-middle-quot-true1

`¬(∀P:ℙ. ⇃(P ∨ (¬P)))`

Proof

Definitions occuring in Statement :  quotient: `x,y:A//B[x; y]` prop: `ℙ` all: `∀x:A. B[x]` not: `¬A` or: `P ∨ Q` true: `True`
Definitions unfolded in proof :  not: `¬A` implies: `P `` Q` equiv_rel: `EquivRel(T;x,y.E[x; y])` and: `P ∧ Q` refl: `Refl(T;x,y.E[x; y])` all: `∀x:A. B[x]` true: `True` member: `t ∈ T` squash: `↓T` or: `P ∨ Q` uall: `∀[x:A]. B[x]` prop: `ℙ` false: `False` sym: `Sym(T;x,y.E[x; y])` trans: `Trans(T;x,y.E[x; y])` so_lambda: `λ2x y.t[x; y]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` so_apply: `x[s1;s2]` uimplies: `b supposing a` subtype_rel: `A ⊆r B` so_lambda: `so_lambda(x,y,z.t[x; y; z])` so_apply: `x[s1;s2;s3]`
Lemmas referenced :  istype-base has-value_wf_base istype-void squash_wf true_wf not-has-value-decidable-quot all_wf base_wf quotient_wf or_wf not_wf equiv_rel_true quotient-dep-function-subtype
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaFormation_alt,  cut independent_pairFormation introduction natural_numberEquality sqequalRule imageMemberEquality hypothesisEquality thin baseClosed sqequalHypSubstitution hypothesis imageElimination extract_by_obid Error :functionIsType,  Error :unionIsType,  Error :universeIsType,  isectElimination because_Cache Error :inhabitedIsType,  Error :lambdaEquality_alt,  closedConclusion independent_isectElimination universeEquality dependent_functionElimination rename independent_functionElimination voidElimination applyEquality

Latex:
\mneg{}(\mforall{}P:\mBbbP{}.  \00D9(P  \mvee{}  (\mneg{}P)))

Date html generated: 2019_06_20-PM-00_32_39
Last ObjectModification: 2018_10_16-PM-02_41_49

Theory : quot_1

Home Index