See how we have P in a premise and P in the conclusion?

We have to get the P out of the conjunction and back into the conclusion.

How can we get P out of this premise?

First we have to ask, What's the connective?

The connective is conjunction. This tells us we want to use a conjunction-rule. But is it the introduction or elimination rule that we need?

It's elimination. Nearly always we need elimination when we're acting on premises.

See how the rule matches our premise.

Because we have a match, we can use this rule to add a line to our proof.

The rule allows us to add 'P' or 'Q' to the proof, but I've chosen to add 'P'.

Now having used the rule we have to explain exactly what we've done. This requires two things ...

We must cite the rule used.

And we must cite the lines we applied the rule to.

So far so good. Can you see what we should do next?

Getting the R out of the second premise can be done in exactly the same way.

Now, how are we going to get to the conclusion?

In general, we use introduction rules to get to the conclusion. And since this conclusion is a conjunction, we'll use conjunction-intro to get to it.

Look at the rule for conjunction intro.

See how our proof fits the pattern of the rule.

So it turns out we already did what we need for conjunction intro.

All that's left is to explain what we've done. As before this requres two things.

We must cite the rule used.

And we must cite the lines we applied the rule to.

Note the pattern of rules that we have for conjunction: introduction and elimination.

For each connective we'll have such a pair of rules, one introduction rule and one elimination rule.

With the elimination rule, we have the connective at the start and we eliminate it in applying the rule.

See how this worked in our proof.

With the introduction rule, we don't have the connective at the start and we introduce it by appling the rule.

Here's how we did it in the proof.

If you've been following all this, you know everything you need to know to use conjunction intro and conjunction elim in proofs. You also know how to do Fitch proofs. The rest is just a matter of learning more rules.

Now it's possible you haven't entirely been following all this ...

... When I was learning logic, I often didn't immediately understand the lectures and needed to go back over my notes after each lecture. Hopefully you will do the same because I don't really have the patience for spoon feeding.

When you start an exercise, you’re already given the basic form of the proof, with a couple of blank lines.

The box you’re working in is just a text editor. You can add lines by pressing ‘return’ and delete lines just like you would in any text editor.

To repeat: the proof is just some text that you edit in the normal way.

We just need to a step here.

I’ve gone ahead and typed A because we need to derive A from the premises.

Here’s the A I typed.

This red dot suggests that there is a problem with the line.

The text under or proof is giving us a clue: we didn’t justify the step yet. Let’s do that now.

Here I’ve added justification.

It’s over here on the right (I just added spaces to move it away from the sentence ‘A’).

I want to mention a couple of conventions.

First, justification needs to start with ‘//’. This is to separate justification from the sentence itself.

If you forget the ‘//’, zoxiy won’t be able to understand your proof and won’t be able to explain to you what went wrong.

The next thing to note is that I typed the word ‘and’ rather than the symbol for conjunction (‘∧’). As a convenience, zoxiy will let us use words rather than making us type symbols. But we can type the symbols if we prefer.

The same is true when we’re writing sentences: you can type ‘A and B’ instead of ‘A ∧ B’ if you like.

This is a handy feature of awFOL vs the language of the textbook we’re using. awFOL let’s you use words where really there should be a symbol, just to make it easy to type things.

Finally, note that we put a number at the end. This is the number 1, which refers to the first line.

zoxiy provides line numbers for us (you can add your own if you prefer, but then you have to be really consistent about starting each line with a number).

Wait a minute. We still have that red dot and the error message telling us our line is not justified. But we have added the justification. What’s going on?

zoxiy might be a bit slow to update. In this situation, just move your cursor up and down to get zoxiy to check your line again. Let me do that now ...

... and the dot has turned green, indicating that this line is ok.

What’s next?

We need to add another step to the proof.

(It just happens that we have the right amount of space for this proof, but generally you are going to have to add lines to your proof. Do this with the return key, as mentioned above.)

Here I’ve added the setntence we need (‘C’).

And here’s the justification as well.

But wait, the red dot is back. That means there’s something wrong with the line. What has gone wrong?

The status message is really unhelpful in this case, as it often will be. (Maybe it will be improved at some point.) Sorry about that.

What could have gone wrong? Note that we’re citing line 1.

So let’s have a look at line 1.

This line contains ‘A and B’.

But actually we’re trying to derive C. And you can’t derive C from A and B.

The C we want to derive is actually here, in line 2.

So we have to edit the line number. (This kind of mistake tends to happen to me quite a bit because I like to copy and paste justification to save typing)

Here I’ve fixed the line number.

What’s next?

There’s a big whole where the justification for the last line should be. (Remember that every line of the proof is either a premise or needs justification.)

So I’ve gone ahead and added the justification.

But it hasn’t worked: we’ve got the red dot again. Unless you’re really good at logic, you’re going to be seeing a lot of the red dot for a few weeks.

Here’s the mistake: we’re still citing and elim. But at this point we’re supposed to be *introducing* a conjunction rather than eliminating one.

We can fix this just by deleting ‘elim’ and replacing it with ‘intro’

And here’s the finished proof. This is correct; if you submit it, zoxiy should say your proof is correct.