Expressing free variables in the metalogic

Skip to first unread message

Cris Perdue

Apr 9, 2014, 7:11:43 PM4/9/14

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.


Raph Levien

Apr 10, 2014, 8:52:45 PM4/10/14
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:
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.


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
For more options, visit

Reply all
Reply to author
0 new messages