The thesis deals with definability of certain Zariski geometries, introduced by Zilber, in the theory of algebraically closed fields. I axiomatise a class of structures, called 'abstract linear spaces', which are a common reduct of these Zariski geometries. I then describe what an interpretation of an abstract linear space in an algebraically closed field looks like. I give a new proof that the structure "quantum harmonic oscillator", introduced by Zilber and Solanki, is not interpretable in an algebraically closed field. I prove that a similar structure from an unpublished note of Solanki is not definable in an algebraically closed field and explain the non-definability of both structures in terms of geometric interpretation of the group law on a Galois cohomology group H¹(k(x), μ_n). I further consider quantum Zariski geometries introduced by Zilber and give necessary and sufficient conditions that a quantum Zariski geometry be definable in an algebraically closed field. Finally, I take an attempt at extending the results described above to complex-analytic setting. I define what it means for quantum Zariski geometry to have a complex analytic model, an give a necessary and sufficient conditions for a smooth quantum Zariski geometry to have one. I then prove a theorem giving a partial description of an interpretation of an abstract linear space in the structure of compact complex spaces and discuss the difficulties that present themselves when one tries to understand interpretations of abstract linear spaces and quantum Zariski geometries in the compact complex spaces structure.

In 1942, Paul C. Rosenbloom put out a definition of a Post algebra after Emil L. Post published a collection of systems of many–valued logic. Post algebras became easier to handle following George Epstein’s alternative definition. As conceived by Rosenbloom, Post algebras were meant to capture the algebraic properties of Post’s systems; this fact was not verified by Rosenbloom nor Epstein and has been assumed by others in the field. In this thesis, the long–awaited demonstration of this oft–asserted assertion is given. After an elemental history of many–valued logic and a review of basic Classical Propositional Logic, the systems given by Post are introduced. The definition of a Post algebra according to Rosenbloom together with an examination of the meaning of its notation in the context of Post’s systems are given. Epstein’s definition of a Post algebra follows the necessary concepts from lattice theory, making it possible to prove that Post’s systems of many–valued logic do in fact form a Post algebra.

The survival of our nation, during a nuclear exchange, depends upon an effective national defense structure. The prime weapon system in this defense structure is the ballistic missile. Although many factors enter into an evaluation of the effectiveness of a ballistic missile, one of the most important measure is accuracy. Without an accurate weapon system we have no weapon system. The Department of Defense has places emphasis on using a method of accuracy evaluation called "Probably Circular Error (CEP)." Probably Circular Error is defined as "The radius of a circle, centered at the intended target, within which 50% of the missiles would be expected to impact" or "The probability is 0.50 that an individual missile will impact within a circle whose radius is equal to the CEP." The statistical techniques and assumptions used in generation a CEP value will be investigated.

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 a realistic theorem proving environment.

<p>Effective definedness checking is crucial for an implementation of a logic with undefinedness. The objective of the MathScheme project is to develop a new approach to mechanized mathematics that seeks to combine the capabilities of computer algebra systems and computer theorem proving systems. Chiron, the underlying logic of MathScheme, is a logic with undefinedness. Therefore, it is important to automate, to the greatest extent possible, the process of checking the definedness of Chiron expressions for the MathScheme project. This thesis provides an overview of information useful for checking definedness of Chiron expressions and presents the design and implementation of an AND/OR tree-based approach for automated definedness checking based on ideas from artificial intelligence. The theorems for definedness checking are outlined first, and then a three-valued AND/OR tree is presented, and finally, the algorithm for reducing Chiron definedness problems using AND/OR trees is illustrated. An implementation of the definedness checking system is provided that is based on the theorems and algorithm. The ultimate goal of this system is to provide a powerful mechanism to automatically reduce a definedness problem to simpler definedness problems that can be easily, or perhaps automatically, checked.</p> / Master of Science (MSc)

<p>In what is supposed to have been a radical break with neo-Hegelian idealism, Bertrand Russell, alongside G.E Moore, advocated the analysis of propositions by their decomposition into constituent concepts and relations. Russell regarded this as a breakthrough for the analysis of the propositions of mathematics. However, it would seem that the decompositional-analytic approach is singularly unhelpful as a technique for the clarification of the concepts of mathematics. The aim of this thesis will be to clarify Russell’s early conception of the analysis of mathematical propositions and concepts in the light of the philosophical doctrines to which his conception of analysis answered, and the demands imposed by existing mathematics on Russell’s logicist program. Chapter 1 is concerned with the conception of analysis which emerged, rather gradually, out of Russell’s break with idealism and with the philosophical commitments thereby entrenched. Chapter 2 is concerned with Russell’s considered treatment of the significance of relations for analysis and the overturning of his “doctrine of internal relations” in his work on Leibniz. Chapter 3 is concerned with Russell’s discovery of Peano and the manner in which it informed the conception of analysis underlying Russell’s articulation of logicism for arithmetic and geometry in PoM. Chapter 4 is concerned with the philosophical and logical differences between Russell’s and Frege’s approaches to logical analysis in the logicist definition of number. Chapter 5 is concerned with connecting Russell’s attempt to secure a theory of denoting, crucial to mathematical definition, to his decompositional conception of the analysis of propositions.</p> / Doctor of Philosophy (PhD)

<p>The purpose of this dissertation is to provide a proper treatment for two groups of logical paradoxes: semantic paradoxes and set-theoretic paradoxes. My main thesis is that the two different groups of paradoxes need different kinds of solution. Based on the analysis of the diagonal method and truth-gap theory, I propose a functional-deflationary interpretation for semantic notions such as ‘heterological’, ‘true’, ‘denote’, and ‘define’, and argue that the contradictions in semantic paradoxes are due to a misunderstanding of the non-representational nature of these semantic notions. Thus, they all can be solved by clarifying the relevant confusion: the liar sentence and the heterological sentence do not have truth values, and phrases generating paradoxes of definability (such as that in Berry’s paradox) do not denote an object. I also argue against three other leading approaches to the semantic paradoxes: the Tarskian hierarchy, contextualism, and the paraconsistent approach. I show that they fail to meet one or more criteria for a satisfactory solution to the semantic paradoxes. For the set-theoretic paradoxes, I argue that the criterion for a successful solution in the realm of set theory is mathematical usefulness. Since the standard solution, i.e. the axiomatic solution, meets this requirement, it should be accepted as a successful solution to the set-theoretic paradoxes.</p> / Doctor of Philosophy (PhD)

In this thesis we present a framework for automatic formal analysis of competitive stochastic systems, such as sensor networks, decentralised resource management schemes or distributed user-centric environments. We model such systems as stochastic multi-player games, which are turn-based models where an action in each state is chosen by one of the players or according to a probability distribution. The specifications, such as “sensors 1 and 2 can collaborate to detect the target with probability 1, no matter what other sensors in the network do” or “the controller can ensure that the energy used is less than 75 mJ, and the algorithm terminates with probability at least 0.5'', are provided as temporal logic formulae. We introduce a branching-time temporal logic rPATL and its multi-objective extension to specify such probabilistic and reward-based properties of stochastic multi-player games. We also provide algorithms for these logics that can either verify such properties against the model, providing a yes/no answer, or perform strategy synthesis by constructing the strategy for the players that satisfies the specification. We conduct a detailed complexity analysis of the model checking problem for rPATL and its multi-objective extension and provide efficient algorithms for verification and strategy synthesis. We also implement the proposed techniques in the PRISM-games tool and apply them to the analysis of several case studies of competitive stochastic systems.

The analysis of variance technique is probably the most popular statistical technique used for testing hypotheses and estimating parameters. Eisenhart presents two classes of problems solvable by the analysis of variance and the assumption underlying each class. Cochran lists the assumptions and also discusses the consequences when these assumptions are not met. It is evident that if all the assumptions are not satisfied, the confidence placed in any result obtained in this manner is adversely affected to varying degrees according to the extent of the violation. One of the assumptions in the analysis of variance procedures is that of uncorrelated errors. The experimenter may not always meet this conditions because of economical or environmental reasons. In fact, Wilk questions the validity of the assumption of uncorrelated errors in any physical situation. For example, consider an experiment over a sequence of years. A correlation due to years may exist, no matter what randomization technique is used, because the outcome of the previous year determines to a great extent the outcome of this year. Another example would be the case of selecting experimental units from the same source, such as, sampling students with the same background or selecting units from the same production process. This points out the fact that the condition such as background, or a defect in the production process may have forced a correlation among the experimental units. Problems of this nature frequently occur in Industrial, Biological, and Psychological experiments.

I explore five topics in topology using set-theoretic techniques. The first of these is a generalization of 2-point sets called slice sets. I show that, for any small-in-cardinality subset A of the real line, there is a subset of the plane meeting every line in a topological copy of A. Under Martin's Axiom, I show how to improve this result to any totally disconnected A. Secondly, I show that it is consistent with and independent of ZFC to have a topologically rigid subset of the real line that is smaller than the continuum. Thirdly, I define and examine a new cardinal function related to cleavability. Fourthly, I explore the Toronto Problem and prove that any uncountable, Hausdorff, non-discrete Toronto space that is not regular falls into one of two strictly-defined classes. I also prove that for every infinite cardinality there are precisely 3 non-T1 Toronto spaces up to homeomorphism. Lastly, I examine a notion of dimension called the "neight", and prove several theorems that give a lower bound for this cardinal function.