Home

Practical Set Theory

Steven Kieffer, Jeremy Avigad, Harvey Friedman (2008). A language for mathematical knowledge management. Carnegie-Mellon tech. report CMU-PHIL-181.

The authors present a compact language for articulating mathematics, PST, which is syntactic sugar for an extension of Zermelo-Frankel set theory, DZFC, previously proposed by Harvey Friedman, which allows the naming of partially defined functions. The article gives some examples which show how for some mathematics, PST allows rather straightfoward expression. The article also gives some statistics gathered from an encoding of Suppes' Set Theory and Munkres' Topology, showing how PST allows a drastic compression compared to plain first-order ZFC.

By Charles Stewart at 2008-07-23 12:08 | Theory | other blogs | 8656 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Ontic

It would be interesting to have some insights into how this relates to Ontic, which is also a language for mathematical knowledge management that purports to have the expressive power of ZFC.

By Paul Snively at Wed, 2008-07-23 15:25 | login or register to post comments

Proofless text

In terms of its aims, this is close to the kind of thing Mizar is about, namely being a representation of mathematical reasing that can be read by humans and verified by machine. It follows in the spirit of Friedman's proofless text, where proofs are series of mathematical statements, either introducing definitions or making assertions that directly follow from previous statements, without the manner of the inference being specified.

I haven't looked at Ontic closely enough to grasp what McAllester is trying to to achieve with it, but the representation does not look condensed enough for it to be a good candidate for this kind of use. There may be some connection between the way that Ontic makes use of nondeterminism and the way PST makes use of underspecified definitions.

Postscript: See correction below: neither PST nor proofless text (as its name suggests) are proposed as formalisms for automatic validation. I still assert that PST and proofless text are closer to Mizar in spirit than to other formalisms for representing mathematics.

By Charles Stewart at Thu, 2008-07-24 10:30 | login or register to post comments

Mizar, Isar and proofless text

It seems to me that proofless text is a language for expressing definitions and assertions and does not cover proofs. The "Practical Set Theory" article talks about definitions only. I would not say that it is a representation of mathematical reasoning that can be verified by a machine. Mizar and Isabelle's Isar (and I guess Ontic) are formal proof languages that allow to write and verify definitions and theorems, where a theorem is an assertion with the accompanying proof.
The human readable rendering of PST is impressive and it would be interesting to see PST expanded to cover proofs as well.

By slawekk at Thu, 2008-07-24 22:58 | login or register to post comments

Correction

Apologies, this is right: PST is intended only to record mathematical knowledge, not to validate it. I had been confused by remarks suggesting this work was partly realising the aims of Friedman's comments in Automated Proof Checking.

The semidecidability of DZFC should suffice to ensure that PST texts cannot be automatically validated.

By Charles Stewart at Fri, 2008-07-25 08:44 | login or register to post comments

A comparison of Mizar and Isar

Wenzel and Wiedijk (2002). A comparison of Mizar and Isar. Journal of Automated Reasoning 29, 389-411.

From the introduction:

The aims of this paper are:

  • To compare the Mizar and Isar proof languages. We demonstrate
    the similarity between proofs in these two languages through a
    simple example from number theory (Sections 2 and 3), but we
    also show that the internal principles of processing those proofs
    are significantly different in both systems (Section 5).

  • To compare the Mizar and Isar systems from the experience of the
    end-user. We give a high level comparison of the Mizar and Isar
    systems from a user’s point of view, by pointing out the relative
    strengths and weaknesses of both systems (Section 4).

  • To attract more attention to declarative provers. The declarative
    proof style of the Mizar and Isar languages can draw more people to formal proofs. The small example that we present in both
    languages acts as a gentle introduction to declarative proof.

By Charles Stewart at Fri, 2008-07-25 09:16 | login or register to post comments