The cut rule A => B, B=>C |- A=>C violates subformula property. A new cut elimination method (in particular a new proof of Herbrand's Theorem) is obtained here by "proof mining" (unwinding) from the familiar non-effective proof. That proof begins with extracting an infinite branch when the canonical search tree for a given formula of first order logic is not closed. Our reduction of a cut does not introduce new cuts of smaller complexity preserving instead only one of the branches.
Dynamic Topological Logics (DTLs) are propositional modal systems for reasoning about topological spaces under the action of a function or even non-axiomatizable. In this talk, we will consider the logic of arbitrary topological spaces, where f is taken to be a continuous function. One difficulty in studying these spaces is the absence of Kripke completeness, and we will give an example to show why this is the case. Then we will present non-deterministic semantics. Under these semantics, f is allowed to be a relation, so that time now looks more like a tree than a linear ordering. And yet, the logic we obtain is identical, because we force all formulas that we are interested in to be uniquely determined independently of the path we take through time. Best of all, Kripke semantics are complete under this interpretation. This has many applications, including a proof of axiomatizability of DTL and of completeness for metric spaces, which we will get into as time allows.
The sum of two periodic functions need not be periodic. Consider for example the sum of the functions sin(x) and sin(sqrt(2)x). Fortunately, such a sum is almost periodic and much of the (Fourier) theory of periodic funcitions carries over. Unfortunately, constructively matters are complicated by the fact that the almost periodic functions form an inseparable normed space. As such, it has been a challenge for constructive mathematicians to find a natural treatment of them. In this talk, we will present a simple constructive proof of Bohr's fundamental theorem for almost periodic functions which we then generalise to almost periodic functions as an example to indicate some problems and methods in constructive analysis, i.e. analysis with intuitionistic logic.
The lecture will be loosely based on my paper: Almost Periodic Functions, Consturctively
Although it is undecidable whether a first-order formula is provable in first-order logic, the problem of determining whether a finite sequence of first-order formulas is a first-order deduction is decidable. But the decidability of the correctness of a deduction comes too high of a cost: it takes too long to formalize an argument in proof systems such as natural deduction of Hilbert-style formalisms. In this talk, I will discuss the MIZAR project, which aims to formalize as much mathematics as possible in the MIZAR proof language. The MIZAR language is close enough to mathematical vernacular to express oneself fairly naturally, but it is still restricted enough that one can check fairly quickly the correctness of a proof expressed in the language. A goal of the MIZAR project is to formalize as much mathematics as possible, and there have already been a number of landmark results that have been entered into the MIZAR system. In this connection, I will discuss my current work on Euler's polyhedron formula ("V-E+F=2"), an outstanding mathematical theorem that has yet to be formalized. I will also discuss some epistemological aspects of the enterprise of computer proof-checking, such as whether a computer-checked formal proof can give certain or near-certain knowledge of its conclusion or is more securely known than any informal analogue of the formal proof. Another subject worth investigating is the social nature of mathematical knowledge, and what role humans have to play in a mathematical practice that includes computer-checked proofs. Finally, I will discuss the claim that set theory is a foundation for mathematics and how that can be evaluated thanks to formalization efforts such as MIZAR.
I will discuss a version of Takeuti's consistency proof for Pi^1_1 analysis which eliminates the use of ordinal notations.