First-Order Quotational Logic

In this dissertation, we construct a consistent, complete quotational logic G$\sb1$. We first develop a semantics, and then show the undecidability of circular quotation and anaphorism . Next, a complete axiom system is presented, and completeness theorems are shown for G$\sb1$. We show that definable truth exists in G$\sb1$. ;Later, we replace equality in G$\sb1$ with an equivalence relation. An axiom system and completeness theorems are provided for this equality-free version of G$\sb1$, which is useful in program verification. ;Interpolation and definability are discussed in intensional and extensional contexts. We show that G$\sb1$ contains the complete first order theory of arithmetic by implicit definitional extension. ;The last chapter deals with representability and fixed points. Derived induction schemata are produced, and G$\sb1$ is shown to be a recursion theory. We give an example of how G$\sb1$ may be used to solve domain equations of Scott