Note on the Strong Normalizability of the Logic with Self-Referential Predicates

IR Web Site

Bibliographic Information

Other Title
  • Note on the Strong Normalizability of t

Search this article

Description

type:text

We consider a logical system in which the second order terms can be also used as first order terms. As a consequence, predicates can be taken as arguments of another predicate. In other words, a predicate can refer to predicates. The proposed framework seems very different from the tradition of formal logic which has been developped since Aristotle, where the distinction between the predicates and the individuals are essential. While in the traditional (Aristotelean) logical language a typical and basic sentence is of the form, e.g., Love(Socrates, Phaidon) "Socrates loves Phaidon", in our proposed language we could also express e.g., Love(Socrates, Love), Socrates "loves (the idea of) love", (which can be also express as Love(Socrates, λx, y. Love(x, y) by the usual η-conversion), or a sentence Love(God, λx ∀y Love(x, y)), "God loves (the idea of) loving everyone", or a predicate on x such as Love(x, λy Love(x, y)), "x loves x's own love". The purpose of this note is to give some proof-theoretic properties of the proposed logic; in particular, the strong normalizability is shown by slightly modifying Girard's strong normalizability proof for the traditional higher order logic. The use of this proposed logical language for the analysis of "self-references" and "intensionality" as Well as a connection with natural language semantics is discussed in Okada", and the connection with mobile communication processes and with linear logic are discussed in Okada.

1. INTRODUCTION 2. LANGUAGE FOR SELF-REFERENTIAL PREDICATES 3. UNTYPED SELF-REFERENTIAL LANGUAGE AND RUSSELL'S PARADOX 4. STRONG NORMALIZABILITY 5. REFERENCES

Journal

  • 哲學

    哲學 95 1-14, 1993-07

    三田哲學會

Details 詳細情報について

Report a problem

Back to top