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))))
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.
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 t1 ... tn) is a formula when the arity of the predicate matches the number of terms. Given two terms
(= t1 t2) is a formula. Given any formula
(! 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
(@ 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 (
There's multiple ways to formalize a proof. One method is as follows. Given a formula
phi and a formula
psi, a proof of
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
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):
(> p p)(self-implication)
(> p (> q p))(simplification)
(> (> p (> q r)) (> (> p q) (> p r))(the Frege axiom)
(> (> (! p) (! q)) (> q p))(contrapositive)
(> p (> q (& p q)))(introduction of the conjunction)
(> (& p q) p)(left elimination)
(> (& p q) q)(right elimination)
(> p (| p q))(left introduction of the disjunction)
(> q (| p q))(right introduction)
(> (> p r) (> (> q r) (> (| p q) r)))(elimination)
(> (@ vx p) p[vx:=t]), where
p[vx:=t]replaces every free instance of
pwith the term
(> (@ vx (> p q)) (> (@ vx p) (@ vx q)))(moving universal quantification past the implication)
(> p (@ vx p))if
vxis not free in
(@ vx (> p (# vy p[vx:=vy])))(introduction of the existential)
(> (@ vx p q) (> (# x p) q))if
vxis not free in
(= vx vx)(reflexivity)
(> (= vx vy) (> p[vz:=vx] p[vz:=vy]))(substitution by equals)
pis an axiom, so is
(@ vx p)(and so is
(@ vx (@ vy p)),etc.). (generalization)
r are arbitrary formulae, 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
# 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