A causality calculus

Let us design a first-order calculus including causality as non-truth-functional connective for which causality semantics is defined at the same level as the rest of the (truth-functional) connectives, according to the philosophical position stated in a previous entry. We assume we are given an infinite set of variables V and a set R of predicate symbols with associated arities.

Propositional constants: F (falsehood).

Connectives: → (only if), > (causal implication).

Quantifiers: V (for all).

Axioms and rules of inference: the usual ones for standard first-order calculus plus the following axiom schemas dealing with causality:

(C₁) p > q, q > r → p > r

(C₂) (p > p) → F

(C₃) p > q → (p and q)

(C₄) p > r → (p or q) > r

(C₅) p > (q and r) → p > q

These axioms deserve some comment: C₁ states the usual transitivity of causation, while C₂ says that no event causes itself; C₃ allows us to speak about causation only among events actually taking place, which makes this a "realist" semantics. C₄ and C₅ translate some usual properties of material implication to causal implication.

Semantics: a valuation v specifies several mappings:

• From V to some set U.
• From each n-ary predicate in R to some n-ary relation in U.
• From each formula to the set {F,T}.

and obeys the following rules:

• v(F) = F.
• v(φ → ψ) = T iff v(φ) = F or v(ψ) = T.
• v(R(t₁,...,t_n)) = T iff (v(t₁),...,v(t_n)) is in v(R).
• v(Vx φ) = T iff v'(φ) = T for every valuation v' identical to v except possibly at x.
• The relation on formulas of the calculus defined by v(φ > ψ) = T is consistent with axiom schemas C₁,..., C₅. In particular, this implies that the relation thus defined is a strict partial order.
  

As usual, a statement is valid if it is true for any valuation. It is easy to see that there are valuations with the properties described above: just take any valuation for standard first-order predicate calculus and augment it with v(φ > ψ) = F for all φ, ψ (we may call this a Humean valuation).