Proof and Prejudice: Why Formalising doesn't make you a Formalist
Fenner Tanswell
Abstract:
The topic of this thesis is the relationship between formal and
informal proofs. Chapter One opens the discussion by examining what a
proof is, when two proofs are identical, what the purpose of proving
is and how to distinguish the two categories of proof. Chapters Two
and Three focus in on informal and formal proof respectively, with the
latter also including descriptions of various computational proof
checkers and the Formalist family of positions in the Philosophy of
Mathematics. In Chapter Four I look at the Formalisability Thesis,
that every informal proof corresponds to a formal proof, and argue
that this breaks apart into a weak and a strong reading. In Chapter
Five, I outline a simple mathematical problem and attempt the
practical process of formalisation, following which I consider the
decisions that were involved in doing so. Finally, in Chapter Six, I
use what was learned from the practicalities of formalisation to argue
in favour of the weak reading of the Formalisability Thesis, which I
take to be closely related to Carnapian explication, but against the
strong reading, which corresponds to the Formalists' approach to
formalisation.