نمایش مبدأ برای حذف عطف

{{جعبه اطلاعات حکم ریاضیاتی|name=حذف عطف|type=[[قاعده استنتاج]]|field=[[حساب گزاره‌ای]]|statement=اگر ترکیب عطفی <math>A</math> و <math>B</math> درست باشد، آنگاه هر دوی <math>A</math> و <math>B</math> درست هستند.|symbolic statement=# <math>\frac{P \land Q}{\therefore P}, \frac{P \land Q}{\therefore Q}</math>
# <math>(P \land Q) \vdash P, (P \land Q) \vdash Q</math>
# <math> (P \land Q) \to P,(P \land Q) \to Q</math>|conjectured by=|conjecture date=|first stated by=|first proof by=|first proof date=|open problem=|known cases=|implied by=|equivalent to=|generalizations=|consequences=}}
{{قواعد تبدیل}}

در [[حساب گزاره‌ای]]، '''حذف عطف''' {{به انگلیسی|Conjunction elimination}}<ref>{{cite book|author=David A. Duffy|title=Principles of Automated Theorem Proving|url=https://archive.org/details/principlesofauto0000duff|location=New York|publisher=Wiley|year=1991}} Sect.3.1.2.1, p.46</ref> یک [[استدلال مباشر]] [[اعتبار (منطق)|معتبر]]، [[صورت منطقی]] و [[قاعده استنتاج|قاعدهٔ استنتاج]] است که این [[استنباط|استنتاج]] را می‌سازد که اگر [[عطف منطقی|ترکیب عطفی]] <math>A</math> و <math>B</math> درست باشد، آنگاه هر دوی <math>A</math> و <math>B</math> درست هستند.

این قاعده شامل دو قاعدهٔ فرعی جداگانه است که می‌تواند به [[نظریه زبان‌ها|زبان صوری]] به‌صورت زیر بیان شود:

: <math>\frac{P \land Q}{\therefore P}</math>
و
: <math>\frac{P \land Q}{\therefore Q}</math>

دو قاعدهٔ فرعی با هم به این معنی است که هر زمان که یک نمونه از "<math>P \land Q</math>"در خط یک اثبات ظاهر می‌شود، "<math>P</math>" یا "<math>Q</math>" را می‌توان به تنهایی در خط بعدی قرار داد.

== نشانه‌گذاری به‌شکل صوری ==
قواعد فرعی ''حذف عطف'' ممکن است به‌صورت زیر نوشته شوند:

: <math>(P \land Q) \vdash P</math>
و
: <math>(P \land Q) \vdash Q</math>

و همچنین <math>\vdash</math> یک نماد [[فرامنطق]] است که به این معنی است که <math>P</math> نتیجهٔ منطقی <math>P \land Q</math> و <math>Q</math> است و همچنین یک نتیجهٔ نحوی از <math>P \land Q</math> در [[دستگاه صوری]] می‌باشد.

و می‌توانند به‌صورت [[همان‌گویی (منطق)|همان‌گویی]]<nowiki/>‌های حساب گزاره‌ای بیان شوند:

: <math>(P \land Q) \to P</math>
و
: <math>(P \land Q) \to Q</math>
== منابع ==
{{پانویس|۲}}
[[رده:قضیه‌ها در حساب گزاره‌ای]]
[[رده:قواعد استنتاج]]