I believe that profiles are (depending on the logic) more expressive
definitions, but it doesn't look like defthm does use the concept of
profiles to me. (The defthm theorem is essentially only a
certification that any variables in your definition can be
> My question: Is 'defthm' also more expressive than (a corrected form of)
> 'def'? So are there conservative extensions that can be expressed with
> 'defthm', but not with 'def'?
I don't think so.
But profiles really are more expressive. For instance, in ZFC, the
axiom of choice says that certain sets exist, but there is no way to
name the sets; in Metamath's set.mm
, there is not necessarily a closed
class expression for a choice function over a particular set (say, the
power set of the reals, minus the empty set). However, with profiles
you could give a name to such a set.