Almost from the inception of Hilbert's program, foundational and structural efforts in proof theory have been directed towards the goal of clarifying the computational content of modern mathematical methods. In this talk, I will survey some of the methods of extracting computational information from proofs in classical first-order arithmetic, and reflect on some of the relationships between them. I will also discuss the sense in which algorithms implicit in classical proofs are “nondeterministic”, and show that a variant of the Gödel-Gentzen double-negation translation provides a canonical and efficient computational interpretation of that theory.
Most of the action in modal logic has been in propositional systems, witness the Handbook of Modal Logic of 2006, where modal predicate logic gets only 1 chapter out of 21. In this talk, I look at modal predicate logic from mathematical perspectives developed for the propositional case, and briefly discuss: frame correspondence, deductive completeness & incompleteness, and finally, the question what sort of logical system ‘modal predicate logic’ really is: this is much less clear than it might seem at first sight.
What, if anything, can you do in linear time? Even sorting of n items requires n·log(n) time. Consider the derivability problem for a fixed logic: decide whether a given set of hypotheses entails a given formula (the query). A typical proof cannot be even written down in linear time.
The logic of interest to us is primal infon logic developed in connection with access control in decentralized computer systems. The problem of interest is multiple derivability: given a set of hypotheses and a set of queries, determine which of the queries follow from the hypotheses. It turns out that the multiple derivability problem for primal infon logic is solvable in linear time.
The talk is self-contained and does not presuppose the knowledge of infon logic or access control. We will try to shed some light on linear time computability. We will recall primal infon logic and explain the intuition behind the linear time result which is a joint work with Itay Neeman of UCLA.
Answer set programming (ASP) is a form of declarative programming oriented towards difficult combinatorial search problems. The semantics of ASP languages is an outgrowth of research on nonmonotonic reasoning, and the computational mechanisms of ASP are similar to those used in fast satisfiability solvers for propositional logic. Proofs of correctness of ASP programs involve distinctions introduced earlier in work on intuitionistic logic.
The purpose of this article is to argue that mathematical logic requires extension in order to express adequately common sense knowledge and reasoning. We propose some of the needed extensions.
Orlov first [1928] and Gödel later [1933] pointed out the connection between the Lewis System S4 and Intuitionistic Logic. McKinsey and Tarski gave an algebraic formulation and proved completeness theorems for propositional systems using as models topological spaces with the interior operator corresponding to the necessitation modality. Earlier, Tarski and Stone had each shown that the lattice of open subsets of a topological space models intuitionistic propositional logic. Expanding on a suggestion of Mostowski about interpreting quantifiers, Rasiowa and Sikorski used the topological models to model first-order logic. After the advent of Solovey's recasting of Cohen's independence proofs as using Boolean-valued models, topological models for modal higher-order logic were studied by Gallin and others. (This very, very brief history does not attempt to acknowledge legions of other researchers and investigations of logics other than S4.) For Boolean-valued logic, the complete Boolean algebra Meas([0,1])/Null of measurable subsets of the unit interval modulo sets of measure zero gives every proposition a probability. Perhaps not as well known is the observation that the measure algebra also carries a nontrivial S4 modality defined with the aid of the sublattice Open([0,1])/Null of open sets modulo null sets. This sublattice is closed under arbitrary joins and finite meets in the measure algebra, but it is not the whole of the measure algebra. Consideration of this model of modality brings up several questions: (1) What completeness results can be expected in the first- order case? (2) How does this model differ from models used by Montague and Gallin for higher-order logic? (3) In employing this model to interpret notions of extensional and intensional functions, what revision of the definition of a topos is appropriate? (4) What kind of definition of random real number should be chosen to go along with the inherent probability? (5) Will the measure-preserving automorphisms of the modal measure algebra give us a connection between properties of the logic and the results of Ergodic Theory?
Hindman's Theorem states that in every finite coloring of the integers, there is an infinite set such that all finite sums of elements are in the same color. A short, elegant proof can be given using the existence of an idempotent ultrafilter, an infinitary object which requires multiple applications of the Axiom of Choice. Many further results in Ramsey Theory have been proven on this model, often with no known proofs which do not require ultrafilters. As a result, these arguments go beyond the methods of second order arithmetic, and are largely inaccessible to proof theoretic and reverse mathematical techniques. As a first step towards a general method of interpreting these arguments in second order arithmetic, we show how to adapt the ultrafilter proof of Hindman's Theorem using "partial" descriptions of the topology of ultrafilters.