Chulalongkorn University Theses and Dissertations (Chula ETD)

An [omega]-order predicate logic with types

Other Title (Parallel Title in Other Language of ETD)

ตรรกศาสตร์พรีดีเคตอันดับโอเมกาที่มีไทป์

Year (A.D.)

1997

Document Type

Thesis

First Advisor

Suwimon Hall

Second Advisor

Hall, Mark Edwin

Faculty/College

Graduate School (บัณฑิตวิทยาลัย)

Degree Name

Master of Science

Degree Level

Master's Degree

Degree Discipline

Mathematics

DOI

10.58837/CHULA.THE.1997.1255

Abstract

A type is a symbol used to separate objects in the universe into different groups. The objects in traditional predicate logic have no types (or, equivalently, they all have the same type), so in some theories which need at least two classes of object, such as the theory of vector spaces or homomorphisms of two groups, we can not write some theorems using untypes predicate logic. This thesis proposes a predicate logic with types. In it we will formulate syntax, sematics, and formal proofs, and prove some metatheorems, including the soundness theorem. Finally, we will give counterexamples to show that the compactness and completeness theorems fail in this logic.

Other Abstract (Other language abstract of ETD)

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

Link to Full Text

Share

COinS