Nuprl Lemma : Peirce's-law-iff-xmiddle

[P,B:ℙ].  (((P  B)  P)  P) ⇐⇒ ∀[P,B:ℙ].  (P ∨ (P  B))


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] prop: iff: ⇐⇒ Q implies:  Q or: P ∨ Q
Definitions unfolded in proof :  iff: ⇐⇒ Q and: P ∧ Q implies:  Q uall: [x:A]. B[x] member: t ∈ T prop: so_lambda: λ2x.t[x] so_apply: x[s] rev_implies:  Q or: P ∨ Q guard: {T}
Lemmas referenced :  uall_wf or_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity independent_pairFormation lambdaFormation isect_memberFormation universeEquality cut instantiate lemma_by_obid sqequalHypSubstitution isectElimination thin sqequalRule lambdaEquality cumulativity functionEquality hypothesisEquality hypothesis independent_functionElimination inrFormation inlFormation because_Cache unionElimination

Latex:
\mforall{}[P,B:\mBbbP{}].    (((P  {}\mRightarrow{}  B)  {}\mRightarrow{}  P)  {}\mRightarrow{}  P)  \mLeftarrow{}{}\mRightarrow{}  \mforall{}[P,B:\mBbbP{}].    (P  \mvee{}  (P  {}\mRightarrow{}  B))



Date html generated: 2016_05_15-PM-03_19_03
Last ObjectModification: 2015_12_27-PM-01_03_37

Theory : general


Home Index