Predicate calculus
Last updated
Was this helpful?
Last updated
Was this helpful?
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.