Leibnizo dėsnis numato, kad jei a ir b yra tas pats objektas, tai visos savybės, kuriomis pasižymi a, yra ir savybės, kuriomis pasižymi b. Įrodymų teorijos kontekste tapatybė apibrėžiama naudojant dvi aksiomas: refleksyvumą ir Leibnizo dėsnį. Refleksyvumo aksioma teigia, kad:
(ref) ⊢ t = t
Leibnizo dėsnis teigia, kad:
(LD) ⊢ t1 = t2 → (φ(t1) → φ(t2)),
– kur φ(t2) gaunama iš φ(t1) pastarojoje pakeitus vieną ar visus termo t1 atvejus termu t2. Esama ir kitų Leibnizo dėsnio versijų, kurios naudoja aukštesnės eilės kvantorius ir taigi šį dėsnį išreiškia sakiniu, o ne schematiniu būdu naudojant metakalbinį kintamąjį φ:
(LD-AEL): ⊢ t1 = t2 → (∀F Ft1 → Ft2)