# Predicate calculus

<https://en.wikipedia.org/wiki/Predicate_calculus>

In first-order predicate calculus, a statement is called well-formed formula (wff). A wff is interpreted as making a statement about some domain of discourse.

The syntax of wffs consists of

* logical operators: ∧, ∨, ¬, →, ⟺
* quantifiers: ∀ (@), ∃ (!)
* punctuation marks: `, . : () {}`
* terms:
  * variable: x, y, z
  * constant: a, b, c
  * function
* predicates
* literals

A *variable* represents potentially any element from the domain of discourse. Variables are distinguished from constants by the context in which they appear: vars are always quantified, constants are not.

A *constant* is a specific element from the domain of discourse, `a`,`b`,`joe`

A *function* is a **functional relation** that maps elements in the domain of discourse to other elements in the domain, e.g. `min(x,y,z)`, `abs(x)`. A function has one or more arguments (1+), which are terms.

A *predicate* is a **relation** on the domain of discourse that **evaluates to a Boolean value**, i.e. a relation that is either true or false within the domain. A predicate has 0 or more (0+) arguments (args are terms).

Examples of predicates:

* `above(a,b)`               "a is above b"
* `animal(child_of((Jerry))` "the child of Jerry is an animal"
* `larger_than(square(x),x)` "the square of x is larger than x"
* `hot`                      "it is hot" (nullary predicate)

A *literal* is a predicate or negation of a predicate.

A *WFF* is defined recursively:

* a literal is a wff
* if `w` is a wff, then so is `¬w`
* if `w` and `v` are wffs, then so are: w ∧ v, w ∨ v, w → v, w <=> v
* if `w` is a wff, then, for any var `x`, so are ∀x.w, ∃x.w

The quantifiers `∀x` and `∃x` are said to have *scope* over `w`, and `x` is a *quantified variable*.

The symbols representing vars are distinguishable from the symbols representing constants because the vars are always quantified, whereas constants are not.