Skip to main content



Heyting Session


On the Early History of Intuitionistic Logic

We describe the early history of intuitonistic logic, its formalization and the genesis of the so-called Brouwer-Heyting-Kolmogorov interpretation. In particular we discuss at some length whether Heyting’s papers contain an anticipation of logic with existence predicate. Finally we publish some source material, in particular letters of Bemays, Glivenko and Kolmogorov to Heyting.
A. S. Troelstra

Heyting and Intuitionistic Geometry

It may seem strange that the second fully committed intuitionist in mathematics entered his career with a treatise on axiomatic geometry, for axiomatics did have a formalist flavour and one cannot suspect Brouwer, Heyting’s teacher, of leanings in that specific direction. There are a number of possible explanations for the choice of this particular topic — which, by the way, had been suggested by Brouwer. One of them is Brouwer’s own interest in the foundations of geometry in the Pasch-Hilbert-style; his Ph.D.Thesis contained a good deal of geometry and he regularly lectured on the foundations of geometry. His inaugural address as a “privaat docent” bore the title “The nature of geometry”. Hence it is not all that surprising that Heyting choose the intuitionistic foundations as a topic for his Ph.D.thesis.
D. van Dalen

Summer School


Provability Logics for Relative Interpretability

In this paper the system IL for relative interpretability described in Visser (1988) is studied.1 In IL formulae A ⊳ B (read: A interprets B) are added to the provability logic L. The intended interpretation of a formula A ⊳ B in an (arithmetical) theory T is: T + B is relatively interpretable in T + A. The system has been shown to be sound with respect to such arithmetical interpretations (Švejdar 1983, Montagna 1984, Visser 1986, 1988P).
Dick de Jongh, Frank Veltman

Constructive Mathematics and Computer-Assisted Reasoning Systems

The relationship between constructive mathematics and computer science has been noticed for a long while. But it is rather recent that live interactions between constructive mathematics and computer science began. In theoretical aspects, metamathematics of constructive mathematics are utilized to give semantics of higher order functional programming languages. Researches of constructive mathematics in computer science are not just theoretical. Quite a few systems based on constructive mathematics have been designed and implemented. They are program verification systems, program extraction systems, and high-level programming languages. These developments of systems need theoretical investigations as well and so give new insights into constructive mathematics. Applications of constructive mathematics to semantics of programming languages have begun to produce significant feedbacks to constructive mathematics and related areas, see Hyland (1987), Longo and Moggi (1988+α). Although researches on constructive systems have not yet been used to unvail new aspects of constructive mathematics, there are clues of possible applications of computer systems to theoretical researches in constructive mathematics Coquand (1986), Howe (1987). It is reasonable to imagine that constructive mathematicians a decade later will be helped by computer systems as mathematicians are now helped by computer algebra systems like REDUCE. In this paper, we will give a survey of existing systems based on constructive mathematics to show the readers how constructive theories are used in actual systems.
Susumu Hayashi

Markov’s Constructive Mathematical Analysis: The Expectations and the Results

Without Abstract
Boris Kushner

Normalization Theorems for the Intuitionistic Systems with Choice Principles

We review here some intuitionistic systems with choice principles
$$\forall x\left( {Ey} \right)A\left( {x,y} \right) \to \left( {Ef} \right)\forall xA\left( {x,f\left( x \right)} \right)$$
for which normalization theorems have been established. These are mainly first order systems or systems close to the first order ones in their deductive power. This is not accidental, since in higher order intuitionistic logic with extensionality choice seems to imply excluded third [1].
Grigorii Mints

Formalizing the Notion of Total Information

Suppose that Λ is a model for untyped λ-calculus and that T is some typed λ-calculus (transfinite, second order or whatever). One standard procedure for obtaining a model for T is to regard all terms in T as untyped terms, interpret each type as a subset of Λ and then prove that each typed term is interpreted into the interpretation of the type.
Dag Normann

Structural Rules and a Logical Hierarchy

Gentzen-type sequent calculi usually contain three structural rules, i.e., exchange, contraction and weakening rules. In recent years, however, there have been various studies on logics that have not included some or any of these structural rules. The motives or purposes of these studies have been so diverse that sometimes close connections between them have been overlooked. Here we will make a brief survey of recent results on these logics in an attempt to make these interrelationships clearer.
Hiroakira Ono

Semantics of Non-Classical First Order Predicate Logics

To describe semantics of a logical system one should define notions of a model and the truth in a model. A major part of classical first order model theory can be developed within the standard semantics, while alternative types of semantics (such as sheaves, forcing, polyadic algebras) play an auxiliary role.
Valentin Shehtman, Dmitrij Skvortsov

On the Computational Power of the Logic Programs

The aim of the present paper is a comparative study of the computational power of the logic programs and search computability [1].
Ivan N. Soskov

Some Relations among Systems for Bounded Arithmetic

In [1], S. Buss introduced systems S 2 i (i = 0, 1, 2,…), Ů 2 1 , and \(\begin{array}{*{20}{c}} ^\circ \\ v \\ \end{array} _{2}^{1}\) for Bounded Arithmetic which are closely related to Δ i p (if i > 0) in the polynomial hierarchy, PSPACE, and EXPTIME respectively. In Bounded Arithmetic weaker systems and stronger systems are interacted each other. As we think in physics that the basic principles are the principles on elementary particles, we believe that the intrinsic nature of Bounded Arithmetic is hidden in very weak systems of Bounded Arithmetic. Therefore it seems to us very useful to define sharply bounded arithmetic and to study it. Unfortunately S 2 0 is too weak to be a good candidate for sharply bounded arithmetic since it is proved in [7] that S 2 0 does not prove ∃x(a = 0 V x + 1 = a). On the other hand, \(\tilde S_2^0\) introduced in [8] seems to us a good candidate for sharply bounded arithmetic. We shall prove that \(\tilde S_2^0 = \tilde S_2^1\) implies EXPTIME = PSPACE, where \(\tilde S_2^1\) is a conservative extension of S 2 1 , and that if \(\begin{array}{*{20}{c}} ^\circ \\ v \\ \end{array} _{2}^{1}\) proves
$$\forall {}^ \ulcorner {\varphi ^ \urcorner }\exists \operatorname{w} (\operatorname{PA} - \Pr \operatorname{f} (\operatorname{w} ,{}^ \ulcorner {\varphi ^ \urcorner })\operatorname{V} \;\operatorname{PA} - \Pr \operatorname{f} (\operatorname{w} ,{}^ \ulcorner \urcorner {\varphi ^ \urcorner }))$$
then PSPACE = NP ⋂ co-NP, where ϕ is a Gödel number of a sharply bounded sentence and PA — Prf(w, ϕ ) is a formalized statement “w is a proof of ϕ in Peano Arithmetic”.
Gaisi Takeuti

A Survey of Intuitionistic Descriptive Set Theory

In descriptive set theory (cf. Moschovakis 1980), a subject which was founded in the early decades of this century by French and Russian mathematicians like Baire, Borel, Lebesgue, Lusin and Suslin, one describes and studies classes of subsets of the set IR of real numbers. Examples of such classes are: the class of open subsets of IR, the class of closed subsets of IR, the class of those subsets of IR which are the union of a countable sequence of closed subsets of IR, and its dual: the class of those subsets of IR which are the intersection of a countable sequence of open subsets of IR,…, the class of Borel subsets of IR, i.e.: the least class of subsets of IR which contains the closed subsets of IR and the open subsets of IR and is closed under the operations of countable union and countable intersection, the class of analytical subsets of IR, i.e.: the class of those subsets of IR that result from projecting a closed subset of IR2 on one of the coordinate-axes, the class of co-analytical subsets of IR, i.e.: the class of those subsets of IR whose complement is analytical,…, the class of projective subsets of IR, i.e.: the class of those subsets of IR which result from a closed subset of some IR n by a finite number of applications of the operations of projection and complementation.
Wim Veldman

Interpretability Logic

Interpretations are much used in metamathematics. The first application that comes to mind is their use in reductive Hilbert-style programs Think of the kind of program proposed by Simpson, Feferman or Nelson (see Simpson[1988], Feferman[1988], Nelson[1986]). Here they serve to compare the strength of theories, or better to prove conservation results within a properly weak theory. An advantage of using interpretations is that even if their use should — perhaps- be classified as a proof-theoretical method, it is often possible to employ a model-theoretical heuristics. An example is given in section 7.2 where a conservation result due to Paris & Wilkie, which is proven by a model-theoretical argument, is formalized in a weak theory. For more discussion of and perspective on the use of interpretability in reductive programs the reader is referred to Feferman[1988].
Albert Visser

Hierarchies of Provably Computable Functions

A computable number theoretic function is (total) recursive if some algorithm for it terminates on all inputs. From the algorithm we can unravel a tree of subcomputations such that termination is equivalent to well-foundedness with respect to the ‘computation-branches’. If the tree is well-founded we can prove termination by induction over it. Linearisation of the tree’s ordering then leads to a countable well-ordering whose size and structure reflects the complexity of the function, in terms of the inductive proof needed to verify its termination. We then say that the function is provably recursive -by induction over the given well-ordering. For example, the Ackermann Function is provably recursive, by induction over the lexicographical well-ordering of pairs of numbers; so the order-type of this well-ordering viz. the ordinal ω 2, in some sense measures its complexity. We further say that a function is provably recursive in a given formal theory (containing basic arithmetic) if the ∀∃-sentence asserting its totality is a theorem of that theory, or alternatively if it is provably recursive by induction over a provable well-ordering of the theory.
S. S. Wainer



Sequent Calculus for Intuitionistic Linear Propositional Logic

Classical linear logic and its phase semantics have been introduced in [GIRARD,1987], with the proof that the sequent calculus for classical linear propositional logic is complete and sound w.r. to the validity in every topolinear space. [GIRARDLAFONT,1987] gives a formulation, but not the semantics, of the sequent calculus for the intuitionistic linear propositional logic.
V. Michele Abrusci

Order Isomorphisms – A Constructive Measure-Theoretic View

Although it can be argued that, as far as the needs of economists are concerned, the problem of representing a preference relation by a real-valued utility function was solved by the work of Debreu [9,10] and others, the years since the publication of Debreu’s classic work “Theory of Value” have seen several significant new approaches to, and generalisations of, that problem [11–14].
Douglas S. Bridges

1-Generic Enumeration Degrees Below O e ’

Enumeration reducibility is the formalisation of the natural concept of relative enumerability between sets of natural numbers. A set A is said to be enumeration reducible to a set B iff there is some effective procedure which gives an enumeration of A from any enumeration of B. This can be shown to be equivalent to the following definition:
Definition 1.1 A set of natural numbers A is enumeration reducible (e-reducible,≦e) to a set of natural numbers B iff there is an i such that for all x
$$x \in A \Leftrightarrow \exists z\left[ {\langle x,z\rangle \in {W_i}\& {D_z} \subset B} \right]$$
where W i and D z are, respectively, the i th recursively enumerable set and the z th finite set in appropriate standard listing of such sets.
C. S. Copestake

Pemarks on Denjoy Sets

Denjoy sets are sets of natural numbers corresponding to reals which are interesting from the point of view of the theory of differentiation of constructive real functions. In this paper, some results concerning the structure of T- and tt-degrees containing Denjoy sets of a special type are presented. Methods of recursion theory and those of constructive mathematical analysis are combined in the proofs.
O. Demuth

Normal Modal Logics in Which the Heyting Propositional Calculus can be Embedded

Let t(A) be the result of prefixing the necessity operator ❑ to every proper subformula, save conjunctions and disjunctions, of the formula A of the language of the Heyting propositional calculus H. It is well-known that H can be embedded by t in S4, i.e. A is provable in H iff t(A) is provable in S4. Esakia (1979), and also Blok (1976), have shown that S4Grz (defined below) is the maximal normal extension of S4 in which H can be embedded by t (as a matter of fact, we find in Esakia (1979) not t, but the translation which prefixes ❑ to every subformula; this translation is equivalent to t as far as S4 and its normal extensions are concerned).
Kosta Došen

Lattices Adequate for Intuitionistic Predicate Logic

In this paper we show that there are many examples of adequate models for intuitionistic predicate logic (IPL) which appear in algebra and logic. We present a class of lattices, which are complete Heyting algebras, such that every lattice from this class is adequate for IPL in the sense that for every formula which cannot be derived in IPL and for every lattice L from the class there is a model of IPL over L in which the formula is not valid.
Wojciech Dzik

A Note on Boolean Modal Logic

We present a proof of a theorem mentioned in an earlier paper “Modal environment for Boolean speculations”, devoted to the study of extended modal languages containing the so-called “window” or “sufficiency” modal operator m. The theorem states that a particular axiom system for the poly-modal logic encompassing union, intersection and complement of relations (a Boolean analog of the propositional dynamic logic of Pratt, Fischer, Ladner and Segerberg) is complete for the standard Kripke semantics. Moreover this system modally defines the standard semantics — so in the terminology of the present paper the axiomatics is adequate. On the other hand our logic has the finite model property. Thus a fragment of second order logic, rather powerful with respect to expressiveness, turns out to be decidable.
George Gargov, Solomon Passy

Completeness and Incompleteness in the Bimodal Base ℒ(R,−R)

The paper deals with a modal language ℒ(R,−R), having an ordinary modality ⊞ (dual — S) with an usual Kripke-semantics x⊧⊞ϕ iff ∀y(Rxy ⇒ y⊧ϕ) and an additional modality ⊟ (dual — S), with the same semantics however over the complement −R of R: x⊧⊟ϕ iff ∀y(−Rxy ⇒ y⊧ϕ). Such a modality has been considered by some authors in different contexts — see e.g. [Hum] and [GPT], where the completeness theorems for the minimal normal ℒ(R,−R) — logic are independently proved. This language appears as a special case of the notion polymodal base, introduced by the author in [Gor]. This notion combines a polymodal language ℒ(□1,…,□n) with a set of formulae Φ, having a usual relational semantics over structures <W,R1,…,Rn> (frames) and a theory T in some language (for definiteness — first-order) for such structures. We shall denote such a base ℒT(R1,…,Rn). The models of the theory T will be called standard frames of this base. In particular, when the theory T determines some of the relations R1,…,Rn by means of the rest of them, the polymodal base becomes an enriched [poly]modal language. A typical example of it provides the modal language for tense logics — it is a bimodal base with a theory T−1 having a single axiom (−1) ∀xy(R1xy ↔ R2yx) and standard frames <W,R,R−1> — it is an enriched modal language for <W,R>. Another example is the language in question. ℒ(R,−R) being a bimodal base with theory T with an axiom (−) ∀xy(R1xy ↔ −R2xy) and standard frames <W,R,−R>.
Valentin Goranko

A Temporal Logic for Event Structures

The formalism of temporal logic has been suggested as an appropriate tool for specifying and proving properties of distributed programs It has become clear that the modalities of temporal logic are well suited for capturing the dynamic properties of distributed programs and systems. Originally, temporal logic was designed in order to analyse and reason about time sequences in general (for example, by Emerson and Halpern. 1985, 1986; Lamport, 1980; Gabbay et al., 1980; Pnueli, 1981). In most of the papers in the area of temporal logic concurrency is represented in terms of an arbitrary nondeterministic interleaving. Because of that the difference between concurrency and non-determinism is lost. This is quite acceptable for many pur-poses, but not always, as shown by Mazurkiewicz et al. (1988). A maior consequence, however, is that one is forced to attach formulas to the global states of a distributed system (program). In general, it is very difficult, if not impossible, to observe such global states; parts of the global state may be changing simultaneously due to independent actions carried out on two separate locations. So, we need a formalism which deals only with local states. In this formalism we incorporate operators representing the relations of causality and conflict.
Wojciech Penczek

Completeness of Propositional Dynamic Logic with Infinite Repeating

Completeness of a finite deductive system for PDL with infinite repeating is proved using the method of tableaux trees.
Jurate Sakalauskaite, Mars K. Valiev

An Equivalence between Polynomial Constructivity of Markov’s Principle and the Equality P=NP

Without Abstract
V. Yu. Sazonov

Effective Enumerations of Abstract Structures

There is a close relationship between the enumerations which admits an abstract structure A and the “effective” computable functions in A, see [1,2,3].
Alexandra A. Soskova, Ivan N. Soskov

Modal Characterization of the Classes of Finite and Infinite Quasi-Ordered Sets

To formulate the main aim of this paper we will begin with some definitions and notations. A system \(\underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{U} \)=(U,≤), where U≠Ø and ≤ is a binary relation in U, is called quasi-ordered set — qoset for short, — if the relation ≤ is reflexive and transitive one. By QO, QOfin and QOinf we will denote respectively the class of all qosets, all finite qosets and all infinite qosets. If U is a qoset and in addition the relation ≤ is an antisymmetric one /x≤y & y≤x → x=y/ then U is called partially ordered set — poset for short. By PO, POfin and POinfwe denote respectively the class of all posets, all finite posets, and all infinite posets. It is a well known fact that the modal logic S4 is complete in the classes QO and QOfin. So QO and QOfin cannot be separated by S4. However, the situation is different when we consider posets: S4 is complete in the class POinf but not in the class POfin and S4Grz / the so called Grzegorczik system/ is complete in POfin but not in POinf /see [l]/. Roughly speaking, we will say in this case, that S4 is a modal characterization of POinf and S4Grz is a modal characterization of POfin.
Dimiter Vakarelov

Least Fixed Points in Preassociative Combinatory Algebras

The intention of the investigations to which the present work belongs is to find an axiomatic basis of the recursion theory for which the following qualities are desirable to possess:(1) to be algebraically styled; that means we expect to find a suitable algebraic language, which is simple and well working and allows us to obtain a connection between recursion theory and same algebraic structures which may be interesting by themselves; (2) to have as large as possible area of applications, i.e. we expect for those structures to have many and easy constructable models: (3) to allow us to prove all the basic facts of the recursion theory in the abstract case, especially the least fixed point or first recursion theorem.
J. Zashev


Weitere Informationen