Defeated defeaters: a pardon restores the vote

Area: Defeasible reasoning Teaches: a defeater that is itself a #[default] and is itself defeated. The attacker stops blocking its target on exactly the tuples where the attacker was defeated — RFD 0028 D4, “defeated defeaters are legal.” Prerequisites: strict vs default vs defeater, lex specialis. Run: ox build examples/defeasible_defeated_defeater_v0 then ox run-scenario examples/defeasible_defeated_defeater_v0 --scenario <scenario.toml> (see Running it for a four-person scenario).

The previous examples have a two-level defeat: a default, and an attacker that blocks it. Here there are three levels — an exception, and an exception to the exception:

adult(p)         →  can_vote(p)              the overridable default
disenfranchised  ⇒  defeats can_vote          felons lose the vote
restored         ⇒  defeats disenfranchised   a pardon restores it

The legal question: a felon is disenfranchised, but a pardon overturns the disenfranchisement. Does the pardoned felon vote? The answer requires the middle rule to be both an attacker (of can_vote) and a target (of restored).

What to read in franchise.ar

The default and its attacker — but the attacker is itself a #[default], so it can be defeated in turn:

#[default]
#[label(adult)]
pub derive can_vote(p) :- Adult(p);

#[default]
#[label(felon)]
#[defeats(can_vote.adult(p))]
pub derive disenfranchised(p) :- Felon(p);

The exception to the exception. restored defeats disenfranchised’s labeled clause for the pardoned felons:

#[defeats(disenfranchised.felon(p))]
pub derive restored(p) :- Pardoned(p);

The subtle part is what disenfranchised is allowed to block. It blocks can_vote only on the felons it itself still survives for — i.e. the unpardoned ones. On a pardoned felon, disenfranchised is defeated, so it no longer blocks can_vote, and the adult default underneath survives. Resolving this correctly means resolving attacker survival in defeat-graph order, not from each attacker’s raw support.

Running it

This package ships no data (no demo.toml, no facts) — its behavior is exercised by registering people, so supply a four-person scenario. Save this as scenario.toml:

[[mutate]]
path = "franchise::register"
args = { p = "adam", age = 40, felon = false, pardoned = false }
[[mutate]]
path = "franchise::register"
args = { p = "ben", age = 30, felon = true, pardoned = false }
[[mutate]]
path = "franchise::register"
args = { p = "cleo", age = 50, felon = true, pardoned = true }
[[mutate]]
path = "franchise::register"
args = { p = "dot", age = 12, felon = false, pardoned = false }

Then ox run-scenario examples/defeasible_defeated_defeater_v0 --scenario scenario.toml:

adam   adult, not felon            → can_vote   (default, unattacked)
ben    adult, felon, NOT pardoned  → blocked    (disenfranchised survives)
cleo   adult, felon, PARDONED      → can_vote   (defeater itself defeated)
dot    minor                       → absent     (not an Adult)

so voters returns 2 rows — adam and cleo. The decisive contrast is ben vs cleo: both are felons, both are disenfranchised, but cleo’s disenfranchisement is itself defeated by the pardon, so the adult default underneath survives for her and not for ben.

This example is compiled and run in CI; the {adam, cleo} voter set — proving the pardoned felon votes and the unpardoned one stays blocked — is pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs), which registers the four people directly, so the defeated-defeater resolution can’t drift.