Predicate Logic — ∀ আর ∃, বা 'সব' ও 'কোনো একটা'
Predicate Logic and Quantifiers
Propositional logic দিয়ে 'array-এর সব element ধনাত্মক' লেখাই যায় না। Quantifier সেই ফাঁক পূরণ করে — এবং এটাই loop invariant, database query আর type system-এর ভাষা।
আগে এটা বুঝি
এই function-টা দেখুন:
def all_positive(arr):
for x in arr:
if x <= 0:
return False
return Trueএটা কী দাবি করে? বাংলায়: “array-এর প্রতিটা element ধনাত্মক।”
এখন এই দাবিটা propositional logic-এ লিখুন।
…লিখতে পারবেন না।
Propositional logic-এ আপনার হাতে আছে p, q, r — অবিভাজ্য সত্য-মিথ্যা।
কিন্তু “প্রতিটা element” বলতে গেলে element-গুলোর ভেতরে তাকাতে হয়,
তাদের সংখ্যা আগে থেকে জানা নেই, আর প্রতিটার জন্য একই দাবি প্রয়োগ করতে হয়।
Propositional logic-এ এর কোনো ব্যবস্থা নেই।
Predicate logic (বা first-order logic) ঠিক এই ফাঁকটা পূরণ করে। এটা যোগ করে দুইটা জিনিস: predicate (variable-সহ template) আর quantifier (কতগুলোর জন্য প্রযোজ্য)।
এই দুইটা ছাড়া আধুনিক computer science-এর প্রায় কিছুই আনুষ্ঠানিকভাবে লেখা যায় না — না algorithm-এর correctness, না database-এর semantics, না type system-এর নিয়ম।
মূল ধারণা
Predicate — variable-সহ proposition
Predicate হলো একটা বাক্য যাতে এক বা একাধিক free variable আছে। নিজে থেকে এর সত্যমান নেই।
P(x) : "x জোড় সংখ্যা"
Q(x) : "x > 5"
R(x,y): "x, y-কে ভাগ করে"P(x) নিজে সত্যও নয়, মিথ্যাও নয়। কিন্তু x-এ মান বসালেই proposition:
P(4) → T
P(7) → F
R(3, 12) → T
R(5, 12) → Fপ্রোগ্রামিং-এর ভাষায়: predicate হলো একটা function যা boolean ফেরত দেয়।
def P(x): return x % 2 == 0 # predicate
P(4) # proposition — এখন সত্যমান আছেDomain of discourse
Predicate-এর সাথে সবসময় একটা domain থাকে — x কোথা থেকে আসতে পারে।
Domain না বললে দাবিটা অর্থহীন।
∀x (x² ≥ 0)- Domain = বাস্তব সংখ্যা → সত্য
- Domain = জটিল সংখ্যা → মিথ্যা (
i² = −1)
আরেকটা:
∀x ∃y (x + y = 0)- Domain = পূর্ণসংখ্যা → সত্য (
y = −x) - Domain = স্বাভাবিক সংখ্যা (0, 1, 2, …) → মিথ্যা (
x = 5-এর জন্যy = −5domain-এ নেই)
দুইটা quantifier
Universal — ∀ (“সব”)
∀x P(x)পড়া: “domain-এর প্রতিটা x-এর জন্য P(x) সত্য।”
সত্য যখন: কোনো ব্যতিক্রম নেই মিথ্যা প্রমাণ করতে: একটা counterexample যথেষ্ট
all(P(x) for x in domain)Existential — ∃ (“অন্তত একটা”)
∃x P(x)পড়া: “এমন অন্তত একটা x আছে যার জন্য P(x) সত্য।”
সত্য প্রমাণ করতে: একটা উদাহরণ যথেষ্ট মিথ্যা প্রমাণ করতে: সব সম্ভাবনা বাতিল করতে হবে
any(P(x) for x in domain)Negation — সবচেয়ে দরকারি নিয়ম
Quantifier negate করার নিয়ম De Morgan-এর সাধারণীকৃত রূপ:
¬∀x P(x) ≡ ∃x ¬P(x)
¬∃x P(x) ≡ ∀x ¬P(x)সূত্র: negation ভেতরে ঢুকলে quantifier উল্টে যায় — ঠিক যেমন
De Morgan-এ ∧ আর ∨ উল্টে যেত।
আসলে এটা কাকতালীয় নয়। Finite domain {a, b, c}-এ:
∀x P(x) ≡ P(a) ∧ P(b) ∧ P(c)
∃x P(x) ≡ P(a) ∨ P(b) ∨ P(c)∀ হলো অসীম AND, ∃ হলো অসীম OR। তাই De Morgan এখানেও খাটে —
এটা একই নিয়মের সম্প্রসারণ।
উদাহরণ:
“সব ছাত্র পাশ করেছে” — এটা মিথ্যা হওয়ার মানে?
¬∀x Passed(x) ≡ ∃x ¬Passed(x)“অন্তত একজন ছাত্র পাশ করেনি।” — সব ছাত্র ফেল করেছে নয়।
এই ভুলটা মানুষ প্রতিদিন করে।
ভেতরে কী ঘটছে
Nested quantifier — ক্রম সব বদলে দেয়
এখান থেকেই predicate logic কঠিন হতে শুরু করে, আর এখানেই এর আসল শক্তি।
∀x ∃y L(x, y) vs ∃y ∀x L(x, y)ধরুন L(x, y) = “x, y-কে ভালোবাসে”, domain = সব মানুষ।
| Formula | পড়া | অর্থ |
|---|---|---|
∀x ∃y L(x,y) | প্রত্যেকের জন্য কেউ একজন আছে | প্রত্যেকে কাউকে ভালোবাসে (আলাদা আলাদা হতে পারে) |
∃y ∀x L(x,y) | কেউ একজন আছে যাকে সবাই | এমন একজন নির্দিষ্ট মানুষ আছে যাকে সবাই ভালোবাসে |
দ্বিতীয়টা অনেক বেশি শক্তিশালী দাবি।
নিয়ম: ভেতরের quantifier-এর variable বাইরেরটার উপর নির্ভর করতে পারে।
∀x ∃y-তে y বেছে নেওয়া হয় x জানার পরে — তাই y হলো x-এর function।
∃y ∀x-তে y বেছে নিতে হয় x জানার আগে — একটাই y সবার জন্য চলতে হবে।
গাণিতিক উদাহরণে স্পষ্ট হয় (domain = পূর্ণসংখ্যা):
∀x ∃y (x + y = 0) সত্য — প্রতিটা x-এর জন্য y = −x নিন
∃y ∀x (x + y = 0) মিথ্যা — একটা y সব x-এর জন্য কাজ করবে নাকখন ক্রম বদলানো নিরাপদ
একই quantifier পাশাপাশি থাকলে ক্রম বদলানো যায়:
∀x ∀y P(x,y) ≡ ∀y ∀x P(x,y) ✓
∃x ∃y P(x,y) ≡ ∃y ∃x P(x,y) ✓
∀x ∃y P(x,y) ≢ ∃y ∀x P(x,y) ✗ কখনোই নাতবে একটা একমুখী সম্পর্ক আছে:
∃y ∀x P(x,y) → ∀x ∃y P(x,y) ✓ (উল্টোটা নয়)শক্তিশালী দাবি দুর্বলটাকে বোঝায়, উল্টোটা নয়।
Bounded quantifier — বাস্তবে যা ব্যবহার হয়
খাঁটি গণিতে domain সীমাহীন, কিন্তু প্রোগ্রামিং-এ আমরা প্রায় সবসময় bounded quantifier ব্যবহার করি:
∀i (0 ≤ i \< n → A[i] > 0)পড়া: “0 থেকে n−1 পর্যন্ত প্রতিটা i-এর জন্য A[i] ধনাত্মক।”
লক্ষ্য করুন গঠনটা: ∀ -এর সাথে implication ব্যবহার হয়েছে।
∃-এর সাথে ব্যবহার হয় conjunction:
∃i (0 ≤ i \< n ∧ A[i] == target)এটা গুলিয়ে ফেলা সবচেয়ে সাধারণ ভুল:
∀i (0 ≤ i \< n ∧ P(i)) ✗ ভুল — দাবি করছে সব পূর্ণসংখ্যাই range-এ আছে
∃i (0 ≤ i \< n → P(i)) ✗ ভুল — range-এর বাইরের যেকোনো i দিয়েই সত্য হয়ে যায়মনে রাখার সূত্র: ∀ চায় →, ∃ চায় ∧।
কেন? ∀-এ আপনি range-এর বাইরের element-দের “ছাড় দিতে” চান —
implication মিথ্যা premise-এ vacuously সত্য হয়ে ছাড় দেয়। ∃-তে আপনি
চান element-টা range-এও থাকুক এবং শর্তও মানুক — সেটা ∧।
উদাহরণ
Loop invariant আনুষ্ঠানিকভাবে লেখা
এখানেই predicate logic-এর সবচেয়ে ব্যবহারিক প্রয়োগ।
int find_max(int A[], int n) {
int max = A[0];
for (int i = 1; i \< n; i++) {
if (A[i] > max) max = A[i];
}
return max;
}এই কোড কি ঠিক? “চালিয়ে দেখলাম” যথেষ্ট না। আমাদের একটা invariant লাগে — এমন একটা দাবি যা প্রতিটা iteration-এর শেষে সত্য থাকে।
Invariant:
INV(i) : (∀k)(0 ≤ k \< i → A[k] ≤ max) ∧ (∃k)(0 ≤ k \< i ∧ A[k] == max)বাংলায়: “এ পর্যন্ত দেখা সব element max-এর চেয়ে ছোট বা সমান, এবং
max আসলেই দেখা element-গুলোর একটা।”
দুইটা অংশই দরকার। প্রথমটা ছাড়া max খুব ছোট হতে পারত; দ্বিতীয়টা ছাড়া
max = INT_MAX করে দিলেও প্রথম শর্ত মানত।
প্রমাণের তিন ধাপ:
Initialization — Loop শুরুর আগে i = 1, max = A[0]:
- অংশ ১:
k = 0-এর জন্যA[0] ≤ A[0]✓ - অংশ ২:
A[0] == max✓
Maintenance — ধরি INV(i) সত্য। Iteration চালানোর পর INV(i+1) সত্য?
- যদি
A[i] > max: নতুনmax = A[i]। পুরনো সবA[k] ≤পুরনোmax < A[i]✓, আরA[i] == max✓ - যদি
A[i] ≤ max:maxঅপরিবর্তিত। নতুন element-ও শর্ত মানে ✓, দ্বিতীয় অংশ আগের মতোই ✓
Termination — Loop শেষে i = n, তাই:
(∀k)(0 ≤ k \< n → A[k] ≤ max) ∧ (∃k)(0 ≤ k \< n ∧ A[k] == max)এটাই তো “max হলো array-এর সর্বোচ্চ মান”-এর সংজ্ঞা। ∎
Database query = predicate logic
SQL আসলে predicate logic-এর একটা syntax।
SELECT * FROM users WHERE age > 18 AND country = 'BD';{ u ∈ Users | age(u) > 18 ∧ country(u) = 'BD' }WHERE clause-টা আক্ষরিকভাবে একটা predicate।
আর quantifier?
-- ∃ : এমন user যার অন্তত একটা order আছে
SELECT * FROM users u
WHERE EXISTS (SELECT 1 FROM orders o WHERE o.user_id = u.id);
-- ∀ : এমন user যার সব order shipped
-- SQL-এ সরাসরি ∀ নেই, তাই ¬∃¬ দিয়ে লিখতে হয়
SELECT * FROM users u
WHERE NOT EXISTS (
SELECT 1 FROM orders o
WHERE o.user_id = u.id AND o.status != 'shipped'
);দ্বিতীয়টা লক্ষ্য করুন — এটাই সেই negation নিয়ম:
∀x P(x) ≡ ¬∃x ¬P(x)SQL-এ FORALL নেই, তাই প্রতিটা “সব”-প্রশ্ন NOT EXISTS দিয়ে লিখতে হয়।
এই রূপান্তরটা না জানলে এই query লেখাই সম্ভব না।
- ∀o (order(o) → shipped(o))গাণিতিক দাবি
- NOT EXISTS (… != shipped)SQL — ¬∃¬ রূপান্তর
- Anti-join operatorquery planner-এর relational algebra
- Hash anti-joinphysical execution plan
- Nested loop over pagesbuffer pool থেকে page পড়া
- read() syscallkernel-এ নামা
- Block device I/Oডিস্ক থেকে byte
আপনি একটা ∀ লিখলেন — আর সাত স্তর নিচে সেটা ডিস্ক থেকে byte পড়ায়
রূপান্তরিত হলো। এই পুরো শৃঙ্খলটা আমরা Level 8-এ ধরে ধরে দেখব।
নিজে চালিয়ে দেখুন
Quantifier আর খালি সংগ্রহ
def demo(name, seq):
print(f"\n{name}: {seq}")
print(f" ∀x (x > 0) = {all(x > 0 for x in seq)}")
print(f" ∃x (x > 0) = {any(x > 0 for x in seq)}")
print(f" ¬∀x (x > 0) = {not all(x > 0 for x in seq)}")
print(f" ∃x ¬(x > 0) = {any(not (x > 0) for x in seq)}")
print(f" ¬∃x (x > 0) = {not any(x > 0 for x in seq)}")
print(f" ∀x ¬(x > 0) = {all(not (x > 0) for x in seq)}")
demo("সব ধনাত্মক", [1, 2, 3])
demo("মিশ্র", [1, -2, 3])
demo("সব ঋণাত্মক", [-1, -2])
demo("খালি", [])প্রতিটা ক্ষেত্রে দেখুন ¬∀ আর ∃¬ মিলে যায়, আর ¬∃ আর ∀¬ মিলে যায়।
De Morgan-এর quantifier রূপ, যাচাই করা।
খালি list-এর সারিটা বিশেষভাবে দেখুন:
খালি: []
∀x (x > 0) = True ← vacuous truth
∃x (x > 0) = Falseএখন একটা বাস্তব ফাঁদ:
def all_users_verified(users):
return all(u.verified for u in users)
# users খালি হলে → True → "সব verified" → access granted!খালি input-এ এই function সবসময় True দেয়। যদি এটা একটা authorization
check হয়, তাহলে user list খালি করে দিতে পারলেই bypass।
সঠিক রূপ:
def all_users_verified(users):
return len(users) > 0 and all(u.verified for u in users)অর্থাৎ ∃x T(x) ∧ ∀x V(x) — “অন্তত একজন আছে এবং সবাই verified”।
Python-এর all()/any() হুবহু ∀/∃, আর De Morgan নিয়মটা কোডে যাচাই করা যায়। খালি sequence-এর আচরণ vacuous truth-এর সরাসরি প্রকাশ।
Nested quantifier-এর ক্রম হাতে-কলমে
people = ['আয়েশা', 'বিলাল', 'চাঁদনি']
# কে কাকে চেনে
knows = {
'আয়েশা': {'বিলাল'},
'বিলাল': {'চাঁদনি'},
'চাঁদনি': {'বিলাল'},
}
def K(x, y):
return y in knows[x]
# ∀x ∃y K(x, y) — প্রত্যেকে কাউকে না কাউকে চেনে
forall_exists = all(any(K(x, y) for y in people) for x in people)
# ∃y ∀x K(x, y) — এমন একজন আছে যাকে সবাই চেনে
exists_forall = any(all(K(x, y) for x in people) for y in people)
print("∀x ∃y K(x,y) =", forall_exists)
print("∃y ∀x K(x,y) =", exists_forall)
# ∃y ∀x কে সত্য বানাতে কী লাগত?
for y in people:
who = [x for x in people if K(x, y)]
print(f" {y} কে চেনে: {who} ({len(who)}/{len(people)})")Output:
∀x ∃y K(x,y) = True
∃y ∀x K(x,y) = False
আয়েশা কে চেনে: [] (0/3)
বিলাল কে চেনে: ['আয়েশা', 'চাঁদনি'] (2/3)
চাঁদনি কে চেনে: ['বিলাল'] (1/3)প্রত্যেকে কাউকে চেনে ✓, কিন্তু এমন কেউ নেই যাকে সবাই চেনে ✗। বিলাল সবচেয়ে কাছে গেছে — কিন্তু বিলাল নিজেকে চেনে না (আমাদের ডেটা অনুযায়ী)।
knows['বিলাল']-এ 'বিলাল' যোগ করে আবার চালান — তখন ∃y ∀x সত্য হবে।
∀∃ আর ∃∀ কেবল তাত্ত্বিকভাবে আলাদা নয় — একই ডেটায় এদের ফল আলাদা হয়, আর সেটা কোড চালিয়ে দেখা যায়।
নিজে বানান
Bounded Quantifier Checker
- ছোট finite domain-এ ∀ ও ∃ evaluate করার function লিখুন
- Nested quantifier সমর্থন করুন
- একটা quantified statement negate করার function লিখুন
- Negation-টা যাচাই করুন — মূল আর negated statement-এর মান সবসময় উল্টো হতে হবে
from itertools import product
def forall(domain, pred):
return all(pred(x) for x in domain)
def exists(domain, pred):
return any(pred(x) for x in domain)
# ── উদাহরণ: গাণিতিক দাবি যাচাই ──────────────────────────────
Z = range(-10, 11) # ছোট domain, পূর্ণসংখ্যার প্রতিনিধি
N = range(0, 11) # স্বাভাবিক সংখ্যা
claims = [
("∀x∈Z ∃y∈Z (x + y = 0)",
forall(Z, lambda x: exists(Z, lambda y: x + y == 0))),
("∃y∈Z ∀x∈Z (x + y = 0)",
exists(Z, lambda y: forall(Z, lambda x: x + y == 0))),
("∀x∈N ∃y∈N (x + y = 0)",
forall(N, lambda x: exists(N, lambda y: x + y == 0))),
("∀x∈Z (x² ≥ 0)",
forall(Z, lambda x: x*x >= 0)),
("∀x∈Z ∀y∈Z (x·y = y·x)",
forall(Z, lambda x: forall(Z, lambda y: x*y == y*x))),
("∃x∈Z ∀y∈Z (x·y = x)", # x = 0 কাজ করে
exists(Z, lambda x: forall(Z, lambda y: x*y == x))),
]
for text, value in claims:
print(f"{'✓' if value else '✗'} {text}")
# ── Negation যাচাই ──────────────────────────────────────────
def check_negation(domain, pred, label):
"""¬∀x P(x) ≡ ∃x ¬P(x) এবং ¬∃x P(x) ≡ ∀x ¬P(x)"""
a = not forall(domain, pred)
b = exists(domain, lambda x: not pred(x))
c = not exists(domain, pred)
d = forall(domain, lambda x: not pred(x))
ok = (a == b) and (c == d)
print(f"{'✓' if ok else '✗'} {label}: ¬∀≡∃¬ is {a==b}, ¬∃≡∀¬ is {c==d}")
check_negation(range(1, 11), lambda x: x > 0, "সব ধনাত্মক")
check_negation(range(-5, 6), lambda x: x > 0, "মিশ্র")
check_negation([], lambda x: x > 0, "খালি domain")নিজে বাড়ান:
forall_bounded(lo, hi, pred)লিখুন যা∀i (lo ≤ i \< hi → pred(i))implement করেfind_max-এর invariant-টা কোডে লিখুন এবং প্রতিটা iteration-এ assert করুন:
ভুল ইচ্ছে করে ঢোকান (def find_max_verified(A): assert len(A) >= 1, "precondition: n ≥ 1" m = A[0] for i in range(1, len(A)): if A[i] > m: m = A[i] # invariant assert all(A[k] <= m for k in range(i+1)) assert any(A[k] == m for k in range(i+1)) return m>কে>=, বাA[0]কে0) আর দেখুন কোন assertion আগে ভাঙে- Binary search-এর invariant লিখুন এবং একইভাবে assert করুন —
এটা কঠিন, কারণ invariant-এ
∀দুইদিকেই লাগে - একটা statement string parse করে quantifier চিনে negate করার function লিখুন
বাস্তব সিস্টেমে
Quantifier যেখানে যেখানে চলছে
Formal verification. Dafny, Coq, Isabelle, TLA+ — এগুলোর পুরো ভাষাই predicate logic-এর উপর। Amazon AWS তাদের S3, DynamoDB আর নেটওয়ার্ক protocol-এর নকশা TLA+ দিয়ে verify করে, এবং সেখানে ধরা পড়া bug-গুলোর কিছু ছিল এমন যেগুলো testing-এ কখনো ধরা পড়ত না।
seL4 microkernel — প্রথম formally verified operating system kernel। প্রায় ১০,০০০ লাইন C কোডের সম্পূর্ণ correctness proof, লেখা হয়েছে Isabelle/HOL-এ। প্রতিটা দাবি quantifier-এ প্রকাশিত। Level 4-এ আমরা এটা নিয়ে কথা বলব।
Type system. Generic type হলো universal quantification:
id :: forall a. a -> aআক্ষরিকভাবে ∀a। আর existential type (∃) হলো abstraction/interface —
“একটা type আছে যা এই operation-গুলো সমর্থন করে, কিন্তু কোনটা তা বলছি না”।
Java-র List<?>, Rust-এর dyn Trait, Go-র interface{} — সবই
existential quantification-এর রূপ।
Database. SQL-এর EXISTS, NOT EXISTS, ALL, ANY সরাসরি quantifier।
Relational algebra-র division operator হলো ∀-এর বাস্তবায়ন।
Query planner এই formula-গুলো নিয়ে যে rewriting করে সেটা predicate
logic-এর বীজগণিত।
Static analysis ও abstract interpretation. “এই pointer কি কখনো NULL
হতে পারে?” — এটা ∃execution (ptr == NULL)। Analyzer এই প্রশ্নের
approximate উত্তর বের করে।
Access control policy. “সব S3 bucket কি private?” — AWS Config এই ধরনের প্রশ্ন quantifier হিসেবে প্রকাশ করে এবং SMT solver দিয়ে উত্তর দেয়।
Smart contract auditing. “কোনো execution path কি contract-এর balance
ঋণাত্মক করতে পারে?” — ∃path (balance \< 0)। এই প্রশ্নের উত্তর না জানার
কারণে বিলিয়ন ডলার হারিয়েছে।
যে ভুলগুলো সবাই করে
“∀ মানে 'সব', তাই খালি সংগ্রহে এটা মিথ্যা হওয়া উচিত।”
উল্টো — খালি সংগ্রহে ∀ সত্য।
∀x P(x) আসলে দাবি করে: “এমন কোনো x নেই যার জন্য P(x) মিথ্যা।”
খালি domain-এ কোনো x-ই নেই, তাই counterexample-ও নেই, তাই দাবিটা সত্য।
গাণিতিকভাবে এটা অপরিহার্য। ধরুন ∀x ∈ S, P(x) খালি S-এ মিথ্যা হতো।
তাহলে S = A ∪ B -এর জন্য এই সহজ নিয়মটা ভেঙে পড়ত:
∀x ∈ (A ∪ B) P(x) ≡ (∀x ∈ A P(x)) ∧ (∀x ∈ B P(x))B খালি হলে ডান পাশ মিথ্যা হয়ে যেত, অথচ বাঁ পাশ A-এর উপর নির্ভর করত।
পুরো বীজগণিত ভেঙে পড়ত।
তবে প্রোগ্রামিং-এ এটা মনে রাখা জরুরি, কারণ authorization বা validation logic-এ vacuous truth নীরব bypass তৈরি করে।
“∀x ∃y আর ∃y ∀x — একই কথা অন্যভাবে বলা।”
সম্পূর্ণ ভিন্ন, আর পার্থক্যটা গভীর।
∀x ∃y P(x,y) — প্রতিটা x-এর জন্য একটা y আছে, এবং সেই y x-এর
উপর নির্ভর করতে পারে। অর্থাৎ একটা function f(x) = y আছে।
∃y ∀x P(x,y) — একটা নির্দিষ্ট y আছে যা সব x-এর জন্য কাজ করে।
একটা ধ্রুবক।
Function বনাম ধ্রুবক — এটাই পার্থক্য।
গণিতে এটা “pointwise” আর “uniform” -এর পার্থক্য। Continuity আর
uniform continuity-র সংজ্ঞার একমাত্র পার্থক্য হলো ∀ε ∀x ∃δ বনাম
∀ε ∃δ ∀x — quantifier-এর ক্রম। আর এই ক্রমের কারণেই দুটো সম্পূর্ণ
আলাদা ধারণা।
Distributed systems-এ এটা সরাসরি কামড়ায়: “প্রতিটা request-এর জন্য একটা
server আছে যে responsive” (∀∃) আর “একটা server আছে যে সব request-এর
জন্য responsive” (∃∀) — দ্বিতীয়টা অনেক শক্ত গ্যারান্টি।
“`∀i (0 ≤ i \< n ∧ A[i] > 0)` — এটা 'array-এর সব element ধনাত্মক' বোঝায়।”
না, এটা সবসময় মিথ্যা (যদি domain সব পূর্ণসংখ্যা হয়)।
কারণ এটা দাবি করছে: “প্রতিটা পূর্ণসংখ্যা i-এর জন্য, i range-এ আছে
এবং A[i] ধনাত্মক।” কিন্তু i = 1000000 range-এ নেই, তাই
conjunction মিথ্যা, তাই ∀ মিথ্যা।
সঠিক রূপ implication দিয়ে:
∀i (0 ≤ i \< n → A[i] > 0)“যদি i range-এ থাকে, তবে A[i] ধনাত্মক।” Range-এর বাইরের i-এর
জন্য premise মিথ্যা, তাই implication vacuously সত্য — ঠিক যেমন চাই।
নিয়ম: ∀ চায় →, ∃ চায় ∧।
“Predicate logic দিয়ে যেকোনো গাণিতিক দাবি প্রকাশ করা যায়।”
First-order logic দিয়ে অনেক কিছু যায়, কিন্তু সব নয়।
FOL-এ আপনি object নিয়ে quantify করতে পারেন (∀x যেখানে x একটা সংখ্যা),
কিন্তু predicate বা set নিয়ে পারেন না (∀P যেখানে P একটা property)।
এই কারণে “প্রতিটা অ-খালি bounded set-এর একটা supremum আছে” — বাস্তব সংখ্যার সবচেয়ে গুরুত্বপূর্ণ ধর্মটা — first-order logic-এ লেখাই যায় না। এর জন্য লাগে second-order logic।
আর এই সীমাবদ্ধতার একটা ভয়ংকর সুন্দর পরিণতি আছে: Gödel দেখিয়েছেন যথেষ্ট শক্তিশালী যেকোনো formal system-এ এমন সত্য বাক্য থাকবে যা সেই system-এ প্রমাণ করা যায় না।
Level 13-এ আমরা এই গল্পটা পুরো করব — এবং দেখব এর সাথে halting problem-এর সরাসরি যোগ আছে।
বুঝেছেন কি না দেখুন
1এই বাক্যটা negate করুন: “প্রতিটা student অন্তত একটা course-এ ভর্তি হয়েছে।”
প্রথমে formula লিখুন, তারপর negate করুন, তারপর ফলাফলটা বাংলায় বলুন।
প্রয়োগ
E(s, c) = “student s, course c-তে ভর্তি”।
মূল দাবি:
∀s ∃c E(s, c)Negate করি, ধাপে ধাপে:
¬∀s ∃c E(s, c)
≡ ∃s ¬∃c E(s, c) [¬∀ → ∃¬]
≡ ∃s ∀c ¬E(s, c) [¬∃ → ∀¬]বাংলায়: “এমন অন্তত একজন student আছে যে কোনো course-এই ভর্তি হয়নি।”
লক্ষ্য করুন কী নয়:
- ❌ “কোনো student কোনো course-এ ভর্তি হয়নি” — সেটা
∀s ∀c ¬E(s,c), অনেক শক্ত দাবি - ❌ “প্রতিটা student কোনো course-এ ভর্তি হয়নি” — একই ভুল
যান্ত্রিক নিয়ম: বাইরে থেকে ভেতরে যান, প্রতিটা quantifier উল্টান
(∀ ↔ ∃), আর শেষে predicate-টা negate করুন। ভুল হওয়ার সুযোগ থাকে না।
2এই দুইটার মধ্যে কোনটা “array sorted” বোঝায়, আর অন্যটা কী বোঝায়?
(a) ∀i (0 ≤ i \< n−1 → A[i] ≤ A[i+1])
(b) ∀i ∀j (0 ≤ i \< j \< n → A[i] ≤ A[j])
যুক্তি
(a) ∀i (0 ≤ i \< n−1 → A[i] ≤ A[i+1])
(b) ∀i ∀j (0 ≤ i \< j \< n → A[i] ≤ A[j])দুটোই “sorted” বোঝায় — এরা logically equivalent। কিন্তু গঠনগতভাবে আলাদা, আর ব্যবহারিক পার্থক্য আছে।
(a) বলে: পাশাপাশি প্রতিটা জোড়া ক্রমে আছে — local শর্ত। (b) বলে: যেকোনো দুইটা element ক্রমে আছে — global শর্ত।
কেন equivalent: (b) → (a) স্পষ্ট (j = i+1 নিন)। (a) → (b) প্রমাণ
হয় induction দিয়ে — A[i] ≤ A[i+1] ≤ … ≤ A[j] transitivity দিয়ে চেইন করে।
ব্যবহারিক পার্থক্য বিশাল:
| (a) | (b) | |
|---|---|---|
| যাচাই করতে | O(n) তুলনা | O(n²) তুলনা |
| Verification-এ | maintenance step সহজ | invariant হিসেবে ব্যবহার সহজ |
তাই কোড লিখলে (a) ব্যবহার করবেন:
def is_sorted(A):
return all(A[i] <= A[i+1] for i in range(len(A)-1))কিন্তু insertion sort-এর correctness প্রমাণ করার সময় (b) বেশি সুবিধাজনক, কারণ সেখানে যেকোনো দুইটা element-এর সম্পর্ক নিয়ে যুক্তি করতে হয়।
একই সত্য, দুইটা রূপ — কোনটা বেছে নেবেন তা নির্ভর করে আপনি কী করতে চান তার উপর। এটা predicate logic-এর একটা গুরুত্বপূর্ণ ব্যবহারিক দক্ষতা।
3Binary search-এর জন্য precondition, postcondition আর loop invariant লিখুন
quantifier ব্যবহার করে।
def bsearch(A, target):
lo, hi = 0, len(A)
while lo \< hi:
mid = (lo + hi) // 2
if A[mid] \< target: lo = mid + 1
else: hi = mid
return lo
ডিজাইন
def bsearch(A, target):
lo, hi = 0, len(A)
while lo \< hi:
mid = (lo + hi) // 2
if A[mid] \< target: lo = mid + 1
else: hi = mid
return loএই version-টা lower bound ফেরত দেয় — প্রথম index যেখানে
A[index] ≥ target।
Precondition:
∀i (0 ≤ i \< n−1 → A[i] ≤ A[i+1])Array sorted হতেই হবে। না হলে ফলাফল অর্থহীন (crash হবে না, নীরবে ভুল হবে — যা আরো খারাপ)।
Loop invariant:
INV : 0 ≤ lo ≤ hi ≤ n
∧ ∀k (0 ≤ k \< lo → A[k] \< target)
∧ ∀k (hi ≤ k \< n → A[k] ≥ target)বাংলায়: “lo-এর বামের সব element target-এর ছোট, hi-এর ডানের সব
element target-এর সমান বা বড়। উত্তরটা [lo, hi) -এর ভেতরে আছে।”
যাচাই:
Initialization — lo = 0, hi = n। দুইটা ∀-ই খালি range-এর উপর,
তাই vacuously সত্য ✓ (এখানে vacuous truth কাজে লাগল!)
Maintenance — A[mid] \< target হলে lo = mid+1। Sorted বলে
∀k ≤ mid, A[k] ≤ A[mid] \< target ✓। অন্যথায় hi = mid, আর
∀k ≥ mid, A[k] ≥ A[mid] ≥ target ✓
Termination — lo == hi। Invariant থেকে:
∀k (0 ≤ k \< lo → A[k] \< target) ∧ ∀k (lo ≤ k \< n → A[k] ≥ target)এটাই lower bound-এর সংজ্ঞা ✓
Postcondition:
0 ≤ result ≤ n
∧ ∀k (0 ≤ k \< result → A[k] \< target)
∧ ∀k (result ≤ k \< n → A[k] ≥ target)Termination প্রমাণ: প্রতিবার hi − lo কঠোরভাবে কমে (mid \< hi
সবসময়, তাই lo = mid+1 ≤ hi আর hi = mid \< পুরনো hi)। ধনাত্মক পূর্ণসংখ্যা
অসীমবার কমতে পারে না। ∎
একটা গুরুত্বপূর্ণ পর্যবেক্ষণ: (lo + hi) // 2 — Python-এ নিরাপদ
(arbitrary precision integer), কিন্তু C/Java-তে overflow করতে পারে।
সঠিক রূপ lo + (hi - lo) // 2। এই bug Java-র standard library-তে
৯ বছর ছিল। Invariant-এ 0 ≤ lo ≤ hi ≤ n লেখা থাকলেও ধরা পড়ত না,
কারণ overflow invariant-এর বাইরের একটা মেশিন-স্তরের সমস্যা —
এটা Level 1-এর বিষয়।
4SQL-এ সরাসরি FORALL নেই কেন? আর “যেসব customer সব product কিনেছে”
এই query কীভাবে লিখবেন?
যুক্তি
FORALL নেই কেন? আর “যেসব customer সব product কিনেছে”
এই query কীভাবে লিখবেন?কেন নেই: SQL-এর ভিত্তি relational algebra, যেখানে মৌলিক operator
হলো selection, projection, union, difference, product। ∀ এদের মধ্যে
মৌলিক নয় — এটা derived, ¬∃¬ দিয়ে।
আর NOT EXISTS implement করা সহজ (anti-join), যেখানে সরাসরি ∀
implement করতে গেলে grouping আর counting লাগত। তাই ভাষা-নকশায় শুধু
EXISTS রাখা হয়েছে।
Query — double negation পদ্ধতি:
∀p Bought(c, p) ≡ ¬∃p ¬Bought(c, p)“এমন কোনো product নেই যেটা এই customer কেনেনি।”
SELECT c.id, c.name
FROM customers c
WHERE NOT EXISTS (
SELECT 1 FROM products p
WHERE NOT EXISTS (
SELECT 1 FROM purchases pu
WHERE pu.customer_id = c.id AND pu.product_id = p.id
)
);দুইটা nested NOT EXISTS — এটাকে বলে relational division, আর
ঐতিহাসিকভাবে এটা SQL-এর সবচেয়ে কুখ্যাত কঠিন pattern।
বিকল্প — counting দিয়ে:
SELECT pu.customer_id
FROM purchases pu
GROUP BY pu.customer_id
HAVING COUNT(DISTINCT pu.product_id) = (SELECT COUNT(*) FROM products);সহজে পড়া যায়, প্রায়ই দ্রুতও। কিন্তু এটা ∀-এর সরাসরি অনুবাদ নয় —
এটা একটা চাতুর্য যা কাজ করে কারণ “সব product কেনা” মানে “distinct
product-এর সংখ্যা = মোট product সংখ্যা”।
তুলনা:
NOT EXISTS | COUNT | |
|---|---|---|
| Logic-এর সাথে মিল | সরাসরি | পরোক্ষ |
| পাঠযোগ্যতা | কঠিন | সহজ |
| NULL-এর আচরণ | সতর্ক থাকতে হয় | DISTINCT NULL বাদ দেয় |
| Performance | প্রায়ই anti-join, দ্রুত | grouping লাগে |
Level 8-এ আমরা দেখব planner এই দুটোর জন্য কী plan বানায়।
5এই দাবিটা কি সত্য? ∀x ∃y (y > x) — domain হিসেবে (ক) পূর্ণসংখ্যা,
(খ) int32, (গ) খালি set নিন।
প্রয়োগ
∀x ∃y (y > x) — domain হিসেবে (ক) পূর্ণসংখ্যা,
(খ) int32, (গ) খালি set নিন।(ক) পূর্ণসংখ্যা — সত্য। যেকোনো x-এর জন্য y = x + 1 নিন। পূর্ণসংখ্যা
অসীম, তাই সবসময় বড় একটা আছে।
(খ) int32 — মিথ্যা। x = 2147483647 (INT_MAX) নিলে এর চেয়ে বড়
কোনো int32 নেই। Counterexample আছে, তাই ∀ মিথ্যা।
এটাই সেই ফাটল যেখানে বাস্তব bug জন্মায়:
for (int i = 0; i <= n; i++) { ... }n == INT_MAX হলে এই loop কখনো শেষ হবে না। i যখন INT_MAX-এ
পৌঁছে i++ করে, তখন signed overflow — C-তে undefined behaviour, বাস্তবে
সাধারণত INT_MIN-এ wrap করে। Loop চিরকাল চলে।
গাণিতিক অন্তর্জ্ঞান বলে “i একসময় n ছাড়িয়ে যাবে” — কিন্তু সেই অন্তর্জ্ঞান অসীম domain ধরে নিয়েছে। Machine-এ domain সসীম।
আরো খারাপ: compiler ধরে নেয় signed overflow ঘটে না (UB), তাই সে এই loop-কে infinite ধরে optimize করতে পারে — বা bound check মুছে দিতে পারে। বাস্তব CVE এভাবেই জন্মেছে।
(গ) খালি domain — সত্য (vacuously)। ∀x -এর কোনো x নেই, তাই
কোনো counterexample নেই।
মজার ব্যাপার, খালি domain-এ ∃y (y > x)-ও প্রশ্নই ওঠে না, কারণ ভেতরের
অংশে পৌঁছানোই যায় না।
মূল শিক্ষা: গাণিতিক দাবি সত্য কি না তা domain-এর উপর নির্ভরশীল। আর প্রোগ্রামিং-এ domain মানে type। “এই code গাণিতিকভাবে ঠিক” বলা যথেষ্ট নয় — “এই type-এ ঠিক” বলতে হবে।
Level 1-এ আমরা ঠিক এই সীমানাগুলো — INT_MAX, overflow, wraparound —
bit ধরে ধরে দেখব।
এরপর কী
এখন আমাদের হাতে দাবি প্রকাশ করার পূর্ণ ভাষা আছে: proposition, connective, predicate, quantifier।
কিন্তু একটা দাবি লিখতে পারা আর সেটা সত্য প্রমাণ করা আলাদা জিনিস।
পরের লেসনে আসছে proof techniques — direct proof, contrapositive, contradiction, case analysis, counterexample। কখন কোনটা ব্যবহার করবেন, আর কীভাবে একটা প্রমাণ এমনভাবে লিখবেন যাতে অন্য কেউ (বা একটা যন্ত্র) সেটা যাচাই করতে পারে।
তারপর induction — যেটা recursion আর loop-এর correctness প্রমাণের একমাত্র হাতিয়ার, আর যেটা ছাড়া এই কারিকুলামের বাকি অংশে এগোনো যাবে না।
আরও পড়ুন
- Discrete Mathematics and Its Applications, §1.4–1.5 — Kenneth Rosen
- Program Proofs — K. Rustan M. Leino · Dafny দিয়ে হাতে-কলমে verification — quantifier-এর সবচেয়ে ব্যবহারিক প্রয়োগ