Logic and Foundations Commons^™

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 …

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

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 ε₀.

In …

On The Conjugacy Problem For Automorphisms Of Trees, Kyle Douglas Beserra

Boise State University Theses and Dissertations

In this thesis we identify the complexity of the conjugacy problem of automorphisms of regular trees. We expand on the results of Kechris, Louveau, and Friedman on the complexities of the isomorphism problem of classes of countable trees. We see in nearly all cases that the complexity of isomorphism of subtrees of a given regular countable tree is the same as the complexity of conjugacy of automorphisms of the same tree, though we present an example for which this does not hold.

Transparency In Formal Proof, Cap Petschulat

Boise State University Theses and Dissertations

The oft-emphasized virtue of formal proof is correctness; a machine-checked proof adds greatly to our confidence in a result. But the rigors of formalization give rise to another possible virtue, namely clarity. Given the state of the art, clarity and formality are at odds: complexity of formalization obscures the content of proof. To address this, we develop a notion of proof strategies which extend the well-known notion of proof tactics. Beginning with the foundations of logic, we describe the methods and structures necessary to implement proof strategies, concluding with a proof-of-concept implementation in CheQED, a web-based proof assistant.