Inspired by Pohlers' local predicativity approach to Pure Proof Theory and Howard's ordinal analysis of bar recursion of type zero we present a short, technically smooth and constructive strong normalization proof for Gödel's system T of primitive recursive functionals of finite types by constructing an ε 0 -recursive function [] 0 : T → ω so that a reduces to b implies [a] $_0 > [b]_0$ . The construction of [] 0 is based on a careful analysis of the Howard-Schütte (...) treatment of Gödel's T and utilizes the collapsing function ψ: ε 0 → ω which has been developed by the author for a local predicativity style proof-theoretic analysis of PA. The construction of [] 0 is also crucially based on ideas developed in the 1995 paper "A proof of strongly uniform termination for Gödel's T by the method of local predicativity" by the author. The results on complexity bounds for the fragments of T which are obtained in this paper strengthen considerably the results of the 1995 paper. Indeed, for given n let T n be the subsystem of T in which the recursors have type level less than or equal to n+2. (By definition, case distinction functionals for every type are also contained in T n .) As a corollary of the main theorem of this paper we obtain (reobtain?) optimal bounds for the T n -derivation lengths in terms of ω n+2 -descent recursive functions. The derivation lengths of type one functionals from T n (hence also their computational complexities) are classified optimally in terms of $ -descent recursive functions. In particular we obtain (reobtain?) that the derivation lengths function of a type one functional a ∈ T 0 is primitive recursive, thus any type one functional a in T 0 defines a primitive recursive function. Similarly we also obtain (reobtain?) a full classification of T 1 in terms of multiple recursion. As proof-theoretic corollaries we reobtain the classification of the IΣ n+1 -provably recursive functions. Taking advantage from our finitistic and constructive treatment of the terms of Gödel's T we reobtain additionally (without employing continuous cut elimination techniques) that PRA + PRWO ( $\varepsilon_0) \vdash \Pi^0_2$ - Refl(PA) and PRA + PRWO ( $\omega_{n+2}) \vdash \Pi^0_2$ - Refl(I Σ n+1 ), hence PRA + PRWO( $\epsilon_0) \vdash$ Con(PA) and PRA + PRWO( $\omega_{n+2}) \vdash$ Con(IΣ n+1 ). For programmatic reasons we outline in the introduction a vision of how to apply a certain type of infinitary methods to questions of finitary mathematics and recursion theory. We also indicate some connections between ordinals, term rewriting, recursion theory and computational complexity. (shrink)

Inspired by Pohlers' local predicativity approach to Pure Proof Theory and Howard's ordinal analysis of bar recursion of type zero we present a short, technically smooth and constructive strong normalization proof for Godel's system T of primitive recursive functionals of finite types by constructing an $\varepsilon_0$-recursive function [ ]$_0$: T $\rightarrow \omega$ so that a reduces to b implies [a]$_0 > [b]_0$. The construction of [ ]$_0$ is based on a careful analysis of the Howard-Schutte treatment of Godel's T and (...) utilizes the collapsing function $\psi: \varepsilon_0 \rightarrow \omega$ which has been developed by the author for a local predicativity style proof-theoretic analysis of PA. The construction of []$_0$ is also crucially based on ideas developed in the 1995 paper "A proof of strongly uniform termination for Godel's T by the method of local predicativity" by the author. The results on complexity bounds for the fragments of T which are obtained in this paper strengthen considerably the results of the 1995 paper. Indeed, for given n let T$_n$ be the subsystem of T in which the recursors have type level less than or equal to n+2. As a corollary of the main theorem of this paper we obtain optimal bounds for the T$_n$-derivation lengths in terms of $\omega_{n+2}$-descent recursive functions. The derivation lengths of type one functionals from T$_n$ are classified optimally in terms of $< \omega_{n+2}$-descent recursive functions. In particular we obtain that the derivation lengths function of a type one functional a $\in T_0$ is primitive recursive, thus any type one functional a in T$_0$ defines a primitive recursive function. Similarly we also obtain a full classification of T$_1$ in terms of multiple recursion. As proof-theoretic corollaries we reobtain the classification of the I$\Sigma_{n+1}$-provably recursive functions. Taking advantage from our finitistic and constructive treatment of the terms of Godel's T we reobtain additionally that PRA + PRWO \vdash \Pi^0_2$ - Refl and PRA + PRWO \vdash \Pi^0_2$ - Refl, hence PRA + PRWO \vdash$ Con and PRA + PRWO \vdash$ Con$. For programmatic reasons we outline in the introduction a vision of how to apply a certain type of infinitary methods to questions of finitary mathematics and recursion theory. We also indicate some connections between ordinals, term rewriting, recursion theory and computational complexity. (shrink)

By combining the methods of two former papers of ours we develop a finitary ordinal analysis of the axiom system KPi of Kripke-P atek set theory with an inaccessible universe. As a main result we obtain an upper bound for the provably recursive functions of KPi.

The paraconsistent system CPQ-ZFC/F is defined. It is shown using strong non-finitary methods that the theorems of CPQ-ZFC/F are exactly the theorems of classical ZFC minus foundation. The proof presented in the paper uses the assumption that a strongly inaccessible cardinal exists. It is then shown using strictly finitary methods that CPQ-ZFC/F is non-trivial. CPQ-ZFC/F thus provides a formulation of set theory that has the same deductive power as the corresponding classical system but is more reliable (...) in that non-triviality is provable by strictly finitary methods. This result does not contradict Gödel's incompleteness theorem because the proof of the deductive equivalence of the paraconsistent and classical systemss use non-finitary methods. (shrink)

This paper studies the metric structure of the space Hr of absolutely summable sequences of real numbers with at most r nonzero terms. Hr is complete, and is located and nowhere dense in the space of all absolutely summable sequences. Totally bounded and compact subspaces of Hr are characterized, and large classes of located, totally bounded, compact, and locally compact subspaces are constructed. The methods used are constructive in the strict sense. MSC: 03F65, 54E50.

In the early 1920s, the German mathematician David Hilbert (1862–1943) put forward a new proposal for the foundation of classical mathematics which has come to be known as Hilbert's Program. It calls for a formalization of all of mathematics in axiomatic form, together with a proof that this axiomatization of mathematics is consistent. The consistency proof itself was to be carried out using only what Hilbert called “finitary” methods. The special epistemological character of finitary reasoning then yields (...) the required justification of classical mathematics. Although Hilbert proposed his program in this form only in 1921, various facets of it are rooted in foundational work of his going back until around 1900, when he first pointed out the necessity of giving a direct consistency proof of analysis. Work on the program progressed significantly in the 1920s with contributions from logicians such as Paul Bernays, Wilhelm Ackermann, John von Neumann, and Jacques Herbrand. It was also a great influence on Kurt Gödel, whose work on the incompleteness theorems were motivated by Hilbert's Program. Gödel's work is generally taken to show that Hilbert's Program cannot be carried out. It has nevertheless continued to be an influential position in the philosophy of mathematics, and, starting with the work of Gerhard Gentzen in the 1930s, work on so-called Relativized Hilbert Programs have been central to the development of proof theory. (shrink)

David Hilbert proposed his well-known Hilbert Program in the early 1920s for foundations of mathematics. The purpose of his program was to prove the consistency of mathematics by using the finitary methods and relying on axiomatic system. Thus, riddles and paradoxes related with the foundations of mathematics could be solved. Hilbert considers, formalizing whole mathematics in a consistent finite way depending on axioms, as an effort to develop a proof theory. So much so that any problems which may (...) occur in a mathematical system, including those related to infinity, will be solved. Hilbert begins with finite number of signs and rules and then proceeds to develop various proved consistent statements. From there, he continues to a higher-order mathematics that includes ideal objects. Hilbert's development of the program started in 1899 with the Foundations of Geometry, and completed by The Grounding of Elementary Number Theory in 1931. In this paper, we will exhibit the various stages and attempts of Hilbert to found the numbers. Our thesis states that Hilbert has always maintained an intuitive apprehension in these foundational attempts i.e. Hilbert advocates intuitional insight prior to any logical inference that makes it possible to found the numbers. Although Hilbert did not define himself as a formalist in any of his works, he was named as a formalist because of Brouwer's criticism of him. Hilbert’s emphasis on intuition reveals that a kind of formalism which is a mere play of signs can be associated with him. In this paper, we will also deal with the relations Hilbert established between signs, axioms, logic and intuition. (shrink)

This is a general account of metavaluations and their applications, which can be seen as an alternative to standard model-theoretic methodology. They work best for what are called metacomplete logics, which include the contraction-less relevant logics, with possible additions of Conjunctive Syllogism, & →.A→C, and the irrelevant, A→.B→A, these including the logic MC of meaning containment which is arguably a good entailment logic. Indeed, metavaluations focus on the formula-inductive properties of theorems of entailment form A→B, splintering into two types, M1- (...) and M2-, according to key properties of negated entailment theorems. Metavaluations have an inductive presentation and thus have some of the advantages that model theory does, but they represent proof rather than truth and thus represent proof-theoretic properties, such as the priming property, if ├ A $\vee$ B then ├ A or ├ B, and the negated-entailment properties, not-├ ∼ and ├ ∼ iff ├ A and ├ ∼ B. Topics to be covered are their impact on naive set theory and paradox solution, and also Peano arithmetic and Godel’s First and Second Theorems. Interesting to note here is that the familiar M1- and M2-metacomplete logics can be used to solve the set-theoretic paradoxes and, by inference, the Liar Paradox and key semantic paradoxes. For M1-logics, in particular, the final metavaluation that is used to prove the simple consistency is far simpler than its correspondent in the model-theoretic proof in that it consists of a limit point of a single transfinite sequence rather than that of a transfinite sequence of such limit points, as occurs in the model-theoretic approach. Additionally, it can be shown that Peano Arithmetic is simply consistent, using metavaluations that constitute finitary methods. Both of these results use specific metavaluational properties that have no correspondents in standard model theory and thus it would be highly unlikely that such model theory could prove these results in their final forms. (shrink)

Sections 1 through 4 define, in the usual inductive style, various classes of object including one which is called the “combinatory terms of polymorphic type”. Section 5 defines a reduction relation on these terms. Section 6 shows that the weak normalizability of the combinatory terms of polymorphic type entails the weak normalizability of the lambda terms of polymorphic type. The entailment is not vacuous, because the combinatory terms of polymorphic type are indeed weakly normalizable, as is proven in Sect. 7 (...) using Tait and Girard’s computability predicates. The remainder of the paper is devoted to arguing that interesting consequences would follow from the existence of an “ordinally informative” proof, i.e. one which uses transfinite induction over recursive ordinal numbers and otherwise finitary methods, of normalizability for as large a class of the terms as possible. (shrink)

The concept of compactness is a necessary condition of any system that is going to call itself a finitary method of proof. However, it can also apply to predicates of sets of formulas in general and in that manner it can be used in relation to level functions, a flavor of measure functions. In what follows we will tie these concepts of measure and compactness together and expand some concepts which appear in d'Entremont's master's thesis, "Inference and Level." We (...) will also provide some applications of the concept of level to the "preservationist" program of paraconsistent logic. We apply the finite level compactness theorem in this paper to get a Lindenbaum flavor extension lemma and a maximal "forcibility" theorem. Each of these is based on an abstract deductive system X which satisfies minimal conditions of inference and has generalizations of 'and' and 'not' as logical words. (shrink)

The lack of specific arithmetical axioms in Book VII has puzzled historians of mathematics. It is hardly possible in our view to ascribe to the Greeks a conscious undertaking to axiomatize arithmetic. The view that associates the beginnings of the axiomatization of arithmetic with the works of Grassman [1861], Dedekind [1888] and Peano [1889] seems to be more plausible. In this connection a number of interesting historical problems have been raised, for instance, why arithmetic was axiomatized so late. This question (...) was first posed and quite conclusively answered by Yanovskaja [1956]. Her major and quite conclusive argument was that “algorithms in arithmetic have absolute character, while in geometry we have to do with reducibility algorithms”. In this paper we are going to draw attention on certain peculiarities of the construction of the arithmetical Books of Euclid’s "Elements" and show that Euclidean arithmetic is constructed by effective procedures. In spite of the use of inference by reductio ad absurdum and methods equivalent to mathematical induction, Euclidean arithmetic retains its finitary character. It is not full arithmetic, but a finitary fragment of classical arithmetic, and thereby there was not any internal reason for its axiomatization. (shrink)

A basic aim of E. Beth's work in philosophy of science was to explore the use of formal semantic methods in the analysis of physical theories. We hope to show that a general framework for Beth's semantic analysis is provided by the theory of semi-interpreted languages, introduced in a previous paper. After developing Beth's analysis of nonrelativistic physical theories in a more general form, we turn to the notion of the 'logic' of a physical theory. Here we prove a (...) result concerning the conditions under which semantic entailment in such a theory is finitary. We argue, finally, that Beth's approach provides a characterization of physical theory which is more faithful to current practice in foundational research in the sciences than the familiar picture of a partly interpreted axiomatic theory. (shrink)

In the 1920s, Ackermann and von Neumann, in pursuit of Hilbert's programme, were working on consistency proofs for arithmetical systems. One proposed method of giving such proofs is Hilbert's epsilon-substitution method. There was, however, a second approach which was not reflected in the publications of the Hilbert school in the 1920s, and which is a direct precursor of Hilbert's first epsilon theorem and a certain "general consistency result" due to Bernays. An analysis of the form of this so-called "failed proof" (...) sheds further light on an interpretation of Hilbert's programme as an instrumentalist enterprise with the aim of showing that whenever a "real" proposition can be proved by ?ideal? means, it can also be proved by "real", finitary means. (shrink)

We describe an infinitary logic for metric structures which is analogous to Lω1,ω. We show that this logic is capable of expressing several concepts from analysis that cannot be expressed in finitary continuous logic. Using topological methods, we prove an omitting types theorem for countable fragments of our infinitary logic. We use omitting types to prove a two-cardinal theorem, which yields a strengthening of a result of Ben Yaacov and Iovino concerning separable quotients of Banach spaces.

This paper offers an elementary proof that formal arithmetic is consistent. The system that will be proved consistent is a first-order theory R♯, based as usual on the Peano postulates and the recursion equations for + and ×. However, the reasoning will apply to any axiomatizable extension of R♯ got by adding classical arithmetical truths. Moreover, it will continue to apply through a large range of variation of the un- derlying logic of R♯, while on a simple and straightforward translation, (...) the classical first-order theory P♯ of Peano arithmetic turns out to be an exact subsystem of R♯. Since the reasoning is elementary, it is formalizable within R♯ itself; i.e., we can actually demonstrate within R♯ (or within P♯, if we care) a statement that, in a natural fashion, asserts the consistency of R♯ itself. The reader is unlikely to have missed the significance of the remarks just made. In plain English, this paper repeals Goedel’s famous second theorem. (That’s the one that asserts that sufficiently strong systems are inadequate to demonstrate their own consistency.) That theorem (or at least the significance usually claimed for it) was a mis- take—a subtle and understandable mistake, perhaps, but a mistake nonetheless. Accordingly, this paper reinstates the formal program which is often taken to have been blasted away by Goedel’s theorems— namely, the Hilbert program of demonstrating, by methods that everybody can recognize as effective and finitary, that intuitive mathematics is reliable. Indeed, the present consistency proof for arithmetic will be recognized as correct by anyone who can count to 3. (So much, indeed, for the claim that the reliability of arithmetic rests on transfinite induction up to ε0, and for the incredible mythology that underlies it.). (shrink)

Herbrand's Theorem, in the form of $$\underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{\exists } $$ -inversion lemmata for finitary and infinitary sequent calculi, is the crucial tool for the determination of the provably total function(al)s of a variety of theories. The theories are (second order extensions of) fragments of classical arithmetic; the classes of provably total functions include the elements of the Polynomial Hierarchy, the Grzegorczyk Hierarchy, and the extended Grzegorczyk Hierarchy $\mathfrak{E}^\alpha $ , α < ε0. A subsidiary aim of the paper is to (...) show that the proof theoretic methods used here are distinguished by technical elegance, conceptual clarity, and wide-ranging applicability. (shrink)

This book is a state-of-the-art review on the Physics of Emergence. Foreword v Gregory J. Chaitin Preface vii Ignazio Licata Emergence and Computation at the Edge of Classical and Quantum Systems 1 Ignazio Licata Gauge Generalized Principle for Complex Systems 27 Germano Resconi Undoing Quantum Measurement: Novel Twists to the Physical Account of Time 61 Avshalom C. Elitzur and Shahar Dolev Process Physics: Quantum Theories as Models of Complexity 77 Kirsty Kitto A Cross-disciplinary Framework for the Description of Contextually Mediated (...) Change 109 Liane Gabora and Diederik Aerts Quantum-like Probabilistic Models Outside Physics 135 Andrei Khrennikov Phase Transitions in Biological Matter 165 Eliano Pessa Microcosm to Macrocosm via the Notion of a Sheaf (Observers in Terms of t-topos) 229 Goro Kato The Dissipative Quantum Model of Brain and Laboratory Observations 233 Walter J. Freeman and Giuseppe Vitiello Supersymmetric Methods in the Traveling Variable: Inside Neurons and at the Brain Scale 253 H.C. Rosu, O. Cornejo-Perez, and J.E. Perez-Terrazas Turing Systems: A General Model for Complex Patterns in Nature 267 R.A. Barrio Primordial Evolution in the Finitary Process Soup 297 Olof Gornerup and James P. Crutchfield Emergence of Universe from a Quantum Network 313 Paola A. Zizzi Occam's Razor Revisited: Simplicity vs. Complexity in Biology 327 Joseph P. Zbilut Order in the Nothing: Autopoiesis and the Organizational Characterization of the Living 339 Leonardo Bich and Luisa Damiano Anticipation in Biological and Cognitive Systems: The Need for a Physical Theory of Biological Organization 371 Graziano Terenzi How Uncertain is Uncertainty? 389 Tibor Vamos Archetypes, Causal Description and Creativity in Natural World 405 Leonardo Chiatti . (shrink)

We develop canonical rules capable of axiomatizing all systems of multiple-conclusion rules over K4 or IPC, by extension of the method of canonical formulas by Zakharyaschev [37]. We use the framework to give an alternative proof of the known analysis of admissible rules in basic transitive logics, which additionally yields the following dichotomy: any canonical rule is either admissible in the logic, or it is equivalent to an assumption-free rule. Other applications of canonical rules include a generalization of the Blok–Esakia (...) theorem and the theory of modal companions to systems of multiple-conclusion rules or (finitary structural global) consequence relations, and a characterization of splittings in the lattices of consequence relations over monomodal or superintuitionistic logics with the finite model property. (shrink)

In lieu of an abstract, here is a brief excerpt of the content:Journal of the History of Philosophy 39.3 (2001) 454-456 [Access article in PDF] Michael Potter. Reason's Nearest Kin: Philosophies of Arithmetic from Kant to Carnap.New York: Oxford University Press, 2000. Pp. x + 305. Cloth, $45.00. This book tells the story of a remarkable series of answers to two related questions:(1) How can arithmetic be necessary and knowable a priori? [End Page 454](2) What accounts for the applicability of (...) arithmetic to matters of empirical fact?These are philosophical questions, part of a "wider puzzle of explaining the link between experience, language, thought, and the world" (18). But answers to them are heavily constrained by technical results in logic and mathematics, and most of Potter's protagonists are either mathematicians (Frege, Dedekind, Ramsey, Hilbert, Gödel) or mathematically trained philosophers (Kant, Russell, Carnap). (Only Wittgenstein fits neither category.) Potter, whose doctorate was in pure mathematics, is an able guide.It is not hard to think of answers to these questions taken singly; what is hard is answering both at the same time. Formalists can easily explain why arithmetic does not depend for its justification on empirical fact—it is just a game with symbols, not responsible to anything beyond its own rules—but they then have trouble explaining why the world of empirical fact is constrained by this game. Empiricists can explain the applicability of arithmetic in just the same way they explain the applicability of physics, but they then must then explain away the apparent a prioricity and necessity of arithmetic. Kant was the first to propose a plausible answer to both questions: arithmetic is both necessary and empirically applicable because it is grounded in the spatio-temporal form of any possible experience.What unites Frege, Dedekind, Russell, Ramsey, Hilbert, and Carnap is that they reject Kant's answer while continuing to seek an answer to his question: how can arithmetic's necessity be reconciled with its applicability? Potter helpfully classifies their projects by the surrogates they substitute for Kant's appeal to the form of spatio-temporal intuition: Frege and Dedekind appeal to thought, Russell to necessary features of the world, Wittgenstein, Ramsey, and Carnap to language, and Hilbert to the necessary structure of our experience of finitary combinations of objects. (Revealingly, the logicists are not grouped together in Potter's taxonomy.) A chapter (or two) is devoted to each of these thinkers, plus Kant and Gödel.This breadth of coverage does not come at the price of superficiality: Potter's chapters are (by and large) accurate, penetrating, and full of interesting insights. I cannot think of another book that offers such clear explanations of the many mathematical concepts and distinctions one must grasp in order to follow debates in the philosophy of arithmetic. The Russell chapters are enhanced by numerous quotations from archival material. The exposition of Hilbert's programme and the implications for it of Gödel's theorems is the best I have seen. The discussions of Wittgenstein's views on arithmetic and of Carnap's syntactical approach also shine. The chapters on Kant and Frege are somewhat weaker; the discussion of Kant, in particular, would have benefited from some engagement with Michael Friedman's views.But the real contribution of Potter's book is its integration of these nine thinkers into a single coherent story. No one will be surprised that Russell's motivations can only be understood in light of Frege's failures, or that many features of Wittgenstein's cryptic work become clearer when seen in light of the specific problems with Russell's system. But there are also some less obvious payoffs: for example, Hilbert's programme is usefully compared with Russell's regressive method (227-8), and Carnap and Russell are shown to face a common dilemma (269, 286).If there is a central theme to Potter's story, it is "how often we have had to reject an [End Page 455] account not for philosophical reasons but for technical ones" (278). Frege's program founders on Russell's paradox, Russell's... (shrink)

An approach to ordinal analysis is presented which is finitary, but highlights the semantic content of the theories under consideration, rather than the syntactic structure of their proofs. In this paper the methods are applied to the analysis of theories extending Peano arithmetic with transfinite induction and transfinite arithmetic hierarchies.

Adolf Lindenbaum Adolf Lindenbaum was a Polish mathematician and logician who worked in topology, set theory, metalogic, general metamathematics and the foundations of mathematics. He represented an attitude typical of the Polish Mathematical School, consisting of using all admissible methods, independently of whether they were finitary. For example, the axiom of choice was freely applied, … Continue reading Lindenbaum, Adolf →.

This is the first paper on constructive concurrent dynamic logic . For the first time, either for concurrent or sequential dynamic logic, we give a satisfactory treatment of what statements are forced to be true by partial information about the underlying computer. Dynamic logic was developed by Pratt [V. Pratt, Semantical considerations on Floyd–Hoare logic, in: 17th Annual IEEE Symp. on Found. Comp. Sci., New York, 1976, pp. 109–121, V. Pratt, Applications of modal logic to programming, Studia Logica 39 257–274] (...) for nondeterministic sequential programs, and by Peleg [D. Peleg, Concurrent dynamic logic, Journal of the Association for Computing Machinery 34 , D. Peleg, Communication in concurrent dynamic logic, Journal of Computer and System Sciences 35 ] for concurrent programs, for the purpose of proving properties of programs such as correctness. Here we define what it means for a dynamic logic formula to be forced to be true knowing only partial information about the results of assignments and tests. This informal CCDL semantics is formalized by intuitionistic Kripke frames modeling this partial information, and each such frame is interpreted as an idealized concurrent machine . In CCDL, proofs and deductions are ω-height, ω-branching, well-founded labeled subtrees of ωω. These are a generalization of the signed tableaux of Nerode [A. Nerode, Some lectures in modal logic, Technical Report, M.S.I. Cornell University, 1989, CIME Logic and Computer Science Montecatini Volume, Springer-Verlag Lecture Notes, 1990, A. Nerode, Some lectures in intuitionistic logic, Technical Report, M.S.I. Cornell University, 1988, Marktoberdorf Logic and Computation NATO Summer School Volume, NATO Science Series, 1990 ] stemming from the prefix tableaux of Fitting [M.C. Fitting, Proof Methods for Modal and Intuitionistic Logic, Reidel, 1983]. We demonstrate the correctness of our tableau proofs, define consistency properties, prove that consistency properties yield models, construct systematic tableaux, prove that systematic tableaux yield a consistency property, and conclude that CCDL is complete. This infinitary semantics and proof procedure will be the primary guide for defining, in a sequel, the correct finitary CCDL based on induction principles. FCCDL is suitable for implementation in constructive logic software systems such as Constable’s NUPRL or Huet-Coquand’s CONSTRUCTIONS. Our goal is to develop a constructive logic programming tool for specification and modular verification of programs in any imperative concurrent language, and for the extraction of concurrent programs from constructive proofs. Subsequent papers will introduce analogous logics for declarative and functional concurrent languages. (shrink)

In this paper, we give a constructive nonstandard model of intuitionistic arithmetic (Heyting arithmetic). We present two axiomatisations of the model: one finitary and one infinitary variant. Using the model these axiomatisations are proven to be conservative over ordinary intuitionistic arithmetic. The definition of the model along with the proofs of its properties may be carried out within a constructive and predicative metatheory (such as Martin-Löf's type theory). This paper gives an illustration of the use of sheaf semantics to (...) obtain effective proof-theoretic results.The axiomatisations of nonstandard intuitionistic arithmetic (to be calledHAIandHAIωrespectively) as well as their model are based on the construction in [5] of a sheaf model for arithmetic using a site of filters. In this paper we present a “minimal” version of this model, built instead on a suitable site of provable filter bases. The construction of this site can be viewed as an extension of the well-known construction of the classifying topos for a geometric theory which uses “syntactic sites”. (Such sites can in fact be used to prove semantical completeness of first order logic in a strictly constructive framework, see [6].)We should mention that for classical nonstandard arithmetics there are several nonconstructive methods of proving conservativity over arithmetic, e.g. the compactness theorem, Mac Dowell–Specker's theorem [3]. (shrink)

A notion called Herbrand saturation is shown to provide the model-theoretic analogue of a proof-theoretic method, Herbrand analysis, yielding uniform model-theoretic proofs of a number of important conservation theorems. A constructive, algebraic variation of the method is described, providing yet a third approach, which is finitary but retains the semantic flavor of the model-theoretic version.

In this paper, we give a constructive nonstandard model of intuitionistic arithmetic (Heyting arithmetic). We present two axiomatisations of the model: one finitary and one infinitary variant. Using the model these axiomatisations are proven to be conservative over ordinary intuitionistic arithmetic. The definition of the model along with the proofs of its properties may be carried out within a constructive and predicative metatheory (such as Martin-Löf's type theory). This paper gives an illustration of the use of sheaf semantics to (...) obtain effective proof-theoretic results.The axiomatisations of nonstandard intuitionistic arithmetic (to be calledHAIandHAIωrespectively) as well as their model are based on the construction in [5] of a sheaf model for arithmetic using a site of filters. In this paper we present a “minimal” version of this model, built instead on a suitable site of provable filter bases. The construction of this site can be viewed as an extension of the well-known construction of the classifying topos for a geometric theory which uses “syntactic sites”. (Such sites can in fact be used to prove semantical completeness of first order logic in a strictly constructive framework, see [6].)We should mention that for classical nonstandard arithmetics there are several nonconstructive methods of proving conservativity over arithmetic, e.g. the compactness theorem, Mac Dowell–Specker's theorem [3]. (shrink)

We consider the equationally orderable quasivarieties and associate with them deductive systems defined using the order. The method of definition of these deductive systems encompasses the definition of logics preserving degrees of truth we find in the research areas of substructural logics and mathematical fuzzy logic. We prove several general results, for example that the deductive systems so defined are finitary and that the ones associated with equationally orderable varieties are congruential.

In 1936, Gerhard Gentzen published a proof of consistency for Peano Arithmetic using transfinite induction up to ε0, which was considered a finitistically acceptable procedure by both Gentzen and Paul Bernays. Gentzen’s method of arithmetising ordinals and thus avoiding the Platonistic metaphysics of set theory traces back to the 1920s, when Bernays and David Hilbert used the method for an attempted proof of the Continuum Hypothesis. The idea that recursion on higher types could be used to simulate the limit-building in (...) transfinite recursion seems to originate from Bernays. The main difficulty, which was already discovered in Gabriel Sudan’s nearly forgotten paper of 1927, was that measuring transfinite ordinals requires stronger methods than representing them. This paper presents a historical account of the idea of nominalistic ordinals in the context of the Hilbert Programme as well as Gentzen and Bernays’ finitary interpretation of transfinite induction. (shrink)

We study classes of right-angled Coxeter groups with respect to the strong submodel relation of a parabolic subgroup. We show that the class of all right-angled Coxeter groups is not smooth and establish some general combinatorial criteria for such classes to be abstract elementary classes (AECs), for them to be finitary, and for them to be tame. We further prove two combinatorial conditions ensuring the strong rigidity of a right-angled Coxeter group of arbitrary rank. The combination of these results (...) translates into a machinery to build concrete examples of AECs satisfying given model-theoretic properties. We exhibit the power of our method by constructing three concrete examples of finitary classes. We show that the first and third classes are nonhomogeneous and that the last two are tame, uncountably categorical, and axiomatizable by a single Lω1,ω-sentence. We also observe that the isomorphism relation of any countable complete first-order theory is κ-Borel reducible (in the sense of generalized descriptive set theory) to the isomorphism relation of the theory of right-angled Coxeter groups whose Coxeter graph is an infinite random graph. (shrink)

One of the main problems in computer science is to ensure that programs are implemented in such a way that they satisfy a given specification. There are many studies about methods to prove correctness of programs. This work presents a method, belonging to the constructive synthesis or proofs-as-programs paradigm, that comes from the Curry-Howard isomorphism and extracts the computational contents of intuitionist proofs. The synthesis process proposed produces a program in an imperative language from a proof in many-sorted intuitionist (...) logic, where the axioms define the abstract data types, using Natural Deduction as deductive system. It is proved the correctness, as well as the completeness of the method regarding the Heyting arithmetic with ω-rule . A discussion about the use of the finitary induction instead of computational ω-rule concludes the work. (shrink)

In lieu of an abstract, here is a brief excerpt of the content:Journal of the History of Philosophy 39.3 (2001) 454-456 [Access article in PDF] Michael Potter. Reason's Nearest Kin: Philosophies of Arithmetic from Kant to Carnap.New York: Oxford University Press, 2000. Pp. x + 305. Cloth, $45.00. This book tells the story of a remarkable series of answers to two related questions:(1) How can arithmetic be necessary and knowable a priori? [End Page 454](2) What accounts for the applicability of (...) arithmetic to matters of empirical fact?These are philosophical questions, part of a "wider puzzle of explaining the link between experience, language, thought, and the world" (18). But answers to them are heavily constrained by technical results in logic and mathematics, and most of Potter's protagonists are either mathematicians (Frege, Dedekind, Ramsey, Hilbert, Gödel) or mathematically trained philosophers (Kant, Russell, Carnap). (Only Wittgenstein fits neither category.) Potter, whose doctorate was in pure mathematics, is an able guide.It is not hard to think of answers to these questions taken singly; what is hard is answering both at the same time. Formalists can easily explain why arithmetic does not depend for its justification on empirical fact—it is just a game with symbols, not responsible to anything beyond its own rules—but they then have trouble explaining why the world of empirical fact is constrained by this game. Empiricists can explain the applicability of arithmetic in just the same way they explain the applicability of physics, but they then must then explain away the apparent a prioricity and necessity of arithmetic. Kant was the first to propose a plausible answer to both questions: arithmetic is both necessary and empirically applicable because it is grounded in the spatio-temporal form of any possible experience.What unites Frege, Dedekind, Russell, Ramsey, Hilbert, and Carnap is that they reject Kant's answer while continuing to seek an answer to his question: how can arithmetic's necessity be reconciled with its applicability? Potter helpfully classifies their projects by the surrogates they substitute for Kant's appeal to the form of spatio-temporal intuition: Frege and Dedekind appeal to thought, Russell to necessary features of the world, Wittgenstein, Ramsey, and Carnap to language, and Hilbert to the necessary structure of our experience of finitary combinations of objects. (Revealingly, the logicists are not grouped together in Potter's taxonomy.) A chapter (or two) is devoted to each of these thinkers, plus Kant and Gödel.This breadth of coverage does not come at the price of superficiality: Potter's chapters are (by and large) accurate, penetrating, and full of interesting insights. I cannot think of another book that offers such clear explanations of the many mathematical concepts and distinctions one must grasp in order to follow debates in the philosophy of arithmetic. The Russell chapters are enhanced by numerous quotations from archival material. The exposition of Hilbert's programme and the implications for it of Gödel's theorems is the best I have seen. The discussions of Wittgenstein's views on arithmetic and of Carnap's syntactical approach also shine. The chapters on Kant and Frege are somewhat weaker; the discussion of Kant, in particular, would have benefited from some engagement with Michael Friedman's views.But the real contribution of Potter's book is its integration of these nine thinkers into a single coherent story. No one will be surprised that Russell's motivations can only be understood in light of Frege's failures, or that many features of Wittgenstein's cryptic work become clearer when seen in light of the specific problems with Russell's system. But there are also some less obvious payoffs: for example, Hilbert's programme is usefully compared with Russell's regressive method (227-8), and Carnap and Russell are shown to face a common dilemma (269, 286).If there is a central theme to Potter's story, it is "how often we have had to reject an [End Page 455] account not for philosophical reasons but for technical ones" (278). Frege's program founders on Russell's paradox, Russell's... (shrink)

SummaryFinite, or Fermat arithmetic, as we call it, differs from Peano arithmetic in that it does not involve the existence of an infinite set or Peano's induction postulate. Fermat's method of infinite descent takes the place of bound induction, and we show that a con‐structivist interpretation of logical connectives and quantifiers can account for the predicative finitary nature of Fermat's arithmetic. A non‐set‐theoretic arithemetical logic thus seems best suited to a constructivist‐inspired number theory.

This is easily the most systematic survey of the foundations of logic and mathematics available today. Although Beth does not cover the development of set theory in great detail, all other aspects of logic are well represented. There are nine chapters which cover, though not in this order, the following: historical background and introduction to the philosophy of mathematics; the existence of mathematical objects as expressed by Logicism, Cantorism, Intuitionism, and Nominalism; informal elementary axiomatics; formalized axiomatics with reference to (...) class='Hi'>finitary theory of proof; non-elementary metamathematics, embracing formal syntax and semantics; applications of set theory and topology in metamathematics—especially in the theory of models; recursive function theory; the logical paradoxes; the relation of philosophy of mathematics to general philosophy. This is a mere skeleton of the whole, but it indicates the broad sweep of the work. One unifying feature is the author's use of his "semantic tableau" method of examining the truth or falsity of sentences. Although the author is an Intuitionist, classical metamathematical proof techniques are by no means slighted; they are used throughout much of the book, and are indispensable, of course, when dealing with classical logic. Exercises are scattered throughout and at the end; few of them are trivial. There is a very extensive bibliography, brought up to date from the first edition. This extraordinary book will be of use to logicians as a reference tool and to philosophers trying to survey the field of modern formal logic; its appearance in a fine paper edition is therefore doubly welcome—P. J. M. (shrink)

I argue for the use of the adjunction operator (adding a single new element to an existing set) as a basis for building a finitary set theory. It allows a simplified axiomatization for the first-order theory of hereditarily finite sets based on an induction schema and a rigorous characterization of the primitive recursive set functions. The latter leads to a primitive recursive presentation of arithmetical operations on finite sets.

A notion of finitary inductively presented (f.i.p.) logic is proposed here, which includes all syntactically described logics (formal systems)met in practice. A f.i.p. theory FS0 is set up which is universal for all f.i.p. logics; though formulated as a theory of functions and classes of expressions, FS0 is a conservative extension of PRA. The aims of this work are (i)conceptual, (ii)pedagogical and (iii)practical. The system FS0 serves under (i)and (ii)as a theoretical framework for the formalization of metamathematics. The general (...) approach may be used under (iii)for the computer implementation of logics. In all cases, the work aims to make the details manageable in a natural and direct way. (shrink)

It is known that every α-dimensional quasi polyadic equality algebra (QPEA α ) can be considered as an α-dimensional cylindric algebra satisfying the merrygo- round properties . The converse of this proposition fails to be true. It is investigated in the paper how to get algebras in QPEA from algebras in CA. Instead of QPEA the class of the finitary polyadic equality algebras (FPEA) is investigated, this class is definitionally equivalent to QPEA. It is shown, among others, that from (...) every algebra in a β-dimensional algebra can be obtained in QPEA β where , moreover the algebra obtained is representable in a sense. (shrink)

Argumentation, which can be abstractly defined as the interaction of different arguments for and against some conclusion, is an important skill to learn for everyday life, law, science, politics and business. The best way to learn it is to try it out on real instances of arguments found in everyday conversational exchanges and legal argumentation. The introductory chapter of this book gives a clear general idea of what the methods of argumentation are and how they work as tools that (...) can be used to analyze arguments. Each subsequent chapter then applies these methods to a leading problem of argumentation. Today the field of computing has embraced argumentation as a paradigm for research in artificial intelligence and multi-agent systems. Another purpose of this book is to present and refine tools and techniques from computing as components of the methods that can be handily used by scholars in other fields. (shrink)

This is a supplement to the paper “Finitary Algebraic Logic” [1]. It includes corrections for several errors and some additional results. MSC: 03G15, 03G25.

Finitary sketches, i.e., sketches with finite-limit and finite-colimit specifications, are proved to be as strong as geometric sketches, i.e., sketches with finite-limit and arbitrary colimit specifications. Categories sketchable by such sketches are fully characterized in the infinitary first-order logic: they are axiomatizable by σ-coherent theories, i.e., basic theories using finite conjunctions, countable disjunctions, and finite quantifications. The latter result is absolute; the equivalence of geometric and finitary sketches requires (in fact, is equivalent to) the non-existence of measurable cardinals.