Work on how to axiomatize the subtheories of a first-order theory in which only a proper subset of their extra-logical vocabulary is being used led to a theorem on recursive axiomatizability and to an interpolation theorem for first-order logic. There were some fortuitous events and several logicians played a helpful role.

We study the formal first order system TIND in the standard language of Gentzen's LK . TIND extends LK by the purely logical rule of term-induction, that is a restricted induction principle, deriving numerals instead of arbitrary terms. This rule may be conceived as the logical image of full induction.

Gentzen writes in the published version of his doctoral thesis Untersuchungen über das logische Schliessen that he was able to prove the normalization theorem only for intuitionistic natural deduction, but not for classical. To cover the latter, he developed classical sequent calculus and proved a corresponding theorem, the famous cut elimination result. Its proof was organized so that a cut elimination result for an intuitionistic sequent calculus came out as a special case, namely the one in which the (...) sequents have at most one formula in the right, succedent part. Thus, there was no need for a direct proof of normalization for intuitionistic natural deduction. The only traces of such a proof in the published thesis are some convertibilities, such as when an implication introduction is followed by an implication elimination [1934–35, II.5.13]. It remained to Dag Prawitz in 1965 to work out a proof of normalization. Another, less known proof was given also in 1965 by Andres Raggio.We found in February 2005 an early handwritten version of Gentzen's thesis, with exactly the above title, but with rather different contents: Most remarkably, it contains a detailed proof of normalization for what became the standard system of natural deduction. The manuscript is located in the Paul Bernays collection at the ETH-Zurichwith the signum Hs. 974: 271. Bernays must have gotten it well before the time of his being expelled from Göttingen on the basis of the racial laws in April 1933. (shrink)

Gentzen writes in the published version of his doctoral thesis Untersuchungen über das logische Schliessen that he was able to prove the normalization theorem only for intuitionistic natural deduction, but not for classical. To cover the latter, he developed classical sequent calculus and proved a corresponding theorem, the famous cut elimination result. Its proof was organized so that a cut elimination result for an intuitionistic sequent calculus came out as a special case, namely the one in which the (...) sequents have at most one formula in the right, succedent part. Thus, there was no need for a direct proof of normalization for intuitionistic natural deduction. The only traces of such a proof in the published thesis are some convertibilities, such as when an implication introduction is followed by an implication elimination [1934–35, II.5.13]. It remained to Dag Prawitz in 1965 to work out a proof of normalization. Another, less known proof was given also in 1965 by Andres Raggio.We found in February 2005 an early handwritten version of Gentzen's thesis, with exactly the above title, but with rather different contents: Most remarkably, it contains a detailed proof of normalization for what became the standard system of natural deduction. The manuscript is located in the Paul Bernays collection at the ETH-Zurichwith the signum Hs. 974: 271. Bernays must have gotten it well before the time of his being expelled from Göttingen on the basis of the racial laws in April 1933. (shrink)

The 'no-supervenience' theorem (Reason, 2019; Reason and Shah, 2021) is a proof that no fully self-aware system can entirely supervene on any objectively observable system. I here present a simple, non-technical summary of the proof and demonstrate its implications for four separate theories of consciousness: the 'property dualism' theory of David Chalmers; the 'reflexive monism' of Max Velmans; Galen Strawson's 'realistic monism'; and the 'illusionism' of Keith Frankish. It is shown that all are ruled out in their current form (...) by the no-supervenience theorem, except for Chalmers' theory, which I show requires humans to behave irrationally. (shrink)

Conscious macrostates are usually assumed to be emergent from the underlying physical microstates comprising the brain and nervous system of biological organisms. However, a major problem with this assumption is that consciousness is essentially nonmeasurable unlike all other proven emergent properties of physical systems. In an earlier paper, using a no-go theorem, it was shown that conscious states cannot be comprised of processes that are physical in nature (Reason, 2019). Combining this result with another unrelated work on causal emergence (...) in physical systems (Hoel, Albantakis and Tononi, 2013), we show in this paper that conscious macrostates are not emergent from physical systems and they also do not supervene on physical microstates. An important implication of our work is that there must be some form of violation of energy conservation in biological systems that are conscious. (shrink)

ABSTRACT In this paper we study consequence relations on the set of many sided sequents over a propositional language. We deal with the consequence relations axiomatized by the sequent calculi defined in [2] and associated with arbitrary finite algebras. These consequence relations are examples of what we call Gentzen systems. We define a semantics for these systems and prove a Strong Completeness Theorem, which is an extension of the Completeness Theorem for provable sequents stated in [2]. For the (...) special case of the finite linear MV-algebras, the Strong Completeness Theorem was proved in [10], as a consequence of McNaughton's Theorem. The main tool to prove this result for arbitrary algebras is the deduction-detachment theorem for Gentzen systems. (shrink)

The papers collected in this volume exemplify some of the trends in current approaches to logic, language and computation. Written by authors with varied academic backgrounds, the contributions are intended for an interdisciplinary audience. The first part of this volume addresses issues relevant for multi-agent systems: reasoning with incomplete information, reasoning about knowledge and beliefs, and reasoning about games. Proofs as formal objects form the subject of Part II. Topics covered include: contributions on logical frameworks, linear (...) logic, and different approaches to formalized reasoning. Part III focuses on representations and formal methods in linguistic theory, addressing the areas of comparative and temporal expressions, modal subordination, and compositionality. (shrink)

We formulate a polarized version of Ramsey’s theorem for trees. For those exponents greater than 2, both the reverse mathematics and the computability theory associated with this theorem parallel that of its linear analog. For pairs, the situation is more complex. In particular, there are many reasonable notions of stability in the tree setting, complicating the analysis of the related results.

In the 1920s, Paul Hertz (1881-1940) developed certain calculi based on structural rules only and established normal form results for proofs. It is shown that he anticipated important techniques and results of general proof theory as well as of resolution theory, if the latter is regarded as a part of structural proof theory. Furthermore, it is shown that Gentzen, in his first paper of 1933, which heavily draws on Hertz, proves a normal form result which corresponds to the completeness of (...) prepositional SLD-resolution in logic programming. (shrink)

We use Herbrand’s theorem to give a new proof that Euclid’s parallel axiom is not derivable from the other axioms of first-order Euclidean geometry. Previous proofs involve constructing models of non-Euclidean geometry. This proof uses a very old and basic theorem of logic together with some simple properties of ruler-and-compass constructions to give a short, simple, and intuitively appealing proof.

In this paper I will argue that (principled) attempts to ground a priori knowledge in default reasonable beliefs cannot capture certain common intuitions about what is required for a priori knowledge. I will describe hypothetical creatures who derive complex mathematical truths like Fermat’s last theorem via short and intuitively unconvincing arguments. Many philosophers with foundationalist inclinations will feel that these creatures must lack knowledge because they are unable to justify their mathematical assumptions in terms of the kind of basic (...) facts which can be known without further argument. Yet, I will argue that nothing in the current literature lets us draw a principled distinction between what these creatures are doing and paradigmatic cases of good a priori reasoning (assuming that the latter are to be grounded in default reasonable beliefs). I will consider, in turn, appeals to reliability, coherence, conceptual truth and indispensability and argue that none of these can do the job. (shrink)

In advanced books and courses on logic (e.g. Sm], BM]) Gentzen-type systems or their dual, tableaux, are described as techniques for showing validity of formulae which are more practical than the usual Hilbert-type formalisms. People who have learnt these methods often wonder why the Automated Reasoning community seems to ignore them and prefers instead the resolution method. Some of the classical books on AD (such as CL], Lo]) do not mention these methods at all. Others (such as Ro]) do, (...) but the connections and reasons for preference remain unclear after reading them (at least to the present author, and obviously also the authors of OS], in which a theorem-prover, based exclusively on tableaux, is described). The confusion becomes greater when the reader is introduced to Kowalski's form of a clause ( Ko], Bu]), which is nothing but a Gentzen's sequent of atomic formulae, and when he realizes that resolution is just a form of a Cut, and so that while the elimination of cuts is the principal tool in proof-theory, its use is the main technique in AD! (shrink)

This study introduces refutation-aware Gentzen-style sequent calculi and Kripke-style semantics for propositional until-free linear-time temporal logic. The sequent calculi and semantics are constructed on the basis of the refutation-aware setting for Nelson’s paraconsistent logic. The cut-elimination and completeness theorems for the proposed sequent calculi and semantics are proven.

Let B be a p-uniformly convex Banach space, with p≥2. Let T be a linear operator on B, and let Anx denote the ergodic average ∑i.

Herbrand disjunctions are a means for reducing the problem ofwhether a first-oder formula is valid in an open theory T or not to theproblem whether an open formula, one of the so called Herbrand disjunctions,is T -valid or not. Nevertheless, the set of Herbrand disjunctions, which hasto be examined, is undecidable in general. Fore this reason the practicalvalue of Herbrand disjunctions has been estimated negatively .Relying on completeness proofs which are based on the algebraizationtechnique presented in [30], but taking a (...) more optimistic view, we show howHerbrand disjunctions become the base of a method for building in theoriesinto automatic theorem provers [26]. Surveying newer results we discusshow to treat heterogeneous theories [29] as well as practical implications ofdifferent normal form transformations. (shrink)

A structure which generalizes formulas by including substitution terms is used to represent proofs in classical logic. These structures, called expansion trees, can be most easily understood as describing a tautologous substitution instance of a theorem. They also provide a computationally useful representation of classical proofs as first-class values. As values they are compact and can easily be manipulated and transformed. For example, we present an explicit transformations between expansion tree proofs and cut-free sequential proofs. A theorem prover (...) which represents proofs using expansion trees can use this transformation to present its proofs in more human-readable form. Also a very simple computation on expansion trees can transform them into Craig-style linear reasoning and into interpolants when they exist. We have chosen a sublogic of the Simple Theory of Types for our classical logic because it elegantly represents substitutions at all finite types through the use of the typed -calculus. Since all the proof-theoretic results we shall study depend heavily on properties of substitutions, using this logic has allowed us to strengthen and extend prior results: we are able to prove a strengthen form of the firstorder interpolation theorem as well as provide a correct description of Skolem functions and the Herbrand Universe. The latter are not straightforward generalization of their first-order definitions. (shrink)

Heidegger holds that our age is dominated by the ambition of reason to possess the world. And he sees in Leibniz the man who formulated the theorem of our modern age: nothing happens without a reason. He calls this attitude `calculating thought' and opposes to it a kind of thought aimed at preserving the essence of things, which he calls `meditating thought'. Cristin's book ascribes great importance to this polarity of thinking for the future of contemporary philosophy, and thus (...) compares the basic ideas of the two thinkers. Leibniz announces the conquest of reason; Heidegger denounces the dangers of reason. Their diversity becomes manifest in the difference between the idea of reason and the image of the path. But is Leibniz's thought really only `calculating'? And do we not perhaps also encounter the traces of reason along Heidegger's path? With these questions in mind we may begin to redefine the relation between the two thinkers and between two different conceptions of reason and philosophy. The hypothesis is advanced that Heidegger's harsh judgment of Leibniz may be mitigated, but it also becomes clear that Heidegger's rewriting of the code of reason is an integral part of our age, in which many signs point to new loci of rationality. With his original interpretation, aware of the risks he is taking, Renato Cristin offers a new guide to the understanding of reason: he shows forth Leibniz as one who defends the thought of being in the unity of monadology, and Heidegger as a thinker who preserves the sign of reason in his meditating thought. (shrink)

The tridecompositional uniqueness theorem of Elby and Bub (1994) shows that a wavefunction in a triple tensor product Hilbert space has at most one decomposition into a sum of product wavefunctions with each set of component wavefunctions linearly independent. I demonstrate that, in many circumstances, the unique component wavefunctions and the coefficients in the expansion are both hopelessly unstable, both under small changes in global wavefunction and under small changes in global tensor product structure. In my opinion, this means (...) that the theorem cannot underlie lawlike solutions to the problems of the interpretation of quantum theory. I also provide examples of circumstances in which there are open sets of wavefunctions containing no states with various decompositions. (shrink)

Peter Gärdenfors has proved (Philosophical Review, 1986) that the Ramsey rule and the methodologically conservative Preservation principle are incompatible given innocuous-looking background assumptions about belief revision. Gärdenfors gives up the Ramsey rule; I argue for preserving the Ramsey rule and interpret Gärdenfors's theorem as showing that no rational belief-reviser can avoid reasoning nonmonotonically. I argue against the Preservation principle and show that counterexamples to it always involve nonmonotonic reasoning. I then construct a new formal model of belief (...) revision that does accommodate nonmonotonic reasoning. (shrink)

This paper introduces an anthropological approach to the foundations of mathematics. Traditionally, the philosophy of mathematics has focused on the nature and origins of mathematical truth. Mathematicians, however, treat mathematical arguments as determining mathematical truth: if an argument is found to describe a witnessably rigorous proof of a theorem, that theorem is considered—until the need for further examination arises—to be true. The anthropological question is how mathematicians, as a practical matter and as a matter of mathematical practice, make (...) such determinations. This paper looks first at the ways that the logic of mathematical argumentation comes to be realized and substantiated by provers as their own immediate, situated accomplishment. The type of reasoning involved is quite different from deductive logic; once seen, it seems to be endemic to and pervasive throughout the work of human theorem proving. A number of other features of proving are also considered, including the production of notational coherence, the foregrounding of proof-specific proof-relevant detail, and the structuring of mathematical argumentation. Through this material, the paper shows the feasibility and promise of a real-world anthropology of disciplinary mathematical practice. (shrink)

A theorem for embedding a first-order linear- time temporal logic LTL into its intuitionistic counterpart ILTL is proved using Baratella-Masini's temporal extension of the Gödel-Gentzen negative translation of classical logic into intuitionistic logic. A substructural counterpart LLTL of ILTL is introduced, and a theorem for embedding ILTL into LLTL is proved using a temporal extension of the Girard translation of intuitionistic logic into intuitionistic linear logic. These embedding theorems are proved syntactically based on Gentzen-type sequent calculi.

I demonstrate that Bell's theorem is based on circular reasoning and thus a fundamentally flawed argument. It unjustifiably assumes the additivity of expectation values for dispersion-free states of contextual hidden variable theories for non-commuting observables involved in Bell-test experiments, which is tautologous to assuming the bounds of ±2 on the Bell-CHSH sum of expectation values. Its premises thus assume in a different guise the bounds of ±2 it sets out to prove. Once this oversight is ameliorated from Bell's (...) argument by identifying the impediment that leads to it and local realism is implemented correctly, the bounds on the Bell-CHSH sum of expectation values work out to be ±2√2 instead of ±2, thereby mitigating the conclusion of Bell's theorem. Consequently, what is ruled out by any of the Bell-test experiments is not local realism but the linear additivity of expectation values, which does not hold for non-commuting observables in any hidden variable theories to begin with. (shrink)

Gentzen’s sequent calculi LK and LJ are landmark proof systems. They identify the structural rules of weakening and contraction as notable inference rules, and they allow for an elegant statement and proof of both cut elimination and consistency for classical and intuitionistic logics. Among the undesirable features of those sequent calculi is that their inferences rules are low-level and frequently permute over each other. As a result, large-scale structures within sequent calculus proofs are hard to identify. In this paper, we (...) present a different approach to designing a sequent calculus for classical logic. Starting with Gentzen’s LK proof system, we examine the proof search meaning of his inference rules and classify those rules as involving either don’t care nondeterminism or don’t know nondeterminism. Based on that classification, we design the focused proof system LKF in which inference rules belong to one of two phases of proof construction depending on which flavor of nondeterminism they involve. We then prove that the cut rule and the general form of the initial rule are admissible in LKF. Finally, by showing that the inference rules for LK are all admissible in LKF, we can give a relative completeness proof for LKF provability with respect to LK provability. We shall also apply these properties of the LKF proof system to establish other meta-theoretic properties of classical logic, including Herbrand’s theorem. (shrink)

Attempts to articulate the real meaning or ultimate significance of a famous theorem comprise a major vein of philosophical writing about mathematics. The subfield of mathematical logic has supplie...

In February 2015 the UK became the first country to legalise high-profile mitochondrial replacement techniques, which involve the creation of offspring using genetic material from three individuals. The aim of these new cell reconstruction techniques is to prevent the transmission of maternally inherited mitochondrial disorders to biological offspring. During the UK debates, MRTs were often positioned as a straightforward and unique solution for the ‘eradication’ of mitochondrial disorders, enabling hundreds of women to have a healthy, biologically-related child. However, many questions (...) regarding future applications and potential users remain. Drawing on a current qualitative study on reproductive choices in the context of mitochondrial disorders, this article illustrates how the potential limitations of MRTs have been obscured in public debates by contrasting the claims made about the future beneficiaries with insights from families affected by mitochondrial disorders and medical experts. The analysis illuminates the complex choices with which families and individuals affected by mitochondrial disorders are faced, which have thus far remained invisible. An argument is presented for improved information for the public as well as an intensification of critical empirical research around the complex and specific needs of future beneficiaries of new reproductive biotechnologies. (shrink)

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

A translation of the Écrits logiques, edited by Jean Van Heijenoort, published in 1968.

The $$\varepsilon $$ -elimination method of Hilbert’s $$\varepsilon $$ -calculus yields the up-to-date most direct algorithm for computing the Herbrand disjunction of an extensional formula. A central advantage is that the upper bound on the Herbrand complexity obtained is independent of the propositional structure of the proof. Prior (modern) work on Hilbert’s $$\varepsilon $$ -calculus focused mainly on the pure calculus, without equality. We clarify that this independence also holds for first-order logic with equality. Further, we provide upper bounds analyses (...) of the extended first $$\varepsilon $$ -theorem, even if the formalisation incorporates so-called $$\varepsilon $$ -equality axioms. (shrink)

This monograph provides a new account of justified inference as a cognitive process. In contrast to the prevailing tradition in epistemology, the focus is on low-level inferences, i.e., those inferences that we are usually not consciously aware of and that we share with the cat nearby which infers that the bird which she sees picking grains from the dirt, is able to fly. Presumably, such inferences are not generated by explicit logical reasoning, but logical methods can be used to (...) describe and analyze such inferences. Part 1 gives a purely system-theoretic explication of belief and inference. Part 2 adds a reliabilist theory of justification for inference, with a qualitative notion of reliability being employed. Part 3 recalls and extends various systems of deductive and nonmonotonic logic and thereby explains the semantics of absolute and high reliability. In Part 4 it is proven that qualitative neural networks are able to draw justified deductive and nonmonotonic inferences on the basis of distributed representations. This is derived from a soundness/completeness theorem with regard to cognitive semantics of nonmonotonic reasoning. The appendix extends the theory both logically and ontologically, and relates it to A. Goldman's reliability account of justified belief. This text will be of interest to epistemologists and logicians, to all computer scientists who work on nonmonotonic reasoning and neural networks, and to cognitive scientists. (shrink)

The first known statements of the deduction theorems for the first-order predicate calculus and the classical sentential logic are due to Herbrand [8] and Tarski [14], respectively. The present paper contains an analysis of closure spaces associated with those sentential logics which admit various deduction theorems. For purely algebraic reasons it is convenient to view deduction theorems in a more general form: given a sentential logic C (identified with a structural consequence operation) in a sentential language I, a quite arbitrary (...) set P of formulas of I built up with at most two distinct sentential variables p and q is called a uniform deduction theorem scheme for C if it satisfies the following condition: for every set X of formulas of I and for any formulas and , C(X{{a}}) iff P(, ) AC(X). [P(, ) denotes the set of formulas which result by the simultaneous substitution of for p and for q in all formulas in P]. The above definition encompasses many particular formulations of theorems considered in the literature to be deduction theorems. Theorem 1.3 gives necessary and sufficient conditions for a logic to have a uniform deduction theorem scheme. Then, given a sentential logic C with a uniform deduction theorem scheme, the lattices of deductive filters on the algebras A similar to the language of C are investigated. It is shown that the join-semilattice of finitely generated (= compact) deductive filters on each algebra A is dually Brouwerian. (shrink)

I criticize a recent paper by Thomas Tymoczko in which he attributes fundamental philosophical significance and novelty to the lately-published computer-assisted proof of the four color theorem (4CT). Using reasoning precisely analogous to that employed by Tymoczko, I argue that much of traditional mathematical proof must be seen as resting on what Tymoczko must take as being "empirical" evidence. The new proof of the 4CT, with its use of what Tymoczko calls "empirical" evidence is therefore not so novel (...) as he maintains. Finally, without attempting to give a full account of the notion of empirical mathematical evidence, I sketch a view showing how the use of calculation injects an empirical ingredient into proof. (shrink)

A general Gentzen-style framework for handling both bilattice (or strong) negation and usual negation is introduced based on the characterization of negation by a modal-like operator. This framework is regarded as an extension, generalization or re- finement of not only bilattice logics and logics with strong negation, but also traditional logics including classical logic LK, classical modal logic S4 and classical linear logic CL. Cut-elimination theorems are proved for a variety of proposed sequent calculi including CLS (a conservative extension (...) of CL) and CLScw (a conservative extension of some bilattice logics, LK and S4). Completeness theorems are given for these calculi with respect to phase semantics, for SLK (a conservative extension and fragment of LK and CLScw, respectively) with respect to a classical-like semantics, and for SS4 (a conservative extension and fragment of S4 and CLScw, respectively) with respect to a Kripke-type semantics. The proposed framework allows for an embedding of the proposed calculi into LK, S4 and CL. (shrink)

The paper discusses the origin of dark matter and dark energy from the concepts of time and the totality in the final analysis. Though both seem to be rather philosophical, nonetheless they are postulated axiomatically and interpreted physically, and the corresponding philosophical transcendentalism serves heuristically. The exposition of the article means to outline the “forest for the trees”, however, in an absolutely rigorous mathematical way, which to be explicated in detail in a future paper. The “two deductions” are two successive (...) stage of a single conclusion mentioned above. The concept of “transcendental invariance” meaning ontologically and physically interpreting the mathematical equivalence of the axiom of choice and the well-ordering “theorem” is utilized again. Then, time arrow is a corollary from that transcendental invariance, and in turn, it implies quantum information conservation as the Noether correlate of the linear “increase of time” after time arrow. Quantum information conservation implies a few fundamental corollaries such as the “conservation of energy conservation” in quantum mechanics from reasons quite different from those in classical mechanics and physics as well as the “absence of hidden variables” (versus Einstein’s conjecture) in it. However, the paper is concentrated only into the inference of another corollary from quantum information conservation, namely, dark matter and dark energy being due to entanglement, and thus and in the final analysis, to the conservation of quantum information, however observed experimentally only on the “cognitive screen” of “Mach’s principle” in Einstein’s general relativity. therefore excluding any other source of gravitational field than mass and gravity. Then, if quantum information by itself would generate a certain nonzero gravitational field, it will be depicted on the same screen as certain masses and energies distributed in space-time, and most presumably, observable as those dark energy and dark matter predominating in the universe as about 96% of its energy and matter quite unexpectedly for physics and the scientific worldview nowadays. Besides on the cognitive screen of general relativity, entanglement is available necessarily on still one “cognitive screen” (namely, that of quantum mechanics), being furthermore “flat”. Most probably, that projection is confinement, a mysterious and ad hoc added interaction along with the fundamental tree ones of the Standard model being even inconsistent to them conceptually, as far as it need differ the local space from the global space being definable only as a relation between them (similar to entanglement). So, entanglement is able to link the gravity of general relativity to the confinement of the Standard model as its projections of the “cognitive screens” of those two fundamental physical theories. (shrink)

Set theoretic formulation of Arrow's theorem, viewedin light of a taxonomy of transitive relations,serves to unmask the theorem's understatedgenerality. Under the impress of the independenceof irrelevant alternatives, the antipode of ceteris paribus reasoning, a purported compilerfunction either breaches some other rationalitypremise or produces the effet Condorcet. Types of cycles, each the seeming handiwork of avirtual voter disdaining transitivity, arerigorously defined. Arrow's theorem erects adilemma between cyclic indecision anddictatorship. Maneuvers responsive theretoare explicable in set theoretic terms. None (...) ofthese gambits rival in simplicity the unassistedescape of strict linear orderings, which, by virtueof the Arrow–Sen reflexivity premise, are notcaptured by the theorem. Yet these are therelations among whose n-tuples the effetCondorcet is most frequent. A generalization andstronger theorem encompasses these and all otherlinear orderings and total tierings. Revisions tothe Arrow–Sen definitions of `choice set' and`rationalization' similarly enable one to generalizeSen's demonstration that some rational choicefunction always exists. Similarly may onegeneralize Debreu's theorems establishing conditionsunder which a binary relation may be represented bya continuous real-valued order homomorphism. (shrink)

Formal verification involves the use of logical and computational methods to establish claims that are expressed in precise mathematical terms. These can include ordinary mathematical theorems, as well as claims that pieces of hardware or software, network protocols, and mechanical and hybrid systems meet their specifications. In practice, there is not a sharp distinction between verifying a piece of mathematics and verifying the correctness of a system: formal verification requires describing hardware and software systems in mathematical terms, at which point (...) establishing claims as to their correctness becomes a form of theorem proving. Conversely, the proof of a mathematical theorem may require a lengthy computation, in which case verifying the truth of the theorem requires verifying that the computation does what it is supposed to do. The gold standard for supporting a mathematical claim is to provide a proof, and twentieth-century developments in logic show most if not all conventional proof methods can be reduced to a small set of axioms and rules in any of a number of foundational systems. With this reduction, there are two ways that a computer can help establish a claim: it can help find a proof in the first place, and it can help verify that a purported proof is correct. Automated theorem proving focuses on the “finding” aspect. Resolution theorem provers, tableau theorem provers, fast satisfiability solvers, and so on provide means of establishing the validity of formulas in propositional and first-order logic. Other systems provide search procedures and decision procedures for specific languages and domains, such as linear or nonlinear expressions over the integers or the real numbers. Architectures like SMT combine domain-general search methods with domain-specific procedures. Computer algebra systems and specialized mathematical software packages provide means of carrying out mathematical computations, establishing mathematical bounds, or finding mathematical objects. A calculation can be viewed as a proof as well, and these systems, too, help establish mathematical claims. Automated reasoning systems strive for power and efficiency, often at the expense of guaranteed soundness. Such systems can have bugs, and it can be difficult to ensure that the results they deliver are correct. In contrast, interactive theorem proving focuses on the “verification” aspect of theorem proving, requiring that every claim is supported by a proof in a suitable axiomatic foundation. This sets a very high standard: every rule of inference and every step of a calculation has to be justified by appealing to prior definitions and theorems, all the way down to basic axioms and rules. In fact, most such systems provide fully elaborated “proof objects” that can be communicated to other systems and checked independently. Constructing such proofs typically requires much more input and interaction from users, but it allows us to obtain deeper and more complex proofs. The Lean Theorem Prover aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs. The goal is to support both mathematical reasoning and reasoning about complex systems, and to verify claims in both domains. (shrink)

Contemporary decision theory places crucial emphasis on a family of mathematical results called representation theorems, which relate criteria for evaluating the available options to axioms pertaining to the decision-maker’s preferences. Various claims have been made concerning the reasons for the importance of these results. The goal of this article is to assess their semantic role: representation theorems are purported to provide definitions of the decision-theoretic concepts involved in the evaluation criteria. In particular, this claim shall be examined from the perspective (...) of philosophical theories of the meaning of theoretical terms. (shrink)

I study definability and types in the linear fragment of continuous logic. Linear variants of several definability theorems such as Beth, Svenonus and Herbrand are proved. At the end, a partial study of the theories of probability algebras, probability algebras with an aperiodic automorphism and AL-spaces is given.

Standard proofs of generalized Bell theorems, aiming to restrict stochastic, local hidden-variable theories for quantum correlation phenomena, employ as a locality condition the requirement of conditional stochastic independence. The connection between this and the no-superluminary-action requirement of the special theory of relativity has been a topic of controversy. In this paper, we introduce an alternative locality condition for stochastic theories, framed in terms of the models of such a theory (§2). It is a natural generalization of a light-cone determination condition (...) that is essentially equivalent to mathematical conditions that have been used to derive Bell inequalities in the deterministic case. Further, it is roughly equivalent to a condition proposed by Bell that, in one investigation, needed to be supplemented with a much stronger assumption in order to yield an inequality violated by some quantum mechanical predictions. It is shown here that this reflects a very general situation: from the proposed locality condition, even adding the strict anticorrelation condition and the auxiliary hypotheses needed to derive experimentally useful (and theoretically telling) inequalities, no Bell-type inequality is derivable. (These independence claims are the burden of §4.) A certain limitation on the scope of the proposed stochastic locality condition is exposed (§5), but it is found to be rather minor. The conclusion is thus supported that conditional stochastic independence, however reasonable on other grounds, is essentially stronger than what is required by the special theory.Our results stand in apparent contradiction with a class of derivations purporting to obtain generalized Bell inequalities from locality alone. It is shown in Appendix (B) that such proofs do not achieve their goal. This fits with our conclusion that generalized Bell theorems are not straightforward generalizations of theorems restricting deterministic hidden-variable theories, and that, in fact, such generalizations do not exist. This leaves open the possibility that a satisfactory, non-deterministic account of the quantum correlation phenomena can be given within the framework of the special theory. (shrink)