This non-implication, Form 76 \( \not \Rightarrow \) Form 1, whose code is 4, is constructed around a proven non-implication as follows:

  • An (optional) implication of code 1 or code 2 is given. In this case, it's Code 2: 9685, whose string of implications is:
    426 \(\Rightarrow\) 76
  • A proven non-implication whose code is 3. In this case, it's Code 3: 84, Form 426 \( \not \Rightarrow \) Form 1 whose summary information is:
    Hypothesis Statement
    Form 426 <p> If \((X,\cal T) \) is a first countable topological space and \((\cal B(x))_{x\in X}\) is a family such that for all \(x \in X\), \(\cal B(x)\) is a local base at \(x\), then there is a family \(( \cal V(x))_{x\in X}\) such that for every \(x \in X\), \(\cal V(x)\) is a countable local base at \(x\) and \(\cal V(x) \subseteq \cal B(x)\). </p>

    Conclusion Statement
    Form 1 <p> \(C(\infty,\infty)\):  The Axiom of Choice: Every  set  of  non-empty sets has a choice function. </p>

  • This non-implication was constructed without the use of this last code 2/1 implication

The conclusion Form 76 \( \not \Rightarrow \) Form 1 then follows.

Finally, the
List of models where hypothesis is true and the conclusion is false:

Name Statement

Edit | Back