Theory mere_addition_max

section ‹The Mere Addition Paradox: Max Rule›

  text ‹There are surprising results with the max rule. Transitivity alone generates an inconsistencty
only when combined with totality. What is more, given transitivity (or quasi-transitivity) alone, 
the formulas turn out to be all satisfiable in an infinite model. ›

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

begin

consts A::σ Aplus::σ B::σ  i1::i i2::i i3::i i4::i i5::i i6::i i7::i i8::i 

axiomatization where
 ―‹A is striclty better than B›
 PP0: "⌊(❙¬○<❙¬A|A❙∨B>❙∧○<❙¬B|A❙∨B>)⌋" and
 ―‹Aplus is at least as good as A›
 PP1: "⌊❙¬○<❙¬Aplus|A❙∨Aplus>⌋" and
 ―‹B is strictly better than Aplus›
 PP2: "⌊(❙¬○<❙¬B|Aplus❙∨B> ❙∧ ○<❙¬Aplus|Aplus❙∨B>)⌋" 


  text ‹Nitpick finds no finite model when the betterness 
   relation is assumed to be transitive:›

theorem T0:
  assumes transitivity  
  shows True
  nitpick [satisfy,expect=none] ―‹no model found›
  oops  

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

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

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

theorem T2:
  assumes reflexivity and Ferrers
  shows False
  ―‹sledgehammer›
  by (metis PP0 PP1 PP2 assms(1) assms(2))
  
  text ‹Nitpick shows consistency if transitivity is weakened into acyclicity:›

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

  text ‹If transitivity or quasi-transitivity is assumed, Nitpick shows inconsistency assuming a finite model
   of cardinality (up to) seven (if we provide the exact dependencies)--for higher cardinalities 
   it returns a time out (depending on the computer it may prove falsity also for cardinality eight, 
   etc.:›

theorem T4:
    assumes
      transitivity and
      OnlyOnes: "∀y. y=i1 ∨ y=i2 ∨ y=i3 ∨ y=i4 ∨ y= i5 ∨ y= i6 ∨ y= i7"
    shows False
    using assfactor_def PP0 PP1 PP2 assms 
  ―‹sledgehammer()› 
  ―‹proof found by Sledgehammer, but reconstruction fails›
  oops

theorem T5:
    assumes
      Quasitransit and
      OnlyOnes: "∀y. y=i1 ∨ y=i2 ∨ y=i3 ∨ y=i4 ∨ y= i5 ∨ y= i6 ∨ y=i7"
    shows False
  using assfactor_def PP0 PP1 PP2 assms
  ―‹sledgehammer()›
  ―‹proof found by Sledgehammer, but reconstruction fails›
  oops

text ‹Infinity is encoded as follows: there is a surjective mapping G from 
   domain i to a proper subset M of domain i. Testing whether infinity holds in general Nitpick 
finds a countermodel:›

abbreviation "infinity ≡ ∃M. (∃z::i. ¬(M z) ∧ (∃G. (∀y::i. (∃x. (M x) ∧ (G x) = y))))"

lemma "infinity" nitpick[expect=genuine] oops ―‹countermodel found›

  text ‹Now we run the same query under the assumption of (quasi-)transitivity: we do 
not get any finite countermodel reported anymore:›

lemma 
  assumes transitivity
  shows   infinity
  ―‹nitpick›   ―‹no countermodel found anymore; nitpicks runs out of time›
  ―‹sledgehammer›  ―‹but the provers are still too weak to prove it automatically; see \cite{J68} for a pen and paper proof›
  oops

lemma 
  assumes Quasitransit 
  shows   infinity
  ―‹nitpick›   ―‹no countermodel found anymore; nitpicks runs out of time›
  ―‹sledgehammer›  ―‹but the provers are still too weak to prove it automatically; see \cite{J68} for a pen and paper proof›
   oops

   text ‹Transitivity and totality together give inconsistency:›

theorem T0':
  assumes transitivity and totality  
  shows False
  ―‹sledgehammer›
  by (metis PP0 PP1 PP2 assms(1) assms(2)) 

end