Profile

Cover photo
Carl Hewitt
Works at iRobust
Lives in Silicon Valley
66,262 views
AboutPosts

Stream

Carl Hewitt

Shared publicly  - 
 
The list moderator censored the following post.

To: Foundations of Mathematics<fom@cs.nyu.edu>

Dear Monroe,
 
In Computer Science, we need very strong foundations for mathematics so that our computer systems are not handicapped.  Consequently, having the Use Theorem rule is highly valuable. For example, the Use Theorem rule is essential to Natural Deduction and is used in many mathematical proofs including the proof of consistency of mathematics.  We would have inconsistency if Gödel’s result held that mathematics cannot prove its own consistency if it is consistent. It is important not to have inconsistencies in mathematical foundations of Computer Science because they represent security vulnerabilities.
 
Of course, since there are uncountably many propositions (e.g. one for each real number), it is not possible to code them using natural numbers.
 
Large cardinals are not fundamental to Computer Science and consequently theories of large cardinals do not belong in the mathematical foundations of Computer Science.  On the other hand, being able to reason about theories is of fundamental importance.  The existence of nonstandard models of first-order Peano axioms (with infinite numbers) represents a severe defect for using these axioms in the mathematical foundations of Computer Science.
 
Cheers,
Carl
 
PS.  I have attached the article with the above results that will be presented at IR’14.
 
From: Monroe Eskew [mailto:meskew@math.uci.edu]
Sent: Monday, June 09, 2014 11:50
To: Carl Hewitt
Subject: Re: [FOM] Panel on "Inconsistency Robustness in Foundations of Mathematics" at IR'14 (http://ir14.org)
 
Dear Carl,
 
I remember perplexing myself with a similar argument during my first quarter in grad school.  The resolution is that the “Use Theorem” rule as you call it is not valid in the kinds of systems to which Godel’s theorem applies.  In a first-order system, we refer to propositions indirectly by coding them as natural numbers.  The faithfulness of the coding to its intended meaning may fail in nonstandard models.  This is of course a meta-statement and cannot be expressed within the first-order system.  Godel’s argument generates many concrete examples of statements P such that the statement, “There is x coding a proof of #P” does not imply P modulo the axioms.  
 
If \Phi(x) is the formula for there is no proof of sentence x in PA, and \sigma is a sentence is given by the fixed point lemma, so that PA proves "\sigma iff \Phi(#\sigma)", then PA does not prove “If #\sigma is provable then \sigma.”
 
If you think PA is a bad example because it is weak, note that Godel’s theorem applies to very strong systems such as ZFC + large cardinals.  You can do a lot of math there, some would say all.
 
Monroe
1

Carl Hewitt

Shared publicly  - 
 
The list moderator censored the following post.

To: Foundations of Mathematics<fom@cs.nyu.edu>

Dear Marcin,
 
Thanks for your remark and your question.
 
I agree that Gödel’s proof has been very well checked for correct reasoning.  However, things could still go wrong:
      1)  Gödel’s proof makes assumptions that are undesirable for Computer Science.  For example, the assumption that propositions are countable is inconsistent with there being a distinct proposition for each real number such that the proposition holds for only that number.
       2) Gödel’s proof makes assumptions that result in contradiction. For example, the proof assumes the existence of self-referential sentences constructed using fixed points on an untyped grammar for mathematical sentences. Simply checking the proof for correctness will not reveal a contradiction in the assumptions.
       3) There is a simple proof of the consistency of mathematics which contradicts the thrust of Gödel’s original result that powerful systems like Principia Mathematica cannot prove their own consistency.
 
The IR'14 conference paper maintains all three of the above do in fact hold.
 
With respect to your question, see page 32 of the following:
              Morris Kline. Mathematical Thought from Ancient to Modern Times Oxford University Press, 1990.
 
Cheers,
Carl
 
-----Original Message---
From: fom-bounces@cs.nyu.edu[mailto:fom-bounces@cs.nyu.edu] On Behalf Of Marcin Mostowski
Sent: Sunday, June 08, 2014 15:55
To: Foundations of Mathematics
Subject: Re: [FOM] Panel on "Inconsistency Robustness in Foundations of Mathematics" at IR'14 (http://ir14.org)
 
Dear all,
 
I have two things related to the message by Carl Hewitt, one remark and a question.
 
Remark:
 
You write: "Was Wittgenstein after all correct that Gödel’s proof is erroneous because inconsistency results from allowing self-referential sentences constructed using fixed points for an untyped grammar of mathematical sentences?"
 
You have two isomorphic reasonings. One about numbers and one rather logical. The first one was very well checked and we have very good reasons to accept it as a correct reasoning. The claim that the second one is incorrect seems to be a simple mistake. I do not see any use of discussing the issue.
 
Question:
 
You write: "Perhaps the first foundational crises was due to Hippasus “for having produced an element in the universe which denied the…doctrine that all phenomena in the universe can be reduced to whole numbers and their ratios.” Legend has it because he wouldn’t recant, Hippasus was literally thrown overboard to drown by his fellow Pythagoreans."
 
Have you any good historical reference to the story? I agree that it was one of crucial points in our intellectual history.
 
Marcin Mostowski
 
 
_____________________________________________
FOM mailing list
FOM@cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/fom
1

Carl Hewitt

Shared publicly  - 
 
Wikipedia does not like Inconsistency Robustness

Section was remove.  See link below.
3
1
Marius Buliga's profile photo
 
Types are better than sets for foundations of programming.

Harvey Friedman wrote:
  "Henk Barendregt wrote:
    'Now a Foundation of Mathematics has as task to be able to represent proofs, so that others can check them. Set theory is a very awkward theory to represent computations.'
  Can't we simply prove outright that all formalisms, including ZFC with abbreviation power, represent large computations awkwardly?
  If so, awkwardness of representing computations would not be a credible consideration in choice of foundations."
 
Types are better than sets a a foundation for programming, which is why widely-used programming languages are based on types and use type-parametrized sets and lists as data types.

On the other hand programming languages using sets as the foundation
have failed to gain traction because of the following limitations:
·  Lack of support for type and interface abstractions
·  Lack of efficiency
1

Carl Hewitt

Shared publicly  - 
 
Re: Categorical Sets for Computer Science
To: Foundations of Mathematics
Cc:  Dana Scott, Vladik Kreinovich,  Mitchell Spector, Harvey Friedman

Mitchell Specter wrote:
    >Yes, as Scott said, a theory of types appears to be needed to escape the paradoxes (while still having an interestingly large mathematical universe).
 
    >This shows a compelling foundational feature of ZF: a theory of types, in the form of well-ordered set-theoretic ranks, arises naturally and elegantly, emerging surprisingly from simply stated and straightforward properties of the membership relation.
 
On the other hand, sets can be categorically axiomatized by a unique isomorphism as follows:
   1) Natural numbers can be categorically axiomatized by a unique isomorphism  [Dedekind 1888, Peano 1889].
   2) Function types can be categorically axiomatized by a unique isomorphism using types as follows:
   Order 0 is type of functions from
        natural numbers to natural numbers
   Order i+1 is type of functions from
         natural numbers joined with functions of order i to natural numbers joined with functions of order i
   3) A set is defined by the type of a characteristic function from above
 
The above sets suffice for ordinary mathematics.

Categoricity proves that the above sets have been adequately and precisely axiomatized.
 
Of course, the above sets are not going to satisfy fans of large cardinals ;-)
 
There is a more technical exposition of the above in an article on my website at http://consistency.carlhewitt.info
1

Carl Hewitt

Shared publicly  - 
 
IR’14 Panel on “Inconsistency Robustness in Cyberspace Security and Privacy” http://ir14.org

This panel will discuss current issues in cyberspace security and privacy grounded in an ongoing saga including the following hypotheses about the future and recent events:
 · Computation and storage on phones, personal computers, etc. can be made more trustworthy (e.g., secure, reliable, robust, and resilient) than on large datacenters (Amazon, Google, Microsoft, NSA, etc.).  Mass cyberspace surveillance can be made uneconomical by greater endpoint security for phones, personal computers, etc.
 · Public key encryption communication will become ubiquitous.  Trans-national directories will be created to enable authentication of public keys. NSA has targeted for surveillance parties communicating using encryption (with keys not available to NSA) and stored their communications forever.
 · Criminals (including in government) should be brought to justice.
 · Law enforcement will increasingly rely on cell tower tracking, automobile tracking, ubiquitous video tracking (including drones) using facial recognition in public places.
 · Surveillance and remote attacks via the Internet are almost universal, whether by nation states, corporations, or others. Whistleblowers are persecuted everywhere. Reporters who refuse to reveal their sources are being jailed. Journalists and publishers have been subject to government surveillance in their purely investigative and reporting activities.
 · In US, leakers to the press have been dealt long prison sentences based on the justification that leaking to the press is espionage for a foreign power. These leakers have not been allowed to raise whistleblower defenses at their trials.
 · In US, the Constitution is the ultimate law of the land.    
 · US companies face diminished foreign business prospects because US claims jurisdiction (in secret using gag orders) over foreign operations of US companies. CEOs of major tech companies have complained loudly about how NSA surveillance has been ruining their business. Facebook founder and CEO Mark Zuckerberg recently called the US a “threat” to the Internet, and Google Board Chair Eric Schmidt called some of the NSA tactics “outrageous” and potentially “illegal”. Governments can issue (unexplained) gag orders to Internet companies that they surrender their encryption keys and any other data they possess both domestically and in other countries. “It is not blowing over,” said Microsoft General Counsel Brad Smith, adding “In June of 2014, it is clear it is getting worse, not better.”
 · Governments are preparing military offensive and defensive forces for devastating massive cyberwar attacks that can be delivered without prior detection.  Offensive retaliation is often challenged by not being certain of the identity of attacker(s). Greater endpoint security could mitigate the dangers of such attacks.
 · Al Gore proclaimed that the Internet is a “stalker economy.” Almost all consumers have Internet services (e.g. Internet search, email, etc.) paid by exploiting (and even selling) their personal information and attention. Unlike credit information, personal information held by Internet service companies does not have to be revealed to consumers. In “Why we fear Google”, Axel Springer CEO Mathias Döpfner recently declared,
“Nobody knows as much about its [users] as Google. Even private or business emails are read by Gmail [arbitrary server programs without legal restriction]. You [Eric Schmidt] yourself said in 2010: ‘We [Google] know where you [Google users] are [and] where you’ve been. We can more or less know what you're thinking about.’ Are users happy with the fact that this information ... [can] end up in the hands of [government] intelligence services ...?”
 · Sir Martin Sorrell, CEO WPP (the world’s largest advertising company) recently declared:
“People understate the importance of Snowden and NSA.  [They] underestimate the impact on consumers.

We have been removing third-party networks for our sites, those ads are also data-gathering mechanisms. We want to be more respectful of privacy and also want to monetise our audiences our way. Being more focused on privacy is not bad for business, it can be good.”
 
What precise contradictions (including goals, norms, and values) are contained in the above information?  How can they be rigorously stated? (A very long-term goal is for computer systems to have a formal understanding of these contradictions.)
 
Please join us for an exciting discussion.
3
1
Marius Buliga's profile photo

Carl Hewitt

Shared publicly  - 
 
My interview at 40th anniversary of TCP/IP.
6
3
Harold Giménez's profile photoMarius Buliga's profile photo

Carl Hewitt

Shared publicly  - 
 
Panel on "Inconsistency Robustness in Foundations of Mathematics" at IR’14 (http://ir14.org)

This panel will discuss current issues in the history and practice of avoiding and repairing inconsistency in powerful mathematical systems grounded in an ongoing saga including the following:
    • Perhaps the first foundational crises was due to  Hippasus “for having produced an element in the universe which denied the…doctrine that all phenomena in the universe can be reduced to whole numbers and their ratios.”  Legend has it because he wouldn’t recant, Hippasus was literally thrown overboard to drown by his fellow Pythagoreans. 
    •  Frege expressed despair that his life work had been in vain when he received Russell’s letter with its revelation of the paradoxical set of all sets that are not members of themselves.
    •  Fearing that he was dying and the influence that Brouwer might have after his death, Hilbert [1928] fired  Brouwer as an associate editor of Mathematische Annalen because of “incompatibility of our views on fundamental matters”   (i.e. Hilbert ridiculed Brouwer for challenging the validity of the Principle of Excluded Middle).
    •  According to Church [1934]: “in the case of any system of symbolic logic, the set of all provable theorems is [computationally] enumerable...  any system of symbolic logic not hopelessly inadequate ... would contain the formal theorem that this same system ... was either insufficient [theorems are not computationally enumerable] or over-sufficient [that theorems are computationally enumerable means that the system is inconsistent]…This, of course, is a deplorable state of affairs... Indeed, if there is no formalization of logic as a whole, then there is no exact description of what logic is, for it in the very nature of an exact description that it implies a formalization. And if there no exact description of logic, then there is no sound basis for supposing that there is such a thing as logic.”  What is the way out of this fundamental paradox?
    •   Dana Scott [1967] claimed that “there is only one satisfactory way of avoiding the paradoxes: namely, the use of some form of the theory of types.”  But exactly which theory of types should be used?  Russell's ramified theory of types is generally regarded to be a failure.
    •   A paper presented at this conference challenges the validity of one of the most famous results of mathematical logic:  namely, Gödel’s result that mathematics cannot prove its own consistency. Currently there is an overwhelming consensus among professional working logicians that Gödel proved that mathematics cannot prove its own consistency if mathematics is consistent.  But could they be wrong?  Was Wittgenstein after all correct that Gödel’s proof is erroneous because inconsistency results from allowing self-referential sentences constructed using fixed points for an untyped grammar of mathematical sentences?

In each of the above cases, means were devised to avoid known inconsistencies while increasing mathematical power. What lessons can be drawn and how should they affect practice? 

Join us in an exciting discussion.
3

Carl Hewitt

Shared publicly  - 
 
Wikipedia censorship by David Eppstein

On Wikipedia, someone had the temerity to cite the following work that I have done  (which was immediately censored by David Eppstein who called it "crankery"):

== Hewitt on Wittgenstein ==
 
[[Carl Hewitt]] (2014) has proposed that Wittgenstein correctly argued that contradictions result from allowing self-referential sentences of the kind that Gödel constructed using fixed points on an overly-loose untyped grammar of mathematical sentences. Furthermore, Hewitt discovered a remarkably short proof that mathematics self-proves its own consistency; thereby further discrediting self-referential sentences.
 
* Carl Hewitt. "Formalizing common sense for scalable inconsistency-robust information integration using Direct Logic(TM) reasoning and the Actor Model" Inconsistency Robustness. College Publications. 2014.
1

Carl Hewitt

Shared publicly  - 
 
Computer systems are all about types for both programs and information.  Although there is some intellectual heritage from Russell and Church, types in Computer Science are more developed because they
* allow the type Any
* make extensive use of interface types
* have parametrized types with restrictions.
 
Jack Schwartz developed a programming language based on sets but it did not gain traction because it lacked type abstractions.
 
Zermelo made important contributions to axiomatizing the sets used in classical mathematics.  However, casting his axioms as a first-order theory is entirely inadequate for computer science because sets are not characterized up to isomorphism.  Computers need categorical axioms so they can be certain what is and what is not a set. Otherwise, there is potential for security violations.  See the article linked with this post for a proposal for categorical axioms for sets in Computer Science using types on page 11. Of course, there is no set corresponding to the type Any ;-)
2
1
neo anderson's profile photo
Story
Places
Map of the places this user has livedMap of the places this user has livedMap of the places this user has lived
Currently
Silicon Valley
Links
Links
Work
Employment
  • iRobust
    Board Chair, present
Basic Information
Gender
Other or Decline to State