Axiom of Foundation

There is no chapter with that name in Halmos' book, so let Google be your friend and type "Axiom of Foundation". Then we find:

Every non-empty set $x$ contains some member $y$ such that $x$ and $y$ are disjoint sets. Every non-empty set is disjoint from at least one of its elements.

Some consequences:

No set is an element of itself
A set contains no infinitely descending (membership) sequence
Any set contains a (membership) minimal element
foundation states that every set can be built up from the empty set
[ ... ] least useful ingredient of ZFC

My first confrontation with the Axiom of Foundation has been when I tempted to argue that an element should be equal to the set containing only that element. Because what would be the difference between an object and an object with an abstract (i.e. invisible) envelope surrounding it? This has been called the "ZFC Killer Axiom" (but only by this author)-: $$ a = \{ a \} $$ Adding it to ZFC is indeed disastrous. It's killing power comes from the fact that it is in direct conflict with the axiom of Foundation. But it's much worse than this: $$ \{\} = 0 \quad \Longrightarrow \quad 0 = \{0\} = 1 $$ Do we have to proceed? One can easily prove herefrom that every number is zero. Thus $a = \{ a \}$ does not only kill (Implementable) Set Theory, but all Natural numbers as well - they become zero - and therefore it kills All Mathematics. Who said that Foundation is generally considered as the 'least useful ingredient of ZFC' .. ?
Let's start with a couple of examples, to prove the validity of the axiom within Abian's "simple model" / our implementable set theory. $$ S = \{0,1,2,3,4,5\} $$ And examine Foundation: \begin{eqnarray*} 0 \cap S = \{\} \cap S = \emptyset\\ 1 \cap S = \{0\} \cap S = \{0\} = 1 \\ 2 \cap S = \{1\} \cap S = \{1\} = 2 \\ 3 \cap S = \{0,1\} \cap S = \{0,1\} = 3 \\ 4 \cap S = \{2\} \cap S = \{2\} = 4 \\ 5 \cap S = \{2,0\} \cap S = \{2,0\} = 5 \end{eqnarray*} There is only one element disjoint from the set, namely $0$ (because it's empty from itself). Therefore let's drop that first element: $$ S = \{1,2,3,4,5\} $$ And examine Foundation again: \begin{eqnarray*} 1 \cap S = \{0\} \cap S = \{\} = \emptyset\\ 2 \cap S = \{1\} \cap S = \{1\} = 2 \\ 3 \cap S = \{0,1\} \cap S = \{1\} = 2 \\ 4 \cap S = \{2\} \cap S = \{2\} = 4 \\ 5 \cap S = \{2,0\} \cap S = \{2\} = 4 \end{eqnarray*} So again there is only one element disjoint from the set, namely $1$ .
The following function, named $^2log$ and coded as below in Delphi Pascal, is essential for the rest of our argument. The function $^2log$ essentially determines the position of the leftmost bit in an integer $\ge 0$.

function log2(n : integer) : integer;
{
  Logarithm base 2
  ---------------- }
var
  k : integer;
begin
  log2 := 0;
  if n < 2 then Exit;
  k := 0;
  while n > 0 do
  begin
    n := n shr 1 ; k := k + 1;
  end;
  log2 := k-1;
end;

Lemma. $^2log(n) < n \quad \mbox{for each integer} \; n \ge 0$

Theorem. The minimal element in a set, when implemented as a natural array, is always disjoint from the set.

Proof. This is a direct consequence of the above lemma: the leftmost bit position of an integer $\ge 0$ has a numeric value which is always less than the numeric value of the integer itself.
This completes the proof, of the assertion that the axiom of Foundation is just a Theorem in our implementable set theory.