Theory mere_addition_lewis

section ‹The Mere Addition Paradox: Lewis' rule›

  text ‹We run the same queries as before, but using Lewis' rule. The outcome is pretty
 much the same. Thus, the choice between the opt rule and Lewis' rule does not make a difference.› 

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

begin

consts a::σ aplus::σ b::σ

axiomatization where
 ―‹A is striclty better than B›
 PPP0: "⌊(❙¬∘<❙¬a|a❙∨b>❙∧∘<❙¬b|a❙∨b>)⌋" and
 ―‹Aplus is at least as good as A›
 PPP1: "⌊❙¬∘<❙¬aplus|a❙∨aplus>⌋" and
 ―‹B is strictly better than Aplus›
 PPP2: "⌊(❙¬∘<❙¬b|aplus❙∨b> ❙∧ ∘<❙¬aplus|aplus❙∨b>)⌋"

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

theorem T0:
  assumes transitivity
  shows False 
  ―‹sledgehammer›
  by (metis PPP0 PPP1 PPP2 assms)
  
  text ‹Nitpick shows consistency in the absence of transitivity:›

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

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

theorem T2:
  assumes reflexivity Ferrers
  shows False
  ―‹sledgehammer›
  by (metis PPP0 PPP1 PPP2 assms(1) 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