of it, and Σ Lit-independence of a literal implies its ϕ Lit-independence. Accordingly, natural inference prevents us from considering p V q as a consequence of p (it is a relevant implication). All our characterization results about Lit-independence, including complexity results, have an immediate impact on such a natural inference relation (especially, they directly show that the complexity of natural inference is in A 2 ).

Proposition 1 is easily extended to formula-variable independence:
Corollary 1 A formula Σ is Var-independent from variable ν if and only if, for any interpretation ω ∈ Ω p 5 , we have ω |= Σ if and only if Switch(ω, v) |= Σ .

The following metatheoretic properties of FL-independence are used in the rest of this section.

## Proposition 2

(1) DepLit(Σ) ⊆ Lit(Σ); (2) If Σ ≡ Φ, then DepLit(Σ) = DepLit(Φ);
(3a) DepLit(Σ ∧ Φ) ⊆ DepLit(Σ) ∪ DepLit(Φ);
(3b) DepLit(Σ V Φ) ⊆ DepLit(Σ) ∪ DepLit(Φ);
(4) l E DepLit(E) if and only if ¬ l E DepLit(¬E).

FV-independence exhibits similar properties, plus negation stability (point (4) below),
which is not satisfied by FL-independence.

## Proposition 3

(1) DepVar(Σ)⊆ Var(Σ);
(2) If Σ ≡ Φ, then DepVar(Σ) = DepVar(Φ);
(3a) DepVar(ΣΛΦ) ⊆ DepLit(Σ)∪ DepLit(Φ);
(3b) DepVar(Σ VΦ) ⊆ DepLit(Σ) ∪ DepLit(Φ); (4) DepVar(¬Σ) = DepVar(Σ).

Beyond these properties, FL-independence and FV-independence do not exhibit any particularly interesting structure. In particular, FL-independence and FV-independence neither are monotonic nor anti-monotonic w.r.t. expansion of Σ (strengthening or weakening E can easily make it no longer independent from a set of literals or variables).

Recall that L → Σ if and only if L ∩ DepLit (Σ) ̸= ∅. This means that the Lit-dependence of Σ on L only implies the Lit-dependence on a literal of L , not a "full" Lit-dependence on any literal of L .  In other words, if we want to check whether a formula Σ is Lit-dependent on any literal of L , we need a notion stronger than FL-dependence, called full FL-dependence. The same can be said for FV-dependence.

Definition 5 (full FL/FV-dependence) Let Σ be a formula from PROPps, L be a subset of Lps and V be a subset of PS.

- Σ is fully Lit-dependent on L if and only if L ⊆ DepLit(Σ).

- Σ is fully Var-dependent on V if and only if V ⊆ DepVar(Σ) .