User jessealama - MathOverflow

Answer by jessealama for What are some other uses for Ehrenfeucht-Fraïssé games?

2013-01-15T01:30:52Z

These games have many uses. I think they're a lot of fun, but proofs that Duplicator has a winning strategy tend to get tedious quickly. Several applications are given (either in the body of the text or as exercises) in Elements of Finite Model Theory by Libkin. One application of E-F games that I like: to show that in first-order logic with equality and a single unary relation symbol R there is no sentence such that for all structures A the sentence holds in A iff the cardinality of the interpretation of R in A is even. Lots of other "cardinality properties" can be similarly shown with E-F games to be undefinable in FOL, such as FOL's inability to capture that the cardinality of the interpretation of two unary relations R and S are equal (in the finite case, without regard for the infinite case). In my Ph.D. dissertation I applied E-F games to a fun little example in the same spirit: given a first-order signature with three unary relation symbols V, E, and F, one cannot give a formula that captures the class of structures A for which V^A - E^A + F^A = 2. That is to say, in a suitable sense Euler's polyhedron formula cannot be captured in FOL.

Answer by jessealama for Has anyone thought about creating a formal proof wiki with verifier?

2013-01-12T02:54:59Z

As part of the MathWiki project at Radboud University Nijmegen (The Netherlands), a wiki for Mizar and for Coq-CoRN wiki were built. Concerning Brouwer's fixed-point theorem, for example, see the entry BROUWER in the Mizar wiki.

Answer by jessealama for When are two proofs of the same theorem really different proofs

2013-01-11T22:40:46Z

The other posters have well pointed out that the proof identity problem can be approached from various directions. If you're interested in proof theory and are willing to delve into natural deduction and category theory, you might be interested in two proposals for addressing the proof identity problem: the Normalization Conjecture and the Generality Conjecture. See Dozen's "Identity of proofs based on normalization and generality" for a nice introduction to these two ways of viewing the proof identity problem.

Answer by jessealama for How do proof verifiers work?

2013-01-11T22:30:31Z

You ask how proof verifiers work, but it seems you are asking a somewhat more precise question: how do proof verifiers based on various higher-order logics work? If you are interested only in classical first-order logic (or less, e.g., propositional logic), then you don't need to worry about higher-order issues. (There are important caveats. For example, the expressiveness of plain first-order logic has limits that you might consider unwelcome for various purposes, such as its inability to capture, e.g., reachability in a graph.) The Mizar system, for example, is based on classical first-order logic plus (a rather strong) set theory.

Answer by jessealama for Do you know any good introductory resource on sequent calculus?

2013-01-11T22:18:06Z

I second here the recommendations of Troelstra and Schwichtenberg's Basic Proof Theory for learning sequent calculus because of its exercises; focus on chapter 3 and do the exercises to get a good grip on standard sequent calculi for classical and intuitionistic logic, as well as get some exposure to a few variations (e.g., single-sided calculi). von Plato and Negri's Structural Proof Theory is also very good, but it is more of a monograph than a textbook (there are no exercises). In von Plato and Negri you will find detailed and systematic discussion of the relationship between natural deduction and sequent calculi throughout the book, a discussion that is is largely missing from Troelstra and Schwichtenberg (though it must be said that T and S do prove that various sequent calculi are equivalent with natural deduction and with certain Hilbert/Frege-style proof systems).

Answer by jessealama for Sequent calculus: is there a complete linear reasoning (i.e., no trees)?

2013-01-11T16:42:16Z

By "linear" do you mean (following Smullyan and Craig) that all rules have one premise? If so, I have nothing to add. But if you're willing to relax this requirement, there's another sense of "linear reasoning" that can be found in discussions of linear refinements of resolution. Linearity in this context means that every application of resolution is such that one of the (two) premises was derived immediately before the conclusion. Here one deals with trees, but of a very limited kind. There are completeness theorems for such restrictions of resolution (see, e.g., Donald Loveland's Automated Theorem Proving: A Logical Basis).

Comment by jessealama

2013-01-15T12:08:59Z

You may also consider working wit prenex formulas rather than arbitrary formulas. One can then formulate tableau rules that avoid branching. See, e.g., chapter 10 section 2 of Smullyan's First-Order Logic.