First-order Predicate Logic Study Notes

First-order Predicate Logic

Propositional Logic ၏ ကန့်သတ်ချက်များ (Limitation of Propositional Logic)

• လက်တွေ့ကျသော ပြဿနာအများအပြားကို Propositional Logic (အဆိုပြုကိန်းယုတ္တိဗေဒ) ဖြင့် ဖော်ပြရန် ခက်ခဲခြင်း သို့မဟုတ် အဆင်မပြေခြင်းများ ရှိပါသည်။
• ဥပမာ - စက်ရုပ်၏တည်နေရာ (Robot Position Example):
  • "Robot 7 သည် တည်နေရာ $xy(35, 79)$ တွင် ရှိသည်" ဆိုသော အချက်ကို ဖော်ပြရန် Robot_7_is_situated_at_xy_position_(35, 79) ဟူသော variable တစ်ခုလုံးကို အသုံးပြုရမည်ဖြစ်သည်။
  • အကယ်၍ စက်ရုပ်အစီးရေ $100$ ရှိပြီး $100 \times 100$ ရှိသော grid ကွက်ပေါ်တွင် ရပ်နားနိုင်သည်ဟု ယူဆပါက၊ စက်ရုပ်တိုင်း၏ တည်နေရာအားလုံးကို ဖော်ပြရန် $100 \times 100 \times 100 = 1,000,000 = 10^6$ သော မတူညီသည့် variables ပေါင်းများစွာ လိုအပ်မည်ဖြစ်သည်။
  • "Robot 7 သည် Robot 12 ၏ ညာဘက်တွင် ရှိသည်" ဟူသော အချက်ကို ဖော်ပြရန် $Robot_7\_is\_to\_the\_right\_of\_robot\_12 \Leftrightarrow Robot_7\_is\_situated\_at\_xy\_position\_(35, 79) \wedge Robot_{12}\_is\_situated\_at\_xy\_position\_(10, 93) \vee \dots$ စသည်ဖြင့် အလွန်ရှည်လျားစွာ ရေးသားရမည်ဖြစ်သည်။
• ဖြေရှင်းချက်: First-order predicate logic တွင် Position(number, xPosition, yPosition) ဟူသော predicate တစ်ခုတည်းဖြင့် လွယ်ကူစွာ ဖော်ပြနိုင်သည်။

Syntax (သဒ္ဒါစည်းမျဉ်းများ)

• Definition 3.1: Terms (အခေါ်အဝေါ်များ)

  • Variable များအစု $V$၊ Constant (ကိန်းသေ) များအစု $K$ နှင့် Function သင်္ကေတများအစု $F$ တို့သည် တစ်ခုနှင့်တစ်ခု မထပ်သော (pairwise disjoint) အစုများဖြစ်သည်။
  • Variable များ နှင့် Constant များအားလုံးသည် (atomic) terms များဖြစ်သည်။
  • အကယ်၍ $t_1, \dots, t_n$ တို့သည် terms များဖြစ်ပြီး $f$ သည် $n-place$ ရှိသော function သင်္ကေတဖြစ်ပါက $f(t_1, \dots, t_n)$ သည်လည်း term တစ်ခုဖြစ်သည်။

• Definition 3.2: Predicate Logic Formulas (ပုံသေနည်းများ တည်ဆောက်ပုံ)

  • အကယ်၍ $t_1, \dots, t_n$ တို့သည် terms များဖြစ်ပြီး $p$ သည် $n-place$ ရှိသော predicate သင်္ကေတဖြစ်ပါက $p(t_1, \dots, t_n)$ သည် (atomic) formula တစ်ခုဖြစ်သည်။
  • အကယ်၍ $A$ နှင့် $B$ တို့သည် formulas များဖြစ်ပါက $\neg A$, $(A)$, $A \wedge B$, $A \vee B$, $A \Leftrightarrow B$, $A \Rightarrow B$ တို့သည်လည်း formulas များဖြစ်သည်။
  • အကယ်၍ $x$ သည် variable တစ်ခုဖြစ်ပြီး $A$ သည် formula တစ်ခုဖြစ်ပါက $\forall x A$ ( universal quantifier) နှင့် $\exists x A$ (existential quantifier) တို့သည်လည်း formulas များဖြစ်သည်။
  • Literals: $p(t_1, \dots, t_n)$ နှင့် $\neg p(t_1, \dots, t_n)$ တို့ကို literals ဟု ခေါ်သည်။
  • First-order Sentences (Closed Formulas): variable အားလုံးသည် quantifier တစ်ခုခု၏ scope အတွင်း၌ ရှိနေသော formulas များကို ခေါ်သည်။
  • Free Variables: quantifier ၏ scope အတွင်း၌ မရှိသော variables များကို ခေါ်သည်။
  • အခြား: CNF (Conjunctive Normal Form) နှင့် Horn clauses सम्ဗန္ဓသော အဓိပ္ပာယ်ဖွင့်ဆိုချက်များသည် predicate logic literals များအတွက်လည်း အလားတူ သက်ရောက်သည်။

First-order Predicate Logic ပုံသေနည်း ဥပမာများ

• $\forall x \, \text{frog}(x) \Rightarrow \text{green}(x)$: ဖားအားလုံးသည် အစိမ်းရောင်ဖြစ်သည်။
• $\forall x \, \text{frog}(x) \wedge \text{brown}(x) \Rightarrow \text{big}(x)$: ဖားအညိုရောင်အားလုံးသည် ကြီးမားသည်။
• $\forall x \, \text{likes}(x, \text{cake})$: လူတိုင်း ကိတ်မုန့်ကြိုက်သည်။
• $\neg \forall x \, \text{likes}(x, \text{cake})$: လူတိုင်း ကိတ်မုန့်ကြိုက်သည်မဟုတ်။
• $\neg \exists x \, \text{likes}(x, \text{cake})$: ဘယ်သူမှ ကိတ်မုန့်မကြိုက်ပါ။
• $\exists x \, \forall y \, \text{likes}(y, x)$: လူတိုင်းကြိုက်သော အရာတစ်ခုရှိသည်။
• $\exists x \, \forall y \, \text{likes}(x, y)$: အရာအားလုံးကို ကြိုက်သော လူတစ်ယောက်ရှိသည်။
• $\forall x \, \exists y \, \text{likes}(y, x)$: အရာအားလုံးသည် တစ်စုံတစ်ယောက်၏ အကြိုက်ဖြစ်ခြင်း ခံရသည်။
• $\forall x \, \exists y \, \text{likes}(x, y)$: လူတိုင်းတွင် သူတို့ကြိုက်သောအရာ တစ်ခုခုရှိသည်။
• $\forall x \, \text{customer}(x) \Rightarrow \text{likes}(\text{bob}, x)$: Bob သည် customer တိုင်းကို ကြိုက်သည်။
• $\exists x \, \text{customer}(x) \wedge \text{likes}(x, \text{bob})$: Bob ကို ကြိုက်သော customer တစ်ယောက်ရှိသည်။
• $\exists x \, \text{baker}(x) \wedge \forall y \, \text{customer}(y) \Rightarrow \text{likes}(x, y)$: မိမိ၏ customer အားလုံးကို ကြိုက်သော မုန့်ဖုတ်သမားတစ်ယောက်ရှိသည်။
• $\forall x \, \text{older}(\text{mother}(x), x)$: အမေတိုင်းသည် သူမ၏ကလေးထက် အသက်ကြီးသည်။
• $\forall x \, \text{older}(\text{mother}(\text{mother}(x)), x)$: အဘွားတိုင်းသည် မြေးထက် အသက်ကြီးသည်။
• $\forall x \, \forall y \, \forall z \, \text{rel}(x, y) \wedge \text{rel}(y, z) \Rightarrow \text{rel}(x, z)$: rel သည် ကူးပြောင်းဆက်နွယ်မှု (transitive relation) တစ်ခုဖြစ်သည်။

Semantics (အဓိပ္ပာယ်ဗေဒ)

• Example 3.1: $c_1, c_2, c_3$ များသည် constants များဖြစ်ပြီး plus သည် two-place function ဖြစ်ကာ gr သည် two-place predicate ဖြစ်သည်။ ပုံသေနည်း $F \equiv \text{gr}(\text{plus}(c_1, c_3), c_2)$ ၏ အမှန်တရားမှာ interpretation ပေါ်တွင် မူတည်သည်။
  • Interpretation $I_1$: $c_1 \rightarrow 1, c_2 \rightarrow 2, c_3 \rightarrow 3, plus \rightarrow +, gr \rightarrow >$
    • ရလဒ်: $1 + 3 > 2$ သို့မဟုတ် $4 > 2$ (မှန်သည်)။
    • အစု $G = \{(4, 3), (4, 2), (4, 1), (3, 2), (3, 1), (2, 1)\}$ တွင် $(4, 2) \in G$ ဖြစ်၍ မှန်ခြင်းဖြစ်သည်။
  • Interpretation $I_2$: $c_1 \rightarrow 2, c_2 \rightarrow 3, c_3 \rightarrow 1, plus \rightarrow -, gr \rightarrow >$
    • ရလဒ်: $2 - 1 > 3$ သို့မဟုတ် $1 > 3$ (မှားသည်)။

မိသားစုသစ်ပင် ဥပမာ (Family Tree Example)

• အချက်အလက်များ:
  • Constant များ: Karen A., Franz A., Anne A., Oscar A., Mary B., Oscar B., Henry A., Eve A., Isabelle A., Clyde B.
  • Child (ကလေး) ဆက်နွယ်မှု: (Oscar A., Karen A., Franz A.) ၏ အဓိပ္ပာယ်မှာ Oscar A. သည် Karen A. နှင့် Franz A. တို့၏ ကလေးဖြစ်သည်။
  • Female (အမျိုးသမီး): {Karen A., Anne A., Mary B., Eve A., Isabelle A.} အစုဖြစ်သည်။
• ယုတ္တိဗေဒဆိုင်ရာ စည်းမျဉ်းများ (Rules):
  • $\forall x \, \forall y \, \forall z \, \text{child}(x, y, z) \Leftrightarrow \text{child}(x, z, y)$ (မိဘနှစ်ပါးနေရာလဲလှယ်နိုင်ခြင်း)
  • $\forall x \, \forall y \, \text{descendant}(x, y) \Leftrightarrow \exists z \, \text{child}(x, y, z) \vee (\exists u \, \exists v \, \text{child}(x, u, v) \wedge \text{descendant}(u, y))$ (မျိုးဆက်ဆိုင်ရာ အဓိပ္ပာယ်ဖွင့်ဆိုချက်)
• Knowledge Base (KB): အမျိုးသမီးဖြစ်ခြင်း၊ ကလေးဖြစ်ခြင်း အချက်အလက်များနှင့် အထက်ပါ စည်းမျဉ်းများကို $\wedge$ (and) ဖြင့် ချိတ်ဆက်ထားသော ပုံစံဖြစ်သည်။

Equality (တူညီခြင်း)

• တူညီခြင်းဆိုင်ရာ အခြေခံစည်းမျဉ်းများ:
  • $\forall x \, x = x$ (Reflexivity - ရောင်ပြန်ဟပ်ခြင်း)
  • $\forall x \, \forall y \, x = y \Rightarrow y = x$ (Symmetry - အချိုးညီခြင်း)
  • $\forall x \, \forall y \, \forall z \, x = y \wedge y = z \Rightarrow x = z$ (Transitivity - ကူးပြောင်းခြင်း)
  • Substitution Axioms (အစားထိုးခြင်း):
    • $\forall x \, \forall y \, x = y \Rightarrow f(x) = f(y)$
    • $\forall x \, \forall y \, x = y \Rightarrow p(x) \Leftrightarrow p(y)$
• သတိပြုရန် (Example 3.3): $\forall x \, x = y$ တွင် free variable $y$ ကို အစားထိုးရာ၌ $x + 1$ ဖြင့် မှားယွင်းအစားထိုးပါက $\forall x \, x = x + 1$ ဖြစ်သွားနိုင်သည်။ မှန်ကန်သော အစားထိုးမှုမှာ $\forall x \, x = y + 1$ ဖြစ်သင့်ပြီး ၎င်းတို့သည် semantic အားဖြင့် မတူညီပါ။

Quantifier များ၏ ဂုဏ်သတ္တိများ

• $\forall x \, p(x)$ သည် variable $x$ ၏ interpretations အားလုံးအတွက် မှန်မှသာ မှန်ကန်သည်။
• Constants များအစု $K = \{a_1, \dots, a_n\}$ ဖြစ်ပါက:
  • $\forall x \, p(x) = p(a_1) \wedge \dots \wedge p(a_n)$
  • $\exists x \, p(x) = p(a_1) \vee \dots \vee p(a_n)$
• de Morgan’s law: $\forall x \, \phi \equiv \neg \exists x \, \neg \phi$ (တစ်ဦးနှင့်တစ်ဦး အပြန်အလှန် အစားထိုးနိုင်သည်)
• Expressive Power: Quantifiers များသည် predicate logic ၏ ဖော်ပြနိုင်စွမ်းကို မြှင့်တင်ပေးသော်လည်း Automatic Inference (အလိုအလျောက် အနုမာနပြုခြင်း) တွင် အနှောင့်အယှက် ဖြစ်စေနိုင်သည်။ အကြောင်းမှာ:
  • Formula များ၏ တည်ဆောက်ပုံကို ပိုမိုရှုပ်ထွေးစေသည်။
  • Proof process ၏ အဆင့်တိုင်းတွင် အသုံးပြုနိုင်သော inference rules အရေအတွက်ကို တိုးပွားစေသည်။

ပုံမှန်သဏ္ဌာန်များ (Normal Forms)

NORMALFORMTRANSFORMATION(Formula) အဆင့်ဆင့်:

1. Prenex normal form သို့ ပြောင်းလဲခြင်း:
   • Equivalences များကို ဖယ်ရှားခြင်း။
   • Implications များကို ဖယ်ရှားခြင်း။
   • de Morgan's law နှင့် distributive law များကို ထပ်ခါတလဲလဲ အသုံးပြုခြင်း။
   • လိုအပ်ပါက variables များကို နာမည်အသစ်ပေးခြင်း (Renaming)။
   • Universal quantifiers များကို အပြင်ထုတ်ခြင်း (Factoring out)။
2. Skolemization:
   • Existentially quantified variables ($\exists$) များကို Skolem functions အသစ်များဖြင့် အစားထိုးခြင်း။
   • ကျန်ရှိနေသော universal quantifiers များကို ဖယ်ရှားခြင်း။

Skolemization အသေးစိတ်

• Existential quantifiers ($\exists$) အားလုံးကို ဖယ်ရှားခြင်း ဖြစ်သည်။
• ဥပမာ: $\forall x_1 \, \forall x_2 \, \exists y_1 \, \forall x_3 \, \exists y_2 \, p(f(x_1), x_2, y_1) \vee q(y_1, x_3, y_2)$
  • $y_1$ ကို $g(x_1, x_2)$ ဖြင့် အစားထိုးသည်။
  • $y_2$ ကို $h(x_1, x_2, x_3)$ ဖြင့် အစားထိုးသည်။
• General rule: $\forall x_1 \, \dots \, \forall x_n \, \exists y \, \phi$ ကို $\forall x_1 \, \dots \, \forall x_n \, \phi[y / f(x_1, \dots, x_n)]$ ဖြင့် အစားထိုးသည်။
• $\exists y \, p(y)$ ကဲ့သို့သော အခြေအနေတွင် $y$ ကို constant (zero-place function) ဖြင့် အစားထိုးရမည်။
• ထိရောက်မှု: Skolemization သည် literlas အရေအတွက်ပေါ် မူတည်၍ polynomial runtime ရှိသော်လည်း၊ normal form ပြောင်းရာတွင် literals အရေအတွက်သည် exponential အဆမတန် တိုးလာနိုင်သဖြင့် တွက်ချက်မှုကြာချိန်နှင့် memory အသုံးပြုမှု များပြားနိုင်သည်။

Proof Calculi (သက်သေပြမှုတွက်နည်းများ)

• Modus Ponens (MP): $\frac{A, A \Rightarrow B}{B}$
• Universal Elimination ($\forall E$): $\frac{\forall x A}{A[x/t]}$

Child(eve, oscar, anne) အတွက် သက်သေပြချက် (Simple Proof)

1. child(eve, anne, oscar) (Fact)
2. $\forall x \, \forall y \, \forall z \, \text{child}(x, y, z) \Rightarrow \text{child}(x, z, y)$ (KB rule)
3. child(eve, anne, oscar) → child(eve, oscar, anne) (From step 2 by $\forall E$: x/eve, y/anne, z/oscar)
4. child(eve, oscar, anne) (From 1 and 3 by Modus Ponens)

Resolution (ပြန်လည်ဖြေရှင်းမှုနည်းလမ်း)

• သက်သေပြလိုသော အချက် (Q) ကို ငြင်းဆိုချက် ($\neg Q$) အဖြစ် ယူဆပြီး KB နှင့် ပေါင်းစပ်ကာ ဖြစ်ရပ်မရှိ (empty clause/contradiction) ထွက်သည်အထိ လုပ်ဆောင်ခြင်းဖြစ်သည်။
• Unification (ယူနီဖီကေးရှင်း): variables များအား terms များဖြင့် အစားထိုး၍ match ဖြစ်အောင် လုပ်ဆောင်ခြင်း။
• Resolution Rule:
  • $\frac{(A_1 \vee \dots \vee A_m \vee B), (\neg B' \vee C_1 \vee \dots \vee C_n), \sigma(B) = \sigma(B')}{(\sigma(A_1) \vee \dots \vee \sigma(A_m) \vee \sigma(C_1) \vee \dots \vee \sigma(C_n))}$
  • ဤတွင် $\sigma$ သည် B နှင့် B' တို့၏ MGU (Most General Unifier) ဖြစ်သည်။
• Factorization Rule:
  • $\frac{(A_1 \vee A_2 \vee \dots \vee A_n), \sigma(A_1) = \sigma(A_2)}{(\sigma(A_2) \vee \dots \vee \sigma(A_n))}$
• Theorem 3.6: Resolution rule နှင့် Factorization rule တို့ ပေါင်းစပ်ပါက Refutation Complete ဖြစ်သည်။ ဆိုလိုသည်မှာ မမှန်ကန်သော (unsatisfiable) ပုံသေနည်းတိုင်းမှ empty clause ကို ထုတ်ယူနိုင်သည်။

Barber Paradox Resolution Example

• "မိမိကိုယ်ကို မရိတ်သောသူတိုင်းကို ရိတ်ပေးသော ဆံပင်ညှပ်ဆရာတစ်ဦးရှိသည်။"
• $\forall x \, \text{shaves}(\text{barber}, x) \Leftrightarrow \neg \text{shaves}(x, x)$
• ပုံစံပြောင်းလဲပြီး literals နှစ်ခုရရှိ:
  1. $(\neg \text{shaves}(\text{barber}, x) \vee \neg \text{shaves}(x, x))$
  2. $(\text{shaves}(\text{barber}, x) \vee \text{shaves}(x, x))$
• Factorization (x/barber အစားသွင်းခြင်း):
  3. $(\neg \text{shaves}(\text{barber}, \text{barber}))$
  4. $(\text{shaves}(\text{barber}, \text{barber}))$
• Resolution (3 နှင့် 4 ကြား): ထွက်ပေါ်လာသော ရလဒ်မှာ Empty clause ( ) ဖြစ်ပြီး ပုစ္ဆာသည် ရှေ့နောက်မညီသော paradox ဖြစ်ကြောင်း သက်သေပြသည်။

Automated Theorem Provers

• ကွန်ပျူတာပေါ်တွင် သက်သေပြမှုတွက်နည်းများ (Proof Calculi) ကို လက်တွေ့အကောင်အထည်ဖော်ထားသော စနစ်များကို Theorem Provers ဟု ခေါ်ဆိုသည်။