Proof Rondo

Javascript First-Order Logic Proof Checker

Source: https://github.com/hbasold/folproof-rondo

Instructions:

Enter your proof in the input box, below. As you type, the formatted proof will appear on the right, along with a validation status, beneath that. To learn the syntax, try playing with the examples, below, or see the language reference.

Notes:

  • Please be sure you have a modern browser, and that Javascript is enabled.
  • There is currently a limitation in the parser, where the last substitution quantifier rules cannot contain spaces. Thus, you have to write x/g(c,d) instead of x/g(c, d)!
  • The rules for equality are used as "= i" instead of (Refl) and "= e" instead of (Repl).

Examples:

Result:

1 ∀x.P(c, x) : premise | with x0 2 | P(c,x0) : A.x/x0 e 1 3 | ∃y.P(y,x0) : E.y/c i 2 4 ∀x.∃y.P(y,x) : A.x/x0 i 2-3
1 r and u -> w : premise 2 u and ~w : premise 3 | r 4 | u : and e1 2 5 | r and u : and i 3,4 6 | w : -> e 1, 5 7 | ~w : and e2 2 8 | ⊥ : neg e 6,7 9 ~r : neg i 3-8
# To use lemmas and previous results, you can include them as extra premises ¬(∃x.¬P(x)) → ∀x.¬¬P(x) : premise example ¬(∀x.P(x)) | ¬(∃x.¬P(x)) | ∀x.¬¬P(x) : -> e 1,3 || with x0 || ¬¬P(x0) : A.x/x0 e 4 ||| ¬P(x0) ||| ⊥ : neg e 5,6 || P(x0) : contra 6-7 | ∀x.P(x) : A.x/x0 i 5-8 | ⊥ : neg e 2,9 ∃x.¬P(x) : contra 3-10
¬(∀x.P(x) → D(x)) → (∃x. P(x) ∧ ¬D(x)) ∃x.P(x) (∀x.P(x) → D(x)) ∨ ¬(∀x.P(x) → D(x)) : lem | ∀x.P(x) → D(x) || with x0 || P(x0) ||| P(x0) ∧ D(x0) ||| ∀x.P(x) → D(x) : copy 4 || (P(x0) ∧ D(x0) -> (∀x.P(x) → D(x))) : -> i 6-7 || (∃y. P(y) ∧ D(y) -> (∀x.P(x) → D(x))) : E.y/x0 i 8 | (∃y. P(y) ∧ D(y) -> (∀x.P(x) → D(x))) : E.x/x0 e 2, 5-9 ------ | ¬(∀x.P(x) → D(x)) | (∃x. P(x) ∧ ¬D(x)) : -> e 1, 11 || with x0 || P(x0) ∧ ¬D(x0) ||| P(x0) ∧ D(x0) ||| ¬D(x0) : and e2 13 ||| D(x0) : and e2 14 ||| ⊥ : neg e 15,16 ||| ∀x.P(x) → D(x) : bot e 17 || (P(x0) ∧ D(x0) -> (∀x.P(x) → D(x))) : -> i 14-18 || (∃y. P(y) ∧ D(y) -> (∀x.P(x) → D(x))) : E.y/x0 i 19 | (∃y. P(y) ∧ D(y) -> (∀x.P(x) → D(x))) : E.x/x0 e 12, 13-20 ------ (∃y. P(y) ∧ D(y) -> (∀x.P(x) → D(x))) : or e 3, 4-10, 11-21
An. L(n,n) An.Am. L(n,m) -> L(n, s(m)) L(z,z) : B.n/z 1 L(z,s(z)) : B.n/z;m/z 2,3 Em. L(z, m) : E.m/s(z) i 4
# We write o for 1, and p(x,y) for x + y. # We also leave of the quantifier range to not overload the proof, as we do not have definitions available here. | with x0 || ∃y. x0 = p(y,y) ||| with y0 ||| x0 = p(y0,y0) ||| p(x0, o) = p(x0, o) : = i ||| p(x0, o) = p(p(y0,y0), o) : = e 2,3 ||| ∃y. p(x0, o) = p(p(y,y), o) : E.y/y0 i 4 || ∃y. p(x0, o) = p(p(y,y), o) : E.y/y0 e 1,2-5 | (∃y. x0 = p(y,y)) -> ∃y. p(x0, o) = p(p(y,y), o) : -> i 1-6 ∀x. (∃y. x = p(y,y)) -> (∃y. p(x, o) = p(p(y,y), o)) : A.x/x0 i 1-7
# This is a possible solution to the exam question that asks for a proof of a formula from # the given formulas, here in lines 1 - 3. 1 (Ex0. Ax1. x0 = i(g(x0), i(x1 , i(x0 , x1)))) & (Ax2. x2 = x2) 2 (Ex3. O(i(i(g(x3), d(x3 , x3 , x3)), x3), x3 , x3) & T(x3)) & (Ax4. x4 = x4) 3 Ex5. (Ax6. x6 = g(g(d(x5 , x6 , x5)))) v x5 = x5 4 Ex0. Ax1. x0 = i(g(x0), i(x1 , i(x0 , x1))) : and e1 1 | with y0 5 | Ax1. y0 = i(g(y0), i(x1 , i(y0 , x1))) 6 | y0 = i(g(y0), i(y0 , i(y0 , y0))) : A.x1/y0 e 5 7 || T(y0) 8 || T(i(g(y0), i(y0 , i(y0 , y0)))) : = e 6,7 9 | T(y0) -> T(i(g(y0), i(y0 , i(y0 , y0)))) : -> i 7-8 10 | Ey. T(y) -> T(i(g(y), i(y , i(y , y)))) : E.y/y0 i 9 11 Ey. T(y) -> T(i(g(y), i(y , i(y , y)))) : E.x0/y0 e 4, 5-10
# Horn theory exam exercise # We use the following interpretation: # d(x, y, z) : assigns to the colour combination of hair, paints and shows a person with that colour combination # g(x) : maps x to the next colour # i(p, x) : maps (p,x) to next person after p with pants colour x # O(p, q, x) : person p sees person q with pants colour x # T(x) : x is a colour # Q() : someone has a yellow backpack # We introduce one extra constant c for the base colour ∀p. O(p, p, c) ∀p. ∀q. ∀x. O(p, q, x) & T(x) -> O(p, i(q, x), g(x)) ∀x. T(x) -> T(g(x)) T(c) # ---------------------- O(d(c,c,c), d(c,c,c), c) : B.p/d(c,c,c) 1 O(d(c,c,c), i(d(c,c,c), c), g(c)) : B.p/d(c,c,c); q/d(c,c,c); x/c 2,5,4 T(g(c)) : B.x/c 3,4 O(d(c,c,c), i(i(d(c,c,c), c), g(c)), g(g(c))) : B.p/d(c,c,c); q/i(d(c,c,c), c); x/g(c) 2,6,7 T(g(g(c))) : B.x/g(c) 3,7 O(d(c,c,c), i(i(i(d(c,c,c), c), g(c)), g(g(c))), g(g(g(c)))) : B.p/d(c,c,c); q/i(i(d(c,c,c), c), g(c)); x/g(g(c)) 2,8,9 T(g(g(c))) ∧ O(d(c,c,c), i(i(i(d(c,c,c), c), g(c)), g(g(c))), g(g(g(c)))) : and i 9,10 ∃q. T(g(g(c))) ∧ O(d(c,c,c), q, g(g(g(c)))) : E.q/i(i(i(d(c,c,c),c),g(c)),g(g(c))) i 11 ∃x. ∃q. T(x) ∧ O(d(c,c,c), q, g(x)) : E.x/g(g(c)) i 12 ∃p. ∃x. ∃q. T(x) ∧ O(p, q, g(x)) : E.p/d(c,c,c) i 13
# You may use the admissible rules for symmetry and transitivity as follows. # First turn these rules into Horn clauses like so: Ax. Ay. x = y -> y = x : premise # (Sym) proven in theorem 9.10 Ax. Ay. Az. x = y & y = z -> x = z : premise # (Trans) proven in theorem 9.10 # Then you can use thes Horn clauses easily with the backchaining rule in proofs: a = b b = c a = c : B.x/a;y/b;z/c 2,3,4