A reverse characterization of „property P can be checked on its finite subsets“ (motivation: $\mathscr L$ = sets of n-ary formulas under signature $τ$, $P$ = satisfiability wrt a theory $T$)
Let $\mathscr L = (0,1,\wedge,\vee)$ be a bounded atomic lattice, whose elements will be called finite if they are the join of finitely many atoms.
Let's say a property $P$ on elements in $L$ can be checked finitely if

*

*it is downward closed and

*for all $M \in \mathscr L$, $P(M)$ holds if and only if $P(F)$ holds for every finite $F \leq M$.

So given any $M$ satisfying property $P$, we can associate to it the set $\mathscr F_M := \{F\mid F\text{ finite, }F\leq M\}$, every element of which satisfies $P$.  Of course, $M = \bigvee \mathscr F$.
Question: If we instead start from an arbitrary set of finite elements $\mathscr F$, all of which satisfy $P$, what does $ℱ$ have to fulfill in addition such that $\bigvee \mathscr F$ satisfies $P$?
 A: I unfortunately do not think much can be said in general. If $\mathscr{L}$ is infinitely distributive, then we have the following criterion: $\bigvee\mathscr{F}$ satisfies $P$ if and only if $\bigvee\mathscr{F}_0$ satisfies $P$ for every finite subset $\mathscr{F}_0\subseteq\mathscr{F}$. Since $P$ is downward closed, the "only if" direction is clear. For the "if" direction, suppose that $\bigvee\mathscr{F}$ fails to satisfy $P$. Then, since $P$ can be checked finitely, there exists a finite $F\leqslant\bigvee\mathscr{F}$ not satisfying $P$. Let $a_1,\dots,a_n\in\mathscr{L}$ be atoms such that $F=\bigvee_{i=1}^n a_i$. Since $F\leqslant\bigvee\mathscr{F}$, or in other words $F\wedge\bigvee\mathscr{F}=F$, by distributivity and the fact that the $a_i$ are atoms, there must exist some $b_1,\dots,b_n\in\mathscr{F}$ such that $a_i\leqslant b_i$ for each $i$.  Now $F\leqslant \bigvee_{i=1}^n b_i$, so by downward closure $\bigvee_{i=1}^n b_i$ fails to satisfy $P$, whence taking $\mathscr{F}_0=\{b_1,\dots,b_n\}$ gives a finite subset of $\mathscr{F}$ whose join does not satisfy $P$, as desired.
So, for example, $\bigvee\mathscr{F}$ will satisfy $P$ if $\mathscr{F}$ is closed under $\vee$. This is precisely the situation with the set $\mathscr{F}_M$ that you describe, which is closed under $\vee$ for any $M\in\mathscr{L}$. But we unfortunately cannot do much better than that; for instance, it is not in general even enough to ask that $\bigvee\mathscr{F}_0$ satisfies $P$ for every proper subset $\mathscr{F}_0\subset\mathscr{F}$! Indeed, let $X$ be any finite set of size $>1$, and let $\mathscr{L}$ be the power set of $X$. Then the property $P$ of being a proper subset of $X$ can be checked finitely. However, if $\mathscr{F}\subset\mathscr{L}$ is the set of singleton subsets of $X$, then $\bigvee\mathscr{F}_0$ satisfies $P$ for every proper subset $\mathscr{F}_0\subset\mathscr{F}$, even though $\bigvee\mathscr{F}$ does not satisfy $P$.

If $\mathscr{L}$ is not distributive, then things can get even worse; it is possible to have a case where $\mathscr{F}$ is infinite and $\bigvee\mathscr{F}_0$ satisfies $P$ for every proper subset $\mathscr{F}_0\subset\mathscr{F}$, but $\bigvee\mathscr{F}$ nonetheless fails to satisfy $P$. For instance, let $\mathscr{L}$ be the union of the power set of an infinite set $X$ with a single new element $\star$, where $\star\wedge S=\varnothing$ for each $S\neq X$ and $\star\wedge X=\star$. Then, taking $P$ to hold precisely on $L\setminus\{X,\star\}$, $P$ can be checked finitely. However, if $\mathscr{F}$ is the set of singleton subsets of $X$, then $\bigvee\mathscr{F}_0$ satisfies $P$ for every proper subset $\mathscr{F}_0\subset\mathscr{F}$, even though $\bigvee\mathscr{F}=X$ does not.
