Proving a closed form is true on finite domain

Question

I have a question about a variation of the content in this answer: https://math.stackexchange.com/a/694319/418401

It states (variated) that: $$ (\forall x)(\forall y)(\forall z) [ \lnot A(x,x)\land (A(x,y)\land A(y,z) \rightarrow A(x,z) ) \land (A(x,y) \lor A(y,x))] \land (\forall y)(\exists x)\lnot A(y,x) $$

This sentence must be false for all finite domains, but is true for some infinite domain (indeed, take the set of integers and define $A(y,x)$ as $y > x$, then this implication is true).

However, how can I proof that the form is false for a domain with $n$ elements? Then, by the last part of the disjunction, for every $y$, there exist $0 < k \leq n$ elements $x_k$ where $A(y,x_k)$ is true. Also, there are $i= n-k$ elements $x_i$ where $A(y,x_i)$ is false. But this doesn't say anything about the part of the form that says $(A(x,y) \land A(y,x))$ except that $A(x,y)$ must be true for some $x,y$..

Note that this is the negation of the form $$ (\forall x)(\forall y)(\forall z) [ \lnot A(x,x)\land (A(x,y)\land A(y,z) \rightarrow A(x,z) ) \land (A(x,y) \lor A(y,x))] \implies (\exists y)(\forall x)A(y,x) $$ Maybe we must proof that this is always true, but then again I can't make the next step in my thinking.

Answer 1

First of all: the statement as you have it can be true for any domain, finite, or infinite. ... That second part $(\forall y)(\exists x)\lnot A(y,x)$ is trivially true once you already have from the first part that $(\forall x) \neg A(x,x)$

So ... I am fairly certain that the statement should be:

$$ (\forall x)(\forall y)(\forall z) [ \lnot A(x,x)\land (A(x,y)\land A(y,z) \rightarrow A(x,z) ) \land (A(x,y) \lor A(y,x))] \land (\forall y)(\exists x)A(x,y) $$

Now: the first part of the sentence states that $A$ is a total order: $A$ is irreflexive, transitive, and total. What this means is that all the objects in the domain can be 'lined up' from left to right, where for any object $x$ and any object $y$: $x$ is to the left of $y$ if and only if $A(x,y)$ (and so of course you can do this for any domain, finite, or infinite, which is again why your original statement can be made true for any size domain)

So: if you have a finite number of objects in your domain, then you must have a 'left most' (or 'smallest') object with no further object to the left of it. Hence, $(\forall y)(\exists x)A(x,y)$ will have to be false if $ (\forall x)(\forall y)(\forall z) [ \lnot A(x,x)\land (A(x,y)\land A(y,z) \rightarrow A(x,z) ) \land (A(x,y) \lor A(y,x))]$ is true ... if you have a finite domain. For infinite domain, we can of course consider something like the integers, that can be ordered using $<$, but where there is no 'smallest' (or 'biggest') object.

EDIT

I see that you try to understand why

$$ (\forall x)(\forall y)(\forall z) [ A(x,x)\land (A(x,y)\land A(y,z) \rightarrow A(x,z) ) \land (A(x,y) \lor A(y,x))] \rightarrow (\exists y)(\forall x)A(y,x) $$

has to be true for any finite sized domain.

Hint: try induction to show that for any $n \ge 1$: this claim has to be true for any domain with $n$ objects. Here's a start:

Base: 1 object (the base is 1 ... in logic we typically assume the domain is non-empty ... in fact, if the domain were empty, the claim would be false!).

OK, call this object $a$. For the antecedent to be true we must have $A(a,a)$ ... but asince $a$ is the only object from the domain we have $(\exists y)(\forall x)A(y,x)$

Step: Take any $n \ge 1$. Suppose claim is true for this $n$ (inductive hypothesis)

Now show it is true for $n+1$. So take domain with $n+1$ objects. Put 1 object (call it a) aside. Apply inductive hypothesis on the remaining $n$ ... and I think you can take it from here ...

Answer 2

Let $A$ be a relation as stated, and construct $B$ so that $B(x,x)$ for all $x$, and otherwise $B(x,y)$ if and only if $A(x,y)$. We show that $B$ is a nonwellfounded total order.

$B$ is reflexive by definition.

It's transitive. To show that if $B(x,y)$ and $B(y,z)$ then $B(x,z)$:

• if $x,y,z$ are all different then we just use $A$'s transitivity;
• if $x=z$ then it's vacuous;
• if $x=y \not = z$ then it's trivial;
• if $x \not = y$ and $y=z$ then it's trivial.

It's antisymmetric: if $x \not = y$, and $B(x,y)$, then $A(x,y)$ and so $\neg A(y,x)$, so $\neg B(y,x)$.

It's total: if $x \not = y$ and $\neg B(x,y)$, then $\neg A(x,y)$ and so $A(y,x)$, and hence $B(y,x)$.

The final criterion for $A$ tells us that $(\forall y)(\exists x) \neg A(y,x)$; since $A$ is antireflexive, we know that for any given $y$, the corresponding $x$ is not equal to $y$. But then $\forall y \exists x: \neg B(y,x)$ and hence $\forall y \exists x: B(x,y)$.

So $B$ is a nonwellfounded total order; and they only exist on infinite sets. Indeed, if $B$ is a nonwellfounded total order on a finite set, then pick any element, and iterate the procedure "take some nonequal previous element" (which exists because $B$ is nonwellfounded, and doesn't require choice because the underlying set is finite). By antisymmetricity, we can't pick the same element twice; so this procedure must terminate after finitely many steps, which is a contradiction to the fact that every element has a smaller element.

Answer 3

You can try a simple case with three elements: $1,2,3$ and $>$ ($\ge$ is ruled out by the first clause : $¬A(x,x)$).

We have $3>2$ and $2>1$ and also $3>1$ by the 2nd clause (transitivity)

The 3rd clause is satisfied, because every pair is "comparable".

We are left with the "tricky" part:

$(\forall y)(\exists x) \lnot (y > x)$

and this is trivially satisfied by the fact that:

$\lnot (3 > 3), \ldots$

---

A similar formula which has no finite models is:

$(∀x)(∀y)(∀z)[¬A(x,x)∧(A(x,y)∧A(y,z) → A(x,z)) ∧ (∀x)(∃y)A(x,y)]$

In order to show that it is false in every finite domain, we can use again a simple case: $1,2,3$ and $<$.

All the reasoning above works well except for the last clause: $(∀x)(∃y)(x < y)$. What happens with $3$ ?

We have no "successor" for it in the (finite) chain and if we try a "loop", i.e. we set: $3 < 1$; but by transitivity we end with $1 < 1$, which is not.