ExistsLink

The ExistsLink is a type of Link used to represent existential quantification.

For example: ∃x((x is human) and (x eats dirt)) is written as:

ExistsLink
    VariableNode $X
    AndLink
         InheritanceLink $X human
         EvaluationLink
              eats
              ListLink $X dirt

ExistsLink and ForAllLink are both subtypes of ScopeLink, that is, they bind any variables occurring under the link, so that those variables are not free. So, in the above example, the variable $X is not a free variable.

The PresentLink is a form of ExistsLink which does not bind it's variables, but keeps them free. This allows the PresentLink to be composed with other links having the same variable names, so as to form more complex patterns. Likewise, AlwaysLink is the non-binding form for ForAllLink.

Keeping this in mind, the above example is equivalent to

LambdaLink
    VariableNode $X
    PresentLink
         InheritanceLink $X human
         EvaluationLink
              eats
              ListLink $X dirt

See the link comparison chart for further discussion.

Related ideas

The SatisfactionLink is more-or-less the same thing as the ExistsLink, except that the SatisfactionLink is directly coupled into the pattern matching apparatus, and so can be directly evaluated to find out if it holds true or not, at any given point in time. By contrast, ExistsLink is merely a declarative form, making a statement without being directly evaluatable (to determine it's truth).

As a result, the ExistsLink is more amenable to operations that require probabilities or fractional TruthValues, whereas the SatisfactionLink always evaluates to a crisp true/false value.