a logic for statements over objects, including quantified statements like "for all objects it holds that..." and "there exists objects such that..."
a set D called domain is the set of all objects
formulae are based upon:
variables etc. stand for objects (elements of the domain D)
predicates, possibly combined with connectives and quantifiers, can be true or false
two kinds of values:
| terms | build upon variables, constants
and function symbols |
examples: f(x,c) d h(x) y g(f(y,x),c,x) |
value is an element of the domain |
| formulae | build upon literals,
which are predicates applied to terms |
examples: P(x,f(c,d)) P(c) ∧ R(h(d)) ∃x P(f(x,c),x) |
value is true or false |
a model comprises:
an interpretation gives values to variables
note that the value of a variable is an element of the domain
(not true/false like in propositional logic)
a model and an interpretation:
a model is made of a doman D and an assignments I, which assign:
an element of D to each constant
a function from Dn to D to each function symbol of
arity n
a function from Dn to {true, false} to each
predicate symbol of arity n
an interpretation μ assigns an element of D to every variable
given a model ⟨D,I⟩ and an interpretation μ, we can evaluate every term and formula:
| constants | c | I(c) | ||
| variables | x | μ(x) | ||
| terms made of functions | f(t,...,s) | I(f)(value of t,...,value of s) | (note that I(f) is a function) | (value of t, etc. are elements of the domain obtained recursively) |
| literals | P(t,...,s) | I(P)(value of t,...,value of s) | (note that I(P) is a function) | (t,...,s are terms) |
| formulae built upon propositional connectives | P(c)∨R(f(c,d)) | as usual: every literal is either true or false | ||
| formulae based on an existential quantifier | ∃x P(c, x) | true if there exists μ', that differs from μ only on the value of x, such that ⟨D,I⟩ and μ' evaluate P(c,x) to true | ||
| formulae based on an universal quantifier | ∀x P(c, x) | true if, for all μ' that differs from μ only on the value of x, we have that ⟨D,I⟩ and μ' evaluate P(c,x) to true |
a formula is satisfiable if there exists a model and an interpretation making it true
an occurrence of a variable in a formula is bounded if it falls within the scope of a quantifier, free otherwise
P(c,x) ∧ ∃x P(x,d)
first occurrence of x is free, second is bounded
if a formula contains no free variables, then its truth value does not depend on the interpretation μ
we can change the name of a quantified variable:
∃x P(x) is equivalent to ∃y P(y)
∀x P(x) is equivalent to ∀y P(y)
this can be done in general, if for example y is a new variable:
∃x (P(c,d) ∧ ∀x R(x) ∧ P(x,x)) is equivalent to
∃y (P(c,d) ∧ ∀x R(x) ∧ P(y,y) and to
∃y (P(c,d) ∧ ∀y R(y) ∧ P(y,y)
the occurrences of x relative to a quantification that is inside the formula, like ∀x R(x) in this case, can be renamed or not
relevant to automated reasoning
if x does not occur in A, then:
∀x (A∧B) ≡ A∧∀x B
∀x (A∨B) ≡ A∨∀x B
quantifiers can be "moved in" if the "skipped formula" does not contain the variable they quantify upon
operation can be iterated: ∃x (P(c,d) ∧ (∀y R(y) ∨ P(d, x)) ∧ R(c)) is equivalent to P(c,d) ∧ (∀y R(y) ∨ ∃ x P(d, x)) ∧ R(c)