Open Access. Powered by Scholars. Published by Universities.®
- Discipline
-
- Computer Sciences (11)
- Algebra (9)
- Arts and Humanities (9)
- Analysis (8)
- Philosophy (8)
-
- Discrete Mathematics and Combinatorics (7)
- Set Theory (7)
- Theory and Algorithms (7)
- Applied Mathematics (6)
- Education (6)
- Logic and Foundations of Mathematics (6)
- Other Mathematics (5)
- Statistics and Probability (5)
- Engineering (4)
- Geometry and Topology (4)
- Higher Education (4)
- Philosophy of Science (4)
- Artificial Intelligence and Robotics (3)
- Dynamic Systems (3)
- Epistemology (3)
- Other Computer Sciences (3)
- Physics (3)
- Probability (3)
- Quantum Physics (3)
- Software Engineering (3)
- Applied Statistics (2)
- Computer Engineering (2)
- Institution
-
- City University of New York (CUNY) (15)
- Claremont Colleges (6)
- Boise State University (5)
- Marshall University (5)
- University of Malaya (4)
-
- Utah State University (4)
- Morehead State University (3)
- Bucknell University (2)
- California Polytechnic State University, San Luis Obispo (2)
- University at Albany, State University of New York (2)
- University of Arkansas, Fayetteville (2)
- University of Denver (2)
- University of Northern Iowa (2)
- Air Force Institute of Technology (1)
- California State University, San Bernardino (1)
- Central Washington University (1)
- Dartmouth College (1)
- Florida Institute of Technology (1)
- Illinois Math and Science Academy (1)
- Louisiana State University (1)
- Rhode Island School of Design (1)
- Stephen F. Austin State University (1)
- The College of Wooster (1)
- The University of Akron (1)
- University of Connecticut (1)
- University of Missouri, St. Louis (1)
- University of Nevada, Las Vegas (1)
- Wilfrid Laurier University (1)
- Keyword
-
- Logic (8)
- Mathematics (6)
- Model theory (4)
- Model Theory (3)
- Category theory (2)
-
- Computer Science (2)
- Epistemic Game Theory (2)
- Formal Methods (2)
- Free monoid (2)
- Graph theory (2)
- Philosophy (2)
- Proof theory (2)
- Residuated lattices (2)
- Reverse Mathematics (2)
- #antcenter (1)
- (LAD)Retention (1)
- 05B15 (1)
- 91A44 (1)
- <p>Differential equations.</p> (1)
- <p>Differential equations.</p> <p>Differential analyzers.</p> (1)
- <p>Mathematical statistics.</p> (1)
- <p>Poisson processes.</p> <p>Poisson distribution.</p> <p>Sex differences in education.</p> (1)
- <p>Reverse mathematics.</p> <p>Logic - Mathematics.</p> (1)
- ACL2 (1)
- ADNI database (1)
- Adaptive Nawaz Enscore Ham (NEH) (1)
- Algebraic geometry (1)
- Algebraic logic (1)
- Alzheimer’s disease (1)
- Analytics (1)
- Publication Year
- Publication
-
- Dissertations, Theses, and Capstone Projects (15)
- Boise State University Theses and Dissertations (5)
- Theses, Dissertations and Capstones (5)
- All Graduate Theses and Dissertations, Spring 1920 to Summer 2023 (4)
- CMC Senior Theses (3)
-
- Electronic Theses and Dissertations (3)
- HMC Senior Theses (3)
- Master's Theses (3)
- Morehead State Theses and Dissertations (3)
- Dissertations and Theses @ UNI (2)
- Electronic Theses & Dissertations (2024 - present) (2)
- Graduate Theses and Dissertations (2)
- Honors Theses (2)
- Student Works (2000-2009) (2)
- Theses and Dissertations (2)
- All Master's Theses (1)
- Dartmouth College Ph.D Dissertations (1)
- Doctoral Dissertations (1)
- Electronic Theses, Projects, and Dissertations (1)
- Honors College Theses (1)
- LSU Doctoral Dissertations (1)
- Masters Theses (1)
- Senior Independent Study Theses (1)
- Student Works (2010-2019) (1)
- Student Works (2020-2029) (1)
- Theses (1)
- Theses and Dissertations (Comprehensive) (1)
- Williams Honors College, Honors Research Projects (1)
Articles 1 - 30 of 69
Full-Text Articles in Logic and Foundations
Model-Theoretic Arguments In Philosophy, Peter Susanszky
Model-Theoretic Arguments In Philosophy, Peter Susanszky
Dissertations, Theses, and Capstone Projects
This dissertation is on model-theoretic arguments in philosophy, especially those of Quine, Davidson, and Putnam. In the first part, to ground the debate, I give a rigorous introduction to the salient parts of first-order model theory. I start the second part by giving an introduction to Quine's philosophy, and how the model-theoretic arguments fit into it. After considering how Donald Davidson adopted the Quinean lesson, I move on to Putnam's model-theoretic arguments. Putnam's spin on these model-theoretic considerations significantly departs from Quine and Davidson, while retaining many of the core ideas. Most importantly, I argue that the target of Putnam's …
A New Approach To Generate Combinatorial Patterns In Logical Analysis Of Data And Its Application To Predict College Retention, Salihah Ahmed E. Jaafari
A New Approach To Generate Combinatorial Patterns In Logical Analysis Of Data And Its Application To Predict College Retention, Salihah Ahmed E. Jaafari
Theses and Dissertations
Student retention and degree completion remain central challenges for higher-education institutions, with significant implications for student success, institutional effectiveness, and public accountability. While advances in predictive analytics have enabled earlier identification of students at risk of withdrawal, many commonly used machine learning approaches suffer from limited interpretability, constraining their practical usefulness for advising, intervention, and policy decision making. This dissertation addresses the problem of predicting student persistence by developing and evaluating optimization based, interpretable classification models within the Logical Analysis of Data (LAD) framework. Building on existing LAD formulations, this research introduces two novel pattern generation models, the Best Term …
Demystifying Hardware Formal Verification For Undergraduate Education: A Risc-V Processor Case Study With Coursework Implementation, Riley A. Peters
Demystifying Hardware Formal Verification For Undergraduate Education: A Risc-V Processor Case Study With Coursework Implementation, Riley A. Peters
Master's Theses
Hardware verification engineers apply formal methods to prove that a digital device always behaves according to its specification. This differs from traditional functional verification, in which engineers establish correctness by repeatedly sending test inputs to the device and comparing the outputs against a reference model. With the growing complexity of integrated circuits, the demand for digital verification engineers with formal methods experience has continued to increase. However, California Polytechnic State University: San Luis Obispo's current curriculum lacks dedicated material to prepare students for these roles.
This thesis seeks to address the lack of formal methods material through two efforts. First, …
Toward Completeness Theorem For Guarded Kleene Algebra With Tests, Hung Pham
Toward Completeness Theorem For Guarded Kleene Algebra With Tests, Hung Pham
Honors Theses
Code refactoring is a fundamental practice in software engineering, in which a program is restructured without changing the actions it performs and the results it produces. To carry out refactoring with confidence, one requires a formal method for verifying that two programs are equivalent. Guarded Kleene Algebra with Tests (GKAT) provides such a framework, an algebraic system designed to reason about a natural class of programs, namely those in which every branch and loop is governed by a Boolean condition, such as if–else and while statements. Central to GKAT is a finite set of algebraic axioms for deriving program equivalences. …
A Nonstandard Exploration Of Approximate Identity And Unitization, Tong (Nicole) Wu
A Nonstandard Exploration Of Approximate Identity And Unitization, Tong (Nicole) Wu
HMC Senior Theses
The goal of this senior thesis is to explore general nonstandard analysis and some possible applications to 𝐶*-algebras in functional analysis. More specifically, we shall define an approximate identity of a 𝐶*-algebra using nonstandard analysis and study nonstandard hulls of internal 𝐶*-algebra in the context of different unitizations. We shall also prove a few results for ideals in 𝐶*-algebra using nonstandard definitions of approximate identities. We shall also briefly discuss the history and developments of nonstandard analysis.
On Quantum Processes And The Epistemic Constraints, Varun Immanuel Premkumar Immanuel
On Quantum Processes And The Epistemic Constraints, Varun Immanuel Premkumar Immanuel
Electronic Theses & Dissertations (2024 - present)
This doctoral dissertation on the foundations of quantum theory tells the story of a conceptual protagonist I have called “Epistemic Constraint.” Here, epistemic constraints are the definite, intersubjectively agreeable, ordinary-language conditions under which experiments are described.
The usual formulation of the quantum measurement problem, which I call the Schrodingerian measurement problem, has the structure of an anomaly: if we take quantum theory at face value, we expect no definite values, and yet we see definite values in experiments. The responses to this problem have been either to solve it or to dissolve it. These responses, which have taken the form …
A Realizability Approach To Constructing Higher Types Via Classifiers, Benjamin Carrick Logsdon
A Realizability Approach To Constructing Higher Types Via Classifiers, Benjamin Carrick Logsdon
Dartmouth College Ph.D Dissertations
We construct an interpretation of higher types into Peano arithmetic, showing in particular that every model of PA is a model of higher types. This is a reversal of Gödel’s Dialectica construction. We also define the classifier degrees, a degree structure which subsumes the Turing degrees, the enumeration degrees, and the many-one degrees. The classifier degrees boast a rich structure and many well-behaved operations.
Computability Theoretic Aspects Of Profinite Groups And Models Of Presburger Arithmetic, Jason Block
Computability Theoretic Aspects Of Profinite Groups And Models Of Presburger Arithmetic, Jason Block
Dissertations, Theses, and Capstone Projects
Profinite groups, which are exactly the Galois groups, are all either finite or uncountable. However, all second countable profinite groups can be presented as the set of paths through a countable tree. We use these tree presentations to find upper bounds on the complexity of the existential theories of profinite groups, as well as to prove sharpness for these bounds. These complexity results enable us to distinguish the class of profinite groups that are isomorphic to a direct product of finite groups, for which we find an upper bound on the complexity of the entire first order theory. Additionally, given …
Mathematics And Determinism: Chaos, Quantum Mechanics, And The Limits Of Predictive Structure, Jackson T. Salumbides
Mathematics And Determinism: Chaos, Quantum Mechanics, And The Limits Of Predictive Structure, Jackson T. Salumbides
CMC Senior Theses
This thesis examines the relationship between mathematics and determinism by analyzing how chaos theory, quantum mechanics, and formal mathematical limits challenge traditional conceptions of predictability and causal structure. Chaos theory shows that deterministic systems can exhibit practical unpredictability due to sensitivity to initial conditions. Quantum mechanics introduces probabilistic outcomes that complicate deterministic interpretation, though alternative frameworks such as Bohmian mechanics and superdeterminism attempt to restore determinism at conceptual cost. Additionally, results from mathematical logic, including Gödel’s incompleteness theorems and Turing’s undecidability, demonstrate intrinsic limitations on what can be deduced or computed, even in fully deterministic systems. By synthesizing these areas, …
Studies On Convexity Of Dnf Formulae, Josue A. Ruiz
Studies On Convexity Of Dnf Formulae, Josue A. Ruiz
Electronic Theses & Dissertations (2024 - present)
In this dissertation, we investigate the problem of determining whether a Boolean formula given in disjunctive normal form (DNF) is convex. Although Boolean formulas have various applications, our research focuses on the practical application for rule-based access control policies, where policies are often expressed as a set of Boolean rules. Understanding the structural properties of such formulas is crucial for determining whether a policy can be efficiently represented within a specific access control model.
The main contribution of this research is the conception and analysis of convexity derived from the “gap problem.” In this context, convexity is characterized by the …
A Thesis, Or Digressions On Sculptural Practice: In Which, Concepts & Influences Thereof Are Explained, Set Forth, Catalogued, Or Divulged By Way Of Commentaries To A Poem, First Conceived By The Artist, Fed Through Chatg.P.T., And Re-Edited By The Artist, To Which Are Added, Annotated References, Impressions And Ruminations Thereof, Also Including Private Thoughts & Personal Accounts Of The Artist, Jaimie An
Masters Theses
This thesis is an exercise in, perhaps a futile, attempt to trace just some of the ideas, stories, and musings I might meander through in my process. It’s not quite a map, nor is it a neat catalogue; it is a haphazard collection of tickets and receipts from a travel abroad, carelessly tossed in a carry-on, only to be stashed upon returning home. These ideas are derived from much greater thinkers and authors than myself; I am a mere collector or a translator, if that, and not a very good one, for much is lost. I do not claim comprehensive …
Formalization Of A Security Framework Design For A Health Prescription Assistant In An Internet Of Things System, Thomas Rolando Mellema
Formalization Of A Security Framework Design For A Health Prescription Assistant In An Internet Of Things System, Thomas Rolando Mellema
Electronic Theses and Dissertations
Security system design flaws will create greater risks and repercussions as the systems being secured further integrate into our daily life. One such application example is incorporating the powerful potential of the concept of the Internet of Things (IoT) into software services engineered for improving the practices of monitoring and prescribing effective healthcare to patients. A study was performed in this application area in order to specify a security system design for a Health Prescription Assistant (HPA) that operated with medical IoT (mIoT) devices in a healthcare environment. Although the efficiency of this system was measured, little was presented to …
Towards Erasing The Distinction Between The Computational And Syntactic Accounts Of Scientific Theories, Timothy Luft
Towards Erasing The Distinction Between The Computational And Syntactic Accounts Of Scientific Theories, Timothy Luft
Theses
One of the main goals of philosophy of science is to give a proper account of scientific theories and their structure. One way that accounts of the structure of scientific theories can be distinguished is by the mathematical or logical structures that they involve. For instance, syntactic accounts of scientific theories hold that theories are axioms in a logical framework, whereas semantic accounts are more liberal in the range of mathematical and logical structures they take as pertinent to the structure of scientific theories. Paul Thagard (1988) offers a computational account of scientific theories, which holds that theories are complex …
Adaptive Neh With Constrained Nearest Neighbor Subtours For The Electric Vehicle Routing Problem With Time Windows, Andrew Struthers
Adaptive Neh With Constrained Nearest Neighbor Subtours For The Electric Vehicle Routing Problem With Time Windows, Andrew Struthers
All Master's Theses
The development of electric vehicles is currently considered one of the most innovative areas in manufacturing. Largely driven by the desire to reduce greenhouse emissions, electric vehicles are seen as a viable alternative to internal combustion engine cars. Starting from consumer cars, a dedicated effort is being made to translate this into commercial vehicles for freight and delivery. This research introduces a novel adaptive Nawaz, Enscore, Ham (NEH) algorithm with constrained nearest neighbor subtour (NEH-NN). This algorithm is tested on the standard benchmark problems in literature and used as a seed solution for the Genetic Algorithm (GA). The performance and …
Multiscale Modelling Of Brain Networks And The Analysis Of Dynamic Processes In Neurodegenerative Disorders, Hina Shaheen
Multiscale Modelling Of Brain Networks And The Analysis Of Dynamic Processes In Neurodegenerative Disorders, Hina Shaheen
Theses and Dissertations (Comprehensive)
The complex nature of the human brain, with its intricate organic structure and multiscale spatio-temporal characteristics ranging from synapses to the entire brain, presents a major obstacle in brain modelling. Capturing this complexity poses a significant challenge for researchers. The complex interplay of coupled multiphysics and biochemical activities within this intricate system shapes the brain's capacity, functioning within a structure-function relationship that necessitates a specific mathematical framework. Advanced mathematical modelling approaches that incorporate the coupling of brain networks and the analysis of dynamic processes are essential for advancing therapeutic strategies aimed at treating neurodegenerative diseases (NDDs), which afflict millions of …
Soundness And Completeness Results For The Logic Of Evidence Aggregation And Its Probability Semantics, Eoin Moore
Soundness And Completeness Results For The Logic Of Evidence Aggregation And Its Probability Semantics, Eoin Moore
Dissertations, Theses, and Capstone Projects
The Logic of Evidence Aggregation (LEA), introduced in 2020, offers a solution to the problem of evidence aggregation, but LEA is not complete with respect to the intended probability semantics. This left open the tasks to find sound and complete semantics for LEA and a proper axiomatization for probability semantics. In this thesis we do both. We also develop the proof theory for some LEA-related logics and show surprising connections between LEA-related logics and Lax Logic.
Deep Learning Recommendations For The Acl2 Interactive Theorem Prover, Robert K. Thompson, Robert K. Thompson
Deep Learning Recommendations For The Acl2 Interactive Theorem Prover, Robert K. Thompson, Robert K. Thompson
Master's Theses
Due to the difficulty of obtaining formal proofs, there is increasing interest in partially or completely automating proof search in interactive theorem provers. Despite being a theorem prover with an active community and plentiful corpus of 170,000+ theorems, no deep learning system currently exists to help automate theorem proving in ACL2. We have developed a machine learning system that generates recommendations to automatically complete proofs. We show that our system benefits from the copy mechanism introduced in the context of program repair. We make our system directly accessible from within ACL2 and use this interface to evaluate our system in …
Reverse Mathematics Of Ramsey's Theorem, Nikolay Maslov
Reverse Mathematics Of Ramsey's Theorem, Nikolay Maslov
Electronic Theses, Projects, and Dissertations
Reverse mathematics aims to determine which set theoretic axioms are necessary to prove the theorems outside of the set theory. Since the 1970’s, there has been an interest in applying reverse mathematics to study combinatorial principles like Ramsey’s theorem to analyze its strength and relation to other theorems. Ramsey’s theorem for pairs states that for any infinite complete graph with a finite coloring on edges, there is an infinite subset of nodes all of whose edges share one color. In this thesis, we introduce the fundamental terminology and techniques for reverse mathematics, and demonstrate their use in proving Kőnig's lemma …
Asymptotic Classes, Pseudofinite Cardinality And Dimension, Alexander Van Abel
Asymptotic Classes, Pseudofinite Cardinality And Dimension, Alexander Van Abel
Dissertations, Theses, and Capstone Projects
We explore the consequences of various model-theoretic tameness conditions upon the behavior of pseudofinite cardinality and dimension. We show that for pseudofinite theories which are either Morley Rank 1 or uncountably categorical, pseudofinite cardinality in ultraproducts satisfying such theories is highly well-behaved. On the other hand, it has been shown that pseudofinite dimension is not necessarily well-behaved in all ultraproducts of theories which are simple or supersimple; we extend such an observation by constructing simple and supersimple theories in which pseudofinite dimension is necessarily ill-behaved in all such ultraproducts. Additionally, we have novel results connecting various forms of asymptotic classes …
Interpolation And Sampling In Analytic Tent Spaces, Caleb Parks
Interpolation And Sampling In Analytic Tent Spaces, Caleb Parks
Graduate Theses and Dissertations
Introduced by Coifman, Meyer, and Stein, the tent spaces have seen wide applications in harmonic analysis. Their analytic cousins have seen some applications involving the derivatives of Hardy space functions. Moreover, the tent spaces have been a recent focus of research. We introduce the concept of interpolating and sampling sequences for analytic tent spaces analogously to the same concepts for Bergman spaces. We then characterize such sequences in terms of Seip's upper and lower uniform density. We accomplish this by exploiting a kind of Mobius invariance for the tent spaces.
Applications Of Nonstandard Analysis In Probability And Measure Theory, Irfan Alam
Applications Of Nonstandard Analysis In Probability And Measure Theory, Irfan Alam
LSU Doctoral Dissertations
This dissertation broadly deals with two areas of probability theory and investigates how methods from nonstandard analysis may provide new perspectives in these topics. In particular, we use nonstandard analysis to prove new results in the topics of limiting spherical integrals and of exchangeability.
In the former area, our methods allow us to represent finite dimensional Gaussian measures in terms of marginals of measures on hyperfinite-dimensional spheres in a certain strong sense, thus generalizing some previously known results on Gaussian Radon transforms as limits of spherical integrals. This first area has roots in the kinetic theory of gases, which is …
Zariski Geometries And Quantum Mechanics, Milan Zanussi
Zariski Geometries And Quantum Mechanics, Milan Zanussi
Boise State University Theses and Dissertations
Model theory is the study of mathematical structures in terms of the logical relationships they define between their constituent objects. The logical relationships defined by these structures can be used to define topologies on the underlying sets. These topological structures will serve as a generalization of the notion of the Zariski topology from classical algebraic geometry. We will adapt properties and theorems from classical algebraic geometry to our topological structure setting. We will isolate a specific class of structures, called Zariski geometries, and demonstrate the main classification theorem of such structures. We will construct some Zariski structures where the classification …
Some Model Theory Of Free Groups, Christopher James Natoli
Some Model Theory Of Free Groups, Christopher James Natoli
Dissertations, Theses, and Capstone Projects
There are two main sets of results, both pertaining to the model theory of free groups. In the first set of results, we prove that non-abelian free groups of finite rank at least 3 or of countable rank are not A-homogeneous. We then build on the proof of this result to show that two classes of groups, namely finitely generated free groups and finitely generated elementary free groups, fail to form A-Fraisse classes and that the class of non-abelian limit groups fails to form a strong A-Fraisse class.
The second main result is that if a countable group is elementarily …
Alternative Cichoń Diagrams And Forcing Axioms Compatible With Ch, Corey B. Switzer
Alternative Cichoń Diagrams And Forcing Axioms Compatible With Ch, Corey B. Switzer
Dissertations, Theses, and Capstone Projects
This dissertation surveys several topics in the general areas of iterated forcing, infinite combinatorics and set theory of the reals. There are two parts. In the first half I consider alternative versions of the Cichoń diagram. First I show that for a wide variety of reduction concepts there is a Cichoń diagram for effective cardinal characteristics relativized to that reduction. As an application I investigate in detail the Cichoń diagram for degrees of constructibility relative to a fixed inner model of ZFC. Then I study generalizations of cardinal characteristics to the space of functions from Baire space to Baire space. …
Conjugacy Separability And Cyclic Conjugacy Separability Of Certain Hnn Extensions, Generalised Free Products And Tree Products, Hui Min Lim
Student Works (2020-2029)
In this thesis, we study two interrelated strong residually finite properties of groups, namely conjugacy separability and cyclic conjugacy separability. We extend them to certain HNN extensions, generalized free products and tree products where the associated subgroups and amalgamated subgroups are not necessarily cyclic. In the first part of the thesis, we consider HNN extensions. We begin by establishing two criteria, one for conjugacy separability and another for cyclic conjugacy separability. Using these two criteria we establish conditions for HNN extensions where the associated subgroups are central or they are a finite extension of a central subgroup or cyclic to …
Model Theory Of Groups And Monoids, Laura M. Lopez Cruz
Model Theory Of Groups And Monoids, Laura M. Lopez Cruz
Dissertations, Theses, and Capstone Projects
We first show that arithmetic is bi-interpretable (with parameters) with the free monoid and with partially commutative monoids with trivial center. This bi-interpretability implies that these monoids have the QFA property and that finitely generated submonoids of these monoids are definable. Moreover, we show that any recursively enumerable language in a finite alphabet X with two or more generators is definable in the free monoid. We also show that for metabelian Baumslag-Solitar groups and for a family of metabelian restricted wreath products, the Diophantine Problem is decidable. That is, we provide an algorithm that decides whether or not a given …
A Coherent Proof Of Mac Lane's Coherence Theorem, Luke Trujillo
A Coherent Proof Of Mac Lane's Coherence Theorem, Luke Trujillo
HMC Senior Theses
Mac Lane’s Coherence Theorem is a subtle, foundational characterization of monoidal categories, a categorical concept which is now an important and popular tool in areas of pure mathematics and theoretical physics. Mac Lane’s original proof, while extremely clever, is written somewhat confusingly. Many years later, there still does not exist a fully complete and clearly written version of Mac Lane’s proof anywhere, which is unfortunate as Mac Lane’s proof provides very deep insight into the nature of monoidal categories. In this thesis, we provide brief introductions to category theory and monoidal categories, and we offer a precise, clear development of …
Modest Automorphisms Of Presburger Arithmetic, Simon Heller
Modest Automorphisms Of Presburger Arithmetic, Simon Heller
Dissertations, Theses, and Capstone Projects
It is interesting to consider whether a structure can be expanded by an automorphism so that one obtains a nice description of the expanded structure's first-order properties. In this dissertation, we study some such expansions of models of Presburger arithmetic. Building on some of the work of Harnik (1986) and Llewellyn-Jones (2001), in Chapter 2 we use a back-and-forth construction to obtain two automorphisms of sufficiently saturated models of Presburger arithmetic. These constructions are done first in the quotient of the Presburger structure by the integers (which is a divisible ordered abelian group with some added structure), and then lifted …
Computable Reducibility Of Equivalence Relations, Marcello Gianni Krakoff
Computable Reducibility Of Equivalence Relations, Marcello Gianni Krakoff
Boise State University Theses and Dissertations
Computable reducibility of equivalence relations is a tool to compare the complexity of equivalence relations on natural numbers. Its use is important to those doing Borel equivalence relation theory, computability theory, and computable structure theory. In this thesis, we compare many naturally occurring equivalence relations with respect to computable reducibility. We will then define a jump operator on equivalence relations and study proprieties of this operation and its iteration. We will then apply this new jump operation by studying its effect on the isomorphism relations of well-founded computable trees.
Formally Verifying Peano Arithmetic, Morgan Sinclaire
Formally Verifying Peano Arithmetic, Morgan Sinclaire
Boise State University Theses and Dissertations
This work is concerned with implementing Gentzen’s consistency proof in the Coq theorem prover.
In Chapter 1, we summarize the basic philosophical, historical, and mathematical background behind this theorem. This includes the philosophical motivation for attempting to prove the consistency of Peano arithmetic, which traces itself from the first attempted axiomatizations of mathematics to the maturation of Hilbert’s program. We introduce many of the basic concepts in mathematical logic along the way: first-order logic (FOL), Peano arithmetic (PA), primitive recursive arithmetic (PRA), Gödel's 2nd Incompleteness theorem, and the ordinals below ε0.
In …