ground terms in logic and $\lambda$-calculus?

Question

What are the differences of ground terms in first-order logic and higher-order logic?

I found on the Wikipedia: "In mathematical logic, a ground term of a formal system is a term that does not contain any free variables."

That mentioned "free variable" is the same thing with free variables of $\lambda$-terms?

I know the closed terms and open terms $\lambda$-calculus. How can we connect closed terms of $\lambda$-calculus with ground terms of logic?

I am bit confused between these concepts, could anyone explain?

Answer 1

I think you're basically correct. "Ground term" is more or less the same as "closed term". Certainly the definition you gave is the same as closed term. Personally, I don't think I've seen "ground term" used much for first-order logic or any system with binders. The place where I most commonly see "ground term" used is universal algebra where there are no binders and so "ground term" means a term with no variables at all.

To be pedantic, the notion of "free variable" is used defined when defining the syntax of whatever formal system you're using. As such, the notion is tied to the system being defined. Conceptually, though, the it's the same idea. In the last decade or so, there's been a lot of research in the CS community in capturing and manipulating binders in a languange-agnostic manner so that tools, libraries, and languages can be defined that allow easy definition and manipulation of languages with binders. For example, the languange Beluga and the various "nominal" systems.