The essential structure of proofs is proposed as the basis for a measure of complexity of formulas in FOL. The motivating idea was the recognition that distinct theorems can have the same derivation modulo some non essential details. Hence the difficulty in proving them is identical and so their complexity should be the same. We propose a notion of complexity of formulas capturing this property. With this purpose, we introduce the notions of schema calculus, schema derivation and description complexity of (...) a schema formula. Based on these concepts we prove general robustness results that relate the complexity of introducing a logical constructor with the complexity of the component schema formulas as well as the complexity of a schema formula across different schema calculi. (shrink)

Machines were introduced as calculating devices to simulate operations carried out by human computers following fixed algorithms. The mathematical study of (paper) machines is the topic of our essay. The first three sections provide necessary logical background, examine the analyses of effective calculability given in the thirties, and describe results that are central to recursion theory, reinforcing the conceptual analyses. In the final section we pursue our investigation in a quite different way and focus on principles that govern the operations (...) of physically realizable machines. (shrink)

In recent years two different axiomatic characterizations of the intuitive concept of effective calculability have been proposed, one by Sieg and the other by Dershowitz and Gurevich. Analyzing them from the perspective of Carnapian explication, I argue that these two characterizations explicate the intuitive notion of effective calculability in two different ways. I will trace back these two ways to Turing’s and Kolmogorov’s informal analyses of the intuitive notion of calculability and to their respective outputs: the notion of computorability and (...) the notion of algorithmability. I will then argue that, in order to adequately capture the conceptual differences between these two notions, the classical two-step picture of explication is not enough. I will present a more fine-grained three-step version of Carnapian explication, showing how with its help the difference between these two notions can be better understood and explained. (shrink)

In 1933 Godel introduced a calculus of provability (also known as modal logic S4) and left open the question of its exact intended semantics. In this paper we give a solution to this problem. We find the logic LP of propositions and proofs and show that Godel's provability calculus is nothing but the forgetful projection of LP. This also achieves Godel's objective of defining intuitionistic propositional logic Int via classical proofs and provides a Brouwer-Heyting-Kolmogorov style provability semantics for Int which (...) resisted formalization since the early 1930s. LP may be regarded as a unified underlying structure for intuitionistic, modal logics, typed combinatory logic and λ-calculus. (shrink)