Existence of non-existing recursive functions

[zwergziege]

TLAPS can prove the existence of invalid recursive functions. This leads to inconsistent logic.

DefSilly(Silly, n) == ~Silly[n]
Silly[n \in Nat] == DefSilly(Silly,n)

THEOREM BuggyTheorem == Silly = [n \in Nat |-> DefSilly(Silly,n)] BY DEF Silly
THEOREM FALSE
  <1> Silly[0] = ~Silly[0] BY BuggyTheorem DEF DefSilly
  <1> QED OBVIOUS

[muenchnerkindl]

Thank you for reporting this serious bug. According to preliminary inspection, this appears to be triggered by an unsound rewriting rule in the SMT backend.

[zwergziege]

Probably related: I can prove the continuity of arbitrary operators assuming Seq is continuous (which it should be unless there is a bug in my proof of it). Here is the corresponding theorem

THEOREM ASSUME NEW CONSTANT Next(_),
               NEW CONSTANT f,
               f = [n \in Nat |-> f[n]] ,
               \A n \in Nat : f[n] \subseteq f[n + 1] ,
               Seq(UNION {f[n] : n \in Nat}) = UNION {Seq(f[n]) : n \in Nat}
        PROVE  UNION {Next(f[n]) : n \in Nat} = Next(UNION {f[n] : n \in Nat})
        OBVIOUS

[quicquid]

I just saw this report open - on my machine with the latest development version, I can not prove BuggyTheorem although I have not checked if I can reproduce the issue on an older release version.

I can indeed prove the second theorem about Seq on my machine. It is proved by the SMT backend and I could veryify the generated smt file with a current z3-4.8.17 (within about one minute) outside of TLAPS.

tlapm_50fbc0.smt.txt

I have not looked into the file / TLA+ theorem statement yet to check where things turn out unexpected though.