Step * 1 1 2 of Lemma better-not-not-Ramsey


1. : ℕ ⟶ ℕ ⟶ ℙ
2. ∀[s:StrictInc]. ⇃(∃n,m,p,q:ℕ((n < m ∧ R[s n;s m]) ∧ p < q ∧ R[s p;s q])))
3. ∀s:StrictInc. ⇃(∃m:ℕ. ∃n,p:{m 1...}. (R[s m;s n] ∧ R[s m;s p])))
4. ¬(∀s:StrictInc. ∃n:ℕhomogeneous(R;n;s)))
5. ⇃(∀s:StrictInc. ∃m:ℕ. ∃n,p:{m 1...}. (R[s m;s n] ∧ R[s m;s p])))
⊢ False
BY
((MoveToConcl (-1) THEN Fold `not` 0)
   THEN RWO  "not-quotient-true" 0
   THEN Auto
   THEN RepeatFor (ParallelLast)
   THEN ExRepD) }

1
1. : ℕ ⟶ ℕ ⟶ ℙ
2. ∀[s:StrictInc]. ⇃(∃n,m,p,q:ℕ((n < m ∧ R[s n;s m]) ∧ p < q ∧ R[s p;s q])))
3. ∀s:StrictInc. ⇃(∃m:ℕ. ∃n,p:{m 1...}. (R[s m;s n] ∧ R[s m;s p])))
4. ∀s:StrictInc. ∃m:ℕ. ∃n,p:{m 1...}. (R[s m;s n] ∧ R[s m;s p]))
5. StrictInc
6. : ℕ
7. {m 1...}
8. {m 1...}
9. R[s m;s n]
10. ¬R[s m;s p]
⊢ ∃n:ℕhomogeneous(R;n;s))


Latex:


Latex:

1.  R  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
2.  \mforall{}[s:StrictInc].  \00D9(\mexists{}n,m,p,q:\mBbbN{}.  ((n  <  m  \mwedge{}  R[s  n;s  m])  \mwedge{}  p  <  q  \mwedge{}  (\mneg{}R[s  p;s  q])))
3.  \mforall{}s:StrictInc.  \00D9(\mexists{}m:\mBbbN{}.  \mexists{}n,p:\{m  +  1...\}.  (R[s  m;s  n]  \mwedge{}  (\mneg{}R[s  m;s  p])))
4.  \mneg{}(\mforall{}s:StrictInc.  \mexists{}n:\mBbbN{}.  (\mneg{}homogeneous(R;n;s)))
5.  \00D9(\mforall{}s:StrictInc.  \mexists{}m:\mBbbN{}.  \mexists{}n,p:\{m  +  1...\}.  (R[s  m;s  n]  \mwedge{}  (\mneg{}R[s  m;s  p])))
\mvdash{}  False


By


Latex:
((MoveToConcl  (-1)  THEN  Fold  `not`  0)
  THEN  RWO    "not-quotient-true"  0
  THEN  Auto
  THEN  RepeatFor  2  (ParallelLast)
  THEN  ExRepD)




Home Index