Workshop Miscellany

Norm Megill
nm at alum dot mit dot edu

This page was part of an informal talk I gave at the AWARD-2003 Workshop on Jul. 12, 2003. My other (main) talk was "Orthomodular Lattices and Beyond" (PDF slide show) given on Jul. 11. (To make the slide show, I used the command "pdflatex megillaward2003.tex".)

Back to the AWARD-2003 Workshop page.
And the AWARD-2004 Workshop page.

These are a few miscellaneous things you can explore at your leisure.


1. Quick overview of Metamath web site. If this page is down, select another mirror site.

2. Open problem: Does a single axiom (e.g. Sheffer-stroke) exist for weakly orthomodular lattices (WOML)? Related question: will one side of this single axiom evaluate to 1? (I haven't been able to find a WOML-law equivalent without this property, so if that is not the case that would be interesting to me.)

3. Kalmbach's CN (implication, negation) quantum propositional calculus with modus ponens as sole rule of inference. Open problems: (1) independence of axioms; (2) more elegant, shorter axiomatization; (3) is A16 needed for completeness? (4) is the system D-complete? (5) is there a single axiom!? Another note on Kalmbach's system is here.

4. Using the standard three classical propositional calculus axioms, here are condensed detachment proofs of the 193 propositional calculus theorems in Principia Mathematica. Open problem: Are these the shortest proofs? Update 4-May-04: Greg Bush has found shorter proofs for 67 of these. See this note.

5. The 3-variable (weak) orthoarguesian law ax-3oa can be derived from the modular law av(b^(avc))=(avb)^(avc) added to an OL. Open problem: can the standard orthoarguesian law ax-4oa be derived from the modular law + OL?

6. The Arguesian law is the same as the orthoarguesian law in the form of oa6 with its 3 hypotheses removed. It has been proved to be strictly stronger than the modular law, and the modular law can be derived from it. Open(?) problem: does there exist a finite ortholattice that is modular but non-Arguesian? [This lattice might also answer the previous question (5)].

7. Open problem: can Godowski's 3-variable equation (see slide 17 in my AWARD-2003 Workshop presentation (PDF)) be derived from OL + modular law? How about the 4-, 5-,... variable versions? How about the new equation (32) in slide 17?

8. A short equivalent of the Axiom of Choice. Open problem: Does a shorter equivalent (expressed in first-order logic primitives) exist? (Here's a another cute version using some abbreviations.) Update 6-May-04: In April 2004, Kurt Maes found a version of the Axiom of Choice that has about the same length. More importantly, his version has only 5 quantifiers in prenex normal form, setting a new record. See this theorem ackm.

9. Metamath's axiom system. If the apparent willy-nilly mixing of free and bound variables confuses you, read this. Open problems: (1) Are the axioms for predicate calculus independent? (2) Can the axiomatization be simplified?

9a. The open problem stated in Remark 9.5 on p. 16 (PDF p. 17) of "A Finitely Axiomatized Formalization of Predicate Calculus with Equality" is still open. In terms of Metamath's axiom system, the problem asks whether ax-11 can be proved from ax-1 through ax-10, ax-12 through ax-15, ax-mp, and ax-gen, and no others. It should be noted that any specific instance of ax-11, where phi is replaced with a subformula containing only set (meta)variables but no wff (meta)variables, is provable from the others mentioned.

10. A weak deduction theorem for classical propositional calculus. Example of its use. Open problem: In quantum propositional calculus, the standard deduction theorem fails (and so does this weak deduction theorem). What kind of "weak" deduction theorems are possible?

11. Axiomatization for complex numbers. Open problem: are the axioms independent?

12. Consider the "pure" fragment of Metamath axiom system, ax-1 through ax-7 (and ax-mp, ax-gen). Open problem: Can this fragment directly prove all such theorem schemes of its kind*, i.e. is it complete for this fragment? (I think so.) [* No predicate symbols, no distinct variable restrictions.] Possible clue (suggested by Bob Meyer): this fragment seems analogous to modal logic S5 (or monadic predicate calculus), extended by introducing the second variable y in ax-7.

13. Set theory can be added to standard first order logic without equality by making epsilon the only primitive predicate and introducing equality as a defined symbol. The usual axioms of equality then become theorems of set theory (see comments under the Axiom of Extensionality). This provides a system that is quite beautiful from a minimalist point of view. However, in Metamath's axiom system predicate calculus there is no primitive notion of proper substitution, and additional equality axioms serve this role (see the definition of proper substitution and related theorems). So dispensing with equality would almost certainly require some additional axioms with epsilon, beyond Extensionality, to fill the gap. Problem: What would a "nice" set of epsilon-only axioms look like? (The existing axioms could be expanded with the definition of equality, of course, but they would be long and ugly with possible redundancies.) Philosophical problem: Would these additional axioms be part of set theory or logic? If they are considered part of logic, in what ways does such a "minimal" predicate calculus, with a single arbitrary binary predicate calculus, differ from standard predicate calculus? How much of proper substitution is "pushed" into set theory, and what is the character of the non-set-theory part left over?

14. In this bizarre formalization of set theory axioms with no distinct variable restrictions, is the "Axiom of Twoness" essential for completeness? (I think so.)

15. Stuff related to the OI3 conjecture (slide 22 of PDF file Orthomodular Lattices and Beyond) [whose solution will earn a $100 prize (slide 23)]:

  1. As a "sanity check" it might be useful to show Otter can prove OI3 from OA3+OML. The proof is relatively simple (for Otter too, I think) and is shown in Th. 4.10, p. 26, of http://xxx.lanl.gov/abs/quant-ph/0009038.
  2. It might be interesting to see which of the known implications on slide 26 of http://www-unix.mcs.anl.gov/~mccune/award-2003/megill.pdf that Otter is able to do. Some are easy, but others seemed tricky (to do by hand anyway). I can provide the proofs of any of them if desired.
  3. I would be interested in seeing a proof of (or counterexample to) any of the open implication directions on slide 26, such as 48+OML => 47 or 45+OML => 49. (If a counterexample is found, that would of course also disprove the OI3 conjecture and be eligible for the prize.)
  4. I would also be interested in any combinations of equations in slide 26 that together might produce others, in directions that are currently unknown. For example, can OML+46+49+53 prove 44?
  5. The equations in slide 26 that aren't known OA3 equivalents are 45, 46, 47, 48, 49, 50, 51, and 53. It would be interesting to see if any equations in this set, or even all of them together, could (when added to OML) prove the equation of slide 24. (The equation of slide 24 can be derived from OA3+OML.) It would not solve the OI3 conjecture but might provide further clues.

16. (Predicate calculus) In A Note on the (Metamath) Axioms, 3rd paragraph, an open problem is whether "E.x4 x4 = x4" can be proved from "E.x3 x3 = x3" in the absence of ax-9. Or expressed as a Metamath problem: can

|- E.x x = x   =>   |- E.y y = y

be proved without using ax-9? To play with this problem, you can add this to the end of set.mm (or somewhere after ax-17): 

 ${
    exeqid.1 $e |- E. x x = x $.
    $( Open problem 16 in award2003.html $)
    exeqid $p |- E. y y = y $=
      ? $.
 $}

To make sure ax-9 was not used in your proof, use the metamath program command "show trace_back exeqid /essential /axioms".