The concept of “necessity of thought” plays a central role in Dag Prawitz’s essay “Logical Consequence from a Constructivist Point of View” (Prawitz 2005). The theme is later developed in various articles devoted to the notion of valid inference (Prawitz, 2009, forthcoming a, forthcoming b). In section 1 I explain how the notion of necessity of thought emerges from Prawitz’s analysis of logical consequence. I try to expound Prawitz’s views concerning the necessity of thought in sections 2, 3 and 4. (...) In sections 5 and 6 I discuss some problems arising with regard to Prawitz’s views. (shrink)

After an introductory discussion on Martin-Löf's Intuitionistic Theory of Types , the paper introduces the notion of assumption of high-arity variable. Then the original theory is extended in a very uniform way by means of the new assumptions. Some improvements allowed by high-arity variables are shown. The main result of the paper is a normal form theorem for HITT. The detailed proof follows a computability method ‘a la Tait’. The main consequences of the normal form theorem are: the consistency of (...) HITT, which also implies the consistency of ITT, and the computability of any judgement derived within HITT. Besides that, a canonical form theorem is shown: to any derivable judgement we can associate a canonical one whose derivation ends with an introductory rule. The standard disjunction and existential properties follow. Moreover, by using the computational interpretation of types it immediately follows that the execution of any proved correct program terminates. (shrink)

A notion of feasible function of finite type based on the typed lambda calculus is introduced which generalizes the familiar type 1 polynomial-time functions. An intuitionistic theory IPVω is presented for reasoning about these functions. Interpretations for IPVω are developed both in the style of Kreisel's modified realizability and Gödel's Dialectica interpretation. Applications include alternative proofs for Buss's results concerning the classical first-order system S12 and its intuitionistic counterpart IS12 as well as proofs of some of Buss's conjectures concerning IS12, (...) and a proof that IS12 cannot prove that extended Frege systems are not polynomially bounded. (shrink)

We present a general schema of easy normalization proofs for finite systems S like first-order arithmetic or subsystems of analysis, which have good infinitary counterparts S ∞ . We consider a new system S ∞ + with essentially the same rules as S ∞ but different derivable objects: a derivation d∈S ∞ + of a sequent Γ contains a derivation Φ∈S of Γ . Three simple conditions on Φ including a normal form theorem for S ∞ + easily imply a (...) weak normalization theorem for S . We give three examples of application of this schema. First, we take S≡PA but restrict the attention to derivations of Σ 1 0 -sentences. In this case it is possible to take S ∞ + to be essentially standard formulation of PA ∞ . Next, we illustrate extension to subsystems of analysis and consider the system BI 1 ∗ of W. Buchholz having the strength of ID 1 , again for derivations of Σ 1 0 -sentences. Finally, we return to the first-order arithmetic to illustrate changes needed to treat derivations of arbitrary formulas. (shrink)

This collection of papers, celebrating the contributions of Swedish logician Dag Prawitz to Proof Theory, has been assembled from those presented at the Natural Deduction conference organized in Rio de Janeiro to honour his seminal research. Dag Prawitz’s work forms the basis of intuitionistic type theory and his inversion principle constitutes the foundation of most modern accounts of proof-theoretic semantics in Logic, Linguistics and Theoretical Computer Science. The range of contributions includes material on the extension of natural deduction with higher-order (...) rules, as opposed to higher-order connectives, and a paper discussing the application of natural deduction rules to dealing with equality in predicate calculus. The volume continues with a key chapter summarizing work on the extension of the Curry-Howard isomorphism, via methods of category theory that have been successfully applied to linear logic, as well as many other contributions from highly regarded authorities. With an illustrious group of contributors addressing a wealth of topics and applications, this volume is a valuable addition to the libraries of academics in the multiple disciplines whose development has been given added scope by the methodologies supplied by natural deduction. The volume is representative of the rich and varied directions that Prawitz work has inspired in the area of natural deduction. (shrink)

This volume is dedicated to Prof. Dag Prawitz and his outstanding contributions to philosophical and mathematical logic. Prawitz's eminent contributions to structural proof theory, or general proof theory, as he calls it, and inference-based meaning theories have been extremely influential in the development of modern proof theory and anti-realistic semantics. In particular, Prawitz is the main author on natural deduction in addition to Gerhard Gentzen, who defined natural deduction in his PhD thesis published in 1934. The book opens with an (...) introductory paper that surveys Prawitz's numerous contributions to proof theory and proof-theoretic semantics and puts his work into a somewhat broader perspective, both historically and systematically. Chapters include either in-depth studies of certain aspects of Dag Prawitz's work or address open research problems that are concerned with core issues in structural proof theory and range from philosophical essays to papers of a mathematical nature. Investigations into the necessity of thought and the theory of grounds and computational justifications as well as an examination of Prawitz's conception of the validity of inferences in the light of three “dogmas of proof-theoretic semantics” are included. More formal papers deal with the constructive behaviour of fragments of classical logic and fragments of the modal logic S4 among other topics. In addition, there are chapters about inversion principles, normalization of proofs, and the notion of proof-theoretic harmony and other areas of a more mathematical persuasion. Dag Prawitz also writes a chapter in which he explains his current views on the epistemic dimension of proofs and addresses the question why some inferences succeed in conferring evidence on their conclusions when applied to premises for which one already possesses evidence. (shrink)

The main objective of this PhD Thesis is to present a method of obtaining strong normalization via natural ordinal, which is applicable to natural deduction systems and typed lambda calculus. The method includes (a) the definition of a numerical assignment that associates each derivation (or lambda term) to a natural number and (b) the proof that this assignment decreases with reductions of maximal formulas (or redex). Besides, because the numerical assignment used coincide with the length of a specific sequence of (...) reduction - the worst reduction sequence - it is the lowest upper bound on the length of reduction sequences. The main commitment of the introduced method is that it is constructive and elementary, produced only through analyzing structural and combinatorial properties of derivations and lambda terms, without appeal to any sophisticated mathematical tool. Together with the exposition of the method, it is presented a comparative study of some articles in the literature that also get strong normalization by means we can identify with the natural ordinal methods. Among them we highlight Howard[1968], which performs an ordinal analysis of Godel’s Dialectica interpretation for intuitionistic first order arithmetic. We reveal a fact about this article not noted by the author himself: a syntactic proof of strong normalization theorem for the system of typified lambda calculus λ⊃ is a consequence of its results. This would be the first strong normalization proof in the literature. (written in Portuguese). (shrink)

The investigations on higher-order type theories and on the related notion of parametric polymorphism constitute the technical counterpart of the old foundational problem of the circularity of second and higher-order logic. However, the epistemological significance of such investigations has not received much attention in the contemporary foundational debate.We discuss Girard’s normalization proof for second order type theory or System F and compare it with two faulty consistency arguments: the one given by Frege for the logical system of the Grundgesetze and (...) the one given by Martin-Löf for the intuitionistic type theory with a type of all types.The comparison suggests that the question of the circularity of second order logic cannot be reduced to Russell’s and Poincaré’s 1906 “vicious circle” diagnosis. Rather, it reveals a bunch of mathematical and logical ideas hidden behind the hazardous idea of impredicative quantification, constituting a vast domain for foundational research. (shrink)

We constructively prove completeness for intuitionistic first-order logic, iFOL, showing that a formula is provable in iFOL if and only if it is uniformly valid in intuitionistic evidence semantics as defined in intuitionistic type theory extended with an intersection operator.Our completeness proof provides an effective procedure that converts any uniform evidence into a formal iFOL proof. Uniform evidence can involve arbitrary concepts from type theory such as ordinals, topological structures, algebras and so forth. We have implemented that procedure in the (...) Nuprl proof assistant.Our result demonstrates the value of uniform validity as a semantic notion for studying logical theories, and it provides new techniques for showing that formulas are not intuitionistically provable. Here we demonstrate its value for minimal and intuitionistic first-order logic. (shrink)

In this paper we give a strong normalization proof for a set of reduction rules for classical logic. These reductions, more general than the ones usually considered in literature, are inspired to the reductions of Felleisen's lambda calculus with continuations.

The usual rule used to obtain natural deduction formulations of classical logic from intuitionistic logic, namely.

Barendregt gave a sound semantics of the simple type assignment system λ → by generalizing Tait’s proof of the strong normalization theorem. In this paper, we aim to extend the semantics so that the completeness theorem holds.

Calculi with control operators have been studied as extensions of simple type theory. Real programming languages contain datatypes, so to really understand control operators, one should also include these in the calculus. As a first step in that direction, we introduce λμTλμT, a combination of Parigotʼs λμ-calculus and Gödelʼs T, to extend a calculus with control operators with a datatype of natural numbers with a primitive recursor.We consider the problem of confluence on raw terms, and that of strong normalization for (...) the well-typed terms. Observing some problems with extending the proofs of Baba et al. and Parigotʼs original confluence proof, we provide new, and improved, proofs of confluence and strong normalization for our system.We conclude with some remarks about extensions, choices, and prospects for an improved presentation. (shrink)

The eta rule for a set A says that an arbitrary element of A is judgementally identical to an element of constructor form. Eta rules are not part of what may be called canonical Martin-Löf type theory. They are, however, justified by the meaning explanations, and a higher-order eta rule is part of that type theory. The main aim of this paper is to clarify this somewhat puzzling situation. It will be argued that lower-order eta rules do not, whereas the (...) higher-order eta rule does, accord with the understanding of judgemental identity as definitional identity. A subsidiary aim is to clarify precisely what an eta rule is. This will involve showing how such rules relate to various other notions of type theory, proof theory, and category theory. (shrink)

Substantial facts are not well-understood entities. Many philosophers object to their existence on this basis. Yet facts, if they can be understood, promise to do a lot of philosophical work: they can be used to construct theories of property possession and truthmaking, for example. Here, I give a formal theory of facts, including negative and logically complex facts. I provide a theory of reduction similar to that of the typed λ -calculus and use it to provide identity conditions for facts. (...) This theory validates truthmaker maximalism : it provides truthmakers for all truths. I then show how the usual truth-in-a-model relation can be replaced by two relations: one between models and facts, saying that a given fact obtains relative to the model, and the other between facts and propositions: the truthmaking relation. (shrink)

The new concept of lambda calculi with monotone inductive types is introduced byhelp of motivations drawn from Tarski's fixed-point theorem (in preorder theory) andinitial algebras and initial recursive algebras from category theory. They are intendedto serve as formalisms for studying iteration and primitive recursion ongeneral inductively given structures. Special accent is put on the behaviour ofthe rewrite rules motivated by the categorical approach, most notably on thequestion of strong normalization (i.e., the impossibility of an infinitesequence of successive rewrite steps). It (...) is shown that this key propertyhinges on the concrete formulation. The canonical system of monotone inductivetypes, where monotonicity is expressed by a monotonicity witness beinga term expressing monotonicity through its type, enjoys strong normalizationshown by an embedding into the traditional system of non-interleavingpositive inductive types which, however, has to be enriched by the parametricpolymorphism of system F. Restrictions to iteration on monotone inductive typesalready embed into system F alone, hence clearly displaying the differencebetween iteration and primitive recursion with respect to algorithms despitethe fact that, classically, recursion is only a concept derived from iteration. (shrink)

We introduce a linear analogue of Läuchli's semantics for intuitionistic logic. In fact, our result is a strengthening of Läuchli's work to the level of proofs, rather than provability. This is obtained by considering continuous actions of the additive group of integers on a category of topological vector spaces. The semantics, based on functorial polymorphism, consists of dinatural transformations which are equivariant with respect to all such actions. Such dinatural transformations are called uniform. To any sequent in Multiplicative Linear Logic (...) , we associate a vector space of“diadditive” uniform transformations. We then show that this space is generated by denotations of cut-free proofs of the sequent in the theory MLL + MIX. Thus we obtain a full completeness theorem in the sense of Abramsky and Jagadeesan, although our result differs from theirs in the use of dinatural transformations.As corollaries, we show that these dinatural transformations compose, and obtain a conservativity result: diadditive dinatural transformations which are uniform with respect to actions of the additive group of integers are also uniform with respect to the actions of arbitrary cocommutative Hopf algebras. Finally, we discuss several possible extensions of this work to noncommutative logic.It is well known that the intuitionistic version of Läuchli's semantics is a special case of the theory of logical relations, due to Plotkin and Statman. Thus, our work can also be viewed as a first step towards developing a theory of logical relations for linear logic and concurrency. (shrink)

We give an elementary proof of the strong normalization of the atomic polymorphic calculus Fat.

The standard natural deduction rules for the identity predicate have seemed to some not to be harmonious. Stephen Read has suggested an alternative introduction rule that restores harmony but presupposes second-order logic. Here it will be shown that the standard rules are in fact harmonious. To this end, natural deduction will be enriched with a theory of definitional identity. This leads to a novel conception of canonical derivation, on the basis of which the identity elimination rule can be justified in (...) a proof-theoretical manner. (shrink)

In the recent past, the reduction-based and the model-based methods to prove cut elimination have converged, so that they now appear just as two sides of the same coin. This paper details some of the steps of this transformation.

We introduce a new model construction for Martin-Löf intensional type theory, which is sound and complete for the 1-truncated version of the theory. The model formally combines, by gluing along the functor from the category of contexts to the category of groupoids, the syntactic model with a notion of realizability. As our main application, we use the model to analyse the syntactic groupoid associated to the type theory generated by a graph G, showing that it has the same homotopy type (...) as the free groupoid generated by G. (shrink)

In the course of ten short sections, we comment on Gödel's seminal dialectica paper of fifty years ago and its aftermath. We start by suggesting that Gödel's use of functionals of finite type is yet another instance of the realistic attitude of Gödel towards mathematics, in tune with his defense of the postulation of ever increasing higher types in foundational studies. We also make some observations concerning Gödel's recasting of intuitionistic arithmetic via the dialectica interpretation, discuss the extra principles that (...) the interpretation validates and comment on extensionality and higher order equality. The latter sections focus on the role of majorizability considerations within the dialectica and related interpretations for extracting computational information from ordinary proofs in mathematics. (shrink)

A general definition theory should serve as a foundation for the mathematical study of definitional structures. The central notion of such a theory is a precise explication of the intuitively given notion of a definitional structure. The purpose of this paper is to discuss the proof theory of partial inductive definitions as a foundation for this kind of a more general definition theory. Among the examples discussed is a suggestion for a more abstract definition of lambda-terms (derivations in natural deduction) (...) that could provide a basis for a more systematic definitional approach to general proof theory. (shrink)

The paper studies a simply typed term system Mω providing a primitive recursive concept of parallelism in the sense of Plotkin. The system aims at defining and computing partial continuous functionals. Some connections between denotational and operational semantics → for Mω are investigated. It is shown that → is correct with respect to the denotational semantics. Conversely, → is complete in the sense that if a program denotes some number k, then it is reducible to the numeral nk. Restricting to (...) the primitive recursive kernel Rω of Mω, it is shown that → is strongly normalising with uniquely determined normal forms. The twist is the design of fixed point style conversion rules for constants accounting for parallelly bounded parallel search such that correctness and strong normalisation hold. Thereupon, minor alternations to → bring about that every reduction sequence for a program of Rω terminates either in a numeral nk if the program denotes k, or in the term 0 if the program denotes the “undefined” object. Thus, Rω can be considered a primitive recursive version of Plotkin's PA+·. (shrink)

It was observed by Curry that when λ-terms can be assigned types, for example, simple types, these terms have nice properties . Coppo, Dezani, and Veneri, introduced type systems using conjunctive types, and showed that several important classes of terms can be characterized according to the shape of the types that can be assigned to these terms. For example, the strongly normalizable terms, the normalizable terms, and the terms having head-normal forms, can be characterized in some systems and Ω. The (...) proofs use variants of the method of reducibility. In this paper, we present a uniform approach for proving several meta-theorems relating properties of λ-terms and their typability in the systems and Ω. Our proofs use a new and more modular version of the reducibility method. As an application of our metatheorems, we show how the characterizations obtained by Coppo, Dezani, Veneri, and Pottinger, can be easily rederived. We also characterize the terms that have weak head-normal forms, which appears to be new. We conclude by stating a number of challenging open problems regarding possible generalizations of the realizability method. (shrink)

This paper defines reduction on derivations (cut-elimination) in the Strict Intersection Type Assignment System of an earlier paper and shows a strong normalization result for this reduction. Using this result, new proofs are given for the approximation theorem and the characterization of normalizability of terms using intersection types.

The lecture spells out the difference between the validity of inference (-figure)s and validity applied to demonstrations (‘proof acts’). The latter notion is not an ordinary characterizing one; in Brentano's terminology it is a modifying one. A demonstration lacking validity is not a real demonstration, just as a false friend is no true friend. Throughout, the treatment makes crucial use of an epistemological perspective that is cast in the first person. Furthermore, the difference between (logical) consequence among propositions and the (...) validity of inference from judgement to judgement is explained. Particular attention is paid to alleged issues of circularity in the definition of the validity of inference, and to the ‘explosion’ validity of inference from contradictory premisses. Drawing upon a version of the dialogical framework of Per Martin-Löf, namely, ‘When I say Therefore, I give others my permission to assert the conclusion’, while stressing also the importance of the first person perspective, both difficulties can be neutralized. (shrink)

In this paper, we propose a computational interpretation of the generalized Kreisel–Putnam rule, also known as the generalized Harrop rule or simply the Split rule, in the style of BHK semantics. We will achieve this by exploiting the Curry–Howard correspondence between formulas and types. First, we inspect the inferential behavior of the Split rule in the setting of a natural deduction system for intuitionistic propositional logic. This will guide our process of formulating an appropriate program that would capture the corresponding (...) computational content of the typed Split rule. Our investigation can also be reframed as an effort to answer the following question: is the Split rule constructively valid in the sense of BHK semantics? Our answer is positive for the Split rule as well as for its newly proposed general version called the S rule. (shrink)

Realizability notions in mathematical logic have a long history, which can be traced back to the work of Stephen Kleene in the 1940s, aimed at exploring the foundations of intuitionistic logic. Kleene’s initial realizability laid the ground for more sophisticated notions such as Kreisel’s modified realizability and various modern approaches. In this context, our work aligns with the lineage of realizability strategies that emphasize the accumulation, rather than the propagation of precise witnesses. In this paper, we introduce a new notion (...) of realizability, namely herbrandized modified realizability. This novel form of (cumulative) realizability, presented within the framework of semi-intuitionistic logic is based on a recently developed star combinatory calculus, which enables the gathering of witnesses into nonempty finite sets. We also show that the previous analysis can be extended from logic to (Heyting) arithmetic. (shrink)

A simple proof is given of the property that the set of strongly normalizing lambda terms coincides with the set of lambda terms typable in certain intersection type assignment systems.

This paper introduces a natural deduction calculus for intuitionistic logic of belief \ which is easily turned into a modal \-calculus giving a computational semantics for deductions in \. By using that interpretation, it is also proved that \ has good proof-theoretic properties. The correspondence between deductions and typed terms is then extended to a categorical semantics for identity of proofs in \ showing the general structure of such a modality for belief in an intuitionistic framework.

The technical contribution of this paper is threefold.First we show how to encode functionals in a ‘flat’ applicative structure by adding oracles to untyped λ-calculus and mimicking the applicative behaviour of the functionals with an impredicatively defined reduction relation. The main achievement here is a Church-Rosser result for the extended reduction relation.Second, by combining the previous result with the model construction based on partial equivalence relations, we show how to extend a λ-closed simple type structure to a model of the (...) polymorphic λ-calculus.Third, we specialize the previous result to a counter model against a simple minimization. This minimization is realized by a bar recursive functional, which contrasts the results of Spector and Girard which imply that the bar recursive functions are exactly those that are definable in the polymorphic λ-calculus. As a spin-off, we obtain directly the non-conservativity of the extensions of Gödel's T with bar recursion, fan functional, and Luckhardt's minimization functional, respectively. For the latter two extensions these results are new. (shrink)

We introduce a new typed combinatory calculus with a type constructor that, to each type σ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\sigma $$\end{document}, associates the star type σ∗\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\sigma ^*$$\end{document} of the nonempty finite subsets of elements of type σ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\sigma $$\end{document}. We prove that this calculus enjoys the properties of strong normalization and confluence. With the aid of this star combinatory (...) calculus, we define a functional interpretation of first-order predicate logic and prove a corresponding soundness theorem. It is seen that each theorem of classical first-order logic is connected with certain formulas which are tautological in character. As a corollary, we reprove Herbrand’s theorem on the extraction of terms from classically provable existential statements. (shrink)