Formalization of Thermodynamics

Stream: general

[Youjack]

I have formalized some of the bases of thermodynamics with Lean. You can see it on Github.

The main goal of the project is to precisely state the axioms that are essential to building up the thermodynamics we want. The stuff I have already formalized can be summarized as

• The zeroth law
• Thermodynamic cycles and the first law
• Kelvin-Plank statement, Clausius statement, and Carnot theorem
• The construction of thermodynamic temperature

Is there anybody interested in this? This is actually my first project in both formalization and Lean. Any suggestion of improving my code will be valuable to me.

[Jason Rute]

Are you aware of #general > Formalizing Chemical Theory and #general > Formalizing Chemical Theory pt. 2 ? Seems very similar in spirit.

[Jason Rute]

Conversely, @Tyler Josephson ⚛️ and @Max Bobbin would be interested in your work on Thermodynamics in Lean.

[Jason Rute]

I haven’t really thought how to formalize science, but adding axioms doesn’t seem like a good approach. Either you are really just defining something, in which that is why Lean has definitions, or you are opening your system up to be inconsistent. Maybe someone who has thought about this more can chime in.

[Chris Hughes]

Jason Rute said:

I haven’t really thought how to formalize science, but adding axioms doesn’t seem like a good approach. Either you are really just defining something, in which that is why Lean has definitions, or you are opening your system up to be inconsistent. Maybe someone who has thought about this more can chime in.

I think he means "axioms" in the sense that we might talk about the "axioms" of a ring. Looking briefly at the Lean code that seems to be the way it is setup, there is a structure called cycle for instance which is a function satisfying some properties that have something to do with the first law of thermodynamics.

[Tomas Skrivan]

I'm definitely interested in thermodynamics but I haven't done anything yet. At some point I would like to formalize/automate computations in the book Multi Scale Thermodynamics. For that I might find your formalization of basic thermodynamics useful.

[Jason Rute]

Chris Hughes said:

Jason Rute said:

I haven’t really thought how to formalize science, but adding axioms doesn’t seem like a good approach. Either you are really just defining something, in which that is why Lean has definitions, or you are opening your system up to be inconsistent. Maybe someone who has thought about this more can chime in.

I think he means "axioms" in the sense that we might talk about the "axioms" of a ring. Looking briefly at the Lean code that seems to be the way it is setup, there is a structure called cycle for instance which is a function satisfying some properties that have something to do with the first law of thermodynamics.

I’m referring to their use of the axiom keyword, e.g. https://github.com/Youjack/thermodynamics.lean/blob/4af0748a97e6cb89aef0c87425872d1a901e8c55/src/zeroth_law.lean#L30

[Jason Rute]

Here is a good example: The definition of possible cycle is given as a constant and a list of axioms. Instead it can be rewritten as an inductively defined prop, without constant or axioms.

[Jason Rute]

For example, look at the definition of even and odd given in TPiL. (You don’t need the mutual inductive in your case. A regular inductive will do since you are just defining one inductive definition.)

[Jason Rute]

Another common use case of axioms in this library is asserting that something exists just to prove something else exists. It seems that replacing the axiom with a variable would be better. (If you use a variable, it behaves like an axiom in the section, but the theorem adds that as an assumption.) If writing that assumption every time seems too long, you could make a definition for the statement, then the assumption would be something like (exists_possible : exists_possible_stmt). Alternately, taking inspiration from the “axioms” of groups or the “axioms” of geometry, you can probably use a structure (or class) to package axioms.

[Jason Rute]

Another alternative to all these existence theorems would be to just make a function which takes in, say, an usual_engine_cycle And a proof it is possible, and outputs a usual_engine_cycle with the property you want. Then you can have a corresponding theorem stating the output of this function has this property. But this gets into library design, which others here have much more experience with than me.

[Jason Rute]

The constant equil_system can again be rewritten as an inductive type with one constructor water_triple_point. (Constants are just as bad as axioms.)

[Jason Rute]

Rather than have an axiomatically defined canonical mutual_equivquasi linear order (or whatever a linear order without anti-symmetry is called), you can just have an mutual_equiv structure or class. (This is like having a structure for a group instead of axiomatically fixing a single canvonival group.)

[Jason Rute]

Also I’m pretty sure your equiv_system axioms aren’t correct. You say transitivity in the comments, but you axiomitize equivalence so it also has symmetry, which means the quotient is going to be a set where the relation is removed. Further, by axiomitizing a linear order instance, you don’t even state how the linear order has anything to do with the set (and this is likely a mistake since you want the linear order to be related to the transitive relation, right?) This is where axioms can get you into trouble. :smile:

[Youjack]

@Jason Rute thank you for your advice.

I state the first law of thermodynamics as a field in the structure cycle, as @Chris Hughes said. But the other laws are stated as axioms. I agree that adding axioms may result in inconsistency, and stating all those axioms as definitions or variables may be a more appropriate approach. I will consider this later. But I would like to justify the use of axioma little bit.

I think formalizing a physical theory can have two layers of meaning. One is like formalizing special relativity by defining the spacetime as four dimensional Minkowski space, and then derive theorems from this definition. The other is like deriving the Minkowski space from the principle of relativity and the invariance of the speed of light. I think the former approach is more suitable for writing a library for practical use, and the later approach is more suitable for academic purposes. And what I am doing to formalize thermodynamics is like the later approach. I use axioms as global variables, expect them to hold across the library, and want to know what theorems can these axioms deduce. And these theorems could be restated as definitions in another library which is designed to be of practical use.

[Youjack]

Jason Rute said:

Also I’m pretty sure your equiv_system axioms aren’t correct. You say transitivity in the comments, but you axiomitize equivalence so it also has symmetry, which means the quotient is going to be a set where the relation is removed. Further, by axiomitizing a linear order instance, you don’t even state how the linear order has anything to do with the set (and this is likely a mistake since you want the linear order to be related to the transitive relation, right?) This is where axioms can get you into trouble. :smile:

No, mutual_equil is certainly an equivalence relation. The zeroth law of thermodynamics can be stated as if system A and system B are in mutual equilibrium, and system B and system C are also in mutual equilibrium, then system A and system C will be in mutual equlibrium. This is the transitivity of "mutual equilibrium". But reflexivity and symmetry are also wanted for such a relation, though not stated explicitly in the zeroth law.

I think many physics theories have such implicit hypotheses, and part of my job is to state them explicitly. In fact, axioms like usual_engine_cycle.exists_possible in my code are of this kind.

[Tyler Josephson ⚛️]

Good to meet a fellow thermodynamics enthusiast on Zulip! As Jason mentioned, we've been posting our proofs and manuscript draft here on Zulip - the arxiv-ready version will be coming today, as we've gotten this ready to submit!

[Tyler Josephson ⚛️]

Also as Jason mentioned, definitions, structures, and classes are good ways to start holding information about physical systems and encoding relationships between scientific concepts - something we learned as we've been exploring the formalization of science.

[Tyler Josephson ⚛️]

Philosophically, what should formalization of science look like? I think there are two paradigms here:
First is Hilbert's 6th problem: can physics (or science) be axiomatized? The idea is to write down axioms for physics like we have axioms for math, and then derive the rest of physics from that. This sounds like how you're thinking about it - it's an approach that many have worked on over the years, but is still an unsolved problems.
But second is to think of scientific theory as a collection of proofs (see attached paper). In this paradigm, you're not so much concerned about precisely nailing down the axioms that will hold true forever, but instead simply writing valid proofs, and organizing them into a collection. Another way to frame this is a "model-oriented" formalization - scientists and engineers pose models to describe parts of the world, and they aren't concerned if two models are inconsistent with each other. Each model can be proved to rigorously follow from its specification. We can build up scientific theories without waiting for a "grand unified theory" to hold everything together. If the axiomatization project is successful in the future, such auxilliary theories could be associated with the "grand" one, but in the meantime, we can move forward without defining those axioms.

Paleo-2012-Physics-and-proof-theory.pdf

[Jason Rute]

Good point @Tyler Josephson ⚛️ . Although one thing I'd add to that this topic isn't specific to physics. For example, how does one in Lean follow say Euclid's axioms of mathematics (ok, maybe that isn't a great example, but there are further formalizations of Euclid which are purely symbolic)? I can see a number of approaches both using and not using Lean's axiom:

• Using constant and axiom:
  • add the axioms as Lean axioms and constants whenever they come up
  • package the axioms as an "axiom system" structure/class, and then use Lean's axiom to assert the existence of a canonical axiom system. (This has the advantage of keeping the axioms more organized, but it is harder to add new axioms in a gradual way doing this, compared to where each axiom is a separate Lean axiom)
• Avoiding using constant and axiom:
  • just use the axioms as assumptions in each theorem (possibly by naming the assumptions, or using local variables to make them easier to work with).
  • package the axioms as an "axiom system" structure/class and then work within that structure (like working within the theory of groups)
  • package the axioms as an "axiom system" structure/class, prove they are consistent by showing that the structure has at least one example, and then use choice to choose a canonical version. (This behaves like the second option using Lean's axiom, but replaces Lean's axiom with Lean's choice. Since you use choice, you can only use the axioms, and nothing about the particular example given.

[Yaël Dillies]

I don't see why you would need choice in the last case. Can't you just write down a model?

[Jason Rute]

But then you would have available to use the particulars of that model which maybe isn't what you want. I guess you could make it irreducible or something, but I wanted to capture the purity of just using the axioms that the OP is looking for.

[Jason Rute]

For example, maybe your model is the most trivial example where there is only one element in the whole system or something like that. You don't want to accidentally use that fact to prove later theorems.

[Yaël Dillies]

Ah sure, but using classical.some is even worse! because you're using a particular and don't know which. Probably what you want is make it a local instance.

[Yaël Dillies]

But most likely I expect that there's only one model if you give enough parameters to the typeclass.

[Youjack]

Many thanks to @Jason Rute and @Tyler Josephson ⚛️ .

I think I still have a lot to learn about formalizing and axiomatizing physics. I will reconsider the goal of my project and may rewrite some code.