Searcharxiv⌕ Search

arXiv subjects

Richard Zach

Publications and source records attributed to Richard Zach.

At least 19 recordsLinked to original sources
arXiv2026

Hilbert's Program and Infinity

The primary aim of Hilbert's proof theory was to establish the consistency of classical mathematics using finitary means only. Hilbert's strategy for doing this was to eliminate the infinite (in the form of unbounded quantifiers) from formalized proofs using the so-called epsilon substitution method. The result is a formal proof which does not mention or appeal to infinite objects or "concept-formations." However, as later developments showed, the consistency proof itself lets the infinite back into proof theory, through a back door, so to speak. The paper outlines the epsilon substitution method as an example of how proof-theoretic constructions "eliminate the infinite" from formal proofs, and how they aim to establish conservativity and consistency. The proof also requires an argument that this proof theoretic construction always works. This second argument, however, requires possibly infinitary reasoning at the meta-level, using induction on ordinal notations.

math.LO↗
arXiv2024

Logic in Mathematics and Computer Science

Logic has pride of place in mathematics and its 20th century offshoot, computer science. Modern symbolic logic was developed, in part, as a way to provide a formal framework for mathematics: Frege, Peano, Whitehead and Russell, as well as Hilbert developed systems of logic to formalize mathematics. These systems were meant to serve either as themselves foundational, or at least as formal analogs of mathematical reasoning amenable to mathematical study, e.g., in Hilbert's consistency program. Similar efforts continue, but have been expanded by the development of sophisticated methods to study the properties of such systems using proof and model theory. In parallel with this evolution of logical formalisms as tools for articulating mathematical theories (broadly speaking), much progress has been made in the quest for a mechanization of logical inference and the investigation of its theoretical limits, culminating recently in the development of new foundational frameworks for mathematics with sophisticated computer-assisted proof systems. In addition, logical formalisms developed by logicians in mathematical and philosophical contexts have proved immensely useful in describing theories and systems of interest to computer scientists, and to some degree, vice versa. Three examples of the influence of logic in computer science are automated reasoning, computer verification, and type systems for programming languages.

math.LO↗
arXiv2023

Some Unpublished Letters by G\"odel and von Neumann in the Fraenkel Archive

Several letters by Kurt G\"odel and Johann (J\'anos) von Neumann from the (so far uncatalogued) archive of Abraham (Adolf) Fraenkel at the National Library of Israel are published and discussed. These include two fragments by G\"odel of special interest, since they concern the relationship between G\"odel's incompleteness theorem and work by Herbrand, Presburger, and Zermelo, as well as a long letter from von Neumann from 1923 explaining his own approach to the axiomatization of set theory.

math.LO↗
arXiv2022

An Epimorphism between Fine and Ferguson's Matrices for Angell's AC

Angell's logic of analytic containment AC has been shown to be characterized by a 9-valued matrix NC by Ferguson, and by a 16-valued matrix by Fine. It is shown that the former is the image of a surjective homomorphism from the latter, i.e., an epimorphic image. Some candidate 7-valued matrices are ruled out as characteristic of AC. Whether matrices with fewer than 9 values exist remains an open question. The results were obtained with the help of the MUltlog system for investigating finite-valued logics; the results serve as an example of the usefulness of techniques from computational algebra in logic. A tableau proof system for NC is also provided.

math.LO↗
arXiv2021

The Genealogy of '$\lor$'

The use of the symbol $\lor$ for disjunction in formal logic is ubiquitous. Where did it come from? The paper details the evolution of the symbol $\lor$ in its historical and logical context. Some sources say that disjunction in its use as connecting propositions or formulas was introduced by Peano; others suggest that it originated as an abbreviation of the Latin word for "or", vel. We show that the origin of the symbol $\lor$ for disjunction can be traced to Whitehead and Russell's pre-Principia work in formal logic. Because of Principia's influence, its notation was widely adopted by philosophers working in logic (the logical empiricists in the 1920s and 1930s, especially Carnap and early Quine). Hilbert's adoption of $\lor$ in his Grundzüge der theoretischen Logic guaranteed its widespread use by mathematical logicians. The origins of other logical symbols are also discussed.

math.LO↗
arXiv2021

Epsilon Theorems in Intermediate Logics

Any intermediate propositional logic (i.e., a logic including intuitionistic logic and contained in classical logic) can be extended to a calculus with epsilon- and tau-operators and critical formulas. For classical logic, this results in Hilbert's $\varepsilon$-calculus. The first and second $\varepsilon$-theorems for classical logic establish conservativity of the $\varepsilon$-calculus over its classical base logic. It is well known that the second $\varepsilon$-theorem fails for the intuitionistic $\varepsilon$-calculus, as prenexation is impossible. The paper investigates the effect of adding critical $\varepsilon$- and $τ$-formulas and using the translation of quantifiers into $\varepsilon$- and $τ$-terms to intermediate logics. It is shown that conservativity over the propositional base logic also holds for such intermediate $\varepsilonτ$-calculi. The "extended" first $\varepsilon$-theorem holds if the base logic is finite-valued Gödel-Dummett logic, fails otherwise, but holds for certain provable formulas in infinite-valued Gödel logic. The second $\varepsilon$-theorem also holds for finite-valued first-order Gödel logics. The methods used to prove the extended first $\varepsilon$-theorem for infinite-valued Gödel logic suggest applications to theories of arithmetic.

math.LO↗
arXiv2021

Cut-free Completeness for Modular Hypersequent Calculi for Modal Logics K, T, and D

We investigate a recent proposal for modal hypersequent calculi. The interpretation of relational hypersequents incorporates an accessibility relation along the hypersequent. These systems give the same interpretation of hypersequents as Lellman's linear nested sequents, but were developed independently by Restall for S5 and extended to other normal modal logics by Parisi. The resulting systems obey Dosen's principle: the modal rules are the same across different modal logics. Different modal systems only differ in the presence or absence of external structural rules. With the exception of S5, the systems are modular in the sense that different structural rules capture different properties of the accessibility relation. We provide the first direct semantical cut-free completeness proofs for K, T, and D, and show how this method fails in the case of B and S4.

math.LO↗
arXiv2021

Cut elimination and normalization for generalized single and multi-conclusion sequent and natural deduction calculi

Any set of truth-functional connectives has sequent calculus rules that can be generated systematically from the truth tables of the connectives. Such a sequent calculus gives rise to a multi-conclusion natural deduction system and to a version of Parigot's free deduction. The elimination rules are "general," but can be systematically simplified. Cut-elimination and normalization hold. Restriction to a single formula in the succedent yields intuitionistic versions of these systems. The rules also yield generalized lambda calculi providing proof terms for natural deduction proofs as in the Curry-Howard isomorphism. Addition of an indirect proof rule yields classical single-conclusion versions of these systems. Gentzen's standard systems arise as special cases.

math.LO↗
arXiv2019

Effective Finite-Valued Approximations of General Propositional Logics

Propositional logics in general, considered as a set of sentences, can be undecidable even if they have "nice" representations, e.g., are given by a calculus. Even decidable propositional logics can be computationally complex (e.g., already intuitionistic logic is PSPACE-complete). On the other hand, finite-valued logics are computationally relatively simple - at worst NP. Moreover, finite-valued semantics are simple, and general methods for theorem proving exist. This raises the question to what extent and under what circumstances propositional logics represented in various ways can be approximated by finite-valued logics. It is shown that the minimal $m$-valued logic for which a given calculus is strongly sound can be calculated. It is also investigated under which conditions propositional logics can be characterized as the intersection of (effectively given) sequences of finite-valued logics.

math.LO↗
arXiv2017

Natural Deduction for the Sheffer Stroke and Peirce's Arrow (And Any Other Truth-Functional Connective)

Methods available for the axiomatization of arbitrary finite-valued logics can be applied to obtain sound and complete intelim rules for all truth-functional connectives of classical logic including the Sheffer stroke (NAND) and Peirce's arrow (NOR). The restriction to a single conclusion in standard systems of natural deduction requires the introduction of additional rules to make the resulting systems complete; these rules are nevertheless still simple and correspond straightforwardly to the classical absurdity rule. Omitting these rules results in systems for intuitionistic versions of the connectives in question.

math.LO↗
arXiv2016

Semantics and Proof Theory of the Epsilon Calculus

The epsilon operator is a term-forming operator which replaces quantifiers in ordinary predicate logic. The application of this undervalued formalism has been hampered by the absence of well-behaved proof systems on the one hand, and accessible presentations of its theory on the other. One significant early result for the original axiomatic proof system for the epsilon-calculus is the first epsilon theorem, for which a proof is sketched. The system itself is discussed, also relative to possible semantic interpretations. The problems facing the development of proof-theoretically well-behaved systems are outlined.

math.LO↗
arXiv2015

Carnap's Early Metatheory: Scope and Limits

In his Untersuchungen zur allgemeinen Axiomatik (1928) and Abriss der Logistik (1929), Rudolf Carnap attempted to formulate the metatheory of axiomatic theories within a single, fully interpreted type-theoretic framework and to investigate a number of meta-logical notions in it, such as those of model, consequence, consistency, completeness, and decidability. These attempts were largely unsuccessful, also in his own considered judgment. A detailed assessment of Carnap's attempt shows, nevertheless, that his approach is much less confused and hopeless than it has often been made out to be. By providing such a reassessment, the paper contributes to a reevaluation of Carnap's contributions to the development of modern logic.

math.HO↗
arXiv2015

Heinrich Behmann's 1921 lecture on the decision problem and the algebra of logic

Heinrich Behmann (1891-1970) obtained his Habilitation under David Hilbert in Göttingen in 1921 with a thesis on the decision problem. In his thesis, he solved-independently of Löwenheim and Skolem's earlier work-the decision problem for monadic second-order logic in a framework that combined elements of the algebra of logic and the newer axiomatic approach to logic then being developed in Göttingen. In a talk given in 1921, he outlined this solution, but also presented important programmatic remarks on the significance of the decision problem and of decision procedures more generally. The text of this talk as well as a partial English translation are included.

math.LO↗
arXiv2006

First-order Goedel logics

First-order Goedel logics are a family of infinite-valued logics where the sets of truth values V are closed subsets of [0, 1] containing both 0 and 1. Different such sets V in general determine different Goedel logics G_V (sets of those formulas which evaluate to 1 in every interpretation into V). It is shown that G_V is axiomatizable iff V is finite, V is uncountable with 0 isolated in V, or every neighborhood of 0 in V is uncountable. Complete axiomatizations for each of these cases are given. The r.e. prenex, negation-free, and existential fragments of all first-order Goedel logics are also characterized.

math.LO↗
arXiv2005

The Epsilon Calculus and Herbrand Complexity

Hilbert's epsilon-calculus is based on an extension of the language of predicate logic by a term-forming operator $ε_{x}$. Two fundamental results about the epsilon-calculus, the first and second epsilon theorem, play a role similar to that which the cut-elimination theorem plays in sequent calculus. In particular, Herbrand's Theorem is a consequence of the epsilon theorems. The paper investigates the epsilon theorems and the complexity of the elimination procedure underlying their proof, as well as the length of Herbrand disjunctions of existential theorems obtained by this elimination procedure.

math.LO↗
arXiv2005

Hilbert's Program Then and Now

Hilbert's program was an ambitious and wide-ranging project in the philosophy and foundations of mathematics. In order to "dispose of the foundational questions in mathematics once and for all, "Hilbert proposed a two-pronged approach in 1921: first, classical mathematics should be formalized in axiomatic systems; second, using only restricted, "finitary" means, one should give proofs of the consistency of these axiomatic systems. Although Godel's incompleteness theorems show that the program as originally conceived cannot be carried out, it had many partial successes, and generated important advances in logical theory and meta-theory, both at the time and since. The article discusses the historical background and development of Hilbert's program, its philosophical underpinnings and consequences, and its subsequent development and influences since the 1930s.

math.LO↗