First Order Loigc, as known as first order predicate calculus, is defined by the following terms:
Term, a variable, constant, or the result of a function. Denoted by upper case letters,e.g.,,
A.N-place function, n is the arity of the function. n-place function means a function takes
narguments, and will return an object that has certain relations with thoseninputs. Denoted byf.Predicate, an operator that will return either true or false. Predicates can be seen as a special type of functions which takes a set of arguments and return a true or false based on the definition of this predicate. Denoted by
P.Sentential formula, an expression that represents a setence if we substitute variables to proper words (constants).
atomic statement, constant, variable, 0-place function, and 0-place predicate.
Universal quantifier, $\forall$, for all
Existential quantifier, $\exists$, exists
Scope of the respective quantifier, $\forall x B$, $B$ is the scope of the universal quantifier $\forall$.
Free variable, a variable that is not in the scope of respective quantifier.
With above definitions, first-order predicate calculus is defined by the following rules:
- Any atomic statement is a sentential formula.
- If $B$ and $C$ are sentential formulas, then $\neg B$, $B \land C$, $B \lor C$, $B \implies C$ are all sentential formulas based on propositional calculus.
- If $B$ ia a sentential formula in which $x$ is a free variable, then $\forall x B$, $\exists x B$ are sentential formulas.