Multiple-Life Survival, Joint-and-Survivor Annuities and Contingent Assurances

Motivation

A multiple-life contract has payments depending on the survival of more than one individual. A joint-life pension might stop at the first death, while a last-survivor annuity continues until both lives have died. A retirement pension may continue in a smaller amount to a surviving spouse, and a policy may instead pay one capital sum on the first or second death. These arrangements arise in pension schemes, life insurance and the valuation of dependent beneficiaries. They have different claim events, beneficiaries and settlement dates. The distinction matters in actual valuation, especially when both deaths occur between scheduled pension dates.

The basic mathematical objects are laid out in Promislow's Fundamentals of Actuarial Mathematics, third edition (2015, Chapter 10), and Dickson, Hardy and Waters' Actuarial Mathematics for Life Contingent Risks, third edition (2020, Chapter 10). Both discuss joint and last-survivor states. The latter also treats dependent future lifetimes and common shocks. The mission develops event-consistent formulas from a shared joint mortality law, rather than selecting unrelated survival probabilities for different contract components.

Setting

Let two future lifetimes be represented by death-time states $K_x$ and $K_y$ on a finite grid with right-censoring horizon $h$. For $i<h$, state $K_x=i$ means the first life dies in the interval after anniversary $i$ and its death benefit is payable at tick $i+1$ under the annual settlement convention. The terminal state $K_x=h$ means that this death has not been observed before the horizon. The same convention applies to the second life. More finely spaced ticks can represent payment and death dates within a year, so ordering is retained when the two deaths fall in different subannual intervals.

The joint probability mass function is $p_{ij}=\Pr(K_x=i,K_y=j)$, with $p_{ij}\geq0$ and $\sum_{i=0}^{h}\sum_{j=0}^{h}p_{ij}=1$. It determines both one-life margins and their dependence. In particular, the probability that both lives are alive at tick $t$ is $\sum_{i,j}p_{ij}\mathbf{1}_{\{t\leq i\}}\mathbf{1}_{\{t\leq j\}}$. Products of the two marginal survival probabilities are valid only under an explicit independence assumption.

At a scheduled payment anniversary there are four disjoint in-force states: both alive, member only, spouse only and neither alive. The joint-life status is the both-alive state. The last-survivor status consists of all states except neither alive. The reversionary spouse status is specifically member dead and spouse alive. A reversionary pension starts once member death makes the spouse entitled and pays only when the spouse is alive at the relevant instalment date. This is contractually distinct from an unqualified joint-and-survivor pension, whose original member and survivor amounts may follow a different schedule.

Write $d_t$ for a discount factor taking a payment at tick $t$ to commencement, and $b_t$ for its gross benefit amount. A member pension may pay $b_t$ while the member is alive and $\rho b_t$ when the member is dead but the spouse remains alive. The ratio $\rho$ is the spouse continuation factor. Unless stated otherwise, the status is tested at each scheduled payment date, so a spouse who dies before the first eligible instalment receives no instalment. Death lump sums use the tick immediately after their death-year state and are distinct from these scheduled pension payments.

Formalization targets

Joint-law occupation states

The first group constructs the joint law, marginal survivals and four exclusive occupation states. Their probability sums and event identities must agree without assuming independent lives. Strict order events $K_x<K_y$ and $K_y<K_x$ are accompanied by the tie event $K_x=K_y$; both terminal states are right-censored and must not cause a fictitious death claim. Equal grid times are treated as genuine ties in the grid model. Physical simultaneous death in continuous time requires a separate law assigning it positive mass.

Annuity and reversionary values

The second group gives realised annuity cashflows and expected present values for joint-life, last-survivor, member-only and reversionary spouse statuses. A key identity for identical payment dates and discounting is

$$a_{\text{last}}=a_x+a_y-a_{xy},\qquad a_{y\mid x}=a_y-a_{xy}.$$

The first term values any surviving life, and the second values the spouse-only reversion. These identities are valid under general dependence because all terms come from the same joint distribution. For a member pension with a separately contractual spouse continuation of $\rho$, its expected value is

$$V=a_x+\rho a_{y\mid x} =(1-\rho)a_x+\rho a_{\text{last}}.$$

This formula presumes the member payment and spouse payment are evaluated at the same dates with no overlapping guarantee or independent payment entitlement. Guarantee cashflows require separate contractual events.

Order-sensitive death claims

The third group models a unit claim on the first death, a unit claim on the second death, the member dying first, the spouse dying first and simultaneous-grid death. It also models a later death of the survivor and pure endowments contingent on joint or last-survivor survival. Payment at death and payment on a pension anniversary can differ even when the same person eventually receives a benefit. Both deaths within a year are represented with a sufficiently fine tick grid; annual year-end states alone do not identify their physical order.

Integrated capstone

The capstone values a combined pension and assurance from the realised cashflow across all death-time pairs. It then reconciles the expected value independently against single-life, reversionary and last-survivor annuity factors, together with the disjoint first- and second-death assurance values. The event partition is incorporated in the total cashflow rather than appended as an unrelated identity.

Significance

The identities provide actuarially auditable bridges between benefits administered by member and spouse status and factors calculated by conventional life-contingency methods. In Dickson, Hardy and Waters (2020, Chapter 11), pension mathematics supplies further context. They can be used to check spouse continuation calculations in defined benefit pension administration, premium valuations of first- and second-death assurances, and mortality stress tests where lives in a household may be dependent. A dependent joint law can change the joint annuity and first-death insurance values while preserving each single-life margin.

The formalisation keeps payment timing, benefit entitlement, event order and valuation date visible in the mathematics. In the published sources the classical factor relations are known results, while the present finite-grid cashflow definitions and their combined capstone are original derived formulations. Each proposed theorem remains an open formal target until independently verified by Prove2Me's authoritative remote Lean compiler and, separately, proved.

Difficulty

Marginal survivals do not determine joint survival or within-year death order. A spouse may become entitled before the first payable instalment, and may die between those events. Death settlement, grid ties and terminal censoring therefore require careful treatment. The capstone reconciles expected realised cashflows with independently calculated factors, preserving the same joint law, dates and entitlement rules in both valuations.

Formalization scope

The Lean kernel uses finite double sums over one right-censored joint law. Due, arrears, subannual, deferred and guaranteed member/spouse cashflows are defined. Death timing is represented on an integer grid; periods can be made subannual by changing the tick size. Scheduled pension payments are due at their specified ticks. Lump sums are settled at the following death tick. Discount factors and benefit amounts are parameterised as schedules; no particular flat interest rate is built into the definitions.

In the guarantee kernel, $g$ is an absolute expiry tick and $a$ starts the payment window. Guaranteed member payments do not require survival to $a$: they model an already vested obligation, not a pension conditional on reaching retirement. A guarantee lasting $G$ periods from $a$ would expire at $a+G$ and require a separate retirement-eligibility condition. UK defined benefit death-in-deferment and dependant entitlements are scheme-specific and outside this kernel.

The main decomposition identities do not need independence, and explicit independent/dependent finite counterexamples are staged for remote theorem proofs. Equal-tick ties are explicit. A smooth continuous-time law, arbitrary within-tick death times, integrals for immediate death settlement, changing spouse eligibility and other pension guarantee arrangements require further declarations and remote verification before the complete mission can be released. The finite model does not imply those continuous-time results. Annuity-certain or single-life results from other unpublished owner Drafts are not assumed to be importable.

Formal contributors must preserve the same probability law and the same discount and settlement conventions across all components of any identity. A vacuous statement established by assuming its intended conclusion, using inconsistent marginals or suppressing the tie event does not meet the mission's mathematical contract.

Selected references

• S. David Promislow, Fundamentals of Actuarial Mathematics, third edition, Wiley, 2015, Chapter 10, Sections 10.2–10.8, publisher-linked contents.

• D. C. M. Dickson, M. R. Hardy and H. R. Waters, Actuarial Mathematics for Life Contingent Risks, third edition, Cambridge University Press, 2020, Chapter 10, book DOI.