In 1952, von Neumann (and Pauli) forcefully rejected Carnap's proposal to distinguish the logical from the physical concepts of infomation and entropy. This has remained somewhat of a mystery until now, but I claim an analysis of Gödel's Platonism provides a key to solving the dispute. Influenced by Szilard's famous treatment of Maxwell's demon, von Neumann physicalized epistemological concepts (like information), as is clear from his work on computers and cellular automata. But two hurdles stand in the way: 1. ordinary mathematics is "too big" for the real world (although maybe not in a "hyperuniverse"); 2. assuming it were physicalized anyway, mathematics is still not an empirical theory. Von Neumann actually realized the latter on other occasions, emphasizing that mathematics is essentially aesthetic. If Gödel's notion of mathematical intution were interpreted as the sense of beauty (i.e., that which lends conviction concerning mathematical processes and objects), then mathematics is modally different from empirical science. This justifies Carnap's (analytic-synthetic distinction and his) distinction between physical and logical theories of information -- because they differ modally --, but not his distinction between physical and logical concepts of information (other than that the logical concept is only explicit metatheoretically). Thus it seems that von Neumann and Carnap were thinking at cross purposes, although Carnap was marginally more correct.
This is an organizational meeting.
The theme of this year's logic seminar is mechanical proof-checking, computer assisted construction of proofs, and logical frameworks in which to carry these out. We will concentrate on Godel's incompleteness theorems as test cases. A computer checked proof of the first incompleteness theorem has been carried out by N. Shankar in the Boyer-Moore logic. No comparable proof has yet been given for the second incompleteness theorems. Some of the literature to be covered is:
Seminar leaders: S. Feferman and G. Mints
The theme of this year's logic seminar is mechanical proof-checking, computer assisted construction of proofs, and logical frameworks in which to carry these out. We will concentrate on Godel's incompleteness theorems as test cases. A computer checked proof of the first incompleteness theorem has been carried out by N. Shankar in the Boyer-Moore logic. No comparable proof has yet been given for the second incompleteness theorem.
A logical framework is a formal meta-language for deductive systems. The primary tasks supported in logical frameworks to varying degrees are:
This definition is due to Frank Pfenning (from the Logical Frameworks home page: http://www.lb.cs.cmu.edu/~fp/lfs.html).
I'll describe the main features of logical frameworks, how they are used, how to specify a logic and to do a proof in that logic. For definiteness, I will focus on the Isabelle framework, while making references to others where appropriate.
We present the details of the verification of a proof of Goedel's first incompleteness theorem constructed with the aid of the Boyer-Moore theorem prover. This two-part presentation summarizes the contents of the book "Metamathematics, Machines, and Goedel's Proof" (CUP, 1994). The first part introduces the background ideas and gives the details of the formal statement of the theorem. This statement asserts that a certain formal set theory (Cohen's Z2) is either inconsistent (admits proofs of some sentence and its negations) or incomplete (fails to prove some sentence or its negation). The second part [to take place on Tues. Nov. 9] is an outline of the steps in the mechanical verification. The entire verification involves over 2000 definitions and lemmas.