Wednesday, June 18, 2008

The Logic of Proof: Unifying Classical and Intuitionistic Logic

In a previous post, I mentioned Sergei Artemov. I've now read a couple of his papers there. His work is based in extending one particular modal logic, developed by Godel. Godel's logic introduces a "provability" operator. (More specifically, it takes the meaning of the modal "necessary" to be that a statement is provable.) Part of the purpose of this logic is to pin down the meaning of intuitionistic logic. To translate an intuitionistic statement into a classical statement, we add the provability operator in front of the entire formula and in front of every subformula. Take [] to be the provability operator. "P and Q" stated in intuitionistic logic translates to []([]P and []Q), which means "it is provable that both P and Q are provable." "P or Q" would translate to []([]P or []Q), "it is provable that either P is provable or Q is." And so on for larger statements. The strange altered of intuitionistic logic naturally arise from this. (It is also possible to add slightly less [] operators, interestingly.)

Artemov's main contribution is to provide an explicit provability logic: instead of just containing an operator "x is provable", we can say "y is a proof of x". This can be represented by [y]x (we just fill in the box that was left empty in Godel's original version). Godel was interested in finding such a logic, but had not provided a complete set of axioms for it. The explicit provability has some nice formal properties that implicit provability lacks, and those properties help to prove some tighter relationships between various logics.

No comments:

Post a Comment