Expressive power of 'def' vs. 'defthm'?

[Marnix Klooster]

Hello all,

Older versions of the Ghilbert language had 'def', which basically was an abbreviation mechanism, and currently it has 'defthm', which is basically using the concept of profiles (see, e.g., https://groups.google.com/forum/#!topic/metamath/lcl-OvLyVR0).

Now 'defthm' was introduced to replace the unsafe 'def', which was intended to only allow conservative extensions but didn't (see, e.g., https://sites.google.com/a/ghilbert.org/ghilbert/documents/definitions).  I assume that the switch to the "profiles approach" was made to make it easier to see/prove that the definition mechanism actually only allows conservative extensions.

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 tried, but cannot think of any.

Thanks!

Groetjes,
 <><

Marnix

--

Marnix Klooster
marnix....@gmail.com

[Carl Witty]

On Fri, Jan 30, 2015 at 9:36 AM, Marnix Klooster
<marnix....@gmail.com> wrote:
> Hello all,
>
> Older versions of the Ghilbert language had 'def', which basically was an
> abbreviation mechanism, and currently it has 'defthm', which is basically
> using the concept of profiles (see, e.g.,
> https://groups.google.com/forum/#!topic/metamath/lcl-OvLyVR0).

I believe that profiles are (depending on the logic) more expressive
than textual-substitution-with-careful-handling-of-variables
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
alpha-renamed.)

> 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.

Carl