Sound definitions

Metamath

Metamath does not support definitions, instead axioms are used.

$( Define the number 2.  (Contributed by NM, 27-May-1999.) $)
df-2 $a |- 2 = ( 1 + 1 ) $.

This is states \(2 = 1 + 1\) as an axiom.

${
  $d x A $.
  $( Define power class.  Definition 5.10 of [TakeutiZaring] p. 17, but we
     also let it apply to proper classes, i.e. those that are not members of
     ` _V ` .  When applied to a set, this produces its power set.  A power
     set of S is the set of all subsets of S, including the empty set and S
     itself.  For example, if ` A = { 3 , 5 , 7 } ` , then
     ` ~P A = { (/) , { 3 } , { 5 } , { 7 } , { 3 , 5 } , `
     ` { 3 , 7 } , { 5 , 7 } , { 3 , 5 , 7 } } ` ( ~ ex-pw ).  We will later
     introduce the Axiom of Power Sets ~ ax-pow , which can be expressed in
     class notation per ~ pwexg .  Still later we will prove, in ~ hashpw ,
     that the size of the power set of a finite set is 2 raised to the power
     of the size of the set.  (Contributed by NM, 5-Aug-1993.) $)
  df-pw $a |- ~P A = { x | x C_ A } $.
$}

A definition is sound provided (1) it is eliminable (the wff for any theorem containing a defined symbol can be converted to an equivalent wff without it) and (2) it is conservative (a theorem should be provable from the original axioms after the definition is eliminated).

On definitions that are effectively abreviations:

The soundness of such definitions is simple to check by inspection: if (1) the left-hand constant symbol is new and doesn’t appear in the right-hand side, (2) all variables are distinct (all of them appear in a single $d statement), and (3) we can prove (with a Metamath theorem, e.g. pwjust for df-q) that the right-hand expression equals itself with all variables renamed, then the definition is sound. This convention allows all but 4 definitions to be verified automatically by mmj2 as described above.

${
  $d x A $.  $d y A $.  $d w x $.  $d w y $.  $d w A $.  $d w z $.  $d z x $.
  $d z y $.  $d z A $.
  $( Soundness justification theorem for ~ df-pw .  (Contributed by Rodolfo
     Medina, 28-Apr-2010.)  (Proof shortened by Andrew Salmon,
     29-Jun-2011.) $)
  pwjust $p |- { x | x C_ A } = { y | y C_ A } $=
    ( vz cv wss cab sseq1 cbvabv eqtri ) AEZCFZAGDEZCFZDGBEZCFZBGLNADKMCHINPD
    BMOCHIJ $.
$}

http://us.metamath.org/mpegif/mmset.html#definitions

GHilbert

About Metamath

In Metamath, new definitions are essentially axioms. By convention, most such definitional axioms follow the form definiendum = definiens or definiendum <-> definiens, where the definiens is an expression containing no free variables not appearing in the definiendum, and also where the definiendum does not appear in the definiens. (Definitions which would most naturally be written as recursive are instead stated in terms of explicit recursion operators such as df-rdg.) However, these conventions are nowhere enforced, and, indeed, the constraint on free variables is not directly expressible in the Metamath metalogic.

defthm (df-or
  wff (\/ ph ps)
  () ()
  (<-> (\/ ph ps) (-> (-. ph) ps))
  (-> (-. ph) ps) pm4.2)

https://sites.google.com/a/ghilbert.org/ghilbert/documents/definitions

https://groups.google.com/forum/#!topic/ghilbert/YQLqLFw-KCo

Profiles

https://groups.google.com/forum/#!topic/metamath/lcl-OvLyVR0

Oluś