In this note the proof-theoretic ordinal of the well-ordering principle for the normal functions \ on ordinals is shown to be equal to the least fixed point of \. Moreover corrections to the previous paper are made.

We characterize the proof-theoretic strength of systems of explicit mathematics with a general principle asserting the existence of least fixed points for monotone inductive definitions, in terms of certain systems of analysis and set theory. In the case of analysis, these are systems which contain the Σ12-axiom of choice and Π12-comprehension for formulas without set parameters. In the case of set theory, these are systems containing the Kripke-Platek axioms for a recursively inaccessible universe together with the existence (...) of a stable ordinal. In all cases, the exact strength depends on what forms of induction are admitted in the respective systems. (shrink)

Questions concerning the proof-theoretic strength of classical versus nonclassical theories of truth have received some attention recently. A particularly convenient case study concerns classical and nonclassical axiomatizations of fixed-point semantics. It is known that nonclassical axiomatizations in four- or three-valued logics are substantially weaker than their classical counterparts. In this paper we consider the addition of a suitable conditional to First-Degree Entailment—a logic recently studied by Hannes Leitgeb under the label HYPE. We show in particular that, by (...) formulating the theory PKF over HYPE, one obtains a theory that is sound with respect to fixed-point models, while being proof-theoretically on a par with its classical counterpart KF. Moreover, we establish that also its schematic extension—in the sense of Feferman—is as strong as the schematic extension of KF, thus matching the strength of predicative analysis. (shrink)

KPM is a subsystem of set theory designed to formalize a recursively Mahlo universe of sets. In this paper we show that a certain ordinal notation system is sufficient to measure the proof-theoretic strength ofKPM. This involves a detour through an infinitary calculus RS(M), for which we prove several cutelimination theorems. Full cut-elimination is available for derivations of $\Sigma (L_{\omega _1^c } )$ sentences, whereω 1 c denotes the least nonrecursive ordinal. This paper is self-contained, at least (...) from a technical point of view. (shrink)

In this paper we calibrate the exact proof-theoretic strength of Kruskal's theorem, thereby giving, in some sense, the most elementary proof of Kruskal's theorem. Furthermore, these investigations give rise to ordinal analyses of restricted bar induction.

This paper explores the interface between principles of self-applicable truth and classical logic. To this end, the proof-theoretic strength of a number of axiomatic theories of truth over intuitionistic logic is determined. The theories considered correspond to the maximal consistent collections of fifteen truth-theoretic principles as isolated in Leigh and Rathjen.

The starting point of this article is an old question asked by Feferman in his paper on Hancock's conjecture [6] about the strength of ${\rm ID}_{1}^{\ast}$. This theory is obtained from the well-known theory ID₁ by restricting fixed point induction to formulas that contain fixed point constants only positively. The techniques used to perform the proof-theoretic analysis of ${\rm ID}_{1}^{\ast}$ also permit to analyze its transfinitely iterated variants ${\rm ID}_{\alpha}^{\ast}$. Thus, we eventually know that $|\widehat{{\rm ID}}_{\alpha}|=|{\rm ID}_{\alpha}^{\ast}|$.

The paper aims to provide precise proof theoretic characterizations of Myhill–Friedman-style “weak” constructive extensional set theories and Aczel–Rathjen analogous constructive set theories both enriched by Mostowski-style collapsing axioms and/or related anti-foundation axioms. The main results include full intuitionistic conservations over the corresponding purely arithmetical formalisms that are well known in the reverse mathematics – which strengthens analogous results obtained by the author in the 80s. The present research was inspired by the more recent Sato-style “weak weak” classical extensional (...) set theories whose proof theoretic strengths are shown to strongly exceed the ones of the intuitionistic counterparts in the presence of the collapsing axioms. (shrink)

The Suslin operator is a type-2 functional testing for the well-foundedness of binary relations on the natural numbers. In the context of applicative theories, its proof-theoretic strength has been analyzed in Jäger and Strahm [18]. This article provides a more direct approach to the computation of the upper bounds in question. Several theories featuring the Suslin operator are embedded into ordinal theories tailored for dealing with non-monotone inductive definitions that enable a smooth definition of the application relation.

We use model-theoretic methods described in [3] to obtain ordinal analyses of a number of theories of first-and second-order arithmetic, whose proof-theoretic ordinals are less than or equal to $\Gamma_0$.

We use model-theoretic methods described in [3] to obtain ordinal analyses of a number of theories of first- and second-order arithmetic, whose proof-theoretic ordinals are less than or equal to Γ0.

One objective of this paper is the determination of the proof-theoretic strength of Martin-Löf's type theory with a universe and the type of well-founded trees. It is shown that this type system comprehends the consistency of a rather strong classical subsystem of second order arithmetic, namely the one with Δ 2 1 comprehension and bar induction. As Martin-Löf intended to formulate a system of constructive (intuitionistic) mathematics that has a sound philosophical basis, this yields a constructive consistency (...) proof of a strong classical theory. Also the proof-theoretic strength of other inductive types like Aczel's type of iterative sets is investigated in various contexts.Further, we study metamathematical relations between type theories and other frameworks for formalizing constructive mathematics, e.g. Aczel's set theories and theories of operations and classes as developed by Feferman. (shrink)

We study the proof-theoretic strength and effective content of the infinite form of Ramsey's theorem for pairs. Let RT n k denote Ramsey's theorem for k-colorings of n-element sets, and let RT $^n_{ denote (∀ k)RT n k . Our main result on computability is: For any n ≥ 2 and any computable (recursive) k-coloring of the n-element sets of natural numbers, there is an infinite homogeneous set X with X'' ≤ T 0 (n) . Let IΣ (...) n and BΣ n denote the Σ n induction and bounding schemes, respectively. Adapting the case n = 2 of the above result (where X is low 2 ) to models of arithmetic enables us to show that RCA 0 + IΣ 2 + RT 2 2 is conservative over RCA 0 + IΣ 2 for Π 1 1 statements and that $RCA_0 + I\Sigma_3 + RT^2_{ , is Π 1 1 -conservative over RCA 0 + IΣ 3 . It follows that RCA 0 + RT 2 2 does not imply BΣ 3 . In contrast, J. Hirst showed that $RCA_0 + RT^2_{ does imply BΣ 3 , and we include a proof of a slightly strengthened version of this result. It follows that $RT^2_{ is strictly stronger than RT 2 2 over RCA 0. (shrink)

We measure, in the presence of the axiom of infinity, the proof-theoretic strength of the axioms of set theory which make the theory look really like a “theory of sets”, namely, the axiom of extensionality Ext, separation axioms and the axiom of regularity Reg . We first introduce a weak weak set theory as a base over which to clarify the strength of these axioms. We then prove the following results about proof-theoretic ordinals:1. and (...) ,2. and . We also show that neither Reg nor affects the proof-theoretic strength, i.e., where T is Basic plus any combination of Ext and. (shrink)

We consider extensions of Peano arithmetic suitable for doing some of nonstandard analysis, in which there is a predicate N(x) for an elementary initial segment, along with axiom schemes approximating ω 1 -saturation. We prove that such systems have the same proof-theoretic strength as their natural analogues in second order arithmetic. We close by presenting an even stronger extension of Peano arithmetic, which is equivalent to ZF for arithmetic statements.

In their logical analysis of theorems about disjoint rays in graphs, Barnes, Shore, and the author (hereafter BGS) introduced a weak choice scheme in second-order arithmetic, called the $\Sigma ^1_1$ axiom of finite choice (hereafter finite choice). This is a special case of the $\Sigma ^1_1$ axiom of choice ( $\Sigma ^1_1\text {-}\mathsf {AC}_0$ ) introduced by Kreisel. BGS showed that $\Sigma ^1_1\text {-}\mathsf {AC}_0$ suffices for proving many of the aforementioned theorems in graph theory. While it is not known (...) if these implications reverse, BGS also showed that those theorems imply finite choice (in some cases, with additional induction assumptions). This motivated us to study the proof-theoretic strength of finite choice. Using a variant of Steel forcing with tagged trees, we show that finite choice is not provable from the $\Delta ^1_1$ -comprehension scheme (even over $\omega $ -models). We also show that finite choice is a consequence of the arithmetic Bolzano–Weierstrass theorem (introduced by Friedman and studied by Conidis), assuming $\Sigma ^1_1$ -induction. Our results were used by BGS to show that several theorems in graph theory cannot be proved using $\Delta ^1_1$ -comprehension. Our results also strengthen results of Conidis. (shrink)

In earlier work we introduced two systems for nonstandard analysis, one based on classical and one based on intuitionistic logic; these systems were conservative extensions of first-order Peano and Heyting arithmetic, respectively. In this paper we study how adding the principle of countable saturation to these systems affects their proof-theoretic strength. We will show that adding countable saturation to our intuitionistic system does not increase its proof-theoretic strength, while adding it to the classical system (...) increases the strength from first- to full second-order arithmetic. (shrink)

In this paper, we show that equation image is a equation image-conservative extension of BΣ1 + exp, thus it does not imply IΣ1.

Most axiomatizations of set theory that have been treated metamathematically have been based either entirely on classical logic or entirely on intuitionistic logic. But a natural conception of the settheoretic universe is as an indefinite (or “potential”) totality, to which intuitionistic logic is more appropriately applied, while each set is taken to be a definite (or “completed”) totality, for which classical logic is appropriate; so on that view, set theory should be axiomatized on some correspondingly mixed basis. Similarly, in the (...) case of predicative analysis, the natural numbers are considered to form a definite totality, while the universe of sets (or functions) of natural numbers are viewed as an indefinite totality, so that, again, a mixed semi-constructive logic should be the appropriate one to treat the two together. Various such semiconstructive systems of analysis and set theory are formulated here and their proof-theoretic strength is characterized. Interestingly, though the logic is weakened, one can in compensation strengthen certain principles in a way that could be advantageous for mathematical applications. (shrink)

Universes of types were introduced into constructive type theory by Martin-Löf [12]. The idea of forming universes in type theory is to introduce a universe as a set closed under a certain specified ensemble of set constructors, say $\mathcal{C}$ . The universe then “reflects” $\mathcal{C}$ .This is the first part of a paper which addresses the exact logical strength of a particular such universe construction, the so-called superuniverse due to Palmgren (cf. [16, 18, 19]).It is proved that Martin-Löf type (...) theory with a superuniverse, termed MLS, is a system whose proof-theoretic ordinal resides strictly above the Feferman-Schütte ordinal $\Gamma_0$ but well below the Bachmann-Howard ordinal. Not many theories of strength between $\Gamma_0$ and the Bachmann-Howard ordinal have arisen. MLS provides a natural example for such a theory. (shrink)

We define a class of functions, the descent recursive functions, relative to an arbitrary elementary recursive system of ordinal notations. By means of these functions, we provide a general technique for measuring the proof-theoretic strength of a variety of systems of first-order arithmetic. We characterize the provable well-orderings and provably recursive functions of these systems, and derive various conservation and equiconsistency results.

We interpret intuitionistic theories of (iterated) strictly positive inductive definitions (s.p.-ID i′ s) into Martin-Löf's type theory. The main purpose being to obtain lower bounds of the proof-theoretic strength of type theories furnished with means for transfinite induction (W-type, Aczel's set of iterative sets or recursion on (type) universes). Thes.p.-ID i′ s are essentially the wellknownID i -theories, studied in ordinal analysis of fragments of second order arithmetic, but the set variable in the operator form is restricted (...) to occur only strictly positively. The modelling is done by constructivizing continuity notions for set operators at higher number classes and proving that strictly positive set operators are continuous in this sense. The existence of least fixed points, or more accurately, least sets closed under the operator, then easily follows. (shrink)

We present well-ordering proofs for Martin-Löf's type theory with W-type and one universe. These proofs, together with an embedding of the type theory in a set theoretical system as carried out in Setzer show that the proof theoretical strength of the type theory is precisely ψΩ1Ω1 + ω, which is slightly more than the strength of Feferman's theory T0, classical set theory KPI and the subsystem of analysis + . The strength of intensional and extensional version, (...) of the version à la Tarski and à la Russell are shown to be the same. (shrink)

Universes of types were introduced into constructive type theory by Martin-Löf [3]. The idea of forming universes in type theory is to introduce a universe as a set closed under a certain specified ensemble of set constructors, say ?. The universe then “reflects”?.This is the second part of a paper which addresses the exact logical strength of a particular such universe construction, the so-called superuniverse due to Palmgren (cf.[4–6]).It is proved that Martin-Löf type theory with a superuniverse, termed MLS, (...) is a system whose proof-theoretic ordinal resides strictly above the Feferman-Schütte ordinal Γ0 but well below the Bachmann-Howard ordinal. Not many theories of strength between Γ0 and the Bachmann-Howard ordinal have arisen. MLS provides a natural example for such a theory. In this second part of the paper the concern is with the with upper bounds. (shrink)

This paper is a companion to work of Feferman, Jäger, Glaß, and Strahm on the proof theory of the type two functionals μ and E1 in the context of Feferman-style applicative theories. In contrast to the previous work, we analyze these two functionals in the context of Schlüter's weakened applicative basis PRON which allows for an interpretation in the primitive recursive indices. The proof-theoretic strength of PRON augmented by μ and E1 is measured in terms of (...) the two subsystems of second order arithmetic, Π10-CA and Π11-CA, respectively. (shrink)

In comparing classical and non-classical solutions to the semantic paradoxes arguments relying on strength have been influential. In this paper I argue that non-classical solutions should preserve the proof-theoretic strength of classical solutions. Leitgeb’s logic of HYPE is then presented as an interesting possibility to strengthen FDE with a suitable conditional. It is shown that HYPE allows for a non-classical Kripkean theory of truth, called KFL, that is strong enough for the relevant purposes and has additional (...) attractive properties. (shrink)

We prove that a nonstandard extension of arithmetic is effectively conservative over Peano arithmetic by using an internal version of a definable ultrapower. By the same method we show that a certain extension of the nonstandard theory with a saturation principle has the same proof-theoretic strength as second order arithmetic, where comprehension is restricted to arithmetical formulas.

Saunders Mac Lane has drawn attention many times, particularly in his book Mathematics: Form and Function, to the system of set theory of which the axioms are Extensionality, Null Set, Pairing, Union, Infinity, Power Set, Restricted Separation, Foundation, and Choice, to which system, afforced by the principle, , of Transitive Containment, we shall refer as . His system is naturally related to systems derived from topos-theoretic notions concerning the category of sets, and is, as Mac Lane emphasises, one that (...) is adequate for much of mathematics. In this paper we show that the consistency strength of Mac Lane's system is not increased by adding the axioms of Kripke–Platek set theory and even the Axiom of Constructibility to Mac Lane's axioms; our method requires a close study of Axiom H, which was proposed by Mitchell; we digress to apply these methods to subsystems of Zermelo set theory , and obtain an apparently new proof that is not finitely axiomatisable; we study Friedman's strengthening of , and the Forster–Kaye subsystem of , and use forcing over ill-founded models and forcing to establish independence results concerning and ; we show, again using ill-founded models, that proves the consistency of ; turning to systems that are type-theoretic in spirit or in fact, we show by arguments of Coret and Boffa that proves a weak form of Stratified Collection, and that is a conservative extension of for stratified sentences, from which we deduce that proves a strong stratified version of ; we analyse the known equiconsistency of with the simple theory of types and give Lake's proof that an instance of Mathematical Induction is unprovable in Mac Lane's system; we study a simple set theoretic assertion—namely that there exists an infinite set of infinite sets, no two of which have the same cardinal—and use it to establish the failure of the full schema of Stratified Collection in ; and we determine the point of failure of various other schemata in . The paper closes with some philosophical remarks. (shrink)

This paper contributes to the theory of hybrid substructural logics, i.e. weak logics given by a Gentzen-style proof theory in which there is only a limited possibility to use structural rules. Following the literature, we use an operator to mark formulas to which the extra structural rules may be applied. New in our approach is that we do not see this ▽ as a modality, but rather as the meet of the marked formula with a special type Q. In (...) this way we can make the specific structural behaviour of marked formulas more explicit. The main motivation for our approach is that we can provide a nice, intuitive semantics for hybrid substructural logics. Soundness and completeness for this semantics are proved; besides this we consider some proof-theoretical aspects like cut-elimination and embeddings of the 'strong' system in the hybrid one. (shrink)

This paper deals with: (i) the theory ID # 1 which results from $\widehat{\mathrm{ID}}_1$ by restricting induction on the natural numbers to formulas which are positive in the fixed point constants, (ii) the theory BON(μ) plus various forms of positive induction, and (iii) a subtheory of Peano arithmetic with ordinals in which induction on the natural numbers is restricted to formulas which are Σ in the ordinals. We show that these systems have proof-theoretic strength φω 0.

This paper contributes to the theory of hybrid substructural logics, i.e. weak logics given by a Gentzen-style proof theory in which there is only alimited possibility to use structural rules. Following the literture, we use an operator to mark formulas to which the extra structural rules may be applied. New in our approach is that we do not see this as a modality, but rather as themeet of the marked formula with a special typeQ. In this way we can (...) make the specific structural behaviour of marked formulas more explicit.The main motivation for our approach is that we can provide a nice, intuitive semantics for hybrid substructural logics. Soundness and completeness for this semantics are proved; besides this we consider some proof-theoretical aspects like cut-elimination and embeddings of the strong system in the hybrid one. (shrink)

This paper deals with: (i) the theory $\mathrm{ID}^{\tt\#}_1$ which results from $\widehat{\mathrm{ID}}_1$ by restricting induction on the natural numbers to formulas which are positive in the fixed point constants, (ii) the theory $\mathrm{BON}(\mu)$ plus various forms of positive induction, and (iii) a subtheory of Peano arithmetic with ordinals in which induction on the natural numbers is restricted to formulas which are $\Sigma$ in the ordinals. We show that these systems have proof-theoretic strength $\varphi\omega 0$.

Let ≺ be a primitive recursive well-ordering on the natural numbers and assume that its order-type is greater than or equal to the proof-theoretic ordinal of the theory T. We show that the proof-theoretic strength of T is not increased if we add the negation of the statement which formalizes transfinite induction along ≺.

This book's activities highlight the important cycle of exploration, conjecture, and justification in all five mathematical strands. Students recognize patterns and make conjectures, learn the value of a counterexample, explore the strengths and weaknesses of visual proofs, discover the power of algebraic representations, and learn that theoretical approaches can substantiate empirical results. The supplemental CD-ROM features interactive electronic activities, master copies of activity pages for students, and additional readings for teachers. --publisher description.

The paper investigates inaccessible set axioms and their consistency strength in constructive set theory. In ZFC inaccessible sets are of the form Vκ where κ is a strongly inaccessible cardinal and Vκ denotes the κth level of the von Neumann hierarchy. Inaccessible sets figure prominently in category theory as Grothendieck universes and are related to universes in type theory. The objective of this paper is to show that the consistency strength of inaccessible set axioms heavily depend on the (...) context in which they are embedded. The context here will be the theory CZF− of constructive Zermelo–Fraenkel set theory but without -Induction . Let INAC be the statement that for every set there is an inaccessible set containing it. CZF−+INAC is a mathematically rich theory in which one can easily formalize Bishop style constructive mathematics and a great deal of category theory. CZF−+INAC also has a realizability interpretation in type theory which gives its theorems a direct computational meaning. The main result presented here is that the proof theoretic ordinal of CZF−+INAC is a small ordinal known as the Feferman–Schütte ordinal Γ0. (shrink)

While non-classical theories of truth that take truth to be transparent have some obvious advantages over any classical theory that evidently must take it as non-transparent, several authors have recently argued that there's also a big disadvantage of non-classical theories as compared to their “external” classical counterparts: proof-theoretic strength. While conceding the relevance of this, the paper argues that there is a natural way to beef up extant internal theories so as to remove their proof-theoretic (...) disadvantage. It is suggested that the resulting internal theories should seem preferable to their external counterparts. (shrink)

Let be the basic set theory that consists of the axioms of extensionality, emptyset, pair, union, powerset, infinity, transitive containment, Δ0‐separation and set foundation. This paper studies the relative strength of set theories obtained by adding fragments of the set‐theoretic collection scheme to. We focus on two common parameterisations of the collection: ‐collection, which is the usual collection scheme restricted to ‐formulae, and strong ‐collection, which is equivalent to ‐collection plus ‐separation. The main result of this paper shows (...) that for all, proves that there exists a transitive model of Zermelo Set Theory plus ‐collection, the theory is ‐conservative over the theory. It is also shown that (2) holds for when the Axiom of Choice is included in the base theory. The final section indicates how the proofs of (1) and (2) can be modified to obtain analogues of these results for theories obtained by adding fragments of collection to a base theory (Kripke‐Platek Set Theory with Infinity plus ) that does not include the powerset axiom. (shrink)

Determinacy axioms state the existence of winning strategies for infinite games played by two players on natural numbers. We show that a base theory enriched by a certain scheme of determinacy axioms is proof-theoretically equivalent to -comprehension.

In this dissertation, we shall investigate whether Tennant's criterion for paradoxicality(TCP) can be a correct criterion for genuine paradoxes and whether the requirement of a normal derivation(RND) can be a proof-theoretic solution to the paradoxes. Tennant’s criterion has two types of counterexamples. The one is a case which raises the problem of overgeneration that TCP makes a paradoxical derivation non-paradoxical. The other is one which generates the problem of undergeneration that TCP renders a non-paradoxical derivation paradoxical. Chapter 2 (...) deals with the problem of undergeneration and Chapter 3 concerns the problem of overgeneration. Chapter 2 discusses that Tenant’s diagnosis of the counterexample which applies CR−rule and causes the undergeneration problem is not correct and presents a solution to the problem of undergeneration. Chapter 3 argues that Tennant’s diagnosis of the counterexample raising the overgeneration problem is wrong and provides a solution to the problem. Finally, Chapter 4 addresses what should be explicated in order for RND to be a proof-theoretic solution to the paradoxes. (shrink)

The paper presents a proof-theoretic semantics (PTS) for a fragment of natural language, providing an alternative to the traditional model-theoretic (Montagovian) semantics (MTS), whereby meanings are truth-condition (in arbitrary models). Instead, meanings are taken as derivability-conditions in a dedicated natural-deduction (ND) proof-system. This semantics is effective (algorithmically decidable), adhering to the meaning as use paradigm, not suffering from several of the criticisms formulated by philosophers of language against MTS as a theory of meaning. In particular, Dummett’s (...) manifestation argument does not obtain, and assertions are always warranted, having grounds of assertion. The proof system is shown to satisfy Dummett’s harmony property, justifying the ND rules as meaning conferring. The semantics is suitable for incorporation into computational linguistics grammars, formulated in type-logical grammar. (shrink)

This paper discusses proof-theoretic semantics, the project of specifying the meanings of the logical constants in terms of rules of inference governing them. I concentrate on Michael Dummett’s and Dag Prawitz’ philosophical motivations and give precise characterisations of the crucial notions of harmony and stability, placed in the context of proving normalisation results in systems of natural deduction. I point out a problem for defining the meaning of negation in this framework and prospects for an account of the (...) meanings of modal operators in terms of rules of inference. (shrink)

One of the basic question we can ask about truth in a formal setting is what, if anything, we gain when we have a truth predicate at disposal. For example, does the expressive power of a language change or does the proof strength of a theory increase? Satisfaction classes are often described as complicated model theoretic constructions unable to give useful information toward the notion of truth from a general point of view. Their import is narrowed to (...) a dimension of pure technical utility and curiosity. Here I offer an application of satisfaction classes in order to show that they can have a relevant role in confronting proof theoretical equivalent theories of truth. (shrink)

In this paper we show how Dummett-Prawitz-style proof-theoretic semantics has to be modified in order to cope with paradoxical phenomena. It will turn out that one of its basic tenets has to be given up, namely the definition of the correctness of an inference as validity preservation. As a result, the notions of an argument being valid and of an argument being constituted by correct inference rules will no more coincide. The gap between the two notions is accounted (...) for by introducing the distinction between sense and denotation in the proof-theoretic-semantic setting. (shrink)

The idea of proof-theoretic validity originated in the work of Gentzen, when he suggested that the meaning of each logical expression was encapsulated in its introduction-rules. The idea was developed by Prawitz and Dummett, but came under attack by Prior under the soubriquet 'analytic validity'. Logical truths and logical consequences are deemed analytically valid by virtue of following, in a way which the present chapter clarifies, from the meaning of the logical constants. But different logics are based on (...) different rules, confer different meanings and so validate different theorems and consequences, some of which are arguably not true or valid at all. It seems to follow that some analytic statements are in fact false. The moral is that we must be careful what rules we adopt and what meanings we use our rules to determine. (shrink)

From the point of view of proof-theoretic semantics, it is argued that the sequent calculus with introduction rules on the assertion and on the assumption side represents deductive reasoning more appropriately than natural deduction. In taking consequence to be conceptually prior to truth, it can cope with non-well-founded phenomena such as contradictory reasoning. The fact that, in its typed variant, the sequent calculus has an explicit and separable substitution schema in form of the cut rule, is seen as (...) a crucial advantage over natural deduction, where substitution is built into the general framework. (shrink)

Prawitz conjectured that proof-theoretic validity offers a semantics for intuitionistic logic. This conjecture has recently been proven false by Piecha and Schroeder-Heister. This article resolves one of the questions left open by this recent result by showing the extensional alignment of proof-theoretic validity and general inquisitive logic. General inquisitive logic is a generalisation of inquisitive semantics, a uniform semantics for questions and assertions. The paper further defines a notion of quasi-proof-theoretic validity by restricting (...) class='Hi'>proof-theoretic validity to allow double negation elimination for atomic formulas and proves the extensional alignment of quasi-proof-theoretic validity and inquisitive logic. (shrink)