Recap of first-order logic

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


Elements

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


Terms and formulae

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

Semantics

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:


Models and interpretations, formally

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


Semantics, formally

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

Satisfiability

a formula is satisfiable if there exists a model and an interpretation making it true


Free variables

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 μ


Property of quantifiers

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


Other properties of quantifiers

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)