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 specified at different 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$ finite}\}\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 finite $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.
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}$$