
Principia Mathematica anniversary symposiumEvent summary2010 was the hundredth anniversary of WhiteheadandRussell's Principia. A symposium was held to mark the occasion at the College where the authors were working.
As can probably be discerned from the list of speakers, this meeting was intended to address a broad range of interests: history, foundational mathematics, philosophy, type theory and mechanical theoremproving. The organisers hoped that the symposium would be valuable to people interested in the intersection of these areas, or in relevant subbranches of each area, and that practitioners and students alike would benefit from attending this meeting.
The redacted delegate list can be downloaded here.
Programme
Acknowledgements
The organisers thank the following for their financial or organisational help:
Archive for Mathematical Sciences & Philosophy;
Ms Shirley Bidgood;
British Logic Colloquium;
British Society for the Philosophy of Science;
Cambridge University Press;
Computer Laboratory, Cambridge;
Prof. Neil Dodgson;
Mr Hiro Funakoshi;
Ms Tanya Hall;
Mr Tim Hennock;
Dr Sean Holden;
Morgan Phoa Family Fund;
Microsoft Research;
Ms Carol Nightingale;
Dr Arthur Norman;
Prof. Hugh Osborn;
StudentRun Computing Facility;
Trinity College;
Trinity Mathematical Society;
Mr Michael Wright;
Mr Edward Yang.
Mailing listPlease join our mailing list for more information/discussion.ContactFor further information, or to offer feedback, please contact the organisers:
Abstracts'Logicism in the context of the development of set theory', Ivor GrattanGuinness
Set theory began to be developed on a large scale from the late 1890s onwards; for example, it was part of the mathematical logic that grounded logicism, and for convenience much of Principia mathematica was elaborated in its terms. Several different parts and features of set theory became prominent, and logicism was supposed to embrace all of them. In practice, though, how many did it tackle?
Download timeline and summary. 'The Impact of Principia Mathematica on Computer Science', Robert Constable
I intend to stress the theme that programming languages, starting with Algol 60, introduced a notion of type related to PM that has steadily worked its way deep into the design philosophy of programming languages and into the logics that are used in CS to reason about them. The programming logics arising from CS are distinct from those originating in mathematics and logic because they must deal with partial functions.
Download article. 'Foundations and Language', Mohan Ganesalingam
Principia Mathematica revolutionised our understanding of the nature of
mathematics by showing that mathematics could be put on an objective
footing. Today mathematicians still write mathematics in a largely
informal language, but have a tacit consensus that the underlying content
exists in formal representation like that of the Principia. We show how
one can bridge the gap between these informal and formal representations.
Download article and slides. 'On the cruelty of really doing formal proofs', John Harrison
Principia Mathematica inspired many developments in logic and the
philosophy of mathematics, yet it also acquired a negative reputation
in some quarters. Russell himself in his autobiography remarked that
his intellect "never quite recovered from the strain" of writing it,
while others were repelled by headline comments about their taking
400 pages to prove 1+1=2.
However, thanks to the rise of the computer, we can now contemplate
checking or even generating formal proofs of a size and intricacy
that would have been quite impractical for anyone to do by hand,
with practically perfect reliability. Formal proof in the Principia
style can now be regarded not merely as an ideal but unrealistic
theoretical possibility, but as a practical way of improving the
reliability of proofs, either in mathematics or computer science and
engineering.
In my talk I will describe some of the successes of computerchecked
formal proof and the challenges that remain.
Download slides. 'Automating the ramified theory of types of Principia', M. Randall Holmes
We have formalized the type system implicit in the Principia Mathematica of Russell and Whitehead
(it is nowhere actually presented in a completely formal manner, but
the intention can be deduced) and developed a typechecking
program for propositions and terms. In keeping with the approach
taken in Principia, the types inferred from a term are the most
general types possible. A curious feature, unusual in the context of
type inference, is that reasoning about arithmetic inequalities'
has to be implemented to handle orders. We have begun to develop a
formalization of reasoning in the logic of the Principia and will
discuss this if time permits.
Download article and slides. 'Principia's Types and Orders in Logic and Mathematics', Fairouz Kamareddine
In Russell's Ramified Type Theory RTT as presented in Principia
Mathematica, two hierarchical concepts dominate: orders and types. In
this talk we reflect on the lessons learned from orders and types and on
the progress in the formalisation of mathematics since the work of
Frege, Russell, Whitehead and others. In particular we reflect on how
mathematicians and logicians still use types differently and how types
and orders have developed since Russell to accommodate the formalisation
of mathematics and logic.
Download article. 'Typical ambiguity', Michael Potter
Despite initial appearances, there are actually very few theorems in Principia
Mathematica. This is because of typical ambiguity: most of the strings of signs
which look like theorems only become so once the ambiguities have been
resolved. I shall discuss whether we should care about this.
'The Logic of Classes of the Noclass Theory', Byeonguk Yi
This paper examines the noclass theory of Principia Mathematica. By
drawing the scope distinction for class terms, it argues that the theory
fails to preserve the logic of classes. And the paper presents a
modification of the theory, the plural noclass theory, that resolves
logical problem of PM's theory, and preserves the logic of classes. Then
the paper argues that the plural noclass theory does not yield the view
that there are no classes, but the view that classes can be identified
as propositional functions (or properties) of a special kind, namely,
the predicative ones.
Download article. 