Expressing free variables in the metalogic

[Cris Perdue]

Hi,

I am new to Ghilbert and this mailing list.  The concept sounds very interesting, and I have a few questions.  Please pardon me if I am missing obvious points.

The Ghilbert home page mentions replacing distinct variable conditions with a more traditional technique for expressing free variable conditions. This sounds attractive in that free variable conditions are much more familiar. I have two questions about this:

1) Have you found some proofs that are significantly harder or more cumbersome using the more traditional approach?  (If so can you refer me to a couple in some way?)

2) Does the system currently have a way to specify the conditions (and is there documentation that I may have overlooked)?

I know the system is far from complete, but this is an interesting topic from my point of view.

Thanks,

Cris

[Raph Levien]

Hi and welcome to Ghilbert!

As you mentioned in another thread while this message was stuck in moderation (I thought I was signed up for alerts, guess not), the answer is in this thread:

https://groups.google.com/forum/#!searchin/metamath/distinct$20variable$20conditions/metamath/hJupn_hvqu8/KJg69J8BFAEJ

Feel free to ask followup questions. Lately I've been exploring translating from Ghilbert to Coq, and so questions about free variables have been resurfacing.

Raph

--
You received this message because you are subscribed to the Google Groups "Ghilbert" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ghilbert+u...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.