In our Software Verification module, we've just moved on from truth tables to natural deduction. Truth tables seemed pretty basic, but now we're using the coq theorm prover to prove more complex statements. What confuses me is how we just end up with kinda of, "proven or not proven" type answer, when with truth tables we could have a true or false type result based on the input, does this mean that we use natural deduction to look for tautologies, or am I completely missing something?
They have different meanings. Truth tables correspond to the semantics of the proposition. You establish when the proposition is true or false, depending on when the free variables (any variable not inside a "forall" or "exists", or the "inputs" as you put it) are true or not.
Natural deduction is different, since you don't assign a truth/false value to any input directly. With natural deduction, you start with propositions, and build new ones from those using deduction, or "natural reasoning". Basically, there are a bunch of rules that tell you how to build these propositions, called "inference rules".
Lets use an example: We want to prove |= A->A.
Truth Table
First let's look at the truth table of |= X->Y
X | Y | X-> Y
-------------
T | T | T
T | F | F
F | T | T
F | F | T
So now let's apply it to |= A->A
A | A | A-> A
-------------
T | T | T
T | F | F
F | T | T
F | F | T
Since A has the same value all the time, we can crop 2 rows in there and end up with this:
A | A | A-> A
-------------
T | T | T
F | F | T
What does this mean? It means that |= A->A is always true, so we've semantically proven it.
Natural Deduction
Here we want to prove |- A->A using deduction.
For that let's look at a (simplified) inference rule for the "entails":
A |- B
--------
|- A -> B
This inference rule tells you: "If you can prove B assuming you have A, then you can prove that A entails B, or A->B" That is the rule that allows you to "build" proposition, in the sense that you first build proofs of smaller propositions, and then join them together to build proofs of bigger ones.
We also have another inference rule we can use:
A |- A
What does this one mean? It means you can always prove something if you assume it happens. Makes sense right?
So we can use these new rules to prove |- A->A . How? Easy:
A |- A
------
|- A -> A
We used the inference rule of the "entails", and substituted B with A. Then we have would have to prove A |- A, but that is another inference rule we know! With this, we already prove |- A->A is true. However, we didn't need to use any truth tables at all.
You may notice how one of them is |= A->A while the other one is |- A->A. This is because |= means "entails semantically", while |- means "proves". However, both are equivalente. If one of them is true, then so is the other one, so by proving |- A->A holds true, you prove |= A->A is true, i.e that A->A is a tautology.
does this mean that we use natural deduction to look for tautologies, or am I completely missing something?
You can prove more things other than tautologies.
Tautologies are propositions that are always true, no matter what. This means that no matter what you assume, no matter what value you assign to any "input", it will be true. This is represented by the notation |= X indicating X is a tautology.
However, you can include propositions to the left of it. When you do so, it means that the proposition on the right is true, only when you interpret that the proposition on the left is true. For example A |= A . It means that in any interpretation where you assign the value true to A (left), then A (right) will also have the value true.
You can include any proposition, or list of propositions to the left, for example A,B |= A /\ B, meaning that whenever you interpret that A and B have the value true, so does A /\ B.
Going back to natural deduction, you can do the same (remembering to change |= to |-), for instance: A,B |- A /\ B
You can use the inference rules to prove that is true.
but now we're using the coq theorm prover to prove more complex statements
You have to be careful here. Coq doesn't use Natural Deduction, but something called Intuitionistic Logic. This may be out of the scope of this question, but if you want more information here's the wikipedia page: