(Last modified Wed May 07 23:47 2008)
First-order logic (FOL) extends propositional logic
by considering things that are true and false
of objects or entities in a partial view of the world,
called a domain.
Each different domain (and non-logical symbols pertaining to it)
results in a different
FOL language.
A first-order logic language consist of a
propositional logic (PL) language
extended with the following:
- A domain
consisting of objects we want to reason about.
- Names
of objects in the domain.
- Variables
that refer to objects in the domain,
and are bound by
quantifications (see below).
- Functions
representing relations among objects in the domain;
a function takes an object (or a list of objects)
and identifies an object with that relation to it (or them).
For example,
in the domain of people,
FatherOf("George Washington")
refers to the father of George Washington.
- Predicates
that are true or false of an object or of a list of several objects.
For example,
IsBlue("sky")
might be defined to be true,
and
AreSiblings("the Dalai Lama",
"Arnold Schwarzenegger")
as false.
- Quantifications
that make an assertion about a formula
applied over all objects in the domain.
FOL has two kinds:
- Existential quantification
-
∃u α
asserts that α is true if
u refers to
some object in the domain.
- Universal quantification
-
∀u α
asserts that α is true if
u refers to
any object in the domain
(i.e. that α is true for every domain object
u).
If it is not obvious
which universe U the quantification is over,
write
∃u∈U α
or
∀u∈U α
Names, functions, predicates, and propositional variables form a new category,
non-logical symbols;
these vary from one FOL language to another,
in contrast to the
logical symbols
which are the same for all FOL languages.
-
The logical symbols
are always the same:
PL's ¬, ∧, ∨, and (),
plus FOL's ∀, ∃, and variables.
-
The
non-logical symbols
vary from one FOL language to another:
names,
functions,
predicates,
and propositional variables.
Names, variables, and functions
also form a new category of language constructs:
terms
(or expressions),
consisting of the FOL elements that can refer to an object.
In contrast,
formulae
are either true or false (or unknown).
PL consists only of formulae.
Perhaps the most intriguing features of FOL languages
are that
-
any "interesting" FOL language is not decidable
(there is no procedure for deciding whether
an arbitrary sentence in the language is valid) —
this is Church's undecidability theorem;
and
-
any "interesting" FOL language is necessarily
inconsistent (you can prove false things in it)
or
incomplete (you can't prove every true thing in it) —
this is
Gödel's
first incompleteness theorem.
Here, "interesting" has highly technical meanings,
but roughly indicates any FOL language powerful enough
to express integer mathematics —
in other words, just about any FOL language you would want to use.
Properties of FOL quantifiers
| ∀x α ≡ ¬∃x ¬α
| ∃x α ≡ ¬∀x ¬α
|
Binding precedence
For minimizing parentheses,
the quantifiers ∀x and ∃x
have lower precedence than ¬ ∨ ∧
and higher precedence than → and ↔.
For example,
∃x f(x)∧g(x) is considered to be the same as
(∃x f(x)) ∧g(x),
rather than
∃x (f(x)∧g(x)).
Disproof in FOL
Disproof in FOL generally requires an interpretation.
- To disprove
IsMadeOfGreenCheese("Mars"),
show that the interpretation maps "Mars" to false
for IsMadeOfGreenCheese.
- To disprove
∀s∈People
MasterOfOwnFate(s),
show that
MasterOfOwnFate(s)
is false for some person s.
- To disprove
∃t∈Lunches
IsFree(t),
show that
IsFree(t)
is false for every lunch t
(much harder).
FOL
syntax
semantics
interpretation
