---
title: "Rules of inference: Pokhara and Sarankot"
subject: "Discrete Structure"
chapter: 1
key: "semester_4/discrete_structure:rules-inference-pokhara-sarankot"
source: https://www.bctengineer.com/q/semester_4/discrete_structure/rules-inference-pokhara-sarankot
site: BCT Engineering
---

# Rules of inference: Pokhara and Sarankot

Discrete Structure · Chapter 1: Logic, Induction and Reasoning

- Asked in: 2075 Bhadra, 8 marks
- Video: [Discrete Math - 1.6.2 Rules of Inference for Quantified Statements](https://www.youtube.com/watch?v=zMtToQelLN8) — SawFin Mathematics
- Answer checked by Claude Opus 5.5 (high effort) on 2026-10-14
- Page: https://www.bctengineer.com/q/semester_4/discrete_structure/rules-inference-pokhara-sarankot
- Whole chapter: https://www.bctengineer.com/md/semester_4/discrete_structure/chapter-1

## Question

Show that the premises "There is someone in this class who has been to Pokhara. Everyone who goes to Pokhara visit the Sarankot. Therefore, someone in this class has visited the Sarankot."

## Short answer

From ∃x(C(x)∧P(x)), instantiate a with C(a)∧P(a). Then ∀x(P(x)→S(x)) gives P(a)→S(a). Modus ponens yields S(a). So C(a)∧S(a), existentially generalized to ∃x(C(x)∧S(x)). Thus someone in class visited Sarankot.

## Answer

The question gives two premises and the conclusion "someone in this class has visited the Sarankot". We prove the conclusion follows from the premises using predicate logic rules.

#### Symbols
Domain: all people. C(x): x is in this class. P(x): x has been to Pokhara. S(x): x has visited Sarankot.

- Premise 1: ∃x (C(x) ∧ P(x))
- Premise 2: ∀x (P(x) → S(x))
- Conclusion: ∃x (C(x) ∧ S(x))

#### Proof
| Step | Statement | Reason |
|---|---|---|
| 1 | ∃x (C(x) ∧ P(x)) | Premise 1 |
| 2 | C(a) ∧ P(a) | Existential instantiation from 1 (a is a particular person) |
| 3 | C(a) | Simplification from 2 |
| 4 | P(a) | Simplification from 2 |
| 5 | ∀x (P(x) → S(x)) | Premise 2 |
| 6 | P(a) → S(a) | Universal instantiation from 5 |
| 7 | S(a) | Modus ponens from 4 and 6 |
| 8 | C(a) ∧ S(a) | Conjunction from 3 and 7 |
| 9 | ∃x (C(x) ∧ S(x)) | Existential generalization from 8 |

Step 9 says that someone in this class has visited the Sarankot. Hence the conclusion follows from the premises. ∎

Note: existential instantiation must be done before universal instantiation so that the same name a is used for both.

## Check yourself

The answer's key points as multiple-choice questions, with the correct option and why.

1. How is 'There is someone in this class who has been to Pokhara' written?
   A. ∀x (C(x) → P(x))
   B. ∃x (C(x) ∧ P(x))
   C. ∃x (C(x) → P(x))
   D. ∀x (C(x) ∧ P(x))
   Answer: B. 'Someone in the class who...' is an existential statement with a conjunction. (Key point: Symbolising)

2. Why must existential instantiation be done before universal instantiation?
   A. Because ∃ is a stronger quantifier
   B. So that the same particular name a is used in both steps
   C. Because universal instantiation needs a new name
   D. The order does not matter
   Answer: B. Existential instantiation introduces a particular name a; universal instantiation can then use that same a. (Key point: Order of instantiation)

3. Which rule gives S(a) from P(a) and P(a) → S(a)?
   A. Modus tollens
   B. Disjunctive syllogism
   C. Modus ponens
   D. Existential generalization
   Answer: C. From p and p → q, modus ponens gives q. (Key point: Deriving S(a))

4. How do we get ∃x (C(x) ∧ S(x)) from C(a) ∧ S(a)?
   A. Universal instantiation
   B. Existential generalization
   C. Simplification
   D. Hypothetical syllogism
   Answer: B. A statement about a particular a lets us generalise to 'there exists x' by existential generalization. (Key point: Final step)

## Related in Discrete Structure

- [Rules of inference: cheque book argument](https://www.bctengineer.com/question.md?key=semester_4%2Fdiscrete_structure%3Arules-inference-cheque-book) — Discrete Structure, chapter 1
- [Rules of inference: Randy and the job](https://www.bctengineer.com/question.md?key=semester_4%2Fdiscrete_structure%3Arules-inference-randy-job) — Discrete Structure, chapter 1
- [Rules of inference: sailing race](https://www.bctengineer.com/question.md?key=semester_4%2Fdiscrete_structure%3Arules-inference-sailing-race) — Discrete Structure, chapter 1
- [Rules of inference: Sunday test in MFC](https://www.bctengineer.com/question.md?key=semester_4%2Fdiscrete_structure%3Arules-inference-sunday-test) — Discrete Structure, chapter 1
- [Rules of inference: movie and sunset](https://www.bctengineer.com/question.md?key=semester_4%2Fdiscrete_structure%3Arules-inference-rainy-movie) — Discrete Structure, chapter 1
- [Rules of inference: e-mail and program](https://www.bctengineer.com/question.md?key=semester_4%2Fdiscrete_structure%3Arules-inference-email-program) — Discrete Structure, chapter 1

## Related in other subjects

- [Why FOPL; rules of inference](https://www.bctengineer.com/question.md?key=semester_6%2Fartificial_intelligence%3Afopl-rules-of-inference-learning) — Artificial Intelligence, chapter 4
- [Trip report on visit to a publishing firm](https://www.bctengineer.com/question.md?key=semester_5%2Fcommunication_english%3Atrip-report-publishing-firm) — Communication English, chapter 7
- [City class with operator overloading](https://www.bctengineer.com/question.md?key=semester_3%2Fobject_oriented_programming%3Acity-class-operator-overload) — Object Oriented Programming, chapter 5
- [Every RE has NFA; ε-NFA for bb(a∪b)*ab](https://www.bctengineer.com/question.md?key=semester_3%2Ftheory_of_computation%3Are-to-nfa-bb-aub-ab) — Theory of Computation, chapter 2