Logic Lunch Abstracts

Several new results, including (1) new axiom systems for several logical calculi and some algebraic structures, and (2) solutions to some open questions in algebra and quantum logic will be reported. Each of these was discovered using automated reasoning technqiues. Some discussion of the strategies and techniques will also be included.

We augment the language of set theory by variables for partial operations whose domains are subclasses of the class V of all sets, as well as by constants for specific such operations, depending on the theory of sets under consideration. Since operation variables and constants are identified with elements of V, self-application is possible. The minimal axioms for such are those of partial combinatory algebra. Other, more specifically set-theoretical operations which may be considered are pairing, union, power-set, etc. These permit more natural formulations of standard set-theoretical axioms, such as Replacement, which simply takes the form that the image of a set under any given operation is again a set. Here we have a single axiom in place of the usual scheme; the latter is a consequence by having sufficiently strong principles of operation construction. Another axiom which is more naturally formulated in operational terms is that of Choice in a global as well as local form.

Such an operational theory of sets has several applications. This talk will be devoted to one such, namely: Unified formulations of axioms of infinity. These may be given for various "small" large cardinal axioms (e.g. Mahlo, weakly compact, etc.), which are abstractly the same whether given for impredicative set theory with the power-set operation or admissible set theory without it. The latter replaces analogue formulations in terms of recursive functions on admissible sets. This is part of a program to generalize analogues of small large cardinals that have also been introduced in constructive set theory, explicit mathematics, and ordinal notation systems.

Mathematics and mathematical logic are supposed to rely on complete proofs. Such proofs are to be given by their authors, to be found by an automated deduction program or constructed manually using a proof-checking system. This contradicts practice: in mathematics most proofs are very far from being complete and verification of programs usually checks only ``principal'' parts. This practice is supported here by some existing and new theory.

In particular, a new kind of an ordinal assignment and termination proof for an epsilon substitution process in arithmetic is presented. It is based on a translation of stages of the substitution process into incomplete finite proofs describing some infinite derivations. The whole approach seems to extend easily to subsystems of second order arithmetic admitting proof-theoretical analysis.

The aim of this talk is to examine formal systems of infinitesimal (nonstandard) analysis in two contexts. First, considering classical measures of proof-theoretic strength, we exhibit a subsystem of infinitesimal analysis that is capable of proving a significant fragment of ordinary real analysis, and which has proof-theoretic strength equivalent to Elementary Function Arithmetic. Second, we look at applications of infinitesimal analysis in automated reasoning. In particular, we will survey work of Fleuriot and Paulson using infinitesimal analysis with the theorem prover Isabelle, and the work of Gamboa and Kaufmann using an extension of ACL2.