Question: I am beginning to study Computational Logic, and as an exercise, I want to prove the correctness of merge sort algorithm.

Currently, I’m having difficulties to prove that the output of this algorithm will always correspond to a permutation of a given input.

I’d be very glad if someone can assist me with this.

Thank you very much

Answer: 
The core of this proof will need to show that the "merge" procedure inserts each element once and only once into the result. Since the merge procedure works using a loop, you need to use a [loop invariant](https://en.wikipedia.org/wiki/Loop_invariant) to show this.

Loop invariants can usually be discovered by asking, "what do I know *halfway through* the loop?"

```
to merge arrays A and B:
    let n = length of A, m = length of B
    let R = new array of length (n + m)
    let i = 0, j = 0
    while i < n or j < m:
        if i < n and (j == m or A[i] <= B[j]):
            R[i+j] = A[i]
            i = i + 1
        else:
            R[i+j] = B[j]
            j = j + 1
    return R

```

In this loop, we always know that the first i+j elements of R are some permutation of the first i elements of A and the first j elements of B. That's the loop invariant, so you need to show that:

1. This is true before the loop starts (when i = j = 0).
2. If this is true before an iteration of the loop, then it remains true after that iteration, i.e. the invariant is preserved.
3. If this is true when the loop terminates (when i = m, j = n), then the array R has the required property.

In general, the hard parts of a proof like this are discovering the loop invariant, and showing that the invariant is preserved by each iteration of the loop.
What are the preconditions of a merge sort? What are the post conditions? Do you have any loop invariants? 

These are the three questions you have to ask yourself before you can start writing your proof. 

Then: what are your base cases? Presumably you know how merge sort works if you are working on a proof, so what happens when you have an array of length 1 passed to the mergesort function? What is the postcondition there? 

Here's a [decent primer from Berkeley](http://www-inst.cs.berkeley.edu/~cs170/fa14/tutorials/tutorial1.pdf) on how to prove the correctness of a function. It might take some discrete math (induction) to write the proof.