Examples of Proofs in Maxixe
============================
Note that in these examples the `===> ok` is not part of the proof (or
even part of Maxixe's syntax); these lines are for Falderal's benefit.
-> Tests for functionality "Check Maxixe proof"
Propositional Logic
-------------------
The rules of inference from pages 8-15 of [these slides](http://www.inf.ed.ac.uk/teaching/courses/dmmr/slides/13-14/Ch1c.pdf)
plus the proof on page 17 of same (which only uses a small subset of the rules.)
That proof uses the fact that conjunction is commutative without stating it,
so we've added it as a rule here.
Note that we could also, in this case, have two rules for Simplification
(Left Simplification and Right Simplification) and we have in fact used
that approach in other example proofs in these documents.
Or, we could have stated the rule as an "axiom schema" like
`impl(and(P, Q), and(Q, P))` and used Modus Ponens. However, Maxixe does
require at least one hypothesis on the LHS of a rule, so we would need to
write it like `and(P, Q) |- impl(and(P, Q), and(Q, P))`.
given
Modus_Ponens = impl(P, Q) ; P |- Q
Modus_Tollens = impl(P, Q) ; not(Q) |- not(P)
Hypothetical_Syllogism = impl(P, Q) ; impl(Q, R) |- impl(P, R)
Disjunctive_Syllogism = or(P, Q) ; not(P) |- Q
Addition = P |- or(P, Q)
Simplification = and(P, Q) |- Q
Conjunction = P ; Q |- and(P, Q)
Resolution = or(not(P, R)) ; or(P, Q) |- or(Q, R)
Commutativity_of_Conjunction = and(P, Q) |- and(Q, P)
Premise = |- and(p, impl(p, q))
show
q
proof
Step_1 = and(p, impl(p, q)) by Premise
Step_2 = and(impl(p, q), p) by Commutativity_of_Conjunction with Step_1
Step_3 = impl(p, q) by Simplification with Step_1
Step_4 = p by Simplification with Step_2
Step_5 = q by Modus_Ponens with Step_3, Step_4
qed
===> ok
### Supposition ###
A proof that from a→(b→c) and a→b and d, we can conclude (a→c)^d.
given
Modus_Ponens = impl(P, Q) ; P |- Q
Conjunction = P ; Q |- and(P, Q)
block Suppose
Supposition = A{term} |- A
Conclusion = P ; Q |- impl(P, Q)
end
Premise_1 = |- impl(a, impl(b, c))
Premise_2 = |- impl(a, b)
Premise_3 = |- d
show
and(impl(a, c), d)
proof
Step_1 = impl(a, impl(b, c)) by Premise_1
Step_2 = impl(a, b) by Premise_2
Step_3 = d by Premise_3
block Suppose
Step_4 = a by Supposition with a
Step_5 = impl(b, c) by Modus_Ponens with Step_1, Step_4
Step_6 = b by Modus_Ponens with Step_2, Step_4
Step_7 = c by Modus_Ponens with Step_5, Step_6
Step_8 = impl(a, c) by Conclusion with Step_4, Step_7
end
Step_9 = and(impl(a, c), d) by Conjunction with Step_8, Step_3
qed
===> ok
### Reasoning by Cases ###
A proof that disjunction is commutative.
given
Modus_Ponens = impl(P, Q) ; P |- Q
Disj_Intro_Left = P ; Q{term} |- or(Q, P)
Disj_Intro_Right = P ; Q{term} |- or(P, Q)
block Disjunction
case
Disj_Elim_Left = or(P, Q) |- P
end
case
Disj_Elim_Right = or(P, Q) |- Q
end
end
Tautology = P |- P
Premise = |- or(a, b)
show
or(b, a)
proof
Step_1 = or(a, b) by Premise
block Disjunction
case
Step_2 = a by Disj_Elim_Left with Step_1
Step_3 = or(b, a) by Disj_Intro_Left with Step_2, b
end
case
Step_4 = b by Disj_Elim_Right with Step_1
Step_5 = or(b, a) by Disj_Intro_Right with Step_4, a
end
end
Step_6 = or(b, a) by Tautology with Step_5
qed
===> ok
### Proof by Contradiction ###
If we assume p and show that it leads to a contradiction,
we can then infer ¬p. We can use proof by contradiction
to try to derive Modus Tollens:
given
Modus_Ponens = impl(P, Q) ; P |- Q
Double_Negation = not(not(P)) |- P
Contradiction = P ; not(P) |- bottom
Explosion = bottom |- P
block Reductio_ad_Absurdum
Supposition = A{term} |- A
Conclusion = bottom |- not(A)
end
Premise_1 = |- impl(p, q)
Premise_2 = |- not(q)
show
not(p)
proof
Step_1 = impl(p, q) by Premise_1
Step_2 = not(q) by Premise_2
block Reductio_ad_Absurdum
Step_3 = p by Supposition with p
Step_4 = q by Modus_Ponens with Step_1, Step_3
Step_5 = bottom by Contradiction with Step_4, Step_2
Step_6 = not(p) by Conclusion with Step_5
end
Step_7 = not(p) by Tautology with Step_6
qed
This proof is not yet accepted by Maxixe, and the reason seems to be
a small technical one: the scope of the bound variable `A` does not
extend to the right-hand side of the Conclusion of the
`Reduction_ad_Absurdum` block. That's unfortunate, and I don't know
at the moment how much work it would take to fix.
Predicate Logic
---------------
### Universal Generalization (UG) ###
The following is adapted from the "short, dull proof" from page 13 of John C. Reynold's
_Theories of Programming Languages_.
In the original, the rules of inference aren't named, and the 2nd one (Commutivity_of_Equality)
is an "axiom schema" which has no hypotheses. Maxixe requires that every variable on the RHS
of a turnstile can be filled out by a variable on the LHS, so I've taken the liberty of turning
it into a rule.
The variable being introduced by Universal Generalization need not be unique, because it
is bound in a `forall`.
Note that the substitution operation `P[X -> V]` used in the Universal Generalization rule
first checks that the instance of V does not already occur in P.
(This may in fact be overly restrictive. But it seems like the most hardship it causes at
the moment is that it requires you to select different names for variables in parts of the
proof. For example, below we show a result `forall(y, ...)`. We could just as easily
want to show the result `forall(x, ...)` but x is already a free (arbitrary) variable in
this proof.)
We use `c(zero)` to represent zero because we can't use `zero` because then you could use it as
a variable name and say something silly like `forall(zero, ...)`.
given
Premise = |- eq(add(x, c(zero)), x)
Commutivity_of_Equality = eq(E1, E0) |- impl(eq(E1, E0), eq(E0, E1))
Modus_Ponens = P0 ; impl(P0, P1) |- P1
Universal_Generalization = P ; X{nonlocal term} ; V{atom} |- forall(V, P[X -> V])
show
forall(y, eq(y, add(y, c(zero))))
proof
Step_1 = eq(add(x, c(zero)), x) by Premise
Step_2 = impl(eq(add(x, c(zero)), x), eq(x, add(x, c(zero)))) by Commutivity_of_Equality with Step_1
Step_3 = eq(x, add(x, c(zero))) by Modus_Ponens with Step_1, Step_2
Step_4 = forall(y, eq(y, add(y, c(zero)))) by Universal_Generalization with Step_3, x, y
qed
===> ok
### Universal Instantiation (UI) ###
All bugs are creepy and all bugs are crawly therefore all bugs are both creepy and crawly.
Note that the term introduced as the variable in the UI need not be unique, because if
something is true for all `x`, it is true for *all* `x`, even if `x` is something else
you've already been thinking about and given the name `x`. Note that it also need not
be an atom.
Note that the substitution operation `P[X -> V]` used in the Universal Instantiation rule
first checks that the instance of V does not already occur in P. This prevents situations
like instantiating ∀x.∃y.x≠y with y, to obtain ∃y.y≠y.
given
Modus_Ponens = impl(P, Q) ; P |- Q
Conjunction = P ; Q |- and(P, Q)
block Suppose
Supposition = A{term} |- A
Conclusion = P ; Q |- impl(P, Q)
end
Universal_Generalization = P ; X{nonlocal term} ; V{atom} |- forall(V, P[X -> V])
Universal_Instantiation = forall(X, P) ; V{term} |- P[X -> V]
Premise_1 = |- forall(x, impl(bug(x), creepy(x)))
Premise_2 = |- forall(x, impl(bug(x), crawly(x)))
show
forall(x, impl(bug(x), and(creepy(x), crawly(x))))
proof
Step_1 = forall(x, impl(bug(x), creepy(x))) by Premise_1
Step_2 = impl(bug(y), creepy(y)) by Universal_Instantiation with Step_1, y
Step_3 = forall(x, impl(bug(x), crawly(x))) by Premise_2
Step_4 = impl(bug(y), crawly(y)) by Universal_Instantiation with Step_3, y
block Suppose
Step_5 = bug(y) by Supposition with bug(y)
Step_6 = creepy(y) by Modus_Ponens with Step_2, Step_5
Step_7 = crawly(y) by Modus_Ponens with Step_4, Step_5
Step_8 = and(creepy(y), crawly(y)) by Conjunction with Step_6, Step_7
Step_9 = impl(bug(y), and(creepy(y), crawly(y))) by Conclusion with Step_5, Step_8
end
Step_10 = forall(x, impl(bug(x), and(creepy(x), crawly(x)))) by Universal_Generalization with Step_9, y, x
qed
===> ok
About that gratuitous variable name restriction in the previous example.
What if we really did want to show `forall(x, eq(x, add(x, c(zero))))`?
Can we do it with an instantiation step?
given
Premise = |- eq(add(x, c(zero)), x)
Commutivity_of_Equality = eq(E1, E0) |- impl(eq(E1, E0), eq(E0, E1))
Modus_Ponens = P0 ; impl(P0, P1) |- P1
Universal_Generalization = P ; X{nonlocal term} ; V{atom} |- forall(V, P[X -> V])
Universal_Instantiation = forall(X, P) ; V{term} |- P[X -> V]
show
forall(x, eq(x, add(x, c(zero))))
proof
Step_1 = eq(add(x, c(zero)), x) by Premise
Step_2 = impl(eq(add(x, c(zero)), x), eq(x, add(x, c(zero)))) by Commutivity_of_Equality with Step_1
Step_3 = eq(x, add(x, c(zero))) by Modus_Ponens with Step_1, Step_2
Step_4 = forall(y, eq(y, add(y, c(zero)))) by Universal_Generalization with Step_3, x, y
Step_5 = eq(z, add(z, c(zero))) by Universal_Instantiation with Step_4, z
Step_6 = forall(x, eq(x, add(x, c(zero)))) by Universal_Generalization with Step_5, z, x
qed
===> ok
Yes.
### Existential Generalization (EG) ###
All bugs are creepy therefore there exists a bug which is creepy.
The variable being introduced by Existential Generalization need not be unique, because it
is bound in an `exists`.
Like always with `[X -> V]`, an occurs check occurs. Not sure if necessary atm.
given
Universal_Instantiation = forall(X, P) ; V{term} |- P[X -> V]
Existential_Generalization = P ; X{term} ; V{atom} |- exists(V, P[X -> V])
Premise = |- forall(x, impl(bug(x), creepy(x)))
show
exists(x, impl(bug(x), creepy(x)))
proof
Step_1 = forall(x, impl(bug(x), creepy(x))) by Premise
Step_2 = impl(bug(j), creepy(j)) by Universal_Instantiation with Step_1, j
Step_3 = exists(x, impl(bug(x), creepy(x))) by Existential_Generalization with Step_2, j, x
qed
===> ok
### Existential Instantiation (EI) ###
All men are mortal. There exists a man who is Socrates. Therefore there exists a man who is mortal
and who is Socrates, i.e. Socrates is mortal.
Very unlike UI, to avoid scoping problems, the new variable name introduced during EI needs to be:
* an atom, because instantiating an entire term is probably unjustifiable sometimes
* unique, to avoid clashing with another variable that was previously instantiated
* local, to prevent the name from "leaking out" of the EI block.
Note that the substitution operation `P[X -> V]` used in the Existential Instantiation rule
first checks that the instance of V does not already occur in P. This prevents situations
like instantiating ∃x.∀y.p(y)→x≠y with y, to obtain ∀y.p(y)→y≠y.
given
Modus_Ponens = impl(P, Q) ; P |- Q
Conjunction = P ; Q |- and(P, Q)
Simplification_Left = and(P, Q) |- P
Simplification_Right = and(P, Q) |- Q
Tautology = P |- P
Universal_Instantiation = forall(X, P) ; V{term} |- P[X -> V]
Existential_Generalization = P ; X{term} ; V{atom} |- exists(V, P[X -> V])
block Existential_Instantiation
Let = exists(X, P) ; V{unique local atom} |- P[X -> V]
end
Premise_1 = |- forall(x, impl(man(x), mortal(x)))
Premise_2 = |- exists(x, and(man(x), socrates(x)))
show
exists(x, and(mortal(x), socrates(x)))
proof
Step_1 = forall(x, impl(man(x), mortal(x))) by Premise_1
Step_2 = exists(x, and(man(x), socrates(x))) by Premise_2
block Existential_Instantiation
Step_3 = and(man(k), socrates(k)) by Let with Step_2, k
Step_4 = man(k) by Simplification_Left with Step_3
Step_5 = impl(man(k), mortal(k)) by Universal_Instantiation with Step_1, k
Step_6 = mortal(k) by Modus_Ponens with Step_5, Step_4
Step_7 = socrates(k) by Simplification_Right with Step_3
Step_8 = and(mortal(k), socrates(k)) by Conjunction with Step_6, Step_7
Step_9 = exists(x, and(mortal(x), socrates(x))) by Existential_Generalization with Step_8, k, x
end
Step_10 = exists(x, and(mortal(x), socrates(x))) by Tautology with Step_9
qed
===> ok
For comparison, here are all of the rules for Universal (resp. Existential)
Generalization (resp. Instantiation) shown together in one place, with abbreviated names:
UG = P ; X{nonlocal term} ; V{atom} |- forall(V, P[X -> V])
UI = forall(X, P) ; V{term} |- P[X -> V]
EG = P ; X{term} ; V{atom} |- exists(V, P[X -> V])
block EI
Let = exists(X, P) ; V{unique local atom} |- P[X -> V]
end
Equational Reasoning
--------------------
Maxixe is not restricted to propositional and predicate logic. While
some systems of logic impose their own side conditions that cannot
be expressed in Maxixe (for example, [relevance logic][] requires that
the consequent of every rule be "relevant" to its premiss) and thus
cannot be checked, other systems of logic (or fragments thereof) can
be expressed in it. Maxixe tries to be very general in this way, and
to not impose unnecessary restrictions.
One such logic is [equational logic][], which is the logic that
underpins universal algebra. The basic idea is "replacing equals
with equals", and often it is convenient to work with it without
even regarding it as a logic per se — often this process is referred
to only as "equational reasoning". (A bit of trivia: there was an
early educational version of the programming language Haskell called
"Gofer", which is an acronym for "Good for equational reasoning".)
Here, we give an example of a proof of a simple property of monoids
using equational reasoning.
In this proof, `o(X, Y)` is the monoid operation. `m(X)` means X
is an element of the monoid, `id(X)` means X is an identity element
(meaning, *the* identity element, but we don't assume or prove that it
is unique.) We show that, if `e` is an identity element, then `ee=e`.
given
Closure = m(A) ; m(B) |- m(o(A, B))
Associativity = m(A) ; m(B) ; m(C) |- eq(o(A, o(B, C)), o(o(A, B), C))
Identity = m(A) ; id(E) |- eq(o(A, E), A)
Identity_is_an_Element = id(E) |- m(E)
Premise = |- id(e)
show
eq(o(e, e), e)
proof
Step_1 = id(e) by Premise
Step_2 = m(e) by Identity_is_an_Element with Step_1
Step_3 = eq(o(e, e), e) by Identity with Step_2, Step_1
qed
===> ok
[relevance logic]: http://en.wikipedia.org/wiki/Relevance_logic
[equational logic]: http://en.wikipedia.org/wiki/Equational_logic
Number Theory
-------------
If y is odd, then y+1 is even.
given
UG = P ; X{nonlocal term} ; V{atom} |- forall(V, P[X -> V])
UI = forall(X, P) ; V{term} |- P[X -> V]
EG = P ; X{term} ; V{atom} |- exists(V, P[X -> V])
block EI
Let = exists(X, P) ; V{unique local atom} |- P[X -> V]
end
Weakening = biimpl(X, Y) |- impl(X, Y)
Reverse_Weakening = biimpl(X, Y) |- impl(Y, X)
Modus_Ponens = P ; impl(P, Q) |- Q
block Suppose
Supposition = A{term} |- A
Conclusion = P ; Q |- impl(P, Q)
end
Defn_of_Even = |- forall(n, biimpl(even(n), exists(k, eq(n, add(k, k)))))
Defn_of_Odd = |- forall(n, biimpl(odd(n), exists(k, eq(n, add(add(k, k), c(1))))))
Add_One_to_Both_Sides = eq(X, Y) |- eq(add(X, c(1)), add(Y, c(1)))
Provisional_Algebra = eq(X, add(add(add(A, B), C), D)) |- eq(X, add(add(A, C), add(B, D)))
show
forall(y, impl(odd(y), even(add(y, c(1)))))
proof
block Suppose
Step_1 = odd(x) by Supposition with odd(x)
Step_2 = forall(n, biimpl(odd(n), exists(k, eq(n, add(add(k, k), c(1)))))) by Defn_of_Odd
Step_3 = biimpl(odd(x), exists(k, eq(x, add(add(k, k), c(1))))) by UI with Step_2, x
Step_4 = impl(odd(x), exists(k, eq(x, add(add(k, k), c(1))))) by Weakening with Step_3
Step_5 = exists(k, eq(x, add(add(k, k), c(1)))) by Modus_Ponens with Step_1, Step_4
block EI
Step_6 = eq(x, add(add(j, j), c(1))) by Let with Step_5, j
Step_7 = eq(add(x, c(1)), add(add(add(j, j), c(1)), c(1))) by Add_One_to_Both_Sides with Step_6
Step_8 = eq(add(x, c(1)), add(add(j, c(1)), add(j, c(1)))) by Provisional_Algebra with Step_7
Step_9 = exists(k, eq(add(x, c(1)), add(k, k))) by EG with Step_8, add(j, c(1)), k
Step_10 = forall(n, biimpl(even(n), exists(k, eq(n, add(k, k))))) by Defn_of_Even
Step_11 = biimpl(even(add(x, c(1))), exists(k, eq(add(x, c(1)), add(k, k)))) by UI with Step_10, add(x, c(1))
Step_12 = impl(exists(k, eq(add(x, c(1)), add(k, k))), even(add(x, c(1)))) by Reverse_Weakening with Step_11
Step_13 = even(add(x, c(1))) by Modus_Ponens with Step_9, Step_12
end
Step_14 = impl(odd(x), even(add(x, c(1)))) by Conclusion with Step_1, Step_13
end
Step_15 = forall(y, impl(odd(y), even(add(y, c(1))))) by UG with Step_14, x, y
qed
===> ok
The sum of an odd number and an odd number is an even number.
given
UG = P ; X{nonlocal term} ; V{atom} |- forall(V, P[X -> V])
UI = forall(X, P) ; V{term} |- P[X -> V]
EG = P ; X{term} ; V{atom} |- exists(V, P[X -> V])
block EI
Let = exists(X, P) ; V{unique local atom} |- P[X -> V]
end
Weakening = biimpl(X, Y) |- impl(X, Y)
Reverse_Weakening = biimpl(X, Y) |- impl(Y, X)
Modus_Ponens = P ; impl(P, Q) |- Q
Simplification_Left = and(P, Q) |- P
Simplification_Right = and(P, Q) |- Q
Tautology = P |- P
block Suppose
Supposition = A{term} |- A
Conclusion = P ; Q |- impl(P, Q)
end
Defn_of_Even = |- forall(n, biimpl(even(n), exists(k, eq(n, add(k, k)))))
Defn_of_Odd = |- forall(n, biimpl(odd(n), exists(k, eq(n, add(add(k, k), c(1))))))
Addition_Both_Sides = eq(X0, Y0) ; eq(X1, Y1) |- eq(add(X0, X1), add(Y0, Y1))
Provisional_Algebra = eq(X, add(add(add(A, B), C), add(add(D, E), F))) |- eq(X, add(add(add(A, E), C), add(add(B, E), F)))
show
forall(x, forall(y, impl(and(odd(x), odd(y)), even(add(x, y)))))
proof
block Suppose
Step_1 = and(odd(x0), odd(y0)) by Supposition with and(odd(x0), odd(y0))
Step_2 = odd(x0) by Simplification_Left with Step_1
Step_3 = odd(y0) by Simplification_Right with Step_1
Step_4 = forall(n, biimpl(odd(n), exists(k, eq(n, add(add(k, k), c(1)))))) by Defn_of_Odd
Step_5 = biimpl(odd(x0), exists(k, eq(x0, add(add(k, k), c(1))))) by UI with Step_4, x0
Step_6 = impl(odd(x0), exists(k, eq(x0, add(add(k, k), c(1))))) by Weakening with Step_5
Step_7 = exists(k, eq(x0, add(add(k, k), c(1)))) by Modus_Ponens with Step_2, Step_6
Step_8 = biimpl(odd(y0), exists(k, eq(y0, add(add(k, k), c(1))))) by UI with Step_4, y0
Step_9 = impl(odd(y0), exists(k, eq(y0, add(add(k, k), c(1))))) by Weakening with Step_8
Step_10 = exists(k, eq(y0, add(add(k, k), c(1)))) by Modus_Ponens with Step_3, Step_9
block EI
Step_11 = eq(x0, add(add(k0, k0), c(1))) by Let with Step_7, k0
block EI
Step_12 = eq(y0, add(add(k1, k1), c(1))) by Let with Step_10, k1
Step_13 = eq(add(x0, y0), add(add(add(k0, k0), c(1)), add(add(k1, k1), c(1))))
by Addition_Both_Sides with Step_11, Step_12
Step_14 = eq(add(x0, y0), add(add(add(k0, k1), c(1)), add(add(k0, k1), c(1))))
by Provisional_Algebra with Step_13
Step_15 = exists(k, eq(add(x0, y0), add(k, k))) by EG with Step_14, add(add(k0, k1), c(1)), k
end
Step_16 = forall(n, biimpl(even(n), exists(k, eq(n, add(k, k))))) by Defn_of_Even
Step_17 = biimpl(even(add(x0, y0)), exists(k, eq(add(x0, y0), add(k, k)))) by UI with Step_16, add(x0, y0)
Step_18 = impl(exists(k, eq(add(x0, y0), add(k, k))), even(add(x0, y0))) by Reverse_Weakening with Step_17
Step_19 = even(add(x0, y0)) by Modus_Ponens with Step_15, Step_18
end
Step_20 = impl(and(odd(x0), odd(y0)), even(add(x0, y0))) by Conclusion with Step_1, Step_19
end
Step_21 = forall(y, impl(and(odd(x0), odd(y)), even(add(x0, y)))) by UG with Step_20, y0, y
Step_22 = forall(x, forall(y, impl(and(odd(x), odd(y)), even(add(x, y))))) by UG with Step_21, x0, x
qed
===> ok