Admissibility of Fixed-Point Induction in First-Order Logic of Typed Theories

Abstract

First-order logic is extended so as to deal with typed theories, especially that of continuous functions with fixed-point induction formalized by D. Scott. The translation of his formal system, or the gamma calculus-oriented system derived and implemented by R. Milner, into this logic amounts to adding predicate calculus features to them. In such a logic the fixed-point induction axioms are no longer valid, in general, so that one may characterize formulas for which Scott-type induction is applicable, in terms of syntax which can be checked by machines automatically.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
May 01, 1972
Accession Number
AD0746146

Entities

People

  • Shigeru Igarashi

Organizations

  • Stanford University

Tags

DTIC Thesaurus Topics

  • Aeronautics
  • Applied Mathematics
  • Artificial Intelligence
  • Calculus
  • Compilers
  • Computational Science
  • Computer Programming
  • Computer Science
  • Computers
  • Language
  • Logic
  • Mathematical Logic
  • Mathematics
  • Sequences
  • Theorems
  • Translations
  • Universities

Readers

  • Approximation Theory.
  • Computational Linguistics