Accretive and monotone operator theory are central branches of nonlinear functional analysis and constitute the abstract study of certain set-valued mappings between function spaces. This paper deals with the computational properties of these accretive and (generalized) monotone set-valued operators. In particular, we develop (and extend) for this field the theoretical framework of proof mining, a program in mathematical logic that seeks to extract computational information from prima facie “non-computational” proofs from the mainstream literature. To this end, we establish logical metatheorems (...) that guarantee and quantify the computational content of theorems pertaining to accretive and (generalized) monotone set-valued operators. On the one hand, our results unify a number of recent case studies, while they also provide characterizations of central analytical notions in terms of proof theoretic ones on the other, which provides a crucial perspective on needed quantitative assumptions in future applications of proof mining to these branches. (shrink)

We adapt a continuous logic axiomatization of tracial von Neumann algebras due to Farah, Hart and Sherman in order to prove a metatheorem for this class of structures in the style of proof mining, a research programme that aims to obtain the hidden computational content of ordinary mathematical proofs using tools from proof theory.

Contrary to common misconceptions, today's logic is not devoid of existential import: the universalized conditional ∀ x [S→ P] implies its corresponding existentialized conjunction ∃ x [S & P], not in all cases, but in some. We characterize the proexamples by proving the Existential-Import Equivalence: The antecedent S of the universalized conditional alone determines whether the universalized conditional has existential import, i.e. whether it implies its corresponding existentialized conjunction.A predicate is an open formula having only x free. An existential-import predicate (...) Q is one whose existentialization, ∃ x Q, is logically true; otherwise, Q is existential-import-free or simply import-free.How abundant or widespread is existential import? How abundant or widespread are existential-import predicates in themselves or in comparison to import-free predicates? We show that existential-import predicates are quite abundant, and no less so than import-free predicates. Existential.. (shrink)

This chapter is devoted to the excruciating drudgery of a logical monk actually doing the work that a logical saint would find unnecessary, to establish the metatheorem which states that for all _n_, and for all substituends for Φ, one has _ ∇ n x Φ x ⊣ ⊢ ⋄ n x Φ x. Note that although for any particular n_ one can effectively find the requisite proofs in monadic first-order logic, the proof of the metatheorem itself, because (...) of its general form, does not proceed within monadic first-order logic. An important philosophical corollary of this metatheorem is that no ordering of the Φ s—be it one intrinsic to them, or imposed upon them arbitrarily in the act of counting—can possibly figure into the truth-conditions of numerosity statements to the effect that ‘there are exactly this-many Φ s’. (shrink)

This chapter provides further argument justifying the claim that our use of finite dependency networks entails no loss at all of theoretical generality, as far as belief revision on the part of rational creatures is concerned. Some basic concepts in mathematical logic are defined, to lay the groundwork for the metatheorem, due to Harvey Friedman, that is proved in the next chapter.

A general metatheorem is proved which reduces a wide class of statements about continuous time stochastic processes to statements about discrete time processes. We introduce a strong language for stochastic processes, and a concept of forcing for sequences of discrete time processes. The main theorem states that a sentence in the language is true if and only if it is forced. Although the stochastic process case is emphasized in order to motivate the results, they apply to a wider class (...) of random variables. At the end of the paper we illustrate how the theorem can be used with three applications involving submartingales. (shrink)

This paper presents a metatheorem with the following property: Given a proven axiom-free lemma, which interrelates some of the elementary properties of a binary relation, the metatheorem mechanically transforms this lemma into its uniquely corresponding complementary lemma. Therefore, the metatheorem nearly doubles our knowledge about the elementary properties of binary relations, for application to statistical decision theory. At present we do not know whether there exists a nontrivial axiom-free lemma that is its own complementary lemma.

In this chapter we will introduce Classical Logic, from both a valuational and a proof-theoretical point of view. We will start by defining some basic tools pertaining to both these frameworks, in a general fashion, so they will be useful for subsequent chapters too. Then, we will present Classical inferential Logic, through the sequent calculus LK and boolean bivaluations. We will then prove various metatheorical results about them, such as Soundness and Completeness, Compactness and Decidability. In the second half of (...) the chapter, we will tackle the metainferential side, presenting different concepts of metainferential validity—both semantical and proof-theoretical. We will also show some metainferential versions of the metatheorems previously proved for the inferential part. We end the chapter by proving Cut-elimination and discussing some of its consequences. (shrink)

Despite the renown of ‘On Denoting’, much criticism has ignored or misconstrued Russell's treatment of scope, particularly in intensional, but also in extensional contexts. This has been rectified by more recent commentators, yet it remains largely unnoticed that the examples Russell gives of scope distinctions are questionable or inconsistent with his own philosophy. Nevertheless, Russell is right: scope does matter in intensional contexts. In Principia Mathematica, Russell proves a metatheorem to the effect that the scope of a single occurrence (...) of a description in an extensional context does not matter, provided existence and uniqueness conditions are satisfied. But attempts to eliminate descriptions in more complicated cases may produce an analysis with more occurrences of descriptions than featured in the analysand. Taking alternation and negation to be primitive (as in the first edition of Principia), this can be resolved, although the proof is non-trivial. Taking the Sheffer stroke to be primitive (as proposed by Russell in the second edition), with bad choices of scope the analysis fails to terminate. (shrink)

Reality presents to us in multiple forms, as a layered pyramid. Physics is the foundation, and should be made as solid and complete as possible. More organized levels stand on this fundamental level—chemistry, biology, psychology, social sciences etc. Suppose we will find the unified theory of the fundamental physical laws. Will we then be able to deduce the higher levels, or they have their own life, not completely depending on the foundations? At the higher levels we see goals, life, and (...) even consciousness, which seem to be more than mere constructs of the fundamental constituents. Are all these high level structures completely reducible to the basis, or by contrary, they affect in turn the lower levels? Are mathematics and logic enough to solve these puzzles? Are there questions that objective science cannot even define rigorously? Why is there something rather than nothing? What is the world made of? What is consciousness?. (shrink)

This work makes available to readers without specialized training in mathematics complete proofs of the fundamental metatheorems of standard (i.e., basically ...

The history of the search for a minimal set of inference rules for syllogistic reasoning starts with Aristotle, with one of the metatheorems proved in Prior Analytics stating that all syllogistic deductions are ultimately reducible to two universal moods in the first figure: Barbara and Celarent. In the present work, we will consider what is the greatest reduction one can achieve when proving all the moods indirectly. The question we shall answer is whether, when proved indirectly, syllogisms behave the same (...) way and, consequently, whether the Aristotelian reduction to Barbara and Celarent holds for indirect proofs as well. To achieve this, we shall consider four different scenarios of applying single-premise inference rules to syllogism. The results for each scenario will then be analyzed and displayed as tables. Considering the tables, we shall claim that in certain cases, the Aristotelian reduction does not hold and further propose our division of all the syllogistic moods, which will be different from the usual figure arrangement. Finally, we will analyze the results quantitatively and show that they can provide insight into the nature of the division to regular and the so-called subalternated moods. (shrink)

We discuss a `negative' way of defining frame classes in (multi)modal logic, and address the question of whether these classes can be axiomatized by derivation rules, the `non-ξ rules', styled after Gabbay's Irreflexivity Rule. The main result of this paper is a metatheorem on completeness, of the following kind: If Λ is a derivation system having a set of axioms that are special Sahlqvist formulas and Λ+ is the extension of Λ with a set of non-ξ rules, then Λ+ (...) is strongly sound and complete with respect to the class of frames determined by the axioms and the rules. (shrink)

In this paper we study a new approach to classify mathematical theorems according to their computational content. Basically, we are asking the question which theorems can be continuously or computably transferred into each other? For this purpose theorems are considered via their realizers which are operations with certain input and output data. The technical tool to express continuous or computable relations between such operations is Weihrauch reducibility and the partially ordered degree structure induced by it. We have identified certain choice (...) principles such as co-finite choice, discrete choice, interval choice, compact choice and closed choice, which are cornerstones among Weihrauch degrees and it turns out that certain core theorems in analysis can be classified naturally in this structure. In particular, we study theorems such as the Intermediate Value Theorem, the Baire Category Theorem, the Banach Inverse Mapping Theorem, the Closed Graph Theorem and the Uniform Boundedness Theorem. We also explore how existing classifications of the Hahn—Banach Theorem and Weak Kőnig's Lemma fit into this picture. Well-known omniscience principles from constructive mathematics such as LPO and LLPO can also naturally be considered as Weihrauch degrees and they play an important role in our classification. Based on this we compare the results of our classification with existing classifications in constructive and reverse mathematics and we claim that in a certain sense our classification is finer and sheds some new light on the computational content of the respective theorems. Our classification scheme does not require any particular logical framework or axiomatic setting, but it can be carried out in the framework of classical mathematics using tools of topology, computability theory and computable analysis. We develop a number of separation techniques based on a new parallelization principle, on certain invariance properties of Weihrauch reducibility, on the Low Basis Theorem of Jockusch and Soare and based on the Baire Category Theorem. Finally, we present a number of metatheorems that allow to derive upper bounds for the classification of the Weihrauch degree of many theorems and we discuss the Brouwer Fixed Point Theorem as an example. (shrink)

Since McCall (1966), the heterodox principle of propositional logic that it is impossible for a proposition to be entailed by its own negation—in symbols, ¬(¬φ→φ)—has gone by the name of Aristotle’s thesis, since Aristotle apparently endorses it in Prior Analytics 2.4, 57b3–14. Scholars have contested whether Aristotle did endorse his eponymous thesis, whether he could do so consistently, and for what purpose he endorsed it if he did. In this article, I reconstruct Aristotle’s argument from this passage and show that (...) he accepts this thesis. Further, I show that the argument he gives is, making plausible assumptions, a correct proof in a consistent fragmentary nonclassical metalogic for a metatheorem he previously states concerning his assertoric syllogistic. In this way, Aristotle’s argument emerges as a fascinating case study in the use of a nonclassical metalogic to prove a result about a nonclassical object system. (shrink)

In this short paper I note that a key metatheorem does not hold for the bilateralist inferential framework: harmony does not entail consistency. I conclude that the requirement of harmony will not suffice for a bilateralist to maintain a proof theoretic account of classical logic. I conclude that a proof theoretic account of meaning based on the bilateralist framework has no natural way of distinguishing legitimate definitional inference rules from illegitimate ones (such as those for tonk). Finally, as an (...) appendix to the main argument, I propose an alternative non-bilateral formal solution to the problem of providing a proof-theoretic account of classical logic. (shrink)

Anyone seeking a readable and relatively brief guide to logic can do no better than this classic introduction. A treat for both the intellect and the imagination, it profiles the development of logic from ancient to modern times and compellingly examines the nature of logic and its philosophical implications. No prior knowledge of logic is necessary; readers need only an acquaintance with high school mathematics. The author emphasizes understanding, rather than technique, and focuses on such topics as the historical reasons (...) for the formation of Aristotelian logic, the rise of mathematical logic after more than 2,000 years of traditional logic, the nature of the formal axiomatic method and the reasons for its use, and the main results of metatheory and their philosophic import. The treatment of the Gödel metatheorems is especially detailed and clear, and answers to the problems appear at the end. (shrink)

Presburger's essay on the completeness and decidability of arithmetic with integer addition but without multiplication is a milestone in the history of mathematical logic and formal metatheory. The proof is constructive, using Tarski-style quantifier elimination and a four-part recursive comprehension principle for axiomatic consequence characterization. Presburger's proof for the completeness of first order arithmetic with identity and addition but without multiplication, in light of the restrictive formal metatheorems of Gödel, Church, and Rosser, takes the foundations of arithmetic in mathematical logic (...) to the limits of completeness and decidability. (shrink)

We examine the sense in which logic is a priori, and explain how mathematical theories can be dichotomized non-trivially into analytic and synthetic portions. We argue that Core Logic contains exactly the a-priori-because-analytically-valid deductive principles. We introduce the reader to Core Logic by explaining its relationship to other logical systems, and stating its rules of inference. Important metatheorems about Core Logic are reported, and its important features noted. Core Logic can serve as the basis for a foundational program that could (...) be called Natural Logicism, an exposition of which will build on the (meta)logical ideas explained here. (shrink)

We define a system IR of first-order intuitionistic relevant logic. We show that intuitionistic mathematics (on the assumption that it is consistent) can be relevantized, by virtue of the following metatheorem: any intuitionistic proof of A from a setX of premisses can be converted into a proof in IR of eitherA or absurdity from some subset ofX. Thus IR establishes the same inconsistencies and theorems as intuitionistic logic, and allows one to prove every intuitionistic consequence of any consistent set (...) of premisses. (shrink)

The papers presented in this volume examine topics of central interest in contemporary philosophy of logic. They include reflections on the nature of logic and its relevance for philosophy today, and explore in depth developments in informal logic and the relation of informal to symbolic logic, mathematical metatheory and the limiting metatheorems, modal logic, many-valued logic, relevance and paraconsistent logic, free logics, extensional v. intensional logics, the logic of fiction, epistemic logic, formal logical and semantic paradoxes, the concept of truth, (...) the formal theory of entailment, objectual and substitutional interpretation of the quantifiers, infinity and domain constraints, the Löwenheim-Skolem theorem and Skolem paradox, vagueness, modal realism v. actualism, counterfactuals and the logic of causation, applications of logic and mathematics to the physical sciences, logically possible worlds and counterpart semantics, and the legacy of Hilbert’s program and logicism. The handbook is meant to be both a compendium of new work in symbolic logic and an authoritative resource for students and researchers, a book to be consulted for specific information about recent developments in logic and to be read with pleasure for its technical acumen and philosophical insights. Key Features - Written by leading logicians and philosophers - Comprehensive authoritative coverage of all major areas of contemporary research in symbolic logic - Clear, in-depth expositions of technical detail - Progressive organization from general considerations to informal to symbolic logic to nonclassical logics - Presents current work in symbolic logic within a unified framework - Accessible to students, engaging for experts and professionals - Insightful philosophical discussions of all aspects of logic -Useful bibliographies in every chapter - Written by leading logicians and philosophers - Comprehensive authoritative coverage of all major areas of contemporary research in symbolic logic - Clear, in-depth expositions of technical detail - Progressive organization from general considerations to informal to symbolic logic to nonclassical logics - Presents current work in symbolic logic within a unified framework - Accessible to students, engaging for experts and professionals - Insightful philosophical discussions of all aspects of logic - Useful bibliographies in every chapter. (shrink)

In the paper, the authors discuss two kinds of consequence operations characterized axiomatically. The first one are consequence operations of the type Cn + that, in the intuitive sense, are infallible operations, always leading from accepted (true) sentences of a deductive system to accepted (true) sentences of the deductive system (see Tarski in Monatshefte für Mathematik und Physik 37:361–404, 1930, Comptes Rendus des Séances De la Société des Sciences et des Lettres de Varsovie 23:22–29, 1930; Pogorzelski and Słupecki in Stud (...) Logic 9:163–176, 1960, Stud Logic 10:77–95, 1960). The second kind are dual consequence operations of the type Cn − that can be regarded as anti-infallible operations leading from non-accepted (rejected, false) sentences of a deductive system to non-accepted (rejected, false) sentences of the system (see Słupecki in Funkcja Łukasiewicza, 33–40, 1959; Wybraniec-Skardowska in Teoria zdań odrzuconych, 5–131, Zeszyty Naukowe Wyższej Szkoły Inżynierskiej w Opolu, Seria Matematyka 4(81):35–61, 1983, Ann Pure Appl Logic 127:243–266, 2004, in On the notion and function of rejected propositions, 179–202, 2005). The operations of the types Cn + and Cn − can be ordinary finitistic consequence operations or unit consequence operations. A deductive system can be characterized in two ways by the following triple: $$\begin{array}{ll}{\rm by\,the\,triple}:\hspace{1.4cm} (+ , -)\hspace{0,6cm} \\ {\rm or\,by\,the\,triple}:\hspace{1.0cm} (-, +)\hspace{0,6cm} .\end{array}$$ We compare axiom systems for operations of the types Cn + and Cn −, give some methodological properties of deductive systems defined by means of these operations (e.g. consistency, completeness, decidability in Łukasiewicz’s sense), as well as formulate different metatheorems concerning them. (shrink)

The present article provides an analysis of the existing proof systems for dynamic epistemic logic from the viewpoint of proof-theoretic semantics. Dynamic epistemic logic is one of the best known members of a family of logical systems that have been successfully applied to diverse scientific disciplines, but the proof-theoretic treatment of which presents many difficulties. After an illustration of the proof-theoretic semantic principles most relevant to the treatment of logical connectives, we turn to illustrating the main features of display calculi, (...) a proof-theoretic paradigm that has been successfully employed to give a proof-theoretic semantic account of modal and substructural logics. Then, we review some of the most significant proposals of proof systems for dynamic epistemic logics, and we critically reflect on them in the light of the previously introduced proof-theoretic semantic principles. The contributions of the present article include a generalization of Belnap's cut-elimination metatheorem for display calculi, and a revised version of the display-style calculus D.EAK. We verify that the revised version satisfies the previously mentioned proof-theoretic semantic principles, and show that it enjoys cut-elimination as a consequence of the generalized metatheorem. (shrink)

We provide sufficient conditions for the existence of a conservative translation from a consequence system to another one. We analyze the problem in many settings, namely when the consequence systems are generated by a deductive calculus or by a logic system including both proof-theoretic and model-theoretic components. We also discuss reflection of several metaproperties with the objective of showing that conservative translations provide an alternative to proving such properties from scratch. We discuss soundness and completeness, disjunction property and metatheorem (...) of deduction among others. We provide several illustrations of conservative translations. (shrink)

In his preface, Hunter explains that this volume is intended to provide for non-mathematicians an introduction to the most important results of modern mathematical logic. The reader will find here the work of Post, Skolem, Gödel, Church, Henkin, and others, presented in a terse and closely-knit style. Though acknowledging the trend toward natural deduction systems, Hunter sticks to more classical axiomatic systems on the grounds that the proofs of metatheorems are simplified by that choice. He begins with a formal system (...) of propositional logic, for which he develops proofs of completeness, consistency, and decidability. Systems of first order predicate logic are then dealt with, and Church's and Gödel's results on undecidability and incompleteness are presented. There is a brief, useful discussion indicating what parts of first order predicate logic are decidable. It is assumed that the reader has some familiarity with elementary formal logic: Hunter develops the set-theoretical results he requires. The compactness of the presentation is facilitated by the use of earlier results for propositional logic to obtain certain results for predicate logic. Especially helpful is Hunter's technique of prefacing each of the longer and more difficult proofs with a section explaining the key ideas and the general method of proof; summaries are also often provided in conclusion. Because of the orientation of the book, a more extensive discussion of the significance of the results obtained and the philosophical issues which have been raised concerning some of them, would have been welcome. Nonetheless, this is a good, concise introduction for those who are not yet prepared to tackle the more technical literature. A bibliography is provided for those interested in pursuing the subject in greater detail.--E. M. F. (shrink)

We obtain an equivalent implicit characterization of Lp Banach spaces that is amenable to a logical treatment. Using that, we obtain an axiomatization for such spaces into a higher order logical system, the kind of which is used in proof mining, a research program that aims to obtain the hidden computational content of mathematical proofs using tools from mathematical logic. As an aside, we obtain a concrete way of formalizing Lp spaces in positive-bounded logic. The axiomatization is followed by a (...) corresponding metatheorem in the style of proof mining. We illustrate its use with the derivation for this class of spaces of the standard modulus of uniform convexity. (shrink)

In this article I am going to argue for the possibility of a transcendental source of logic based on a phenomenologically motivated approach. My aim will be essentially carried out in two succeeding steps of reduction: the first one will be the indication of existence of an inherent temporal factor conditioning formal predicative discourse and the second one, based on a supplementary reduction of objective temporality, will be a recourse to a time-constituting origin which has to be assumed as a (...) non-temporal, transcendental subjectivity and for that reason as possibly the ultimate transcendental root of pure logic. In the development of the argumentation and taking into account W.V. Quine’s views in his well-known Word and Object, a special emphasis will be given to the fundamentally temporal character of universal and existential predicative forms, to their status in logical theories in general, and to their underlying role in generating an inherently non-finitistic character reflected, for instance, in the undecidability of certain infinity statements in formal mathematical theories. This is shown also to concern metatheorems of such vital importance as Gödel’s incompleteness theorems in mathematical foundations. Moreover in the course of the discussion the quest for the ultimate limits of predication will lead to the notions of separation and intentional correlation between an ‘observing’ subject and the object of ‘observation’ as well as to the notion of syntactical individuals taken as the irreducible non-analytic nuclei-forms within analytical discourse. (shrink)

In [U. Kohlenbach, Some logical metatheorems with applications in functional analysis, Trans. Amer. Math. Soc. 357 89–128], the second author obtained metatheorems for the extraction of effective bounds from classical, prima facie non-constructive proofs in functional analysis. These metatheorems for the first time cover general classes of structures like arbitrary metric, hyperbolic, CAT and normed linear spaces and guarantee the independence of the bounds from parameters ranging over metrically bounded spaces. Recently ]), the authors obtained generalizations of these metatheorems which (...) allow one to prove similar uniformities even for unbounded spaces as long as certain local boundedness conditions are satisfied. The use of classical logic imposes some severe restrictions on the formulas and proofs for which the extraction can be carried out. In this paper we consider similar metatheorems for semi-intuitionistic proofs, i.e. proofs in an intuitionistic setting enriched with certain non-constructive principles. Contrary to the classical case, there are practically no restrictions on the logical complexity of theorems for which bounds can be extracted. Again, our metatheorems guarantee very general uniformities, even in cases where the existence of uniform bounds is not obtainable by straightforward functional analytic means. Already in the purely intuitionistic case, where the existence of effective bounds is implicit, the metatheorems allow one to derive uniformities that may not be obvious at all from a given constructive proof. Finally, we illustrate our main metatheorem by an example from metric fixed point theory. (shrink)

Starting in 2005, general logical metatheorems have been developed that guarantee the extractability of uniform effective bounds from large classes of proofs of theorems that involve abstract metric structures X. In this paper we adapt this to the class of CAT\)-spaces X for \ and establish a new metatheorem that explains specific bound extractions that recently have been achieved in this context as instances of a general logical phenomenon.

The automatic verification of large parts of mathematics has been an aim of many mathematicians from Leibniz to Hilbert. While Gödel's first incompleteness theorem showed that no computer program could automatically prove certain true theorems in mathematics, the advent of electronic computers and sophisticated software means in practice there are many quite effective systems for automated reasoning that can be used for checking mathematical proofs. This book describes the use of a computer program to check the proofs of several celebrated (...) theorems in metamathematics including those of Gödel and Church-Rosser. The computer verification using the Boyer-Moore theorem prover yields precise and rigorous proofs of these difficult theorems. It also demonstrates the range and power of automated proof checking technology. The mechanization of metamathematics itself has important implications for automated reasoning, because metatheorems can be applied as labor-saving devices to simplify proof construction. (shrink)

Discursive (or discussive) logic, D₂, introduced by Jaśkowski, is widely recognized as a first formal approach to paraconsistency. Jaśkowski applied a quite extraordinary technique at that time to describe his logic. He neither gave a set of the axiom schemata nor presented a direct semantics for D₂ but used a translation function to express his philosophical and logical intuitions. Discursive logic was defined by an interpretation in the language of S₅ of Lewis. The aim of this paper is to present (...) a modified system of the discursive logic that allows some of the weaker versions of Duns Scotus's thesis to be valid. The initial idea is to consider a different characteristic of the connective of negation. We introduce both a direct semantics and an axiomatization of the new system, prove the key metatheorems, and describe labeled tableaux for the system. (shrink)

In this paper we present a logic that determines when implications in a classical logic context express a relevant connection between antecedent and consequent. In contrast with logics in the relevance logic literature, we leave classical negation intact—in the sense that the law of non-contradiction can be used to obtain relevant implications, as long as there is a connection between antecedent and consequent. On the other hand, we give up the requirement that our theory of relevance should be able to (...) define a new standard of deduction. We present and argue for a list of requirements such a logical theory of classical relevance needs to meet and go on to formulate a system that respects each of these requirements. The presented system is a Tarski logic that extends the relevance logic R with a new relevant implication which allows for Disjunctive Syllogism and similar rules. This is achieved by interpreting the logical symbols in the antecedents in a stronger way than the logical symbols in consequents. A proof theory and an algebraic semantics are formulated and interesting metatheorems are proven. Finally we give a philosophical motivation for our non-standard relevant implication and the asymmetric interpretation of antecedents and consequents. (shrink)

From early work of N. Goodman to recent approaches by H. Field and D. Lewis, there have been attempts to combine 2nd order languages with calculi of individuals. This paper is a contribution, containing basic definitions and distinctions and some metatheorems, to the development of a general metatheory of such theories.

This article offers an omissive critique of integral theory. To this objective, the article draws upon dialectical logic to investigate the affinities between integral theory and critical realism. Section 1 identifies new possibilities regarding the role of metatheory in practice by unpacking the metatheoretical coordinates of critical realism and integral theory. After providing a brief history of the origins of critical realism and integral theory, I review the ontological, epistemological, and methodological metatheorems of dialectical critical realism, and I put them (...) to work to provide an omissive critique of integral theory. Then I introduce the notion of strictly non-dialectic because it functions to explain formally how integral theory relates to critical realism. Section 2 isolates the inadequacies at every moment in the passage from the MELD dialectic. Section 3 concludes the article with a discussion of the implications of foregrounding a critical realist ontology for integral theory. (shrink)

This thesis is concerned with extending the underlying logical approach as well as the breadth of applications of the proof mining program to various (mostly previously untreated) areas of nonlinear analysis and optimization, with a particular focus being placed on topics which involve set-valued operators.For this, we extend the current logical methodology of proof mining by new systems and corresponding so-called logical metatheorems that cover these more involved areas of nonlinear analysis. Most of these systems crucially rely on the use (...) of intensional methods, treating sets with potentially high quantifier complexity in the defining matrix via characteristic functions and axioms that describe only their properties and do not completely characterize the elements of the sets.The applicability of all of these metatheorems is then substantiated by a range of case studies for the respective areas which in particular also highlight the naturalness of the use of intensional methods in the design of the corresponding systems.The first new area covered thereby is the theory of nonlinear semigroups induced by corresponding evolution equations for accretive operators. In that context, we present (besides an initial foray into the area from 2015) essentially the first applications of proof mining to the theory of partial differential equations. Concretely, we provide quantitative versions of four central results on the asymptotic behavior of solutions to such equations.The second new area unlocked in this thesis is that of the continuous dual of a Banach space and its norm (which are also approached via intensional methods). This in particular relies on a proof-theoretically tame treatment of suprema over (certain) bounded sets in this intensional context which is further exploited later on. These systems, which give access to this until now untreated fundamental notion from functional analysis, are then used to provide further substantial extensions to treat various notions from convex analysis like the Fréchet derivative of a convex function, Fenchel conjugates, Bregman distances, and monotone operators on Banach spaces in the sense of Browder.These systems are then utilized to provide applications in the context of Picard- and Halpern-style iterations of so-called Bregman strongly nonexpansive mappings where we provide both new quantitative and qualitative results.Lastly, we discuss the key notion of extensionality of a set-valued operator and its relation to set-theoretic maximality principles in more depth (which was already singled out—to some degree—in previous work). We thereby exhibit an issue arising with treating full extensionality in the context of these intensional approaches to set-valued operators and present useful fragments of the full extensionality statement where these issues are avoided.Corresponding to these fragments, we discuss a range of uniform continuity statements for set-valued operators beyond the usual notion involving the Hausdorff-metric. In particular, in that context, we utilize the previous tame treatment of suprema over bounded sets to also provide the first proof-theoretic treatment of that Hausdorff-metric in the context of systems for proof mining.The applicability of this treatment of the Hausdorff-metric is then in particular substantiated by a last case study where we provide quantitative information for a Mann-type iteration of set-valued mappings which are nonexpansive w.r.t. the Hausdorff-metric.The abstract was taken directly from the thesis.Abstract prepared by Nicholas Pischke, Technische Universität Darmstadt, Darmstadt, GermanyE-mail: [email protected]: https://doi.org/10.26083/tuprints-00026584. (shrink)

What has been learned about logic by means of "uninterpreted" logistic systems can be supplemented by comparing the latter with systems which are more uninterpreted, as well as with others which are less uninterpreted than the well-known logistic systems. By somewhat extending the meaning of 'uninterpreted', I hope to establish certain claims about the nature of logistic systems and also to cast some light on the nature of "logic itself." My procedure involves looking at three major "degrees" of interpretation: first, (...) systems uninterpreted both semantically and syntactically, second, systems uninterpreted semantically but not syntactically, and third, systems uninterpreted neither semantically nor syntactically. We shall be forced to limit ourselves to the truth-functional part of logic in this brief study. What are usually called uninterpreted systems can be seen on a continuum of "degrees" of interpretation, from ordinary reasoning at one extreme to a "thoroughly uninterpreted system" at the other. "Logic itself" apparently lies nearer to the interpreted, deformalized end of the spectrum than to the uninterpreted, formalized end. Logic is not identical with any particular logistic system, but is that which the particular logistic systems aim to formalize or model or capture. I propose that it is that minimum set of logical, rather than syntactical, primitive terms, definitions, and rules which is needed to generate logically, rather than syntactically, the principles of ordinary reasoning as it is used by logicians in their metalinguistic discussions and informal proofs of metatheorems. This minimum set is somewhat larger than the primitive bases of most logistic systems; its truth-functional part is presented in the "Deformalized Logic" at degree twelve. (shrink)

In recent years, proof theoretic transformations that are based on extensions of monotone forms of Gödel’s famous functional interpretation have been used systematically to extract new content from proofs in abstract nonlinear analysis. This content consists both in effective quantitative bounds as well as in qualitative uniformity results. One of the main ineffective tools in abstract functional analysis is the use of sequential forms of weak compactness. As we recently verified, the sequential form of weak compactness for bounded closed and (...) convex subsets of an abstract Hilbert space can be carried out in suitable formal systems that are covered by existing metatheorems developed in the course of the proof mining program. In particular, it follows that the monotone functional interpretation of this weak compactness principle can be realized by a functional Ω∗ definable from bar recursion of lowest type. While a case study on the analysis of strong convergence results that are based on weak compactness indicates that the use of the latter seems to be eliminable, things apparently are different for weak convergence theorems such as the famous Baillon nonlinear ergodic theorem. For this theorem we recently extracted an explicit bound on a metastable version of this theorem that is primitive recursive relative to Ω∗.In the current paper we for the first time give the construction of Ω∗ . As a corollary to the fine analysis of the use of bar recursion in this construction we obtain that Ω∗ elevates arguments in Tn at most to resulting functionals in Tn+2 . In particular, one can conclude from this that our bound on Baillon’s theorem is at least definable in T4. (shrink)

In Prior’s [4], Appendix A §4 and §5, and Chapter IV, and more explicitly in Bull’s [2], we find sequences of tense-logical systems which place increasingly more restrictive conditions on the temporal relation “… is before …”. We give here a simple, diagrammatic account of the way in which the successive postulates for temporal order place these conditions on the temporal relation: we do not provide any essentially new semantics for these systems, nor do we prove any rigorous metatheorems. We (...) do, however, quite often assume the completeness results of Lemmon, Bull and others without explicit mention. (shrink)

The purpose of this paper is to justify the claim that Topos theory and Logic (the latter interpreted in a wide enough sense to include Model theory and Set theory) may interact to the advantage of both fields. Once the necessity of utilizing toposes (other than the topos of Sets) becomes apparent, workers in Topos theory try to make this task as easy as possible by employing a variety of methods which, in the last instance, find their justification in metatheorems (...) from Logic. Some concrete instances of this assertion will be given in the form of simple proofs that certain theorems of Algebra hold in any (Grothendieck) topos, in order to illustrate the various techniques that are used. In the other direction, Topos theory can also be a useful tool in Logic. Examples of this are independence proofs in (classical as well as intuitionistic) Set theory, as well as transfer methods in the presence of a sheaf representation theorem, the latter applied, in particular, to model theoretic properties of certain theories. (shrink)

Three aspects of the Everett interpretation of quantum mechanics are considered. It is first shown that the proof of the metatheorem is not complete—thus it is an open question as to whether or not it is true. Next, some difficulties for the Everett interpretation and the metatheorem, which arise from consideration of the physics developed by observers in maverick universes, are discussed. Finally, it is shown that the universal state description of an ever-branching universe with each branch corresponding (...) to a possible perceived universe fails completely in the limit of an infinite number of successive branchings. (shrink)

In this paper we develop a method for finding, under general conditions, explicit and highly uniform rates of convergence for the Picard iteration sequences for selfmaps on bounded metric spaces from ineffective proofs of convergence to a unique fixed point. We are able to extract full rates of convergence by extending the use of a logical metatheorem recently proved by Kohlenbach. In recent case studies we were able to find such explicit rates of convergence in two concrete cases. Our (...) novel method now provides an explanation in logical terms for these findings. This amounts, loosely speaking, to general conditions under which we in this specific setting can transform a ∀∃∀-sentence into a ∀∃-sentence via an argument involving product spaces. This reduction in logical complexity allows us to use the existing machinery to extract quantitative bounds of the sort we need. (shrink)

ABSTRACT In this paper we present a new semantic approach for propositional linear temporal logic with discrete time, strongly based in the well-order of IN (the set of natural numbers). We consider temporal connectives which express precedence, posteriority and simultaneity, and they provide a family of expressively complete temporal logics. The selection of the new semantics and connectives used in this work was principally to obtain a suitable executable temporal logic, which can be used for the specification and control of (...) process behaviour in discrete time in a similar way to thai presented by D. Gabbay in [GAB 89], Our new approach has two advantages: firstly, the connectives are defined intuitively so that they have interpretations which relate to properties of interest in real systems; secondly, it provides a new semantics that facilitates simpler proofs of many valid formulas and metatheorems. To confirm this second advantage, we use our semantics to give a formal proof of the Separation Theorem for one of these logics (specifically LN3). The great interest of this Separation Theorem for the executable temporal logic is emphasised by D. Gabbay in [GAB 89], [GAB 88]. (shrink)