6
\$\begingroup\$

This originally came from Give the best Chaitin incompleteness bound, but I realized that there was a fragment of this problem which still potentially gives a good coding challenge.

First Order Logic With Equality

First, I will need to fix an encoding of first order formulas ('For all x there exists y such that ...'). Since the standard symbols for the mathematical operations are not in ASCII, I will denote "for all" as @, "there exists" as #, "not" as !, "and" as &, "or" as |, "equals" as = and "implies" as >. A variable consists of v followed by an alphanumeric sequence. A function symbol is of the form f, followed by some nonnegative number of _'s, followed by an alphanumeric sequence. The number of underscores indicates the number of inputs to the function. A predicate symbol is of the from P followed by some number of underscores, followed by an alphanumeric name. To make actually putting this into a computer program a little easier, say that everything is in prefix notation, like Lisp.

Following the suggestion of Wheat Wizard, you are free to choose whatever symbols are to be used for 'for all', 'exists', 'is a variable', etc. so long as there are no collisions between variables and functions, between functions of different arity, et cetera. The input of the statement can also be a parse tree or ragged list.

For example, the statement that addition is commutative can be written down as follows: (@ vx0 (@ vx1 (= (f__plus vx0 vx1) (f__plus vx1 vx0))))

The Problem

Write a program that inputs two formulae in first order logic with equality along with a proposed proof of the second statement from the first, and then outputs 1 if the proof is correct, and 0 otherwise. Give an example of the program running on the proof of some simple theorem. Shortest program per language wins.

I don't really care how you encode the notion of a proof so long as it is computably equivalent to the standard notions.

Technical Details

Sentence Formation

The following is essentially transcribed from Wikipedia, rephrased to match the format above.

A term is either a variable name, which is a v followed by a sequence of letters or numbers, or a expression of the form (f_..._A t1 ... tn), where the ti's are terms, f_..._A is a function name, and where the number of underscores equals the number of arguments.

Given a predicate P_..._A, then (P_..._A t1 ... tn) is a formula when the arity of the predicate matches the number of terms. Given two terms t1 and t2, then (= t1 t2) is a formula. Given any formula p, (! p) is a formula. Given another formula q, so are (> p q), (& p q), and (| p q). Finally, given a variable vX and a formula p, (@ vX p) and (# vX p) are formulas. All formulae are produced in this manner.

A sentence is a formula where every occurrence of a variable is bound, i.e. within the scope of a quantifier (@ or #).

Defining Proof

There's multiple ways to formalize a proof. One method is as follows. Given a formula phi and a formula psi, a proof of psi from phi is a list of pairs of sentences and the rule by which they were introduced. The first sentence must be phi and the last must be psi. There are two ways a new sentence can be produced. If there are formulae p and q such that two previously introduced sentences are (> p q) and p, then you can introduce q by modus ponens. Alternatively, the new sentences can be from one of the following axiom schemes (taken from the Wikipedia page on Hilbert Systems):

  1. (> p p) (self-implication)
  2. (> p (> q p)) (simplification)
  3. (> (> p (> q r)) (> (> p q) (> p r)) (the Frege axiom)
  4. (> (> (! p) (! q)) (> q p)) (contrapositive)
  5. (> p (> q (& p q))) (introduction of the conjunction)
  6. (> (& p q) p) (left elimination)
  7. (> (& p q) q) (right elimination)
  8. (> p (| p q)) (left introduction of the disjunction)
  9. (> q (| p q)) (right introduction)
  10. (> (> p r) (> (> q r) (> (| p q) r))) (elimination)
  11. (> (@ vx p) p[vx:=t]), where p[vx:=t] replaces every free instance of vx in p with the term t. (substitution)
  12. (> (@ vx (> p q)) (> (@ vx p) (@ vx q))) (moving universal quantification past the implication)
  13. (> p (@ vx p)) if vx is not free in p.
  14. (@ vx (> p (# vy p[vx:=vy]))) (introduction of the existential)
  15. (> (@ vx p q) (> (# x p) q)) if vx is not free in q.
  16. (= vx vx) (reflexivity)
  17. (> (= vx vy) (> p[vz:=vx] p[vz:=vy])) (substitution by equals)
  18. If p is an axiom, so is (@ vx p) (and so is (@ vx (@ vy p)) ,etc.). (generalization)

p, q, and r are arbitrary formulae, and vx, vy, and vz are arbitrary variables.

Note that if you change up what is demanded of the proof, then it's possible to cut down on the number of axioms. For example, the operations &, |, and # can be expressed in terms of the other operations. Then, if you compute the replacement of the input formulae with the formulae with these operations removed, one can eliminate axioms 5 - 10, 14, and 15. It's possible to compute a proof of the original type from a proof of this reduced type, and vice versa.

For an example of a proof of this type, see below.

 0 (@ vx (P_p vx))
A14 vx vx (P_p vx)
 1 (@ vx (> (P_p vx) (# vx (P_p vx))))
A12 vx (P_p vx) (# vx (P_p vx))
 2 (> (@ vx (> (P_p vx) (# vx (P_p vx)))) (> (@ vx (P_p vx)) (@ vx (# vx (P_p vx)))))
MP 2 1
 3 (> (@ vx (P_p vx)) (@ vx (# vx (P_p vx))))
MP 3 0
 4 (@ vx (# vx (P_p vx)))
GA11 vy vx (# vx (P_p vx))
 5 (@ vy (> (@ vx (# vx (P_p vx))) (# vx (P_p vx))))
A12 vy (@ vx (# vx (P_p vx))) (# vx (P_p vx))
 6 (> (@ vy (> (@ vx (# vx (P_p vx))) (# vx (P_p vx)))) (> (@ vy (@ vx (# vx (P_p vx)))) (@ vy (# vx (P_p vx)))))
MP 6 5
 7 (> (@ vy (@ vx (# vx (P_p vx)))) (@ vy (# vx (P_p vx))))
A13 vy (@ vx (# vx (P_p vx)))
 8 (> (@ vx (# vx (P_p vx))) (@ vy (@ vx (# vx (P_p vx)))))
MP 8 4
 9 (@ vy (@ vx (# vx (P_p vx))))
MP 7 9
10 (@ vy (# vx (P_p vx)))

Between each two lines is indicated the rule by which the next line is produced, where A is an axiom, MP is modus ponens, and GA indicates a single instance of generalization (GGGA would indicate three generalizations on the axiom A).

Improve this question
\$\endgroup\$
10
  • \$\begingroup\$ Please could you give an example of a proof? It would make the question/challenge much easier (for me) to understand... \$\endgroup\$
    – Dominic van Essen
    Oct 17 at 20:45
  • \$\begingroup\$ I suppose some examples of the specific sequent calculus version that I cited above can be found in this section: en.wikipedia.org/wiki/Sequent_calculus#Example_derivations \$\endgroup\$
    – Charles Wang
    Oct 17 at 20:54
  • 3
    \$\begingroup\$ And just as advice, I do think this challenge would be more interesting if it were laxer on the statement structure, and stricter on the proof structure. \$\endgroup\$
    – Wheat Wizard ♦
    Oct 17 at 22:34
  • 2
    \$\begingroup\$ As a first step, I'd recommend letting answers choose which symbols they use for forall, exists etc. Beyond that I'd explicitly add a few alternative options. I'd also let people take it as a parse tree or a ragged list as an example. Parsing isn't the interesting part of this challenge in the first place. If you keep the list specific and include reasonable formats, everything is precise you can avoid pathological encoding. \$\endgroup\$
    – Wheat Wizard ♦
    Oct 18 at 0:49
  • 1
    \$\begingroup\$ @CommandMaster Sure, postfix is o.k. A proof which has a syntax error is not a correct proof. Law of excluded middle is a consequence of the first four axioms, as is double negation, etc. I suppose the proofs of these work as test cases for the propositional part of the language. At some point I'll work out a proof of some fact about quantifiers, and then put that up as a test case. \$\endgroup\$
    – Charles Wang
    Oct 18 at 3:11

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Browse other questions tagged or ask your own question.