search

gleachkr / Carnap-Old

An interactive proof checker that runs in the browser
http://gleachkr.github.io/Carnap/
GNU General Public License v3.0
3 stars 0 forks source link

First Order Logic #3

Closed gleachkr closed 9 years ago

gleachkr commented 9 years ago

We want languages and proof systems for

  1. Monadic Predicate Logic
  2. Polyadic Predicate Logic
  3. FOL with equality and function symbols
gleachkr commented 9 years ago

As of 2191335f9f08653b0feb3be645588443253dcd6a, we have a proof system for polyadic predicate logic (with equality). Some minor tweaks will make it possible to add function symbols. To get the natural deduction interface to mirror the Kalish/Montegue/Hardegree rules will require a little extra work, since they use a version of existential elimination that doesn't mix will with the underlying representation of the proof as a tree. The current system mirrors theirs, except in its treatment of existential out, which is closer to Barwise and Etchemendy.

gleachkr commented 9 years ago

Some reflection suggests that the best way of handling the existential out issue will to write a new pair of modules analogous to proofTreeHandler and judgementHandler, for proof systems where the underlying proof is more like a Rose tree (with a natural ordering of the lines, and context for an inference provided by earlier lines, a la Montegue) and proof systems where the underlying proof is more like an unordered tree (with context for an inference provided by child nodes, a la Gentzen). We'll need to write two sets of inference rules for the two kinds of proof systems, but I think this is unavoidable.

Since we parse text into ProofTrees, which are only turned into something more abstract by the proofTreeHandler, and since we do the visual display in terms of ProofTrees, I think the (eventual) additions will be fairly local, and we won't need to significantly rewrite any parsers or display code.

So, this issue will be closed as soon as we've got FOL with function symbols and equality. The Kalish and Montegue systems will be a separate issue.

gleachkr commented 9 years ago

Provisionally closed by 0ddc5af4c9dca92da4071d41e36429dc0713453a.