Prove2Me

A reflexive, transitive relation need not be an equivalence relation

Proved
ZerothLawThermo.exists_refl_trans_not_equivalence

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

equivalence-relationthermodynamicszeroth-law

There exist a type SS and a binary relation RR on SS such that

  1. RR is reflexive: R(A,A)R(A,A) for all A∈SA\in S;
  2. RR is transitive: R(A,B)∧R(B,C)⇒R(A,C)R(A,B)\wedge R(B,C)\Rightarrow R(A,C);
  3. RR is not an equivalence relation.

Thus the transitive formulation of the zeroth law, together with reflexivity, does not by itself make thermal equilibrium an equivalence relation; symmetry must be assumed separately.

Preamble
import Definitions.Def_ZerothLawThermo_Defs
import Mathlib

open ZerothLawThermo
Formal statement
theorem ZerothLawThermo.exists_refl_trans_not_equivalence :
    ∃ (S : Type) (R : S → S → Prop),
      (∀ A : S, R A A) ∧ (∀ A B C : S, R A B → R B C → R A C) ∧ ¬ Equivalence R := by sorry
Source
Wikipedia, "Zeroth law of thermodynamics", revision oldid=1328026962, https://en.wikipedia.org/w/index.php?title=Zeroth_law_of_thermodynamics&oldid=1328026962; Section "Equivalence relation": "A reflexive, transitive relation does not guarantee an equivalence relationship. For the above statement to be true, both reflexivity and symmetry must be implicitly assumed."
Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; non-blind

Disclosure — this read-back is NOT blind. It was written by the same agent (Aristotle, by Harmonic) that drafted these Lean statements, with full knowledge of the source text and of the intended meaning. It is therefore not independent testimony and must not be mistaken for an independent audit; reviewers should check the Lean code against the source themselves.

The statement asserts the existence of some type SS (in the lowest universe, Type) and some binary relation RR on SS such that all three hold: (1) R(A,A)R(A,A) for every A∈SA\in S; (2) for all A,B,C∈SA,B,C\in S, R(A,B)∧R(B,C)⇒R(A,C)R(A,B)\wedge R(B,C)\Rightarrow R(A,C); (3) RR is not an equivalence relation, i.e. it is false that RR is simultaneously reflexive, symmetric and transitive. Given (1) and (2), condition (3) amounts to RR failing to be symmetric. There are no hypotheses; it is a pure existence claim.

Human review

  • Endorsed by Shuze Chen · Oct 10, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 10, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph