Existential quantification implies search because, computationally, we want to actually deliver at least one example of the existence. For instance, the classi

Existential quantification implies search because, computationally, we want to actually deliver at least one example of the existence. For instance, the classic puzzle where people sit next to one another at dinner, wearing colored outfits, eating certain dishes, talking about certain topics, all subject to a set of constraints is a search problem. It can be phrased with existentials exists (seating in possible_seatings): exists (outfits in possible_outfits): exists (plating in possible_platings): exists (conversation in possible_conversation): constraints(seating, outfits, plating, conversation) This can be seen as an obvious for loop, but for less obvious structures, existential quantification can be powerful. This is especially true when the existentials exist within the language of types that constrain the language of values/computation. Finally, well-moded is a term from logic programming. It's one condition which allows us to prove that searches like the one above will actually converge either to a refutation of the problem or one or more solutions. In general, using existential quantifiers makes it easy to phrase impossible to solve search programs, so it's important to limit the strength of these languages to sit within, for instance, the well-moded subset. I won't go over the technical definition of well-moded, but it's basically designed to force a logic program into a simplistic structure for which various smart search algorithms can easily be applied to it.