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