Grzegorz SOZA:
Asymptotic Density as a Method of Expressing Quantitative Relations in Intuitionistic Logic
A b s t r a c t. Our efforts in this work are mainly directed towards the statistical
properties of tautologies and non-tautologies in intuitionistic logic (which
is equivalent to research in typed lambda calculus because of the Curry-Howard
isomorphism, see [1]). This article is a part of my master's
thesis, which I defended at the Computer Science Department of Jagiellonian
University in 2000. The inspiration for the thesis were the scientific works of the
supervisor of my thesis dr hab. Marek Zaionc. In his [2] and
[3] he dealt with typed lambda calculus considered over a finite
number of ground types. His aim was to study the properties of types according
to their length, defined as the number of occurrences of ground type variables
in a type.
The goal here is quite similar, though we start from a different definition
of the length of a type. In this work the complexity measure function
(the ''length'' of a type) is defined as the height of its
constructing tree. As we show the statistical behaviour of the type
depends vitaly on the definition of its length. In Section 2 we prove
that the asymptotic probability (defined precisely there) that a random one-variable
formula is valid in intuitionistic logic (with implication only) is
exactly 1, while by the linear definition of the length of a type (as
discussed in [2] and [3]) this probability is
equal to ${{1}\over{2}}+{{\sqrt{5}}\over{10}}$.
In Section 3 we shall be concerned with formulas their corresponding
types consist of more than one ground type. We define a subset of
tautologies (called simple tautologies). Then we show that for each
number k of ground type variables, and for each number $ n>1$, the
ratio of types corresponding to this class of length n to all types
of the same length n expressed as a fraction is always positive and
at the same time bounded by ${1}\over{k}$. We show also that the
similarly defined ratio of all types representing tautologies to all
types expressed as a fraction is greater than ${1}\over{k} $, which
implies that we have noticeably more (in terms of asymptotic density
which is defined in Section 1) tautologies than simple tautologies.
However, it does not give us precise information about all tautologies
(as was the case in Section 2). Later on in Section 3 we shall be
occupied with a subset of non-tautologies whose asymptotic density is
positive by the linear definition of the length of a type, and moreover, this
density tends to 1 as k tends to infinity. We show that by our double
exponential definition of the length of a type this density equals 0.
In the last chapter we state some conjectures, which seem to hold but are not
contained in this work.