User matthew wampler-doty - MathOverflow

Bicartesian closed categories and Heyting algebras

2010-07-08T18:04:55Z

In Lambek and Scott's "Introduction to higher order categorical logic" (1988), they state that every Heyting Algebra can be understood as a bicartesian closed category.

On the other hand, fixing a bicartesian closed category, and using $A \cong B$ to denote that morphisms¹ exists between $A$ and $B$, we can see that every bicartesian closed category exhibits the intuitionistic equational axiomatization of a Heyting algebra. Specifically, we can observe that:

If $X \to Y \cong 1$ and $Y \to X \cong 1$ then $X \cong Y$
If $1 \to X \cong 1$ then $X \cong 1$
$X \to (Y \to X) \cong 1$
$(X \to (Y \to Z)) \to (X \to Y) \to (X \to Z) \cong 1$
$X \times Y \to X \cong 1$
$X \times Y \to Y \cong 1$
$X \to Y \to X \times Y \cong 1$
$X \to X + Y \cong 1$
$Y \to X + Y \cong 1$
$(X \to Z) \to (Y \to Z) \to (X + Y \to Z) \cong 1$
$0 \to X \cong 1$

Here $\to$ is an exponential, $\times$ is a product, and $+$ is a co-product, $1$ is a final object and $0$ is an initial object.

I cannot find the statement of this in Lambek & Scott, however. So I have two questions:

(A) Does this follow from some general theorem regarding bicartesian closed categories?
(B) Is this a folk theorem, or is there a place in the literature where this is established?

I originally wrote isomorphism here, but as Andreas Blass notes this is not true (for instance, in the category of sets). However, as noted below, this is true if we weaken the statement to equimorphic.

Answer by Matthew Wampler-Doty for Non-constructive proofs of decidability?

2010-07-08T18:24:19Z

There are lots of theories in model theory that can be proven to be decidable, in a non-constructive manner, by showing that a first order theory exhibits categoricity. One example that comes to mind the the theory of countable densely ordered fields (via Cantor's non-constructive proof that they are all isomorphic).

If one considers a decidable theory in stated in a a countable language, one can obtain a decidable set of numbers it corresponds to using Gödel numbering; ie, $\{\ \overline{\phi} \ |\ T \vdash \phi\}$. If the proof that the theory was non-constructive, then the decidability of the corresponding set of Gödel will also be non-constructive.

Answer by Matthew Wampler-Doty for How do they verify a verifier of formalized proofs?

2010-07-07T02:15:31Z

You are asking a lot of great questions:

[Are computer proof assistants] any use for a mathematician like me?

Yes. Here is how these systems can help you:

On a very basic level, these systems prevent you from making mistakes. Subsequently, it spares one from the peer review process. One of the proofs of Jordan Curve theorem was carried out by Thomas Hales, as part of his attempt to automatically verify the correctness of the Kepler Conjecture. Hales is basically resorting to automated theorem proving because he feels that his proof, which involves establishing that 50,000 linear programming problems are infeasible (last time I checked) cannot possibly be verified by human peer review.
Most systems (Coq, Isabelle, HOL-Light) built in automation. This helps to inform the informal notion that mathematicians have for what constitutes a trivial, mechanical derivation and what is nontrivial - my rule of thumb is, if a computer can't automatically derive a certain, it's probably something I should illustrate explicitly.
Isabelle/HOL lets you use the automated theorem provers E, SPASS and Vampire to automatically prove propositions, employing the entirety of Isabelle/HOL's Library at their disposal. As Isabelle's library grows, this gains more and more power.

But how to make sure that a machine verified the proof correctly?

As Neel Krishnaswami mentioned above, one way one may be convinced is to learn how to program in pure, functional programming languages such as OCAML or SML and read the source code of systems like HOL-light or Isabelle. In both of these systems I have mentioned, there is a file thm.ml that contains the declarations of theorem constructors. These systems also have facilities for declaring new types. HOL-Light has, along with the basic rules and type constructors, three axioms: extensionality (Liebniz's Law), the axiom of infinity and the axiom of choice.

Moreover, HOL-Light has been designed by it's author John Harrison to exhibit relative self-consistency proofs, just like in set theory. You may read about them here: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.97.2210&rep=rep1&type=pdf

Here Harrison shows HOL-Light$-$Infinity has a model in HOL-Light, and HOL-Light has a model in HOL-Light+Grothendiek Cardinal.

The definitions should be chosen carefully - I don't want to dig through a particular construction of the reals from rationals to make sure that this is indeed the reals that I know.

I assume you are aware that all complete ordered fields are isomorphic to one another? Isabelle/HOL happens to construct them using Cauchy sequences, and has in its library there is another formulation using Dedekind Cuts. HOL-Light formulates the positive reals using the limiting slopes of functions $f:\mathbb{N}\to\mathbb{N}$ and then constructs the full reals using a semi-ring completion. Since algebraically all of these formulations are provably isomorphic, in practice the details of their construction are hidden from the users.

Is there such a "dumb" system around? If yes, do formalization projects use it? If not, do they recognize the need and put the effort into developing it? Or do they have other means to make their systems trustable?

They all require training to learn. However, for LCF style systems like Coq, Isabelle, and HOL-Light, its like programming languages: once you learn one, you've learned the principles necessary to understand all of them.

Isabelle, and Mizar have special facilities for making proofs more "human". The system for Isabelle is called Isar. These systems aren't for dummies, sadly; one really needs a bit of special training to master them. On the other hand, they are much better than the "apply-style" proofs that are commonly employed, since they conform much better to human intuition. There's a systems for Coq called Caesar that in its infancy, but I expect it will ultimately make Coq much easier to use.

If the syntax is reasonable, it should be easy to write a program verifying that another stream of bytes represents a deduction of the stated theorem from the listed axioms. Can systems like Mizar, Coq, etc, generate input for such a program? Can they produce proofs verifiable by cores of other systems?

The short answer is YES, the long answer is YES, but it's complicated. Not all deductive systems have the same expressive power. Sets in ZFC are a special kind of object that one cannot construct in Higher Order Logic. To formulate set theory in Isabelle/HOL and HOL-Light use, one needs to postulate that a kind of object that makes true the axioms of Zermelo Fraenkel set theory exists (this is the route that Isabelle/HOLZF takes). On the other hand, one may embed HOL into ZFC without such difficulty - here is a paper where a translation system for Isabelle/HOL into ZFC is given using the theorem prover LF: http://kwarc.info/frabe/Research/RI_isabelle_10.pdf

Chantal Keller has imported HOL-Light into Coq in her MSc thesis here: http://perso.ens-lyon.fr/chantal.keller/Documents-recherche/Stage09/itp10.pdf

Importing back from Coq is difficult. Coq has a much more expressive type system than HOL.

HOL-Light and Isabelle/HOL can be inter-translated, however:

Isabelle/HOL to HOL-Light: http://www.cs.cmu.edu/~seanmcl/papers/modules.pdf
HOL-Light to Isabelle/HOL: http://www.springerlink.com/content/m7621r5258r8n711/

One cannot convert Mizar proofs to any other system because it is closed source, and does not have a small kernel one can use to produce proof code readable by other engines :(

Answer by Matthew Wampler-Doty for Is there any proof assistant based on first-order logic?

2010-07-07T01:01:21Z

Isabelle supports many different logics, and it has a formulation of first order logic which you may browse here: http://isabelle.in.tum.de/dist/library/FOL/index.html. However, even though proofs are natural deduction in flavor, it does not produce anything a logician would understand as a natural deduction derivation upon shallow inspection.

The automated theorem provers Prover9, E, SPASS and Vampire are all first order systems. They do not produce proofs using natural deduction (they are all typically resolution/paramodulation based systems).

It sounds like ProofWeb is exactly like what you want. It provides a system for displaying the accompanying natural deduction/sequent calculus proof along with a computer assisted formalization. It also has a really nice interactive interface for students, and provides the possibility of assigning exercises. On the other hand, I know that it has been largely developed for Coq, which is way, way more expressive than first order logic. And even though I know that there is a development of set theory within Coq, I suspect modifying the system for basic set theory would be a nontrivial exercise.

Answer by Matthew Wampler-Doty for Are there any good nonconstructive "existential metatheorems"?

2010-07-05T21:25:21Z

Arrow's Impossibility Theorem, from Social Choice Theory, provides an example of the sort of thing you're talking about: http://en.wikipedia.org/wiki/Arrow%27s_impossibility_theorem

Specfically, it reads:

For a finite set of individuals and alternatives, where there are at least three alternatives, then any social welfare function that satisfies unanimity and independence of irrelevant alternatives is a dictatorship

The proof may be carried out in higher order logic, employing two inductions. Here is a discussion of a formalization of the proof in Higher Order Logic, in the computer proof assistant Isabelle: http://www4.informatik.tu-muenchen.de/~nipkow/pubs/arrow.pdf

While the statement of the theorem is higher order, for a fixed number of individuals and a fixed number of alternatives it may be expressed in first order logic. Using our meta-theorem from higher order logic, and completeness of first order logic, we know in principle one should be able to prove in first order logic any of the relativisations of Arrow's impossibility theorem...

But actually constructing a proof in first order logic in practice is impossible. Here's a paper where the author provides a first order formulation of the problem and tried to hand it off to an automated theorem prover: http://staff.science.uva.nl/~grandi/Papers/GrandiEndrissLORI2009.pdf

In short, the computer produced a first order proof of the relativised Arrow's theorem for 2 agents and three alternatives in 3 hours, in approximately 200 steps. The author used the first order resolution/paramodulation based program Prover9, and mentioned to me he had somewhat more success with E and Vampire, two other automated proof systems. He also mentioned that, empirically, scaling the problem in either parameter lead to computation time that grew faster than exponential. So proving the theorem for 100000 individuals and 100000 alternatives in first order logic is beyond any person or machine.

TL;DR: Higher Order Logic/First Order completeness affords a metatheorem that all first order instances of Arrow's Impossibility Theorem must be provable in first order logic, but in practice producing a first order proof is transcomputable.

Answer by Matthew Wampler-Doty for The isomorphism inference rule

2010-07-05T20:00:05Z

The "isomorphism inference rule" can be understood in terms of the concept of elementary equivalence in model theory: http://en.wikipedia.org/wiki/Elementary_equivalence

The wikipedia article above discusses elementary equivalence for first order logic, but it may be generalised to higher order logic. Given a language $\mathcal{L}$ with semantics $\models$, two structures $\mathbb{M}$ and $\mathbb{N}$ are elementarily equivalent whenever for all $\phi \in \mathcal{L}$, $\mathbb{M} \models \phi$ holds if and only if $\mathbb{N} \models \phi$.

One can prove for first-order, second-order and higher order logic the following theorem:

if two structures are isomorphic, then they are elementarily equivalent

The proof almost always employs structural induction on the composition of formulae, making use of the fact that the semantics for various logics are usually defined compositionally using recursion. The converse of the above statement is not true in general.

Here is how we can apply the concept of elementary equivalence to the example provided. We can express in second order logic a formula $\phi$ such that $\mathbb{M} \models \phi$ if and only if $\mathbb{M}$ is a simple group. We then know that if $\mathbb{M} \cong \mathbb{N}$, then $\mathbb{M} \models \phi$ if and only if $\mathbb{N} \models \phi$. This means that if $\mathbb{M}$ and $\mathbb{N}$ are isomorphic, $\mathbb{M}$ is a simple group if and only if $\mathbb{N}$ is a simple group.

TL;DR: The "isomorphism inference rule" can be understood model theoretically in terms of elementary equivalence, and is a consequence of the compositionality of semantics.

Comment by Matthew Wampler-Doty

2010-07-07T14:12:21Z

One example of this is where Y is "first order tableaux proof systems" and "X" is the cut rule. In his paper "Don't Eliminate Cut", George Boolos gives a problem which a tableaux with the cut rule can prove in about a page of symbols, but without cut it takes more symbols than there are atoms in the universe. @Darsh - "Don't Eliminate Cut" shows the difficulty can indeed be "can't be done effectively in general" in some situations. Here's Boolos' paper: springerlink.com/content/pj2775t3j0435262