First order logic. Describe that a set has more than 2 elements.

Question

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?

Answer 1

• 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)$$

Answer 2

You want to claim the existence of three elements that are not equal. Then $\exists x\exists y\exists z$ claims they exist. You already seem to have a handle on claiming they are not equal.

Answer 3

This sentence would be true in the empty domain. Provided you've excluded that via convention, it is fine, though quite laborious to prove directly from the definition of truth. An easier example would be to replace the universal quantifier with an additional existential one.

Answer 4

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) <->  (N > 1)  &  (M = N-1)

forall x. same(x,x)

% confirms non empty domain.
legal-pad(paper) <-> min-elements(1, paper)

exactly-n-elements(1,paper) <->
(exists paper word.  
    (   written-on(word,paper) 
      & ~(exists other-word.
           (  written-on(other-word,paper) 
             & ~same(other-word,word)))))

exactly-n-elements(2,paper) <->
(exists paper word1 word2. 
  (  written-on(word1,paper) 
   & written-on(word2,paper) 
   & ~same(word1,word2)   
   & ~ (exists other-word. 
         (   written-on(other-word,paper) 
          & ~same(other-word,word1) 
          & ~same(other-word,word2)))))

exactly-n-elements(N,paper) <-> 
   range-elements(N,N,paper)  

range-elements(N,M,paper) <-> 
 (exists paper.
  ( min-elements(N,paper) 
    & max-elements(M,paper)))

min-elements(1,paper) <-> 
 (exists paper word1.
     (written-on(word1,paper)))

min-elements(2,paper) <->
 (exists paper word1 word2. 
   (  written-on(word1,paper) 
    & written-on(word2,paper)
    & ~same(word1,word2)))

max-elements(2,paper) <->  
(exists paper word1 word2. 
   (  written-on(word1,paper) 
    & written-on(word2,paper) 
    &  ~(exists other-word.
          (  written-on(other-word,paper) 
            & ~same(other-word,word1)
            & ~same(other-word,word2)))))

% exists a paper with no elements
exactly-n-elements(0,paper) <->
  (exists paper
     ~(exists word1. written-on(word1,paper)))

max-elements(1,paper) <->
 exactly-n-elements(0,paper) v exactly-n-elements(1,paper)

containsAtLeastOneUnique(paper1,paper2) <->
  (exists word. (written-on(word,paper1) -> ~written-on(word,paper2)))

disjoint(paper1,paper2) <->
  ~(exists word. (written-on(word,paper1) & written-on(word,paper2)))

subset(paper1,paper2) <-> 
    (forall word.
      written-on(word,paper1) -> written-on(word,paper2) )

union(paper1,paper2,paper) <->
 (forall word.
   (written-on(word,paper) <-> 
       (written-on(word,paper1) v written-on(word,paper2))))

union(paper1,paper2,paper) <->
  (exists scratchpad. 
      union(paper1,paper2,scratchpad)
     & ~containsAtLeastOneUnique(paper,scratchpad))


union-disjoint(paper1,paper2,paper) <-> 
   (   union(paper1,paper2,paper) 
     & disjoint(paper1,paper2))


min-elements(4,paper) <-> 
  (exists paper1 paper2.
     min-elements(2,paper1) 
   & min-elements(2,paper2)
   & union-disjoint(paper1,paper2))

min-elements(N,paper) <-> 
  (exists paper1 paper2.
     min-elements(1,paper1) 
   & min-elements(M,paper2)
   & legal-pad(paper2)
   & union-disjoint(paper1,paper2)
   & my-minus-one(N,M))


max-elements(N,paper) <-> 
  (exists paper1 paper2.
     max-elements(1,paper1) 
   & max-elements(M,paper2)
   & legal-pad(paper1)
   & legal-pad(paper2)
   & union-disjoint(paper1,paper2)
   & my-minus-one(N,M))


equal_papers_v2(paper1,paper2) <->
   ( ~containsAtLeastOneUnique(paper1,paper2)
     & ~containsAtLeastOneUnique(paper2,paper1)
     & legal-pad(paper1)
     & legal-pad(paper2))

equal_papers_v1(paper1,paper2) <->
 ( legal-pad(paper1)
   & (forall word. 
      (written-on(word,paper1) <-> written-on(word,paper2))))