The causal cosmological argument suggests that if every contingent entity has an external cause, then some necessary entity must exist to avoid infinite regress. This paper formalizes this reasoning in a two-sorted first-order setting with explicit quantification over possible worlds, and defines necessary existence by world-invariance of an existence predicate. The main result is a robust independence theorem: the sentence Φ := ∃x Necessary(x) is not decided by the causal axiom together with Robinson arithmetic Q, as witnessed by two explicit countermodels satisfying the same axioms but forcing opposite truth values for Φ. The independence persists under both the literal formulation of the causal axiom and its philosophically stronger variant requiring the cause to exist in the same world. Separately, the paper recalls that the arithmetic enrichment places the theory in the scope of Gödel-Robinson incompleteness phenomena: every recursively axiomatizable consistent extension of the base theory is incomplete, independently of the specific independence of Φ. Optional strengthenings under stronger arithmetic bases (IΣ₁ for Gödel's second theorem; Σ₁-soundness for existential undecidable sentences) are also recorded. Two additional observations are included: a formal counterexample to the universality of the causal premise based on the successor structure on the natural numbers, and a physical illustration from quantum vacuum energy showing why unrestricted causal principles should be treated with care outside their intended formal setting. In short: Φ is independent of CausalQ by explicit countermodels, while Gödel-Robinson incompleteness is an orthogonal limitation that persists in any consistent r.e. arithmetic extension. Keywords: modal logic; first-order translation; two-sorted semantics; possible worlds; Robinson arithmetic Q; model-theoretic independence; essential undecidability; incompleteness. MSC 2020: 03B45, 03B20, 03C10
M. Bakhtaoui (Sat,) studied this question.