ลิงก์ข้ามภาษาในบทความนี้ มีไว้ให้ผู้อ่านและผู้ร่วมแก้ไขบทความศึกษาเพิ่มเติมโดยสะดวก เนื่องจากวิกิพีเดียภาษาไทยยังไม่มีบทความดังกล่าว กระนั้น ควรรีบสร้างเป็นบทความโดยเร็วที่สุด |
ในตรรกศาสตร์เชิงพิสูจน์ ตัวบ่งปริมาณสำหรับตัวมีจริง (อังกฤษ: Existential quantifier) เป็นตัวบ่งปริมาณ ค่าทางตรรกศาสตร์ที่เท่ากับว่า "มี...บางตัว" หรือ "ฟอร์ซัม" หมายความว่า ฟังก์ชันของประพจน์นั้น ๆ สามารถใช้ได้กับบางตัวในโดเมน หรือก็คือ ฟังก์ชันของประพจน์นั้นมีความสัมพันธ์กับสมาชิกแค่เพียงบางตัวในโดเมนนั้น ๆ ซึ่งเงื่อนไขที่ใช้ เพียงเป็นจริงกับสมาชิกตัวใดตัวหนึ่ง ค่าความจริงจะเป็นจริงได้ทันที (เนื่องจากเป็นตัวบ่งปริมาณแบบบางตัว)
ใช้สัญลักษณ์ ∃ วางไว้กับตัวแปร ("∃x" หรือ "∃(x)") ตัวบ่งปริมาณแบบบางตัวนั้นตรงข้ามกับตัวบ่งปริมาณแบบทั้งหมด (สำหรับ...ใด ๆ) ซึ่งจะใช้สมาชิกในโดเมนทุกตัว (ดูหัวข้อใหญ่ที่)
รหัสของสัญลักษณ์นี้คือ U+2203 ∃ THERE EXISTS (HTML ∃
· ∃
) และ U+2204 ∄ THERE DOES NOT EXIST (HTML ∄
) (ไม่มี...ใด ๆ เลย)
พื้นฐาน
ให้เงื่อนไขเป็นจำนวนธรรมชาติใด ๆ ที่คูณด้วยตัวมันเองแล้วมีผลลัพธ์เป็น 25
หรือ หรือ หรือ ฯลฯ
ประโยคนี้ เป็นแบบการเลือกเชิงตรรกศาสตร์ เพราะมีการใช้ "และ" แบบซ้ำ ๆ แต่อย่างไรก็ดี "ฯลฯ" ไม่สามารถเขียนแบบตรรกศาสตร์มาตรฐานได้ จากประโยคดังกล่าวข้างต้น อาจนิยามได้อีกทีว่า:
ประโยคข้างต้น ใช้ตัวบ่งปริมาณแบบบางตัวเข้ามาช่วย
จากรูปประโยคข้างต้น จะมีความแม่นยำกว่าอันที่หนึ่ง ในขณะที่ "ฯลฯ" ไม่ได้เจาะจงว่ารวมจำนวนธรรมชาติทั้งหมด และไม่ได้บอกอะไรเพิ่ม เพราะไม่ได้กำหนดโดเมนอย่างชัดเจน ประโยคก็อาจจะไม่ได้เป็นการตีความอะไรมากนัก หรือจะพูดอีกอย่างก็คือ จำนวนธรรมชาตินั้นได้กำหนดไว้อย่างชัดเจน
ประโยคข้างต้นเป็นจริง เพราะ 5 เป็นจำนวนธรรมชาติ และเมื่อแทน 5 ด้วย n แล้ว จะได้สมการว่า ซึ่งเป็นจริง ไม่สำคัญว่า จะเป็นจริงกับเฉพาะจำนวนธรรมชาติ 5 เท่านั้น เพราะหากมีแค่สมาชิกตัวเดียวที่มาทำให้เงื่อนไขเป็นจริงได้ สำหรับตัวบ่งปริมาณบางตัวแล้ว ประโยคนั้นจะเป็นจริงทันที ในทางตรงกันข้าม หากเป็นประโยค:
เป็นเท็จ เนื่องจากไม่มีจำนวนคู่ใดคูณกันด้วยตัวมันเองแล้วได้ผลลัพธ์เท่ากับ 25
ใช้กำหนดว่าค่าตัวแปร n ใดบ้างที่จะนำมาใช้กับเงื่อนไข แต่ยังมีเรื่องของความเป็นจริงและเท็จของแต่ละประโยคนั้น ๆ ในบางครั้งตัวเชื่อมเชิงตรรกศาสตร์มาใช้กับเอกภพสัมพัทธ์เพื่อพิสูจน์ เช่น
กับ
จากตัวอย่างข้างต้น เราจะเติมการเชื่อมเชิงตรรกศาสตร์มาด้วย
สัญลักษณ์ "∃" (ตัว E กลับหัวในตระกูลฟอนต์ Sans-Serif) ใช้แทนตัวบ่งปริมาณแบบบางตัว (หรือบางทีอาจเขียนเฉพาะตัว V โดด ๆ)
ถ้า แทน และ คือเซตของจำนวนธรรมชาติ แล้ว:
เป็นประโยค (ซึ่งเป็นจริง):
ในทำนองเดียวกัน ถ้า แทน แล้ว :
เป็นประโยค (ซึ่งเป็นเท็จ)
ในเชิงคณิตศาสตร์ การพิสูจน์ตัว "บางตัว" อาจทำได้ในรูปแบบอื่น ซึ่งใช้แทนกันได้ หรือจะพิสูจน์โดยไม่ต้องแสดงเลยว่ายังไงผลลัพธ์ต้องเป็นอย่างนั้นแน่นอน
สมบัติ
การนิเสธ
ฟังก์ชันประพจน์ที่มีตัวบ่งปริมาณก็นับเป็นประโยค ดังนั้น ฟังก์ชันที่มีตัวบ่งปริมาณก็มีนิเสธได้ ส่วนใหญ่สัญลักษณ์แทนการนิเสธใช้
ตัวอย่างเช่น ถ้า P(x) เป็นฟังก์ชันประพจน์ว่า "0 < x < 1" แล้ว ให้เอกภพสัมพัทธ์เป็น x คือจำนวนธรรมชาติใด ๆ ตัวบ่งปริมาณแบบบางตัว "มี x บางตัวซึ่งมากกว่า 0 และน้อยกว่า 1" จะเขียนได้ในรูป:
ประโยคนี้อาจะเป็นเท็จได้ เพราะจริง ๆ ควรใช้ว่า "ไม่มีจำนวนธรรมชาติใด ๆ ที่มากกว่า 0 และน้อยกว่า 1" จะเขียนได้ในรูป:
ไม่มีสมาชิกในเอกภพสัมพัทธ์ใด ๆ ซึ่งจะทำให้เงื่อนไขนี้เป็นจริงได้ ดังนั้น สมาชิกทุกตัวจะขัดกับเงื่อนไข ซึ่งก็คือนิเสธ
สมมูลกับ "สำหรับจำนวนธรรมชาติ x ใด ๆ ซึ่ง x ไม่ได้มากกว่า 0 หรือน้อยกว่า 1"
โดยปกติแล้ว นิเสธของตัวบ่งปริมาณแบบบางตัวคือตัวบ่งปริมาณแบบทั้งหมด หรือนิยามได้ว่า:
เช่น กำหนดให้ว่า "ทุกคนยังไม่ได้แต่งงาน" (หรือ "ไม่มีใครเลยที่แต่งงานแล้ว") คือ "ไม่ใช่ทุกคนที่แต่งงานแล้ว (หรือ "มีคนที่ยังไม่ได้แต่งงาน") จะหมายความว่า
นิเสธของตัวบ่งปริมาณบางตัวยังรวมถึง "ไม่มีเลย":
ซึ่งไม่เหมือนกับตัวบ่งปริมาณแบบทั้งหมด ตัวบ่งปริมาณแบบบางตัวจะกระจายหากเป็นการเลือกเชิงตรรกศาสตร์ได้
กฎอุดมคติ
กฎอุดมคติเป็นกฎซึ่งใช้พิสูจน์ขั้นตอนจากสมมุติฐานสู่การสรุปออกมา มีกฎอุดมคติอยู่หลายกฎ ซึ่งนำไปใช้กับตัวบ่งปริมาณแบบบางตัว
ปริทัศน์ของตัวบ่งปริมาณแบบบางตัว (∃I) กล่าวไว้ว่าถ้าฟังก์ชันของประพจน์นั้นๆเป็นที่ทราบกันทั่วไปว่าเป็นจริง ดังนั้น จะต้องมีสมาชิกของฟังก์ชันของประพจน์ที่เป็นจริง หรือเขียนได้ในรูป:
การตัดทิ้งแบบตัวบ่งปริมาณแบบบางตัว (∃E) กล่าวไว้ว่า เมื่อดำเนินการหักล้างแบบฟิตช์ โดยการเติมนิพจน์ที่ได้จากการหักล้างย่อยเข้าไป โดยการเติมตัวบ่งปริมาณแบบบางตัว (ที่ติดตัวแปร) เข้าไปช่วย ซึ่งตัวบ่งปริมาณนี้ไม่เกี่ยวข้องกับการดำเนินการใด ๆ ของนิพจน์ที่นำมาเติม ถ้าผลได้ภายในการดำเนินการของตัวนิพจน์จากการหักล้างย่อยซึ่งไม่มีตัวบ่งปริมาณแบบบบางตัวนั้น ดังนั้นจะมีสมาชิกหนึ่งตัวซึ่งสามารถหักล้างตัวใดตัวหนึ่งของนิพจน์ที่ได้จากการหักล้างย่อยนั้น โดยเหตุผลของการตัดทิ้งแบบตัวบ่งปริมาณแบบางตัวคือ:
ถ้ากำหนดว่ามีสมาชิกตัวใดตัวหนึ่งที่ทำให้ฟังก์ชันของประพจน์นั้น ๆ เป็นจริง ถ้าผลใช้แทนกับการกำหนดชื่อเจาะจง (Arbitary Name) ได้ ผลนั้นจะเป็นจริงอย่างแน่นอน ตราบใดที่มันยังไม่มีชื่อ
เขียนได้ โดย:
ให้ชื่อเจาะจงเป็น c แล้ว Q เป็นประพจน์ซึ่งไม่มี c
ค่า c จะต้องเป็นจริงทุกตัวบนโดเมนเดียวกันกับ X หรือหากประพจน์ไม่เป็นไปตามตรรกะ จะได้ว่า:
หาก c ไม่ใช่ชื่อเจาะจง แล้วเป็นเพียงสมาชิกเฉพาะ (Specific Element) ในเอกภพสัมพัทธ์ แล้ว P(c) จะไม่สามารถให้เหตุผลแก่ประโยคนั้น ๆ ได้อีก
เซตว่าง
รูปแบบ จะเป็นเท็จเสมอ หากไม่ขึ้นกับ P(x) เนื่องจากเซตว่างจะไม่มีค่าอะไรกับ x
ให้ x โดด ๆ แสดงกับเงื่อนไข P(x) = "มี x ใด ๆ ในเซตว่าง": ดูเพิ่มที่
จุดเชื่อม
หัวข้อหลัก : (ตัวบ่งปริมาณ (ทั้งหมด) § จุดเชื่อม)
ในทฤษฎีประเภท และทฤษฎีทอพอโลยีพื้นฐาน ตัวบ่งปริมาณแบบบางตัว เป็นที่เข้าใจโดยทั่วไปว่าเป็นจุดเชื่อม (Adjoint) ด้านซ้ายของฟังก์เตอร์ (Functor) ระหว่างสองพาวเวอร์เซต ภาพผกผันฟังก์เตอร์ของฟังก์ชันระหว่างสองเซต ตัวบ่งปริมาณแบบทั้งหมดเป็นจุดเชื่อมด้านขวา
ดูเพิ่ม
อ้างอิง
- Saunders Mac Lane, Ieke Moerdijk, (1992) Sheaves in Geometry and Logic Springer-Verlag. ISBN See page 58
wikipedia, แบบไทย, วิกิพีเดีย, วิกิ หนังสือ, หนังสือ, ห้องสมุด, บทความ, อ่าน, ดาวน์โหลด, ฟรี, ดาวน์โหลดฟรี, mp3, วิดีโอ, mp4, 3gp, jpg, jpeg, gif, png, รูปภาพ, เพลง, เพลง, หนัง, หนังสือ, เกม, เกม, มือถือ, โทรศัพท์, Android, iOS, Apple, โทรศัพท์โมบิล, Samsung, iPhone, Xiomi, Xiaomi, Redmi, Honor, Oppo, Nokia, Sonya, MI, PC, พีซี, web, เว็บ, คอมพิวเตอร์
lingkkhamphasa inbthkhwamni miiwihphuxanaelaphurwmaekikhbthkhwamsuksaephimetimodysadwk enuxngcakwikiphiediyphasaithyyngimmibthkhwamdngklaw krann khwrribsrangepnbthkhwamodyerwthisud intrrksastrechingphisucn twbngprimansahrbtwmicring xngkvs Existential quantifier epntwbngpriman khathangtrrksastrthiethakbwa mi bangtw hrux fxrsm hmaykhwamwa fngkchnkhxngpraphcnnn samarthichidkbbangtwinodemn hruxkkhux fngkchnkhxngpraphcnnnmikhwamsmphnthkbsmachikaekhephiyngbangtwinodemnnn sungenguxnikhthiich ephiyngepncringkbsmachiktwidtwhnung khakhwamcringcaepncringidthnthi enuxngcakepntwbngprimanaebbbangtw ichsylksn wangiwkbtwaepr x hrux x twbngprimanaebbbangtwnntrngkhamkbtwbngprimanaebbthnghmd sahrb id sungcaichsmachikinodemnthuktw duhwkhxihythi rhskhxngsylksnnikhux U 2203 THERE EXISTS HTML amp 8707 amp exist aela U 2204 THERE DOES NOT EXIST HTML amp 8708 immi id ely sylksntwbngprimanaebbbangtwphunthanihenguxnikhepncanwnthrrmchatiid thikhundwytwmnexngaelwmiphllphthepn 25 0 0 25 displaystyle 0 cdot 0 25 hrux 1 1 25 displaystyle 1 cdot 1 25 hrux 3 3 25 displaystyle 3 cdot 3 25 hrux 4 4 25 displaystyle 4 cdot 4 25 l praoykhni epnaebbkareluxkechingtrrksastr ephraamikarich aela aebbsa aetxyangirkdi l imsamarthekhiynaebbtrrksastrmatrthanid cakpraoykhdngklawkhangtn xacniyamidxikthiwa n N n n 25 displaystyle exists n in mathbb N rightarrow n cdot n 25 praoykhkhangtn ichtwbngprimanaebbbangtwekhamachwy cakruppraoykhkhangtn camikhwamaemnyakwaxnthihnung inkhnathi l imidecaacngwarwmcanwnthrrmchatithnghmd aelaimidbxkxairephim ephraaimidkahndodemnxyangchdecn praoykhkxaccaimidepnkartikhwamxairmaknk hruxcaphudxikxyangkkhux canwnthrrmchatinnidkahndiwxyangchdecn praoykhkhangtnepncring ephraa 5 epncanwnthrrmchati aelaemuxaethn 5 dwy n aelw caidsmkarwa 5 5 25 displaystyle 5 cdot 5 25 sungepncring imsakhywa n n 25 displaystyle n cdot n 25 caepncringkbechphaacanwnthrrmchati 5 ethann ephraahakmiaekhsmachiktwediywthimathaihenguxnikhepncringid sahrbtwbngprimanbangtwaelw praoykhnncaepncringthnthi inthangtrngknkham hakepnpraoykh n even number n n 25 displaystyle exists n in mathrm even number rightarrow n cdot n 25 epnethc enuxngcakimmicanwnkhuidkhunkndwytwmnexngaelwidphllphthethakb 25 ichkahndwakhatwaepr n idbangthicanamaichkbenguxnikh aetyngmieruxngkhxngkhwamepncringaelaethckhxngaetlapraoykhnn inbangkhrngtwechuxmechingtrrksastrmaichkbexkphphsmphththephuxphisucn echn n positive odd number n n 25 displaystyle exists n in mathrm positive odd number rightarrow n cdot n 25 kb n N n odd number n n 25 displaystyle exists n in mathbb N n in mathrm odd number land n cdot n 25 caktwxyangkhangtn eracaetimkarechuxmechingtrrksastrmadwy sylksn tw E klbhwintrakulfxnt Sans Serif ichaethntwbngprimanaebbbangtw hruxbangthixacekhiynechphaatw V odd tha P a b c displaystyle mathrm P a b c aethn a b c displaystyle a cdot b c aela N displaystyle mathbb N khuxestkhxngcanwnthrrmchati aelw n NP n n 25 displaystyle exists n in mathbb N mathrm P n n 25 epnpraoykh sungepncring n N n n 25 displaystyle displaystyle exists n in mathbb N rightarrow n cdot n 25 inthanxngediywkn tha Q n displaystyle mathrm Q n aethn n odd number displaystyle n in mathrm odd number aelw n N Q n P n n 25 displaystyle exists n in mathbb N big Q n wedge P n n 25 big epnpraoykh sungepnethc n N n odd number n n 25 displaystyle displaystyle exists n in mathbb N n in mathrm odd number land n cdot n 25 inechingkhnitsastr karphisucntw bangtw xacthaidinrupaebbxun sungichaethnknid hruxcaphisucnodyimtxngaesdngelywayngingphllphthtxngepnxyangnnaennxnsmbtikarniesth fngkchnpraphcnthimitwbngprimanknbepnpraoykh dngnn fngkchnthimitwbngprimankminiesthid swnihysylksnaethnkarniesthich displaystyle neg twxyangechn tha P x epnfngkchnpraphcnwa 0 lt x lt 1 aelw ihexkphphsmphththepn x khuxcanwnthrrmchatiid twbngprimanaebbbangtw mi x bangtwsungmakkwa 0 aelanxykwa 1 caekhiynidinrup x XP x displaystyle exists x in mathbf X P x praoykhnixacaepnethcid ephraacring khwrichwa immicanwnthrrmchatiid thimakkwa 0 aelanxykwa 1 caekhiynidinrup x XP x displaystyle lnot exists x in mathbf X P x immismachikinexkphphsmphththid sungcathaihenguxnikhniepncringid dngnn smachikthuktwcakhdkbenguxnikh sungkkhuxniesth x XP x displaystyle exists x in mathbf X P x smmulkb sahrbcanwnthrrmchati x id sung x imidmakkwa 0 hruxnxykwa 1 x X P x displaystyle forall x in mathbf X lnot P x odypktiaelw niesthkhxngtwbngprimanaebbbangtwkhuxtwbngprimanaebbthnghmd hruxniyamidwa x XP x x X P x displaystyle lnot exists x in mathbf X P x equiv forall x in mathbf X lnot P x echn kahndihwa thukkhnyngimidaetngngan hrux immiikhrelythiaetngnganaelw khux imichthukkhnthiaetngnganaelw hrux mikhnthiyngimidaetngngan cahmaykhwamwa x XP x x X P x x XP x x X P x displaystyle lnot exists x in mathbf X P x equiv forall x in mathbf X lnot P x not equiv lnot forall x in mathbf X P x equiv exists x in mathbf X lnot P x niesthkhxngtwbngprimanbangtwyngrwmthung immiely x XP x x XP x displaystyle nexists x in mathbf X P x equiv lnot exists x in mathbf X P x sungimehmuxnkbtwbngprimanaebbthnghmd twbngprimanaebbbangtwcakracayhakepnkareluxkechingtrrksastrid x XP x Q x x XP x x XQ x displaystyle displaystyle exists x in mathbf X P x lor Q x to exists x in mathbf X P x lor exists x in mathbf X Q x kdxudmkhti kdxudmkhtiepnkdsungichphisucnkhntxncaksmmutithansukarsrupxxkma mikdxudmkhtixyuhlaykd sungnaipichkbtwbngprimanaebbbangtw prithsnkhxngtwbngprimanaebbbangtw I klawiwwathafngkchnkhxngpraphcnnnepnthithrabknthwipwaepncring dngnn catxngmismachikkhxngfngkchnkhxngpraphcnthiepncring hruxekhiynidinrup P a x XP x displaystyle P a to exists x in mathbf X P x kartdthingaebbtwbngprimanaebbbangtw E klawiwwa emuxdaeninkarhklangaebbfitch odykaretimniphcnthiidcakkarhklangyxyekhaip odykaretimtwbngprimanaebbbangtw thitidtwaepr ekhaipchwy sungtwbngprimanniimekiywkhxngkbkardaeninkarid khxngniphcnthinamaetim thaphlidphayinkardaeninkarkhxngtwniphcncakkarhklangyxysungimmitwbngprimanaebbbbangtwnn dngnncamismachikhnungtwsungsamarthhklangtwidtwhnungkhxngniphcnthiidcakkarhklangyxynn odyehtuphlkhxngkartdthingaebbtwbngprimanaebbangtwkhux thakahndwamismachiktwidtwhnungthithaihfngkchnkhxngpraphcnnn epncring thaphlichaethnkbkarkahndchuxecaacng Arbitary Name id phlnncaepncringxyangaennxn trabidthimnyngimmichux ekhiynid ody ihchuxecaacngepn c aelw Q epnpraphcnsungimmi c x XP x P c Q Q displaystyle exists x in mathbf X P x to P c to Q to Q kha c catxngepncringthuktwbnodemnediywknkb X hruxhakpraphcnimepniptamtrrka caidwa hak c imichchuxecaacng aelwepnephiyngsmachikechphaa Specific Element inexkphphsmphthth aelw P c caimsamarthihehtuphlaekpraoykhnn idxik estwang rupaebb x P x displaystyle exists x in emptyset P x caepnethcesmx hakimkhunkb P x enuxngcakestwangcaimmikhaxairkb x ih x odd aesdngkbenguxnikh P x mi x id inestwang duephimthicudechuxmhwkhxhlk twbngpriman thnghmd cudechuxm inthvsdipraephth aelathvsdithxphxolyiphunthan twbngprimanaebbbangtw epnthiekhaicodythwipwaepncudechuxm Adjoint dansaykhxngfngketxr Functor rahwangsxngphawewxrest phaphphkphnfngketxrkhxngfngkchnrahwangsxngest twbngprimanaebbthnghmdepncudechuxmdankhwaduephimraykarsylksnthiichkbtrrksastr twbngpriman thnghmd twbngpriman hnungtw xangxingSaunders Mac Lane Ieke Moerdijk 1992 Sheaves in Geometry and Logic Springer Verlag ISBN 0 387 97710 4 See page 58