User matthew wampler-doty - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-21T20:46:54Z http://mathoverflow.net/feeds/user/7348 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/31091/bicartesian-closed-categories-and-heyting-algebras Bicartesian closed categories and Heyting algebras Matthew Wampler-Doty 2010-07-08T18:04:55Z 2010-07-09T14:49:54Z <p>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.</p> <p>On the other hand, fixing a bicartesian closed category, and using $A \cong B$ to denote that morphisms<sup>1</sup> exists between $A$ and $B$, we can see that every bicartesian closed category exhibits the <a href="http://en.wikipedia.org/wiki/Heyting_algebra#Characterization_using_the_axioms_of_intuitionistic_logic" rel="nofollow">intuitionistic equational axiomatization</a> of a Heyting algebra. Specifically, we can observe that:</p> <ol> <li>If $X \to Y \cong 1$ and $Y \to X \cong 1$ then $X \cong Y$</li> <li>If $1 \to X \cong 1$ then $X \cong 1$</li> <li>$X \to (Y \to X) \cong 1$</li> <li>$(X \to (Y \to Z)) \to (X \to Y) \to (X \to Z) \cong 1$</li> <li>$X \times Y \to X \cong 1$</li> <li>$X \times Y \to Y \cong 1$</li> <li>$X \to Y \to X \times Y \cong 1$</li> <li>$X \to X + Y \cong 1$</li> <li>$Y \to X + Y \cong 1$</li> <li>$(X \to Z) \to (Y \to Z) \to (X + Y \to Z) \cong 1$</li> <li>$0 \to X \cong 1$</li> </ol> <p>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. </p> <p>I cannot find the statement of this in Lambek &amp; Scott, however. So I have two questions:</p> <p>(A) Does this follow from some general theorem regarding bicartesian closed categories?<br/> (B) Is this a folk theorem, or is there a place in the literature where this is established?</p> <hr> <p>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 <em>equimorphic</em>.</p> http://mathoverflow.net/questions/14918/non-constructive-proofs-of-decidability/31097#31097 Answer by Matthew Wampler-Doty for Non-constructive proofs of decidability? Matthew Wampler-Doty 2010-07-08T18:24:19Z 2010-07-08T18:24:19Z <p>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 <a href="http://en.wikipedia.org/wiki/Morley%2527s_categoricity_theorem" rel="nofollow">categoricity</a>. 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).</p> <p>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.</p> http://mathoverflow.net/questions/18421/how-do-they-verify-a-verifier-of-formalized-proofs/30846#30846 Answer by Matthew Wampler-Doty for How do they verify a verifier of formalized proofs? Matthew Wampler-Doty 2010-07-07T02:15:31Z 2010-07-08T15:18:35Z <p>You are asking a lot of great questions:</p> <blockquote> <p>[Are computer proof assistants] any use for a mathematician like me?</p> </blockquote> <p>Yes. Here is how these systems can help you:</p> <ul> <li><p>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.</p></li> <li><p>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.</p></li> <li><p>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.</p></li> </ul> <blockquote> <p>But how to make sure that a machine verified the proof correctly?</p> </blockquote> <p>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 <code>thm.ml</code> 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.</p> <p>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: <a href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.97.2210&amp;rep=rep1&amp;type=pdf" rel="nofollow">http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.97.2210&amp;rep=rep1&amp;type=pdf</a></p> <p>Here Harrison shows HOL-Light$-$Infinity has a model in HOL-Light, and HOL-Light has a model in HOL-Light+Grothendiek Cardinal.</p> <blockquote> <p>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.</p> </blockquote> <p>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. </p> <blockquote> <p>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?</p> </blockquote> <p>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.</p> <p>Isabelle, and Mizar have special facilities for making proofs more "human". The system for Isabelle is called <em>Isar</em>. 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 <em>Caesar</em> that in its infancy, but I expect it will ultimately make Coq much easier to use.</p> <blockquote> <p>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?</p> </blockquote> <p>The short answer is <strong>YES</strong>, the long answer is <strong>YES, but it's complicated</strong>. Not all deductive systems have the same expressive power. Sets in ZFC are a special kind of object that one cannot construct in <em>Higher Order Logic</em>. 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: <a href="http://kwarc.info/frabe/Research/RI_isabelle_10.pdf" rel="nofollow">http://kwarc.info/frabe/Research/RI_isabelle_10.pdf</a></p> <p>Chantal Keller has imported HOL-Light into Coq in her MSc thesis here: <a href="http://perso.ens-lyon.fr/chantal.keller/Documents-recherche/Stage09/itp10.pdf" rel="nofollow">http://perso.ens-lyon.fr/chantal.keller/Documents-recherche/Stage09/itp10.pdf</a></p> <p>Importing back from Coq is difficult. Coq has a much more expressive type system than HOL.</p> <p>HOL-Light and Isabelle/HOL can be inter-translated, however:</p> <ul> <li>Isabelle/HOL to HOL-Light: <a href="http://www.cs.cmu.edu/~seanmcl/papers/modules.pdf" rel="nofollow">http://www.cs.cmu.edu/~seanmcl/papers/modules.pdf</a></li> <li>HOL-Light to Isabelle/HOL: <a href="http://www.springerlink.com/content/m7621r5258r8n711/" rel="nofollow">http://www.springerlink.com/content/m7621r5258r8n711/</a></li> </ul> <p>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 :(</p> http://mathoverflow.net/questions/15689/is-there-any-proof-assistant-based-on-first-order-logic/30841#30841 Answer by Matthew Wampler-Doty for Is there any proof assistant based on first-order logic? Matthew Wampler-Doty 2010-07-07T01:01:21Z 2010-07-07T01:01:21Z <p><a href="http://isabelle.in.tum.de/" rel="nofollow">Isabelle</a> supports many different logics, and it has a formulation of first order logic which you may browse here: <a href="http://isabelle.in.tum.de/dist/library/FOL/index.html" rel="nofollow">http://isabelle.in.tum.de/dist/library/FOL/index.html</a>. 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.</p> <p>The automated theorem provers <a href="http://www.cs.unm.edu/~mccune/mace4/" rel="nofollow">Prover9</a>, <a href="http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html" rel="nofollow">E</a>, <a href="http://www.spass-prover.org/" rel="nofollow">SPASS</a> and <a href="http://www.voronkov.com/vampire.cgi" rel="nofollow">Vampire</a> are all first order systems. They do not produce proofs using natural deduction (they are all typically resolution/paramodulation based systems).</p> <p>It sounds like <a href="http://prover.cs.ru.nl/" rel="nofollow">ProofWeb</a> 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.</p> http://mathoverflow.net/questions/6250/are-there-any-good-nonconstructive-existential-metatheorems/30683#30683 Answer by Matthew Wampler-Doty for Are there any good nonconstructive "existential metatheorems"? Matthew Wampler-Doty 2010-07-05T21:25:21Z 2010-07-05T21:47:49Z <p>Arrow's Impossibility Theorem, from Social Choice Theory, provides an example of the sort of thing you're talking about: <a href="http://en.wikipedia.org/wiki/Arrow%27s_impossibility_theorem" rel="nofollow">http://en.wikipedia.org/wiki/Arrow%27s_impossibility_theorem</a></p> <p>Specfically, it reads:</p> <blockquote> <p>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</p> </blockquote> <p>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: <a href="http://www4.informatik.tu-muenchen.de/~nipkow/pubs/arrow.pdf" rel="nofollow">http://www4.informatik.tu-muenchen.de/~nipkow/pubs/arrow.pdf</a></p> <p>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...</p> <p>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: <a href="http://staff.science.uva.nl/~grandi/Papers/GrandiEndrissLORI2009.pdf" rel="nofollow">http://staff.science.uva.nl/~grandi/Papers/GrandiEndrissLORI2009.pdf</a></p> <p>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 <em>Prover9</em>, and mentioned to me he had somewhat more success with <em>E</em> and <em>Vampire</em>, 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.</p> <p>TL;DR: Higher Order Logic/First Order completeness affords a metatheorem that all first order instances of <em>Arrow's Impossibility Theorem</em> must be provable in first order logic, but in practice producing a first order proof is transcomputable.</p> http://mathoverflow.net/questions/28644/the-isomorphism-inference-rule/30660#30660 Answer by Matthew Wampler-Doty for The isomorphism inference rule Matthew Wampler-Doty 2010-07-05T20:00:05Z 2010-07-05T20:00:05Z <p>The "isomorphism inference rule" can be understood in terms of the concept of <em>elementary equivalence</em> in model theory: <a href="http://en.wikipedia.org/wiki/Elementary_equivalence" rel="nofollow">http://en.wikipedia.org/wiki/Elementary_equivalence</a></p> <p>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 <em>elementarily equivalent</em> whenever for all $\phi \in \mathcal{L}$, $\mathbb{M} \models \phi$ holds if and only if $\mathbb{N} \models \phi$.</p> <p>One can prove for first-order, second-order and higher order logic the following theorem:</p> <blockquote> <p><em>if two structures are isomorphic, then they are elementarily equivalent</em></p> </blockquote> <p>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.</p> <p>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.</p> <p>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. </p> http://mathoverflow.net/questions/6250/are-there-any-good-nonconstructive-existential-metatheorems/6255#6255 Comment by Matthew Wampler-Doty Matthew Wampler-Doty 2010-07-07T14:12:21Z 2010-07-07T14:12:21Z One example of this is where Y is &quot;first order tableaux proof systems&quot; and &quot;X&quot; is the cut rule. In his paper &quot;Don't Eliminate Cut&quot;, 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 - &quot;Don't Eliminate Cut&quot; shows the difficulty can indeed be &quot;can't be done effectively in general&quot; in some situations. Here's Boolos' paper: <a href="http://www.springerlink.com/content/pj2775t3j0435262/" rel="nofollow">springerlink.com/content/pj2775t3j0435262</a>