Hoare logic for the set of while-pr

Hoare logic for the set of while-programs with the first-order logical language L and
the first-order theory T ⊂ L is denoted by HL(T ). Bergstra and Tucker have pointed out
that the complete number theory Th(N) is the only extension T of Peano arithmetic PA
for which HL(T ) is logically complete. The completeness result is not satisfying, since it
allows inputs to range over nonstandard models. The aim of this paper is to investigate
under what circumstances HL(T ) is logically complete when inputs range over the standard
model N. PA+ is defined by adding to PA all the unprovable 1-sentences that describe the
nonterminating computations. It is shown that each computable function in N is uniformly
1-definable in all models of PA+, and that PA+ is arithmetical. Finally, it is established,
based on the reduction from HL(T ) to T , that PA+ is the minimal extension T of PA for
which HL(T ) is logically complete when inputs range over N. This completeness result has
an advantage over Bergstra’s and Tucker’s one, in that PA+ is arithmetical while Th(N) is
not.

ผลลัพธ์ (ไทย) 1:

Hoare ตรรกะสำหรับชุดของโปรแกรมในขณะแรกสั่งตรรกะภาษา L และทฤษฎีแรกสั่ง T ⊂ L สามารถระบุโดย HL (T) ทักเกอร์และ Bergstra ได้ชี้ให้เห็นว่าทฤษฎีจำนวนสมบูรณ์ Th(N) T Peano คณิตศาสตร์ PA ส่วนขยายเท่านั้นHL (T) ทางตรรกะไม่เสร็จที่ ผลสมบูรณ์ความพึงพอใจ ไม่นับตั้งแต่อินพุตช่วงเหนือรุ่นเกือบได้ จุดประสงค์ของเอกสารนี้คือการ ตรวจสอบภายใต้สถานการณ์ใด HL (T) เป็นตรรกะสมบูรณ์เมื่อ อินพุตช่วงผ่านมาตรฐานรุ่น PA ตอนเหนือ + กำหนด โดยเพิ่มป่าทั้งหมด unprovable 1-ประโยคที่อธิบายการหนึ่ง nonterminating มันแสดงให้เห็นว่า แต่ละฟังก์ชัน computable ใน N ไม่สม่ำเสมอเมื่อเทียบเคียง1 เองในทุกรุ่นของ PA + และ PA + arithmetical ในที่สุด มันถูกก่อตั้งขึ้นขึ้นอยู่กับการลดจาก HL (T) ให้ T, PA ที่ + คือ นามสกุลน้อย T ของป่าสำหรับซึ่ง HL (T) เป็นตรรกะสมบูรณ์เมื่ออินพุตช่วงกว่า N. มีผลสมบูรณ์นี้ข้อดีกว่าของ Bergstra และของทักเกอร์หนึ่ง PA ที่ + คือ arithmetical ขณะ Th(N)ไม่

ผลลัพธ์ (ไทย) 2:

ตรรกะโฮร์สำหรับชุดของโปรแกรมในขณะที่กับครั้งแรกที่สั่งซื้อ L
ภาษาตรรกะและทฤษฎีลำดับแรกT ⊂ L จะเขียนแทนด้วย HL (T) Bergstra
ทักเกอร์และได้ชี้ให้เห็นว่าทฤษฎีจำนวนสมบูรณ์Th (N) เป็นเพียงส่วนขยายของทีอาโน่คณิตศาสตร์ PA
ที่ HL (T) เสร็จสมบูรณ์เหตุผล
ผลสมบูรณ์ไม่ได้เป็นที่น่าพอใจเพราะมันช่วยให้ปัจจัยการผลิตในช่วงกว่ารุ่นที่ไม่เป็นมาตรฐาน จุดมุ่งหมายของการวิจัยนี้คือการตรวจสอบภายใต้สถานการณ์ HL (T) เป็นเหตุผลเสร็จสมบูรณ์เมื่อช่วงปัจจัยการผลิตที่ผ่านมาตรฐานรุ่นเอ็นPA + จะถูกกำหนดโดยการเพิ่ม PA ทั้งหมดพิสูจน์ 1 ประโยคที่อธิบายคำนวณnonterminating มันแสดงให้เห็นว่าแต่ละฟังก์ชั่นในการคำนวณ N คือสม่ำเสมอ1 กำหนดในทุกรุ่นของ PA + และ PA + เป็นคณิตศาสตร์ ในที่สุดก็จะจัดตั้งขึ้นบนพื้นฐานของการลดลงจาก HL (T) เพื่อ T ที่ PA + เป็นส่วนขยายที่น้อยที่สุด T ของป่าสำหรับที่ HL (T) จะเสร็จสมบูรณ์มีเหตุผลเมื่อช่วงปัจจัยการผลิตมากกว่า N. ผลสมบูรณ์นี้มีประโยชน์มากกว่าBergstra ของ และเป็นหนึ่งของทักเกอร์ใน PA + ที่เป็นคณิตศาสตร์ในขณะ Th (N) เป็นไม่ได้