First-Order Predicate Logic, Nested Quantifiers & Translations
“Universal and existential scope, negation duality, nested quantifier order, and English specification translations.”
1.The Grammar of Predicates & Quantifiers
§ 1.1.Predicates model relations on domains: P(x) evaluates to a truth value when variable x is assigned an element from the Domain of Discourse D.
The Two Fundamental Quantifiers:
1. Universal Quantifier (forall x P(x)): True iff P(a) is true for every a in D.
2. Existential Quantifier (exists x P(x)): True iff P(a) is true for at least one a in D.
De Morgan Laws for Quantifiers:
neg(forall x P(x)) <=> exists x neg P(x)
neg(exists x P(x)) <=> forall x neg P(x)
2.Nested Quantifiers & Ordering Dynamics
§ 1.2.When quantifiers of the same type are adjacent, their order can be swapped without changing meaning:
forall x forall y P(x, y) <=> forall y forall x P(x, y)
exists x exists y P(x, y) <=> exists y exists x P(x, y)
When quantifiers are mixed, ORDER IS CRITICAL:
- forall x exists y text{Loves}(x, y): 'Everybody loves somebody' (each person x can choose a different person y).
- exists y forall x text{Loves}(x, y): 'There is a single universal person who is loved by everybody'.
Theorem: exists y forall x P(x, y) implies forall x exists y P(x, y), but the converse does NOT hold.
3. Worked Problem: Formalizing Complex Natural Language Specifications
Distinguish 'only if' from 'if' when setting up the direction of logical implication.
Problem: Translate the following English statement into first-order predicate logic using predicates Student(x), Course(y), Enrolled(x, y), and Passed(x, y):
'Every student who is enrolled in some course has passed at least one course.'
Step 1: Identify components:
- 'x is a student': Student(x).
- 'x is enrolled in some course': exists y (Course(y) ^ Enrolled(x, y)).
- Combined antecedent: Student(x) ^ exists y (Course(y) ^ Enrolled(x, y)).
- 'x has passed at least one course': exists z (Course(z) ^ Passed(x, z)).
Step 2: Universal quantification over all students x:
forall x [ (Student(x) ^ exists y (Course(y) ^ Enrolled(x, y))) -> exists z (Course(z) ^ Passed(x, z)) ]
Step 3: Verify boundary conditions:
If x is not a student, antecedent is False => implication is vacuously True.
If x is a student not enrolled in any course, antecedent is False => True.
If x is enrolled in a course, x must satisfy the consequent by passing at least one course.
Final Formalized Formula: forall x [ (Student(x) ^ exists y (Course(y) ^ Enrolled(x, y))) -> exists z (Course(z) ^ Passed(x, z)) ].
Primary Academic References & Exam Sources
Every concept in Notes From a B.Tech Brain is synthesized from authoritative academic texts, seminal peer-reviewed research, verified exam archives, and renowned university lectures.
Curated for clarity, rigorous numerical solving, and semester excellence:
GATE-focused discrete maths with formula-sheet style rapid coverage.
All relation/function counting formulas in exam-pattern format.
University-level rigour with engaging visual proofs.