Proving a closed form is true on finite domain 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.
 A: 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 ...
A: 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.
A: 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.
