Predicate abstraction
منطق میں، پیشن گوئی خلاصہ ایک فارمولے سے پیشن گوئی پیدا کرنے کا نتیجہ ہے۔ اگر Q کوئی فارمولا ہے تو اس جملے سے تشکیل شدہ پیش گوئی خلاصہ (λx. Q) ہے، جہاں λ ایک تجریدی آپریٹر ہے اور جس میں x کا ہر واقعہ جو Q میں آزاد ہے λ in (λx. Q) سے جڑا ہوا ہے۔ نتیجے میں پیش گوئی (λx. Q (x)) ایک موناڈک پیش گوئی ہے جو (λx. Q (x)) (t) کی طرح ایک اصطلاح t کو دلیل کے طور پر لینے کی صلاحیت رکھتی ہے، جس میں کہا گیا ہے کہ 't' سے ظاہر ہونے والی شے کی خاصیت ایسی ہے کہ Q. ریاستیں (λx. Q (x)) (t) ष्णق ق (t/x) جہاں ق (t/x) ق میں x کے تمام آزاد واقعات کو t سے تبدیل کرنے کا نتیجہ ہے۔ یہ قانون عام طور پر کم از کم دو صورتوں میں ناکام ثابت ہوتا ہے: (i) جب t غیر حوالہ جاتی ہے اور (ii) جب ق میں موڈل آپریٹرز ہوتے ہیں۔ موڈل منطق میں "ڈی ری/ڈی ڈکٹو فرق" کو 1 کے طور پر بیان کیا گیا ہے۔ (ڈی ڈی سی ٹی او): 2. (ڈی ای آر ای): (1) میں موڈل آپریٹر فارمولا اے (ٹی) پر لاگو ہوتا ہے اور اصطلاح ٹی موڈل آپریٹر کے دائرہ کار میں ہے۔ (2) t میں موڈل آپریٹر کے دائرہ کار میں نہیں ہے۔ سیمنٹکس کے لیے حوالہ جات اور پیش گوئی تجریدی کی مزید فلسفیانہ پیش رفت دیکھیں فٹنگ اور مینڈیلسوہن، فرسٹ آرڈر ماڈل لاجک، سپرنگر، 1999۔ موڈل منطق فلسفیانہ منطق