Adding objects, relations and quantifiers β enough expressiveness for real knowledge.
π Where this lives: every SQL query you write is first-order logic in disguise. SELECT name FROM student WHERE year = 4 is {x : Student(x) β§ year(x) = 4}, a JOIN is a conjunction over two relations, EXISTS is β and NOT EXISTS combined with a join is β. Relational databases are a restricted, decidable fragment of FOPL chosen precisely so queries always terminate β which is the expressiveness trade-off made into a product decision. Search "relational algebra first order logic correspondence".
Syntax: terms, predicates, quantifiers
FIRST-ORDER PREDICATE LOGIC (FOPL, or FOL) commits to a world of
OBJECTS, RELATIONS between them, and FUNCTIONS on them.
THE ONTOLOGICAL COMMITMENT, compared:
PROPOSITIONAL LOGIC facts hold or do not β no structure
FIRST-ORDER LOGIC objects, relations, functions
TEMPORAL LOGIC adds time
PROBABILITY THEORY adds degree of belief
THE ELEMENTS OF THE SYNTAX:
CONSTANT SYMBOLS name particular objects:
Ram, Kathmandu, 2
VARIABLE SYMBOLS stand for unspecified objects: x, y, z
PREDICATE SYMBOLS name relations, and have an ARITY:
Student(x) arity 1
Teaches(x, y) arity 2
Between(x, y, z) arity 3
FUNCTION SYMBOLS name functions returning objects:
FatherOf(Ram), Plus(2, 3)
EQUALITY = , a built-in predicate meaning the two
terms refer to the SAME object
A TERM is a constant, a variable, or a function applied to
terms. TERMS DENOTE OBJECTS.
An ATOMIC SENTENCE is a predicate applied to terms, or an
equality. ATOMIC SENTENCES DENOTE TRUTH VALUES.
THE DISTINCTION MATTERS: FatherOf(Ram) is a TERM (it names a
person); Male(FatherOf(Ram)) is a SENTENCE (it is true or
false). Writing a term where a sentence belongs is the
commonest syntax error in exercises.
THE QUANTIFIERS:
UNIVERSAL βx P(x) "for all x, P(x)"
True if P holds for EVERY object in the domain.
NATURALLY PAIRS WITH β:
βx Student(x) β Studies(x)
"everyone who is a student studies"
EXISTENTIAL βx P(x) "there exists an x such that P(x)"
True if P holds for AT LEAST ONE object.
NATURALLY PAIRS WITH β§:
βx Student(x) β§ Studies(x)
"some student studies"
THE TWO CLASSIC MISTAKES, and they are examined directly:
MISTAKE 1 β using β§ with β:
β βx Student(x) β§ Studies(x)
This says EVERYTHING IN THE UNIVERSE is a student and
studies β including the number 7 and the city of
Kathmandu. Far too strong.
β βx Student(x) β Studies(x)
MISTAKE 2 β using β with β:
β βx Student(x) β Studies(x)
This is satisfied by ANY object that is not a student,
because a false antecedent makes the implication true. It
is therefore almost trivially true and says nothing.
β βx Student(x) β§ Studies(x)
THE RULE: β GOES WITH β, β GOES WITH β§.
QUANTIFIER DUALITY β each is expressible via the other:
βx P(x) β‘ Β¬βx Β¬P(x) "all are P" = "none is not P"
βx P(x) β‘ Β¬βx Β¬P(x)
Β¬βx P(x) β‘ βx Β¬P(x) "not all" = "some is not"
Β¬βx P(x) β‘ βx Β¬P(x) "none" = "all are not"
NESTED QUANTIFIERS AND SCOPE β where meaning turns on order:
βx βy Loves(x, y) everyone loves someone
(possibly a different someone each)
βy βx Loves(x, y) there is someone whom everyone loves
(one person, loved by all)
THESE ARE DIFFERENT STATEMENTS, and the second is strictly
stronger β it implies the first but not conversely. SWAPPING
ADJACENT QUANTIFIERS OF DIFFERENT TYPE CHANGES THE MEANING;
swapping two of the same type does not.
Translating English, and inference
WORKED TRANSLATIONS β the most reliably examined skill in the
topic.
"Ram is a student."
Student(Ram)
"All students study."
βx Student(x) β Studies(x)
"Some students do not study."
βx Student(x) β§ Β¬Studies(x)
"No student fails."
βx Student(x) β Β¬Fails(x)
equivalently Β¬βx Student(x) β§ Fails(x)
"Every student has a supervisor."
βx Student(x) β βy Supervises(y, x)
"Only students may enter."
βx Enters(x) β Student(x)
NOTE THE DIRECTION β "only" reverses the implication. This
is a standard trap: it does NOT say all students enter.
"All students except Ram passed."
(βx Student(x) β§ x β Ram β Passed(x)) β§ Β¬Passed(Ram)
"There is exactly one capital of Nepal."
βx CapitalOf(x, Nepal) β§
βy CapitalOf(y, Nepal) β y = x
EXACTLY-ONE ALWAYS NEEDS EQUALITY: existence plus
uniqueness.
"Ram's father is a teacher."
Teacher(FatherOf(Ram)) using a function
or βx FatherOf(Ram, x) β Teacher(x) using a predicate
"Everyone loves their mother."
βx Loves(x, MotherOf(x))
THE CLASSIC SYLLOGISM, formalised and proved:
All men are mortal. βx Man(x) β Mortal(x)
Socrates is a man. Man(Socrates)
Therefore Socrates is mortal.
PROOF: Universal Instantiation on the first sentence with
x = Socrates gives Man(Socrates) β Mortal(Socrates); modus
ponens with the second gives Mortal(Socrates). β
INFERENCE IN FOPL β the rules that handle quantifiers:
UNIVERSAL INSTANTIATION (UI)
from βx Ξ±, infer SUBST({x/g}, Ξ±) for any GROUND TERM g
βx King(x) β§ Greedy(x) β Evil(x)
β’ King(John) β§ Greedy(John) β Evil(John)
EXISTENTIAL INSTANTIATION (EI)
from βx Ξ±, infer SUBST({x/k}, Ξ±) where k is a BRAND-NEW
constant β a SKOLEM CONSTANT
βx Crown(x) β§ OnHead(x, John)
β’ Crown(Cβ) β§ OnHead(Cβ, John)
THE CONSTANT MUST BE NEW, or you would be asserting
something about an already-named object that you have not
established.
UNIFICATION β the mechanism that makes FOPL inference
practical. UNIFY(p, q) returns a substitution ΞΈ making
p and q identical.
UNIFY(Knows(John, x), Knows(John, Jane)) = {x/Jane}
UNIFY(Knows(John, x), Knows(y, Bill)) = {x/Bill,
y/John}
UNIFY(Knows(John, x), Knows(y, MotherOf(y)))
= {y/John,
x/MotherOf(John)}
UNIFY(Knows(John, x), Knows(x, Bill)) = FAIL
β x cannot be both John and Bill. STANDARDISING APART
(renaming variables) fixes this case.
THE MOST GENERAL UNIFIER (MGU) is the one making the fewest
commitments, and it is what a unification algorithm returns.
GENERALISED MODUS PONENS
from pββ², β¦, pββ² and (pβ β§ β¦ β§ pβ β q)
where ΞΈ unifies each pα΅’β² with pα΅’,
infer SUBST(ΞΈ, q)
This does in ONE STEP what UI followed by modus ponens does
in several, which is why real systems use it.
RESOLUTION IN FOPL works as in PL, with unification finding
the complementary literals. The extra step is SKOLEMISATION:
converting to CNF requires eliminating existential quantifiers
by replacing them with Skolem functions of the enclosing
universals.
βx βy Loves(x, y) β βx Loves(x, F(x))
THE SKOLEM FUNCTION F CAPTURES THE DEPENDENCE: the y depends
on which x, which is exactly the ββ versus ββ distinction
made mechanical.
Properties, and the cost of expressiveness
WHAT FOPL BUYS, quantified against propositional logic:
ONE SENTENCE REPLACES MANY. With n objects in the domain:
βx Man(x) β Mortal(x) 1 FOPL sentence
in PL: one implication per man n sentences
βx βy Loves(x, y) β Knows(x, y) 1 FOPL sentence
in PL: one per ordered pair nΒ² sentences
FOR n = 1,000 the second is 1,000,000 propositional sentences
against one first-order sentence. AND IF THE DOMAIN IS
INFINITE β the integers, say β no propositional expansion
exists at all, so the statement is simply inexpressible.
IT ALSO GAINS:
Β· reference to objects, so functions and equality work
Β· GENERALISATION: a rule about all birds automatically
applies to a bird discovered tomorrow, which propositional
logic cannot do
Β· the ability to state relationships between unnamed objects
WHAT IT COSTS β and this is the honest, examinable trade-off:
PROPERTY PROPOSITIONAL FIRST-ORDER
βββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
expressiveness weak strong
entailment DECIDABLE SEMI-DECIDABLE
(NP-complete) (undecidable in
general)
proof procedure complete and complete but may not
terminating terminate on
non-entailment
practical scale millions of thousands of clauses,
variables (SAT) with careful control
βββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
SEMI-DECIDABILITY, stated precisely because it is often garbled:
if KB β¨ Ξ±, a complete proof procedure WILL find a proof
eventually. If KB β Ξ±, the procedure MAY RUN FOREVER without
ever being able to report that fact. There is no algorithm that
always terminates with the right answer β Church and Turing,
1936.
THE PRACTICAL CONSEQUENCE: a theorem prover must be given a
time limit, and "no proof found in 10 seconds" does not mean
"not entailed".
WHY THE DIFFERENCE ARISES: FOPL can quantify over infinite
domains, so checking all models is not a finite process. That
single capability β the one that makes FOPL useful β is what
destroys decidability.
USEFUL RESTRICTED FRAGMENTS, which is how FOPL is actually
deployed:
HORN CLAUSES / DATALOG definite clauses without function
symbols. Decidable, and the basis of
deductive databases.
PROLOG Horn clauses with backward chaining
and a fixed search order. Turing
complete, so it can loop β the
programmer controls termination.
DESCRIPTION LOGICS the basis of OWL. Deliberately
restricted so that subsumption
reasoning is decidable, which is why
ontology reasoners terminate.
RELATIONAL ALGEBRA / SQL a decidable fragment, which is why
every SQL query terminates.
THE PATTERN ACROSS ALL FOUR: TAKE FOPL AND REMOVE JUST ENOUGH
EXPRESSIVENESS TO RECOVER GUARANTEED TERMINATION. That design
move β restricting a formalism to make it tractable β is one of
the most reusable ideas in computer science, and it appears again
in the type systems, grammars and query languages you meet
elsewhere.
A FINAL NOTE ON WHAT FOPL STILL CANNOT DO: it has no way to
express DEGREES OF BELIEF. "Ram probably has flu" and "most
birds fly" are outside it, because every sentence is simply true
or false. That is the gap the probabilistic topics that follow
are built to fill.
The quantifier pairing rule earns its own line because both errors produce sentences that are syntactically fine and semantically useless: β with β§ claims everything in the universe is a student, and β with β is satisfied by any non-student. Neither is caught by a syntax check β only by reading what the sentence actually asserts.
π Go further: the restricted-fragment idea has its most commercially significant instance in description logics, the formal basis of OWL. The designers deliberately gave up parts of first-order expressiveness β arbitrary quantifier nesting, general n-ary relations β specifically so that class subsumption ("is every Student a Person?") remains decidable and a reasoner always terminates. The OWL profiles (EL, QL, RL) then trade further expressiveness for polynomial-time reasoning, so an ontology author picks their point on the curve explicitly. It is the clearest example of expressiveness being engineered rather than maximised. Search "description logic OWL profiles decidable subsumption".
π‘ Exam angle: name the syntax elements β constants, variables, predicates, functions, equality β and distinguish a term (denotes an object) from an atomic sentence (denotes a truth value). The guaranteed question is translating English into FOPL: practise "all", "some", "no", "only", "except" and "exactly one", remembering that β pairs with β and β with β§, that "only" reverses the implication, and that "exactly one" needs equality. Give the quantifier duality equivalences and explain why βxβy differs from βyβx. Know universal and existential instantiation, unification with a worked MGU, generalised modus ponens, and Skolemisation. State that FOPL is semi-decidable while PL is decidable.
Syllabus points
Syntax, semantics, quantification
Rules of inference
Unification
Resolution refutation system (numerical)
Create a free account to tick topics off, take notes as you read, watch the video lessons and get a day-by-day study plan built around your exam date.