Is this property of derivation relation equivalent to idempotence? In Herre & Schroeder-Heister's "Formal Languages and Systems", on p6,

A formal system is based on a formal language L, endowing it with a consequence
operation C. This operation C can be speciﬁed at diﬀerent levels of abstraction. In the
most general sense C is just an arbitrary function transforming subsets of L into subsets
of L: $2^L\to 2^L$.
$$X ⊆ C(X)\text{ (inclusion)}$$
$$C(C(X)) ⊆ C(X)\text{ (idempotence)}$$
$$X ⊆ Y ⇒ C(X) ⊆ C(Y )\text{ (monotonicity)}$$
$$C(X) ⊆ \cup \{C(Y ) : Y ⊆ X\text{, $Y$ ﬁnite}\}\text{ (compactness)}$$


Equivalently, formal systems can be described by a consequence relation $X \vdash A$
between subsets of L and expressions of L. The four conditions mentioned then become
$$X \cup \{A\} \vdash A$$ $$X \vdash A ⇒ X \cup Y \vdash A$$
$$(X \vdash A \text{ for all $A ∈ Y$ and $Y \cup Z \vdash B$}) ⇒ X \cup Z \vdash B$$ $$X \vdash A ⇒ Y \vdash A \text{ for some ﬁnite $Y ⊆ X$}$$

Is it correct that

*

*the first of the last four is equivalent to inclusion?

*the second is equivalent to monotonicity?

*the fourth is equivalent to compactness?

*how is the third derived from the first four? Is it equivalent to idempotence alone?

Thanks.
p.s.: It doesn't stop me continuing reading the rest. I think I was just curious and unable to understand it on my own.
 A: The idea is that $X \vdash A \longleftrightarrow A \in \mathrm{C}(X)$; that is, a formula $A$ is derivable from $X$ if it is in the set of consequences of $X$.
In this way, we can translate the latter set of four into expressions
$$A \in \mathrm{C}(X \cup \{A\})\\
A \in \mathrm{C}(X) \longrightarrow A \in \mathrm{C}(X \cup Y)\\
(\forall A : A \in Y : A \in \mathrm{C}(X)) \wedge B \in \mathrm{C}(Y \cup Z) \longrightarrow B \in \mathrm{C}(X \cup Z)\\
A \in \mathrm{C}(X) \longrightarrow (\exists Y : \mathop{\mathrm{finite}} Y \wedge Y \subseteq X : A \in \mathrm{C}(Y))$$
Now, by starting with $X = \emptyset$, by repeated application of the first of the above, it follows that $Y \subseteq \mathrm{C}(Y)$, giving the first condition.
In the opposite direction, $X \subseteq \mathrm{C}(X)$ is equivalent to $A \in X \Longrightarrow A \in \mathrm{C}(X)$, which, taking $X = Y \cup \{A\}$ implies that $A \in \mathrm{C}(Y \cup \{A\})$.
For the second condition, $X \subseteq Y$ is the same as saying that, letting $Z = Y \setminus X$, $Y = X \cup Z$. Using this, monotonicity is equivalent to
$$\mathrm{C}(X) \subseteq \mathrm{C}(X \cup Z)$$
and then by set arithmetic that is equivalent to
$$A \in \mathrm{C}(X) \longrightarrow A \in \mathrm{C}(X \cup Z)$$
showing it to be equivalent to the second condition.
For the third condition,
$(\forall A : A \in Y : A \in \mathrm{C}(X))$
is the same as
$Y \subseteq \mathrm{C}(X)$,
and
$B \in \mathrm{C}(Y \cup Z) \longrightarrow B \in \mathrm{C}(X \cup Z)$
is equivalent to
$\mathrm{C}(Y \cup Z) \subseteq \mathrm{C}(X \cup Z)$. Thus it can be rewritten to
$$Y \subseteq \mathrm{C}(X) \longrightarrow \mathrm{C}(Y \cup Z) \subseteq \mathrm{C}(X \cup Z).$$
Taking $Y = \mathrm{C}(X)$ and $Z = \emptyset$, this implies $\mathrm{C}(\mathrm{C}(X)) \subseteq \mathrm{C}(X)$.
The other direction is a bit more complicated.
$$\begin{aligned}
  Y \subseteq \mathrm{C}(X) &\Longrightarrow
    Y \cup Z \subseteq \mathrm{C}(X) \cup Z
    &\text{(set arithmetic)}\\
  &\Longrightarrow
    Y \cup Z \subseteq \mathrm{C}(X) \cup \mathrm{C}(Z)
    &\text{(inclusion + set arith.)}\\
  &\Longrightarrow
    Y \cup Z \subseteq \mathrm{C}(X \cup Z)
    &\text{(monotonicity + set arith.)}\\
  &\Longrightarrow
    \mathrm{C}(Y \cup Z) \subseteq \mathrm{C}(\mathrm{C}(X \cup Z))
    &\text{(monotonicity)}\\
  &\Longrightarrow
    \mathrm{C}(Y \cup Z) \subseteq \mathrm{C}(X \cup Z)
    &\text{(inclusion + set arith.)}
\end{aligned}$$
Note the first monotonicity in the above follows by application on $X \subseteq X \cup Y$ and $Y \subseteq X \cup Y$.
The fourth condition is equivalent to compactness,
$$\begin{aligned}
&\forall A : A \in \mathrm{C}(X) \longrightarrow (\exists Y : \mathop{\mathrm{finite}} Y \wedge Y \subseteq X : A \in \mathrm{C}(Y))\\
&\quad\iff
\mathrm{C}(X) \subseteq \{A \mid \exists Y : \mathop{\mathrm{finite}} Y \wedge Y \subseteq X : A \in \mathrm{C}(Y)\}\\
&\quad\iff
\mathrm{C}(X) \subseteq \bigcup\{\mathrm{C}(Y) \mid \mathop{\mathrm{finite}} Y \wedge Y \subseteq X\}
\end{aligned}$$
