It sounds like the macro- and microstates should also be parameters of the relevant operators (E and possibly epsilon). In formal mathematics, you cannot leave parameters implicit as it is sometimes done on a whiteboard or perhaps on paper: the machine is unforgiving and will not figure out what is implicit. This is not specific to TLA+ but also true of Coq, Isabelle or Lean.I am not sure about the quantifiers, however: do you really mean E(i,s,…) to be the same value for all parameters? Of course, a definition is never wrong: it may simply not represent what you have in mind, and the good thing about formal mathematics is that you can play with your definitions and find out if they say what you mean.Correct, energy level i of some particular state. E_i(s)Each state has n energy levels. There are also m macrostates at eachenergy level i, and each macrostate can have p possible microstates.How would I define them ?--On Monday, April 29, 2024 at 10:41:25 PM UTC+12 Stephan Merz wrote:I presume that should be E_i(s)? But then, I don’t understand the quantifiers, and the bound variables k and j appear nowhere in your definition?Would that translate to something like{ s \in S : \A i \in 1..n, k \in 1..m, j \in 1..p : E_i = \epsilon(i)} }to mean the state s in S such that the energy of s is \epsilon(i)for m macrostates and p microstates.--On Monday, April 29, 2024 at 5:41:46 PM UTC+12 Stephan Merz wrote:TLA+ has bounded set comprehension:{ x \in S : P(x) }Unbounded comprehension is disallowed: this helps making the definition of Russell’s “set” illegal.Stephan--Stephan MerzOn 29 Apr 2024, at 03:23, marta zhango <marta...@xxxxxxxxx> wrote:How can I define State_I as the state at energy level \epsilon(I)} ?
State_I \in {energy_level : energy_level = \epsilon(I)}--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/643c7e96-552f-4ae5-ba67-84a2f2c390d3n%40googlegroups.com.
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/81197891-9342-4c88-867b-b47d47ad1068n%40googlegroups.com.
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4ba993d8-c1cc-4a65-9e9e-c2328bd9f138n%40googlegroups.com.