search

digama0 / mm0

Metamath Zero specification language
Creative Commons Zero v1.0 Universal
302 stars 40 forks source link

mm0-ification of set.mm #77

Open Lakedaemon opened 3 years ago

Lakedaemon commented 3 years ago

If I understand set.mm0 correctly, you suggest to remove

' axiom df_tru {x2: setvar}: $ wb wtru (wi (wal x2 (wceq (cv x2) (cv x2))) (wal x2 (wceq (cv x2) (cv x2)))) $;

and to have a term with a prefix

'term wtru: wff; 'prefix wtru: $T.$ prec max;

then, you have an axiom

'axiom tru: $ T. $;

Why not define wtru as a definition with the formula "phi <-> phi" ? and have theorem tru : $ T. $

Maybe because the definition would then use a dummy variable of the wff sort which is strict ? so this is forbidden, right ?

So I guess that explains why df_tru uses (wi (wal x2 (wceq (cv x2) (cv x2))) (wal x2 (wceq (cv x2) (cv x2)))) to define wtru (dummy var of the setvar sort, which is not strict)

But this would force set.mm.mm0 to define setvar, cv ... early just to define wtru. So, it is simpler to have wtru as a term and an axiom, right ?

digama0 commented 3 years ago

Why not define wtru as a definition with the formula "phi <-> phi" ?

Because this is not a valid definition in MM0; phi is unbound.

Maybe because the definition would then use a dummy variable of the wff sort which is strict ? so this is forbidden, right ?

There are two issues. This is the immediate one - if you tried to write the definition it would be rejected because phi is a dummy variable and the sort is strict. But even if you remove the strict modifier on wff it still wouldn't be allowed, because all dummy variables have to either be bound in the definition or else have to be parameters to the definition. So you could define

def tru (a : wff) = $ a <-> a $;

but then it would have to be used like tru a instead of just tru - it isn't a dummy variable at all. In fact in MM0 there is no way to construct a nullary wff using only wn and wi and definitions, because there are no binders and no nullary constructors so every term of type wff has a (necessarily free) wff variable in it. I consider set.mm's (old, see below) definition of df-tru suspect for this reason.

Once you have binders, it is possible to define closed wff expressions, like A. x x = x, and you could take something like this (or A. x x = x <-> A. x x = x to get something that really requires no non-propositional axioms to prove) as the definition of true. There was a discussion about doing this in set.mm a while ago, and this is now the official definition of df-tru. Personally, I think it is simpler to keep the propositional fragment separate and just axiomatize a truth constant; it's trivial to validate this axiom in the metatheory so I see no reason not to.