Tychonoff and compactness (logic) and another small logic question It is claimed in some logic books that the compactness theorem of first-order logic can be proven using Tychnoff's theorem from topology.
Now, to me this feels very strange because I consider logic as something "lower" in the sense that the theorems of topology follow from the axioms and theorems in logic. How can we avoid circularities then?
Another small question I have is that if we have $A \iff B$ and we prove both directions with contraposition, does there exist a direct proof? You could say we could just follow the steps backwards, but is this always possible?
 A: When we study mathematical logic, we use the same mathematical methods that would be used to study any other area (algebra, analysis, topology, etc.).  This includes the use of set-theoretical techniques.  Otherwise, we would be needlessly hamstringing ourselves.  In principle, the results that we obtain could be built up entirely from primitive axioms, just like the rest of mathematics; but just like the rest of mathematics complete formalization is not usually the goal. 
However, even ignoring those practical considerations, it's not hard to see that none of the axioms of point set topology or set theory used in topology presuppose that the compactness theorem of logic holds. So there is no circularity if we use topological methods to prove the compactness theorem. 
A: For the second question, suppose that in some proof system you can prove $p(x) \Leftrightarrow q(x)$ for some expressions $p,q$, and only $p(x)\Rightarrow q(x)$ requires proof by contradiction. Then to prove $p(x) \land q(y) \Leftrightarrow q(x) \land p(y)$ you probably need proof by contradiction on both sides.
If you only know that $p(x) \Rightarrow q(x)$ requires proof by contradiction ($p(x) \Leftarrow q(x)$ not necessarily being true), then $p(x) \Rightarrow p(x) \land q(x)$ also probably requires proof by contradiction, and this time both sides are equivalent.
