Can you only construct proofs for tautologies?

Question

I'm studying Logic and Discrete Structures and we are covering natural deduction. We're using Jape to construct proofs and I'd like to know if we can only construct proofs for a formula if it is a tautology?

If so would the proofs for these tautologies be in the classical conjecture pane as opposed to the invalid conjecture pane? It seems like the truth tables for the formulas in the invalid conjecture pane are not tautologies.

Answer 1

The first thing to point out is that in Jape you don't so much prove statements to be tautologies, as that you demonstrate that some statement can be derived from other statements.

This is what the $\vdash$ symbol is for that you see in all of the panes: it is used to claim that some statement can be derived from others. For example:

$$P \to Q, P \vdash Q$$

is the claim that $Q$ can be derived from $P \to Q$ and $P$.

Here, the statement that is being derived is typically called the conclusion, while the statements from which you derive the conclusion are called the premises or givens.

Note that this claim is a claim about some relationship between logic expressions. As such, this is a 'meta-logical' statement, rather than a logic statement/expression in and of itself. But, like any claim, this meta-logical claim is true or false, which is why it is called a Conjecture.

All of the Conjectures in the Invalid conjectures window are false conjectures, e.g. $$E \to (F \to G) \vdash (E \to F) \to G$$ claims (conjectures) that $$(E \to F) \to G$$ can be derived from $$E \to (F \to G)$$

but that is false: As it turns out, $(E \to F) \to G$ can not be derived from $E \to (F \to G)$.

On the other hand, all conjectures in the Classical conjectures and the Conjectures windows are true. (the difference between 'Classical conjectures' and 'Conjectures' seems to be that the conjectures in the 'Classical conjectures' window are more 'elementary'.

OK, so with that out of the way, let's see how all of this applies to tautologies.

First, you'll note that some conjectures do not contain the $\vdash$ symbol. For example, the Classical Conjectures window contains $$E \lor \neg E$$ as a conjecture. OK ... so then exactly what is the Conjecture here then? Well, you should treat this as the conjecture $$\vdash E \lor \neg E$$, i.e. that $E \lor \neg E$ can be derived using no premises at all.

[I must say that I am not happy with the fact that the authors of Jape leave out the $\vdash$ in these cases: As I said, something like $$\neg \neg E \vdash E$$ is a meta-logical claim, but $$E \lor \neg E$$ is, by itself, a logical expression, and so we really have two quite different kinds of claims in the conjecture windows. I really would have preferred it had the authors had used $$\vdash E \lor \neg E$$

since that is, undoubtedly, the actual conjecture that is being made here about $$E \lor \neg E$$]

Now, any statement can can be derived from no premises at all is a tautology. Indeed, $E \lor \neg E$ is a tautology. So, that should answer your question that you pose in the body of your post:

would the proofs for these tautologies be in the classical conjecture pane as opposed to the invalid conjecture pane?

The answer is (slightly nuanced) Yes: you will never see a tautology appear in the Invalid conjectures window. Instead, it may appear in the Classical conjectures window ... though (and here's the nuance) a more complicated (less 'elementary') tautology could appear in the Conjectures window. In fact, we see a number of tautologies in the latter window. That very first one:

$$A \to (B \to (A \to B))$$

is a tautology, and so, as a conjecture:

$$\vdash A \to (B \to (A \to B))$$

it is a true conjecture.

OK, so what if a statement is not a tautology? You ask:

I'd like to know if we can only construct proofs for a formula if it is a tautology?

Again, the answer is a (nuanced) Yes: If we have a statement that is not a tautology, e.g.:

$$P \to (P \land Q)$$

then we cannot derive that statement from no premises. That is, the conjecture:

$$\vdash P \to (P \land Q)$$

is False. So, this is something you could find in the Invalid conjectures window (although the authors of Jape would probably drop the $\vdash$ symbol and put

$$P \to (P \land Q)$$

in the Invalid conjectures window. Interestingly, there are no such examples (of a single statement that is not a tautology) in the Invalid conjectures window.

So yes, if a statement is not a tautology, then there is no proof for it ... if (here's the nuance) there are no premises. OK, so what if you do have premises? Well, let's go back to:

$$\neg \neg E \vdash E$$

Here, the conclusion $E$ can be derived from premise $\neg \neg E$. As such, we often say that we 'prove $E$' ... though what we really should say is that we 'prove $E$ from $\neg \neg E$'.

The point is: the way we talk about 'proving statements' is often such that the statement we prove is in fact not a logical tautology. For example, the statement

$$1 + 1 = 2$$

is not a tautology, and accordingly the conjecture:

$$\vdash 1 + 1 = 2$$

is False.

However, we can still prove the statement to be true given a bunch of premises: premises that define the numbers $1$ and $2$, and that define how addition is supposed to work. Thus, we what we do have is that:

$$PA \vdash 1 + 1 = 2$$

where $PA$ ('Peano Arithmetic') is a standard set of axioms that mathematicians and logicians like to work with to prove mathematical theorems.

So, long story short: when in the title of your post you ask:

Can you only construct proofs for tautologies?

one could also say 'No': you can prove statements from other statements, and the proven statements need not be tautologies.

OK, that's a lot to throw at you at once, but read it over a few times, see if it makes sense, and let me know if you have any further questions.