Logical Methods in the Humanities Workshop Abstracts Winter 2007

Philosophical considerations may have a role to play in an eventual solution to the Continuum Problem, since any solution will probably need to be accompanied by some analysis of what it is to be a solution. Conversely, the Continuum Problem presents philosophers with an importatnt case study.

The "official" Cabal philosophy has been dubbed "consciously naive realism". This was an appropriate attitude when the founding fathers were first laying down the new large cardinals/determinacy theory. One had the axioms; the important thing was to develop them. However, it may be useful now to attempt a more sophisticated realism, realated to meaning and evidence in mathematics. In particular, generic absoluteness (i.e. immunity to independence proof via forcing) is attractive as guide to theory choice.

Logic and foundations was an early interest of von Neumann, and he was part of the circle working on Hilbert's program. He was quick to grasp the significance of the incompleteness theorem, and continued to praise Gödel's achievement, but it seems to have ended his direct involvement with the field.

We will discuss various aspects of computable/constructive analysis, namely semantics, proofs and computations. We will present some of the problems and solutions of exact real arithmetic varying from concrete implementations, representations and algorithms to various models for real computation. We then put these models in a uniform framework using realisability, opening the door for the use of type theoretic constructions both in computing and reasoning about these computations. We will indicate that it is often natural to use constructive logic to reason about these computations.

I will show O'Connor's practical monadic implementation of exact real numbers in the Coq proof assistant --- an implementation of constructive type theory. This illustrates how constructive analysis can be used in computational machine verified proofs like the one of the Kepler conjecture.

There is now a web of conjectures which all suggests the same thing--that there is a conception of the universe of sets which yields both answers to all of the known unsolvable problems of set theory and which is compatible with all axioms of strong infinity. I shall discuss some of these conjectures and the prospects for proving them.

Around the mid-20th century, it seemed that analog computation had been eclipsed by digital computation. However, in the last few decades there has been a resurgence of interest in analog computing.

In the first, part of this talk, I will discuss analog computation in general, and try to explain this resurgence of interest.

In the second part, I will describe recent work by John Tucker (Swansea) and myself on fixed point semantics for analog networks of processors and channels containing streams of real numbers or other continuous data.

The mathematical core of Gödel's philosophical challenge is constitued by the incompleteness theorems when given in their "most satisfactory form", i.e., as Gödel saw it, when formal theories are characterized via Turing computability. As Turing machines codify human mechanical procedures (carried out without appealing to higher cognitive capacities) the question naturally arises, whether the theorems justify the claim that the human mind or intellect has mathematical abilities that are not shared by any machine. Turing admits that steps of "intuition" are needed to transcend particular formal theories; thus, there is a substantive point in contrasting Turing's views with Gödel;s assertion, "infinitely surpasses any finite machine". I analyze a seemingly common core that raises central issues in the foundations of mathematics and cognitive science.