On Tue, Apr 29, 2014 at 5:51 AM, Bill Richter <rich...@math.northwestern.edu
> wrote:
<snip>
>
> Here's a more substantive point that's always bothered me. Suppose if one
> is working in one's preferred logical framework (e.g. ZFC), and one engages
> in metamathematics. On what grounds to we believe the metamathematics?
> The point of ZFC was to foundationalize our mathematics, so what justifies
> our ``reasoning about the deductive system''? I speak in ignorance of
> Mathematical Logic here of course, and also with the bias of Pure
> Mathematics, which tends to not think that Mathematical Logic provides any
> firm foundations of math anyway. To me, Math Logic, HOL, Voevodsky's new
> HoTT/UF, are fantastic ways to remove the human error from proof checking,
> but they aren't ways to put our math on firm foundations, so that our
> theorems become truly true.
>
For your interest in firm foundations for mathematics, I suggest you read
about "Hilbert's program", e.g.
http://plato.stanford.edu/entries/hilbert-program/ or perhaps even
https://en.wikipedia.org/wiki/Hilbert's_program as online points of entry.
If you get into this I think it may give you quite a bit of historical
perspective on the development of foundations for math.
About ZFC (and other forms of set theory such as NBG), one of the
attractions is that much of the metamathematics is in fact the
metamathematics of first-order logic, as set theory is generally formalized
as FOL plus some set theory axioms. The basic metamathematics is about
objects such as terms and formulas. Is it much more complicated to you than
reasoning about strings of characters in some alphabet for example?
Cheers,
Cris
------------------------------------------------------------------------------
"Accelerate Dev Cycles with Automated Cross-Browser Testing - For FREE
Instantly run your Selenium tests across 300+ browser/OS combos. Get
unparalleled scalability from the best Selenium testing platform available.
Simple to use. Nothing to install. Get started now for free."
http://p.sf.net/sfu/SauceLabs
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
