MadMode

My quest to to find a good digital preservation technique for my college math and computer science notebooks has been rekindled most recently by idris and earlier by metamath and proofcheck.

Meanwhile, the IPython notebook with MathJax and FLiP makes for an interesting editing and collaboration tool.

Rendering Inference Rules with MathJax¶

This is a typical page of my notes:

Math and C.S. literature is traditionally written with \(\TeX\). I've used it only occasionally and reluctantly, by writing in HTML and converting, but but MathJax seems to do a great job of integrating it into the web.

The first definition on that page of number theory notes is "a divides b":

Using MathJax, I can get a pretty good rendition:

\(\operatorname{Def^n}\) \(a | b\) "a divides b"

Note: universe = \(\Bbb Z\)

\[ a|b \iff \exists k (b = ka)\]

I looked all over for a way to render bi-directional inference rules, but I could only find MathJax support for one direction:

\[ \frac{a|b}{\exists k (b = ka)}\]

Perhaps using this notation for "equivalent by definition" would be better than bi-directional implication in some ways, though it's not much better for visual pattern matching:

\[ a|b \equiv \exists k (b = ka)\]

Proofcheck: Formalizing TeX proofs with Morris Logic¶

The point is not just to render the notes nicely but to capture the knowledge in a way I (and my collaborators) can exploit by machine.

Proofs in the \(\TeX\) dialect in Bob Neveln's ProofCheck system can be checked by a few thousand lines of python code. The dialect imposes very little in the way of logical constraints over and above the way articles are typically written:

I tried to figure out how it works from the python source code but quickly got lost. While attempting a scala port (pfmorris) to sort out the latent types, I realized the python source wasn't the best explanation of what's going on. The common notions file explain the use of Morris Logic with second-order schemators and Hilbert's epsilon for indefinite description.

Working on the scala port got sufficiently repetetive and tedious that I wondered if automating it might work better. The byproduct is py2scala, which turns out to be more directly useful for python refactoring than porting. More on that in another episode, I hope.

Meanwhile, back to the quest to preserve my notebooks...

Natural Deduction and Fitch Diagrams¶

The notation I used for formal proofs throughout my time at U.T. Austin, and to this day for similar tasks, comes from the Philosophy 313K: Logic, Sets and Functions course. The instructors were Kant and Bonevac. I remember Kant giving most of the lectures, but Bonevac wrote the text:

The system is introduced on p. 98:

The idea of an axiomatic system is old, dating at least from the time of Euclid. The Stoics, who were Greek philosophers of the third century B.C. were the first logicians to organize logic aximatically. In contrast, natural deduction systems are relatively new; Gerhard Gentzen, a German logician, and Stanislaw Jaskowski, a Polish student of Jan Lukasiewicz, independently proposed the first natural deduction systems in 1934. The system of this book owes a great deal, as well, to innovations by the American logicians Willard van Orman Quine, Frederic B. Fitch, Donald Kalish and Richard Montague.

The history was lost on me at the time, but it took on practical relevance as I looked at metamath. I could read the proofs fairly well, but when I tried to write even a simple one, I was stuck. It wasn't until I discovered a natural deduction based metamath system that I realized the conventional metamath proofs are written Hilbert-style and the system I learned is a natural deduction system, and converting Hilbert-style to natural deduction is notoriously difficult.

The modern rendition of the text seems to be a more polished book, Deduction. The text isn't handy for me to link to, but the system seems to be based on fitch diagrams, which are supported by various tools around the web.

Consider the first example from chapter 4, Formal Proof, of the '86 text:

It looks like this in proofmood:

In their Input/Output syntax:

derivation = """
[ entails [ p & q entails q :& elim 2 ;p :& elim 2 ;q & p :& intro 3,4 ] ;(p & q) $ (q & p) :$ intro 2-5 ] !line_cnc5"""

Formal Logic in Python (FLiP)¶

I'm increasingly happy with the IPython notebook for immersive hypertext editing with integrated computation. I'd like to integrate it with the idris REPL, but meanwhile, a search for python and natural deduction turned up FLiP.

import * is usually not a good idea, but for interactive use, it makes sense:

from flip.logic.fol_session import *

Python syntax is used to enter formulas and proof steps. FLiP then generates a more traditional notation:

clear()
checkp(And(p, q), assume)

|p & q                    (0)  Assumption

After the assumption, we can apply some elimination and introduction rules:

apropos(And)

[('ai', ['m1', 'm2', 'And(m1,m2)']),
 ('aer', ['And(m1,m2)', 'm1']),
 ('ael', ['And(m1,m2)', 'm2'])]

rapply(ael, 0)
rapply(aer, 0)
rapply(ai, 1, 2)

|q                        (1)  And-Elimination (Left) (0)
|p                        (2)  And-Elimination (Right) (0)
|q & p                    (3)  And-Introduction (1) (2)

That much was pretty obvious, but to use subproofs, I had to read the documentation:

checkp(Impl(And(p, q), And(q, p)), impli, 0, 3)

(p & q) -> (q & p)        (4)  Implication-Introduction (0) (3)

The whole proof looks pretty much like the example from chapter 4:

pp()

|p & q                    (0)  Assumption
|q                        (1)  And-Elimination (Left) (0)
|p                        (2)  And-Elimination (Right) (0)
|q & p                    (3)  And-Introduction (1) (2)
(p & q) -> (q & p)        (4)  Implication-Introduction (0) (3)

Quantification, Rules, and a hint of Type Theory¶

This natural deduction system is not just propositional but first order, with quantification. The "hello world" example we used for semantic web research was socrates.n3:

\[ \operatorname{Man}(\operatorname{socrates}) \\ \forall x (\operatorname{Man}(x) \implies \operatorname{Mortal}(x))\\ \therefore \operatorname{Mortal}(socrates) \]

Kludging the naming a bit, it looks like this in FLiP:

clear()
Man = P
Mortal = Q
socrates = a

checkp(Man(a), given)
checkp(A(x, Impl(Man(x), Mortal(x))), given)
rapply(Ae, 1, a)
rapply(imple, 2, 0)

P(a)                      (0)  Given
Ax.(P(x) -> Q(x))         (1)  Given
P(a) -> Q(a)              (2)  A-Elimination (1), with a
Q(a)                      (3)  Implication-Elimination (Modus Ponens) (2) (0)

Using idris and dependent types is another episode altogether, but to give a hint...

We can state the theorem this way:

thm1 : {thing: Type} -> {Man, Mortal: thing -> Type}
        -> ((x: thing) -> (Man x -> Mortal x))
        -> (socrates: thing) -> (Man socrates)
        -> (Mortal socrates)

and the proof is really simple:

thm1 all_men_mortal socrates socrates_a_man =
  all_men_mortal socrates socrates_a_man

References¶

• Alps, Robert A., and Robert C. Neveln. 1981. “A Predicate Logic Based on Indefinite Description and Two Notions of Identity.” Notre Dame J. Formal Logic 22 (3): 251–263. doi:doi:10.1305/ndjfl/1093883460. http://projecteuclid.org/euclid.ndjfl/1093883460.
• Bonevac, Daniel. 1986. Proof: A Text for Philosophy 313K Logic, Sets and Functions. Austin, Texas: Department of Philosophy, The University of Texas at Austin.

cf. fs86 tag in my zotero library.