[FOM] Inconsistent systems.
a.hazen at philosophy.unimelb.edu.au
Sun Oct 1 23:42:55 EDT 2006
Bill Taylor makes a:
>A brief inquiry.
>In the Lucas/Penrose thread, Panu Raatikainen said:
>> such distinguished logicians as Frege, Curry, Church, Quine, Rosser
>> and Martin-Lof have seriously proposed... theories that... turned out
>> to be inconsistent.
>I am aware of the cases of Frege and Quine, but not the others.
------Church published "A set of postulates for the foundations of
logic" in "Annals of Mathematics" vol. 33 (1932): inconsistent
system. (The lambda calculus was a consistent fragment.) Revised
version, ibid., vol. 34 (1933): inconsitent again. Finally "A proof
of freedom from contradiction," in "P.N.A.S." vol. 21 (1935),
proving that he had finally got it right. Gödel reviewed all three
papers, and there is a BIT more information in Kleene's
introduction to Gödel's reviews in vol. I of G's "Collected Works."
((((The final, consistent, version seems to me to bear comparison
with Myhill's idea of "levels of implication": cf. Myhill's
articles in "Synthese" vol. 60 (1984) and in the Fitch festsschrifft,
"The Logical Way of Doing Things" (I think that's the title) ed.
by A.R. Anderson, R.B. Marcus &....))))
------Curry had presented something inconsistent based on
combinators; it's inconsistency (and that of Church's original
version) was proven by Kleene and Rosser in "The inconsistency of
certain formal logics," in "Annals of Mathematics" vol. 36 (1935);
Curry's own paper of that title, in "JSL" vol. 7 (1942), extracts
the logical coreof their argument from the combinatory machinery: the
Curry Paradox. But see notes in Curry's "Combinatory Logic."
------Matin-Löf at some stage proposed an extension of his type
theory, with something like a "type of types": this fell to what is
known as Girard's Paradox.
------Rosser I'm not sure of.
University of Melbourne
More information about the FOM