First order logic. Describe that a set has more than 2 elements. I would like to describe that a set has at least 3 elements using first order logic, would this be a valid way to do that?

$\forall x\exists y\exists z(\neg(x=y)\wedge\neg(x=z)\wedge\neg(y=z))$

I can't find this example anywhere in my book, but it seems to do what I want, comments?
You need to assert the existence of three elements $x, y, z$ (so $\forall x$ is incorrect), and
you need to assert something about those existent elements, otherwise you are only saying "there exists at least three elements $x, y, z$". Presuming you want to assert that they all belong to some set we'll call $A$, then 
you need a proposition, e.g., $A(x)$ to denote $x \in A$, where $A$ is some set.

Without the proposition, you are claiming only the existence of at least three elements, but nothing about their being contained in some set.


$$\exists x \,\exists y\, \exists z\,\Big(A(x) \land A(y) \land A(z) \land \;\lnot(x= y )\;\land \;\lnot (y= z) \;\land\; \lnot(x= z)\Big)$$

Or, simply, $$\exists x \,\exists y \,\exists z\,\Big(x\in A \;\land\; y\in A\; \land \;z\in A\;\land\; \lnot(x= y )\;\land \;\lnot (y= z) \;\land\; \lnot(x= z)\Big)$$
If we may use universal and existential quantifiers in FOL, then here are some fun axiomatizations. 

#import: written-on(word,paper).


my-minus-one(N,M) &lt;-&gt;  (N &gt; 1)  &amp;  (M = N-1)

forall x. same(x,x)

% confirms non empty domain.
legal-pad(paper) &lt;-&gt; min-elements(1, paper)

exactly-n-elements(1,paper) &lt;-&gt;
(exists paper word.  
    (   written-on(word,paper) 
      &amp; ~(exists other-word.
           (  written-on(other-word,paper) 
             &amp; ~same(other-word,word)))))

exactly-n-elements(2,paper) &lt;-&gt;
(exists paper word1 word2. 
  (  written-on(word1,paper) 
   &amp; written-on(word2,paper) 
   &amp; ~same(word1,word2)   
   &amp; ~ (exists other-word. 
         (   written-on(other-word,paper) 
          &amp; ~same(other-word,word1) 
          &amp; ~same(other-word,word2)))))

exactly-n-elements(N,paper) &lt;-&gt; 
   range-elements(N,N,paper)  

range-elements(N,M,paper) &lt;-&gt; 
 (exists paper.
  ( min-elements(N,paper) 
    &amp; max-elements(M,paper)))

min-elements(1,paper) &lt;-&gt; 
 (exists paper word1.
     (written-on(word1,paper)))

min-elements(2,paper) &lt;-&gt;
 (exists paper word1 word2. 
   (  written-on(word1,paper) 
    &amp; written-on(word2,paper)
    &amp; ~same(word1,word2)))

max-elements(2,paper) &lt;-&gt;  
(exists paper word1 word2. 
   (  written-on(word1,paper) 
    &amp; written-on(word2,paper) 
    &amp;  ~(exists other-word.
          (  written-on(other-word,paper) 
            &amp; ~same(other-word,word1)
            &amp; ~same(other-word,word2)))))

% exists a paper with no elements
exactly-n-elements(0,paper) &lt;-&gt;
  (exists paper
     ~(exists word1. written-on(word1,paper)))

max-elements(1,paper) &lt;-&gt;
 exactly-n-elements(0,paper) v exactly-n-elements(1,paper)

containsAtLeastOneUnique(paper1,paper2) &lt;-&gt;
  (exists word. (written-on(word,paper1) -&gt; ~written-on(word,paper2)))

disjoint(paper1,paper2) &lt;-&gt;
  ~(exists word. (written-on(word,paper1) &amp; written-on(word,paper2)))

subset(paper1,paper2) &lt;-&gt; 
    (forall word.
      written-on(word,paper1) -&gt; written-on(word,paper2) )

union(paper1,paper2,paper) &lt;-&gt;
 (forall word.
   (written-on(word,paper) &lt;-&gt; 
       (written-on(word,paper1) v written-on(word,paper2))))

union(paper1,paper2,paper) &lt;-&gt;
  (exists scratchpad. 
      union(paper1,paper2,scratchpad)
     &amp; ~containsAtLeastOneUnique(paper,scratchpad))


union-disjoint(paper1,paper2,paper) &lt;-&gt; 
   (   union(paper1,paper2,paper) 
     &amp; disjoint(paper1,paper2))


min-elements(4,paper) &lt;-&gt; 
  (exists paper1 paper2.
     min-elements(2,paper1) 
   &amp; min-elements(2,paper2)
   &amp; union-disjoint(paper1,paper2))

min-elements(N,paper) &lt;-&gt; 
  (exists paper1 paper2.
     min-elements(1,paper1) 
   &amp; min-elements(M,paper2)
   &amp; legal-pad(paper2)
   &amp; union-disjoint(paper1,paper2)
   &amp; my-minus-one(N,M))


max-elements(N,paper) &lt;-&gt; 
  (exists paper1 paper2.
     max-elements(1,paper1) 
   &amp; max-elements(M,paper2)
   &amp; legal-pad(paper1)
   &amp; legal-pad(paper2)
   &amp; union-disjoint(paper1,paper2)
   &amp; my-minus-one(N,M))


equal_papers_v2(paper1,paper2) &lt;-&gt;
   ( ~containsAtLeastOneUnique(paper1,paper2)
     &amp; ~containsAtLeastOneUnique(paper2,paper1)
     &amp; legal-pad(paper1)
     &amp; legal-pad(paper2))

equal_papers_v1(paper1,paper2) &lt;-&gt;
 ( legal-pad(paper1)
   &amp; (forall word. 
      (written-on(word,paper1) &lt;-&gt; written-on(word,paper2))))