Reports on Mathematical Logic

No. 36

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.

Back to Main Menu