Lógica de primer orden

Es un sistema formal diseñado para estudiar la inferencia en los lenguajes de primer orden. Lenguajes de primer orden son,  lenguajes formales con cuantificadores que alcanzan sólo a variables de individuo, y con predicados y funciones cuyos argumentos son sólo constantes o variables de individuo.

Predicados

Es una expresión lingüística que puede conectarse con una o varias otras expresiones para formar una oración.

En la lógica de primer orden, los predicados son tratados como funciones. Una función es una máquina que recibe un conjunto de cosas, las procesa, y devuelve como resultado una única cosa. A las cosas que entran a las funciones se las llama argumentos, y a las cosas que salen, valores o imágenes. 

Cuantificador

Un cuantificador es una expresión que indica la cantidad de veces que un predicado o propiedad P se satisface dentro de una determinada clase (por ejemplo, pertenencia, equivalencia u orden).

Cuantificador universal

Cuantificador existencial

Cuantificador existencial único

Mas información

Aquí

Y aquí