SAD as a mathematical assistant—how should we go from here to there?

The System for Automated Deduction (SAD) is developed in the framework of the Evidence Algorithm research project and is intended for automated processing of mathematical texts. The SAD system works on three levels of reasoning: (a) the level of text presentation where proofs are written in a formal natural-like language for subsequent verification; (b) the level of foreground reasoning where a particular theorem proving problem is simplified and decomposed; (c) the level of background deduction where exhaustive combinatorial inference search in classical first-order logic is applied to prove end subgoals.

We present an overview of SAD describing the ideas behind the project, the system's design, and the process of problem formalization in the fashion of SAD. We show that the choice of classical first-order logic as the background logic of SAD is not too restrictive. For example, we can handle binders like Σ or lim without resort to second order or to a full-powered set theory. We illustrate our approach with a series of examples, in particular, with the classical problem .     

Encoding Modal Logics in Logical Frameworks

We present and discuss various formalizations of Modal Logics in Logical Frameworks based on Type Theories. We consider both Hilbert- and Natural Deduction-style proof systems for representing both truth (local) and validity (global) consequence relations for various Modal Logics. We introduce several techniques for encoding the structural peculiarities of necessitation rules, in the typed -calculus metalanguage of the Logical Frameworks. These formalizations yield readily proof-editors for Modal Logics when implemented in Proof Development Environments, such as Coq or LEGO.     

Proof Nets for the Multimodal Lambek Calculus

We present a novel way of using proof nets for the multimodal Lambek calculus, which provides a general treatment of both the unary and binary connectives. We also introduce a correctness criterion which is valid for a large class of structural rules and prove basic soundness, completeness and cut elimination results. Finally, we will present a correctness criterion for the original Lambek calculus Las an instance of our general correctness criterion.     

Why Euclid’s geometry brooked no doubt: J. H. Lambert on certainty and the existence of models

J. H. Lambert proved important results of what we now think of as non-Euclidean geometries, and gave examples of surfaces satisfying their theorems. I use his philosophical views to explain why he did not think the certainty of Euclidean geometry was threatened by the development of what we regard as alternatives to it. Lambert holds that theories other than Euclid’s fall prey to skeptical doubt. So despite their satisfiability, for him these theories are not equal to Euclid’s in justification. Contrary to recent interpretations, then, Lambert does not conceive of mathematical justification as semantic. According to Lambert, Euclid overcomes doubt by means of postulates. Euclid’s theory thus owes its justification not to the existence of the surfaces that satisfy it, but to the postulates according to which these “models” are constructed. To understand Lambert’s view of postulates and the doubt they answer, I examine his criticism of Christian Wolff’s views. I argue that Lambert’s view reflects insight into traditional mathematical practice and has value as a foil for contemporary, model-theoretic, views of justification.