Is it possible for a constant to become inactive?

[Marko Grdinic]

As the language is simple enough, I've decided to try implementing it on my own in F# in order to get a grasp on it.

In the spec (page 132/247 of the Metamath book) it says that constants can only be declared in the outermost block, so I am wondering how it would be possible for them to become inactive? Later on there are specific mentions of constants having to be active, does that mean that they just have to be declared?

[Norman Megill]

On Monday, November 25, 2019 at 11:33:33 AM UTC-5, Marko Grdinic wrote:

As the language is simple enough, I've decided to try implementing it on my own in F# in order to get a grasp on it.

In the spec (page 132/247 of the Metamath book) it says that constants can only be declared in the outermost block, so I am wondering how it would be possible for them to become inactive? Later on there are specific mentions of constants having to be active, does that mean that they just have to be declared?

That is correct.  Once declared, a constant can never become inactive.  Requiring them to be declared in the outermost scope ensures this.

Originally I had considered allowing temporary constants to be declared (or re-declared) in inner scopes, partly thinking that symmetry with the active/inactive behavior of variables would be more elegant.  But eventually I decided it would be too confusing, because you can no longer tell what the constant means without tracing back its scope.  In addition, the rules would become complex and not necessarily obvious:  how would you treat a reference to a theorem that uses a constant that is no longer active?  Or worse, how would you treat a reference to a theorem in a different scope that used a constant that is re-used locally?  Even just forbidding these situations would complicate a verifier with no clear benefit.

I wrote the original spec with these hypothetical possibilities in mind, but in the end - and in keeping with the goal of simplicity - it seemed best not to allow a constant to have two different meanings or become inactive.  So when the spec says a constant must be active, it just means it must be declared.

Good luck on your F# verifier.

Norm