We define a variant of the standard Kripke semantics for intuitionistic logic, motivated by the connection between constructive logic and the Medvedev lattice. We show that while the new semantics is still complete, it gives a simple and direct correspondence between Kripke models and algebraic structures such as factors of the Medvedev lattice.

This paper constructs a cirquent calculus system and proves its soundness and completeness with respect to the semantics of computability logic. The logical vocabulary of the system consists of negation ${\neg}$ , parallel conjunction ${\wedge}$ , parallel disjunction ${\vee}$ , branching recurrence ⫰, and branching corecurrence ⫯. The article is published in two parts, with (the present) Part I containing preliminaries and a soundness proof, and (the forthcoming) Part II containing a completeness proof.

This paper discusses Michael Dummett’s attempt to base the use of intuitionistic logic in mathematics on a proof-conditional semantics. This project is shown to face significant obstacles resulting from the existence of variants of standard intuitionistic logic. In order to overcome these obstacles, Dummett and his followers must give an intuitionistically acceptable completeness proof for intuitionistic logic relative to the BHK interpretation of the logical constants, but there are reasons to doubt that such a proof is possible. The paper concludes (...) by proposing an alternative way of thinking about why one should use intuitionistic logic when doing mathematics. (shrink)

On the one hand, Pavel Tichý has shown in his Transparent Intensional Logic (TIL) that the best way of explicating meaning of the expressions of a natural language consists in identification of meanings with abstract procedures. TIL explicates objective abstract procedures as so-called constructions. Constructions that do not contain free variables and are in a well-defined sense ´normalized´ are called concepts in TIL. On the second hand, Kolmogorov in (Mathematische Zeitschrift 35: 58–65, 1932) formulated a theory of problems, using NL (...) expressions. He explicitly avoids presenting a definition of problems. In the present paper an attempt at such a definition (explication)—independent of but in harmony with Medvedev´s explication—is given together with the claim that every concept defines a problem. The paper treats just mathematical concepts, and so mathematical problems, and tries to show that this view makes it possible to take into account some links between conceptual systems and the ways how to replace a noneffective formulation of a problem by an effective one. To show this in concreto a wellknown Kleene’s idea from his (Introduction to metamathematics. D. van Nostrand, New York, 1952) is exemplified and explained in terms of conceptual systems so that a threatening inconsistence is avoided. (shrink)

We offer an alternative approach to the existing methods for intuitionistic formalization of reasoning about probability. In terms of Kripke models, each possible world is equipped with a structure of the form \(\langle H, \mu \rangle \) that needs not be a probability space. More precisely, though _H_ needs not be a Boolean algebra, the corresponding monotone function (we call it measure) \(\mu : H \longrightarrow [0,1]_{\mathbb {Q}}\) satisfies the following condition: if \(\alpha \), \(\beta \), \(\alpha \wedge \beta \), (...) \(\alpha \vee \beta \in H\), then \(\mu (\alpha \vee \beta ) = \mu (\alpha ) + \mu (\beta ) - \mu (\alpha \wedge \beta )\). Since the range of \(\mu \) is the set \([0,1]_{\mathbb {Q}}\) of rational numbers from the real unit interval, our logic is not compact. In order to obtain a strong complete axiomatization, we introduce an infinitary inference rule with a countable set of premises. The main technical results are the proofs of strong completeness and decidability. (shrink)

Kolmogorov introduced an informal calculus of problems in an attempt to provide a classical semantics for intuitionistic logic. This was later formalised by Medvedev and Muchnik as what has come to be called the Medvedev and Muchnik lattices. However, they only formalised this for propositional logic, while Kolmogorov also discussed the universal quantifier. We extend the work of Medvedev to first-order logic, using the notion of a first-order hyperdoctrine from categorical logic, to a structure which we will call the hyperdoctrine (...) of mass problems. We study the intermediate logic that the hyperdoctrine of mass problems gives us, and we study the theories of subintervals of the hyperdoctrine of mass problems in an attempt to obtain an analogue of Skvortsova’s result that there is a factor of the Medvedev lattice characterising intuitionistic propositional logic. Finally, we consider Heyting arithmetic in the hyperdoctrine of mass problems and prove an analogue of Tennenbaum’s theorem on computable models of arithmetic. (shrink)

A probability function on an algebra of events is assumed. Some of the events are scientific refutations in the sense that the assumption of their occurrence leads to a contradiction. It is shown that the scientific refutations form a a boolean sublattice in terms of the subset ordering. In general, the restriction of to the sublattice is not a probability function on the sublattice. It does, however, have many interesting properties. In particular, (i) it captures probabilistic ideas inherent in some (...) legal procedures; and (ii) it is used to argue against the commonly held view that behavioral violations of certain basic conditions for qualitative probability are indicative of irrationality. Also discussed are (iii) the relationship between the formal development of scientific refutations presented here and intuitionistic logic, and (iv) an interpretation of a belief function used in the behavioral sciences to explain empirical results about subjective, probabilistic estimation, including the Ellsberg paradox. (shrink)

This paper presents a constructive interpretation for the proofs in classical logic of $\Sigma^0_1$ -sentences and for a witness extraction procedure based on Prawitz's reduction rules.