formalWARE
project
Participating
Organizations
Research
Topics
People
formalWARE
results
Overview
Publications
Presentations
Tools
Methods
Examples
Training
formalWARE
information
Events
Index
Links
Contacts |
Abstract
By the theory TT is meant the higher order
predicate logic with the following recursively defined types:
1. 1 is the type of the individuals
2. [t1, ... , tn] is the type
of the predicates with
arguments of
the types t1, ... , tn, where n >=0.
The type [] when
n=0 is the type of truth values.
TT is a version of the simple theory
of types. The theory ITT described in this paper is an impredicative
version of TT. The types of ITT are the same as the types of TT,
but the membership of the type 1 of individuals in ITT is an extension
of the membership of the same type in TT. The extension consists
of allowing any higher order term, in which only variables of type 1 have
a free occurrence, to be a term of type 1. This impredicative feature
of ITT is motivated by a nominalist view of universals.
A nominalist understands a predicate
of a universal to be a predicate of a name of the universal.
For example, a nominalist interprets "Yellow is a colour" as "Yellow is
a colour-word"; the sentence is understood as a description of the use
of the word 'Yellow' in English. Since computers are consumate nominalists,
nominalist interpretations of computer languages should be considered.
But this does require a careful distinction between the use and mention
of predicate names, especially when treating abstraction and quantification.
For example, in "Yellow is a colour-word" the predicate name 'Yellow' is
being mentioned while the predicate name 'colour-word' is being used.
The types of TT prevent impredicative
definitions; as a consequence the logic must be supplemented with non-logical
axioms. The impredicative types of ITT, on the other hand, permit
both wellfounded and non-wellfounded recursive predicates to be defined
as abstraction terms from which all the properties of the predicates can
be derived without the use of axioms. The
technique is demonstrated using higher
order Horn sequent definitions. "Computations" by iteration are also
defined for these predicates.
The consistency proof for TT can
be adapted for ITT, as can also Prawitz's semantic proof of completeness
and cut-elimination.
=============
The talk has been prepared for presentation
at the 14'th Workshop on the Mathematical Foundations for Programming Systems
in London, England, May 10-13.
The workshop is attended by mathematicians
and computer scientists interested in theoretical studies of computer systems.
Download Postscript
Download PDF
|
