|
OK, I think I see what I did wrong. [itex](P\land Q)\Rightarrow R[/itex] is equivalent to [itex]\lnot R\Rightarrow (\lnot P\land Q)\lor(P\land\lnot Q)[/itex], and you can't just drop one of the terms on the right in the last expression, which is essentially what I did. So let's go back to the implication that I want to rewrite:
[tex](I\subset\tau)\ \land\ \bigg(\bigcup_{i\in I}i\supset K\bigg)\Rightarrow\exists I_0(I_0\subset I,\ |I_0|<\infty,\ \bigcup_{i\in I_0}i\supset K)[/tex]
It implies several different things, one of which is
[tex]\bigg(\forall I_0(I_0\subset I,\ |I_0|<\infty) \bigcap_{i\in I_0}F_i\cup K\neq\emptyset\bigg)[/tex]
[tex]\Rightarrow \bigg((I\not\subset\tau)\land\bigg(\bigcup_{i\in I}i\supset K\bigg)\bigg)\lor\bigg((I\subset\tau)\land\bigg(\bigcap_{i\in I}F_i\cup K\neq\emptyset\bigg)\bigg)[/tex]
And this implies
[tex](I\subset\tau)\land\bigg(\forall I_0(I_0\subset I,\ |I_0|<\infty) \bigcap_{i\in I_0}F_i\cup K\neq\emptyset\bigg) \Rightarrow \bigcap_{i\in I}F_i\cup K\neq\emptyset[/tex]
Alternatively:
[tex]\forall I\bigg((I\subset\tau)\land\bigg(\forall I_0(I_0\subset I,\ |I_0|<\infty) \bigcap_{i\in I_0}F_i\cup K\neq\emptyset\bigg)\bigg)\quad \bigcap_{i\in I}F_i\cup K\neq\emptyset[/tex]
This is the expression I want. I thought it would be possible to obtain it in a way that corresponds to [itex]A\Rightarrow B[/itex] if and only if [itex]\lnot B\Rightarrow\lnot A[/itex], but it was more difficult than that.
|