# 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?

• No, not at all. What is this $x$ about? – dfeuer Dec 9 '13 at 13:57
• It means that for any element in the set I can find at least 2 other elements which are different from each other and from x, wouldn't that mean the set has 3 elements or more? – user106421 Dec 9 '13 at 13:59
• I see now I wrote 2 in the topic question, where I meant to write 3, is it correct now? – user106421 Dec 9 '13 at 14:00

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

• Clear and Complete + 1 – Amzoti Dec 10 '13 at 1:54

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.

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.

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.

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

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)
& union-disjoint(paper1,paper2)
& my-minus-one(N,M))

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

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

• As you introduce your post with "use universal and existential quantifiers in FOL", you might make the content clearer by introducing mathematical notation with $\LaTeX$ syntax. – hardmath Jul 29 '17 at 22:23