Theory mere_addition_opt

section ‹The Mere Addition Paradox: Opt Rule›

  text ‹This section studies the mere addition paradox \cite{Parfit1984-PARRAP}, when assuming the opt rule.
The mere addition paradox is a smaller version of Parfit's repugnant conclusion.›

  text ‹We assess the well-known solution advocated by e.g. Temkin \cite{ddl:T87} among others, which consists in 
abandoning the transitivity of the betterness relation.›

theory mere_addition_opt  (* Christoph Benzmüller, Xavier Parent, 2024  *)
  imports DDLcube

begin

consts A::σ Aplus::σ B::σ

  text ‹Here is the formalization of the paradox.›

axiomatization where
 ―‹A is striclty better than B›
 P0: "⌊(❙¬⊙<❙¬A|A❙∨B>❙∧⊙<❙¬B|A❙∨B>)⌋" and
 ―‹Aplus is at least as good as A›
 P1: "⌊❙¬⊙<❙¬Aplus|A❙∨Aplus>⌋" and
 ―‹B is strictly better than Aplus›
 P2: "⌊(❙¬⊙<❙¬B|Aplus❙∨B> ❙∧ ⊙<❙¬Aplus|Aplus❙∨B>)⌋"

  text ‹Sledgehammer finds P0-P2 inconsistent given transitivity of the betterness relation in the models:›

theorem T0:
  assumes transitivity
  shows False 
  ―‹sledgehammer›
  by (metis P0 P1 P2 assms)

  text ‹Nitpick shows consistency in the absence of transitivity:›

theorem T1:
  True
  nitpick [satisfy,expect=genuine,card i=3]  ―‹model found›
  oops

  text ‹Now we consider what happens when transitivity is weakened suitably rather than abandoned wholesale.  We show that 
this less radical solution is also possible, but that not all candidate weakenings are effective.›

  text ‹Sledgehammer confirms inconsistency in the presence of the interval order condition:›

theorem T2:
  assumes reflexivity Ferrers
  shows False
  ―‹sledgehammer›
  by (metis P0 P1 P2 assms(2))
  
  text ‹Nitpick shows consistency if transitivity is weakened into acyclicity or quasi-transitivity:›

theorem T3:
  assumes loopfree
  shows True
  nitpick [satisfy,expect=genuine,card=3]  ―‹model found› 
  oops

theorem T4:
  assumes Quasitransit
  shows True
  nitpick [satisfy,expect=genuine,card=4]  ―‹model found›
  oops

end