ในตรรกศาสตร์ทางคณิตศาสตร์ คุณสมบัติ การเชื่อมโยงแบบ "หรือ" และคุณสมบัติการมีอยู่ ถือเป็น "จุดเด่น" ของ ทฤษฎี เชิงสร้างสรรค์เช่นเลขคณิตของเฮย์ติงและทฤษฎีเซตเชิงสร้างสรรค์ (Rathjen 2005)

• คุณสมบัติการเชื่อมโยงแบบ "หรือ"จะเป็นจริงสำหรับทฤษฎีบทก็ต่อเมื่อ เมื่อใดก็ตามที่ประโยคA ∨ B เป็นทฤษฎีบทแล้วAก็เป็นทฤษฎีบท หรือBก็เป็นทฤษฎีบทเช่นกัน
• คุณสมบัติการมีอยู่หรือคุณสมบัติพยานจะเป็นไปตามทฤษฎีก็ต่อเมื่อ เมื่อใดก็ตามที่ประโยค(∃ x ) A ( x )เป็นทฤษฎีบท โดยที่A ( ​​x ) ไม่มีตัวแปรอิสระอื่นใดแล้ว จะมีเทอมt บางเทอม ที่ทำให้ทฤษฎีบทพิสูจน์A ( t )ได้

Rathjen (2005) ระบุคุณสมบัติห้าประการที่ทฤษฎีอาจมี ซึ่งได้แก่ คุณสมบัติการแยก ( DP ) คุณสมบัติการมีอยู่ ( EP ) และคุณสมบัติเพิ่มเติมอีกสามประการ:

• คุณสมบัติการมีอยู่เชิงตัวเลข ( NEP )ระบุว่า ถ้าทฤษฎีพิสูจน์ได้ว่าโดยที่φไม่มีตัวแปรอิสระอื่นใด ทฤษฎีก็จะพิสูจน์ได้ว่า สำหรับบางค่าโดยที่เป็นพจน์ที่ใช้แทนจำนวนn${\displaystyle (\exists x\in \mathbb {N} )\varphi (x)}$${\displaystyle \varphi ({\bar {n}})}$${\displaystyle n\in \mathbb {N} {\text{.}}}$${\displaystyle {\bar {n}}}$${\displaystyle T}$
• กฎของเชิร์ช ( CR ) ระบุว่า ถ้าทฤษฎีพิสูจน์ได้ว่า มีจำนวนธรรมชาติ eอยู่จริง โดยที่ เมื่อให้เป็นฟังก์ชันที่คำนวณได้ซึ่งมีดัชนี eทฤษฎีจะพิสูจน์ได้ว่า${\displaystyle (\forall x\in \mathbb {N} )(\exists y\in \mathbb {N} )\varphi (x,y)}$${\displaystyle f_{e}}$${\displaystyle (\forall x)\varphi (x,f_{e}(x))}$
• รูปแบบหนึ่งของกฎของ Church, CR ระบุว่า ถ้าทฤษฎีพิสูจน์ได้ว่า ก็จะมีจำนวนธรรมชาติeที่ทำให้ทฤษฎีพิสูจน์ได้ว่าสมบูรณ์และพิสูจน์ได้ว่า${\displaystyle (\exists f\colon \mathbb {N} \to \mathbb {N} )\psi (f)}$${\displaystyle f_{e}}$${\displaystyle \psi (f_{e})}$

คุณสมบัติเหล่านี้สามารถแสดงออกมาได้โดยตรงเฉพาะทฤษฎีที่มีความสามารถในการหาปริมาณของจำนวนธรรมชาติ และสำหรับ CR นั้น ต้องสามารถหาปริมาณของฟังก์ชันจากไปยังได้ ในทางปฏิบัติ อาจกล่าวได้ว่าทฤษฎีหนึ่งมีคุณสมบัติเหล่านี้ข้อใดข้อหนึ่ง หากส่วนขยายเชิงนิยามของทฤษฎีนั้นมีคุณสมบัติที่กล่าวไว้ข้างต้น (Rathjen 2005) ${\displaystyle \mathbb {N} }$${\displaystyle \mathbb {N} }$

โดยทั่วไปแล้ว ทฤษฎีที่ยอมรับ หลักการ ยกเว้นตรงกลางในขณะที่มีข้อความที่เป็นอิสระ จะไม่มีคุณสมบัติการเชื่อมโยงแบบ "หรือ" ดังนั้น ทฤษฎีคลาสสิกทั้งหมดที่แสดงถึงเลขคณิตของโรบินสัน จึง ไม่มีคุณสมบัตินี้ ทฤษฎีคลาสสิกส่วนใหญ่ เช่นเลขคณิตของพีอาโนและZFCเองก็ไม่รับรองคุณสมบัติการมีอยู่เช่นกัน เช่น เพราะทฤษฎีเหล่านั้นรับรอง การมีอยู่ของ หลักการจำนวนน้อยที่สุดแต่ทฤษฎีคลาสสิกบางทฤษฎี เช่น ZFC บวกกับสัจพจน์ของการสร้างได้ก็มีคุณสมบัติการมีอยู่ในรูปแบบที่อ่อนกว่า (Rathjen 2005)

เลขคณิตของเฮย์ติงเป็นที่รู้จักกันดีในเรื่องคุณสมบัติการเชื่อมโยงแบบ "หรือ" และคุณสมบัติการมีอยู่ (เชิงตัวเลข)

แม้ว่าผลลัพธ์แรกสุดจะเป็นทฤษฎีเชิงสร้างสรรค์ของเลขคณิต แต่ก็มีผลลัพธ์มากมายที่เป็นที่รู้จักสำหรับทฤษฎีเซตเชิงสร้างสรรค์เช่นกัน (Rathjen 2005) John Myhill  (1973) แสดงให้เห็นว่าIZFที่ ตัด สัจพจน์ของการรวบรวมออกไปและใช้สัจพจน์ของการแทนที่แทน มีคุณสมบัติการแยกส่วน คุณสมบัติการมีอยู่เชิงตัวเลข และคุณสมบัติการมีอยู่ Michael Rathjen (2005) พิสูจน์ว่าCZFมีคุณสมบัติการแยกส่วนและคุณสมบัติการมีอยู่เชิงตัวเลข

Freydและ Scedrov (1990) สังเกตว่าคุณสมบัติการแยกส่วน (disjunction property) เป็นจริงในพีชคณิต Heyting อิสระ และโทโพ อิอิสระ ในแง่ของ หมวดหมู่ ในโทโพอิอิสระนั้น สอดคล้องกับข้อเท็จจริงที่ว่าวัตถุปลายทางไม่ใช่การรวมกันของวัตถุย่อยที่เหมาะสมสองวัตถุ เมื่อรวมกับคุณสมบัติการมีอยู่ มันจะแปลเป็นการยืนยันว่าเป็นวัตถุเชิงโปรเจก ทีฟที่ไม่สามารถแยกส่วนได้ — ฟังก์ชันที่มันแสดง (ฟังก์ชันส่วนทั่วโลก) รักษาเอพิโมร์ ฟิซึม และโคโปรดักต์ไว้ ${\displaystyle \mathbf {1} }$${\displaystyle \mathbf {1} }$

มีความสัมพันธ์หลายประการระหว่างคุณสมบัติทั้งห้าที่กล่าวถึงข้างต้น

ในบริบทของเลขคณิต คุณสมบัติการมีอยู่ของตัวเลขบ่งบอกถึงคุณสมบัติการเชื่อมโยงแบบ "หรือ" การพิสูจน์ใช้ข้อเท็จจริงที่ว่าการเชื่อมโยงแบบ "หรือ" สามารถเขียนใหม่ได้เป็นสูตรการมีอยู่ซึ่งระบุปริมาณของจำนวนธรรมชาติ:

${\displaystyle A\vee B\equiv (\exists n)[(n=0\to A)\wedge (n\neq 0\to B)]}$.

ดังนั้น ถ้า

${\displaystyle A\vee B}$เป็นทฤษฎีบทของดังนั้น ก็เป็นเช่นกัน${\displaystyle T}$${\displaystyle \exists n\colon (n=0\to A)\wedge (n\neq 0\to B)}$

ดังนั้น เมื่อพิจารณาคุณสมบัติการมีอยู่เชิงตัวเลขแล้ว จะมีอยู่บางค่าที่ทำให้ ${\displaystyle s}$

${\displaystyle ({\bar {s}}=0\to A)\wedge ({\bar {s}}\neq 0\to B)}$

เป็นทฤษฎีบท เนื่องจากเป็นจำนวน เราจึงสามารถตรวจสอบค่าของ ได้อย่างเป็นรูปธรรม กล่าวคือ ถ้าแล้วเป็นทฤษฎีบท และถ้าแล้วเป็นทฤษฎีบท ${\displaystyle {\bar {s}}}$${\displaystyle s}$${\displaystyle s=0}$${\displaystyle A}$${\displaystyle s\neq 0}$${\displaystyle B}$

Harvey Friedman (1974) พิสูจน์ว่าใน ส่วนขยาย ที่นับได้แบบเวียนซ้ำของเลขคณิตเชิงสัญชาตญาณ ใดๆ คุณสมบัติการแยกส่วนบ่งชี้ถึงคุณสมบัติการมีอยู่เชิงตัวเลข การพิสูจน์ใช้ประโยคอ้างอิงตนเองในลักษณะที่คล้ายกับการพิสูจน์ทฤษฎีบทความไม่สมบูรณ์ของ Gödelขั้นตอนสำคัญคือการหาขอบเขตของตัวบ่งปริมาณการมีอยู่จริงในสูตร (∃ x )A( x ) ซึ่งทำให้ได้สูตรการมีอยู่จริงที่มีขอบเขต (∃ x < n )A( x ) จากนั้นสูตรที่มีขอบเขตนี้สามารถเขียนเป็นการแยกส่วนจำกัด A(1)∨A(2)∨...∨A(n) ได้ สุดท้ายการกำจัดการแยกส่วนสามารถใช้เพื่อแสดงว่าหนึ่งในส่วนแยกส่วนนั้นสามารถพิสูจน์ได้

เคิร์ท เกอเดล  (1932) กล่าวโดยไม่มีการพิสูจน์ว่าตรรกศาสตร์เชิงประพจน์แบบสัญชาตญาณ (โดยไม่มีสัจพจน์เพิ่มเติม) มีคุณสมบัติการเชื่อมโยงแบบ "หรือ" ผลลัพธ์นี้ได้รับการพิสูจน์และขยายไปสู่ตรรกศาสตร์เชิงภาคแสดงแบบสัญชาตญาณโดยเกอร์ฮาร์ด เกนท์เซน  (1934, 1935) สตีเฟน โคล คลีน  (1945) พิสูจน์ว่าเลขคณิตของเฮย์ติงมีคุณสมบัติการเชื่อมโยงแบบ "หรือ" และคุณสมบัติการมีอยู่ วิธีการของคลีนได้นำเสนอเทคนิคการทำให้เป็นจริงซึ่งปัจจุบันเป็นหนึ่งในวิธีการหลักในการศึกษาทฤษฎีเชิงสร้างสรรค์ (โคห์เลนบัค 2008; โทรเอลสตรา 1973)

• ทฤษฎีเซตเชิงสร้างสรรค์
• เลขคณิตเฮย์ติง
• กฎของตัวกลางที่ไม่รวม
• ความเป็นไปได้
• ตัวบ่งปริมาณเชิงการดำรงอยู่

• Moschovakis, Joan (16 ธันวาคม 2022). "ตรรกศาสตร์เชิงสัญชาตญาณ"ในZalta, Edward N. (บรรณาธิการ). สารานุกรมปรัชญาแห่งสแตนฟอร์ด (ฉบับฤดูหนาว 2022). ISSN  1095-5054 . OCLC  429049174 .