Extending our approach to sets of formulas

Extending our approach to sets of formulas

Students of logic are usually taught at first about tautologies, contradictions, and contingent propositions. However, these are not the notions you will encounter in more advanced, and more modern, works. This is at least partly because these notions are usually used for individual formulas, while a lot of the times, we want to talk about sets of formulas instead.

One thing that we can immediately extend to sets of formulas is contingency. Sometimes, it is not just one formula that has a model, but a whole set of them. Indeed, perhaps an infinitely large set of them! In these cases, we sometimes say that the set $S$ of formulas is (zeroth-order) satisfiable or semantically consistent. This can be captured in a precise manner as follows:

Here is a useful way to think about consistency and contingency:

Here is an interesting fact about consistency and contradictions:

On the other hand, we have:

Validity

Here comes something magical. So far, we talked about certain sets of formulas that are satisfiable, and certain sets of formulas that are unsatisfiable. And this boiled down to whether the set of formulas have a common model, or they do not. Now as it turns out, satisfiability and unsatisfiability are sufficient to define the central notion of logic: validity.

This may not be apparent at first. Take the usual definition of validity:

(A1) An argument is valid iff whenever the premises are true, the conclusion must also be.

It seems like this has absolutely nothing to do with whether sets of formulas are satisfiable. Not so fast!

What is an argument? We can define it as such:

This could be formalized with more structure, using ordered sets and whatnot, but what I want to emphasize here is that arguments are just sets of formulas with some designated members.

Let’s return to validity. Validity says that if an argument is valid, then whenever its premises are true, its conclusion must also be true. You may ask yourself: is it possible for a valid argument’s premises to be true, but its conclusion to be false? It seems not, since that is exactly what validity excludes. It says that if a valid argument’s premises happen to be true, then whatever else is the case, the conclusion must also be true. Thus, we can also characterize validity as follows:

(A2) An argument is valid iff it is impossible for its premises to be true, but its conclusion to be false.

Note the word ‘impossible’ in italics. What does it mean that it is impossible for the premises to be true and the conclusion to be false? Well, it just means: there cannot be a structure $\mathbf{S}$ such that $\mathbf{S}$ models the premises, but $\mathbf{S}$ does not model the conclusion. Let’s use some specific variables to make this more precise.

Suppose you have an argument with (possibly infinite) premises $P=\{X_1, X_2, …\}$, and conclusion $Y$. Then, by the above, if this argument is valid, that means there is no structure $\mathbf{S}$ such that $\mathbf{S} \models X$ for all $X \in P$, but $\mathbf{S} \not\models Y$ (the conclusion). We also know that $\mathbf{S} \not\models Y$ iff $\mathbf{S} \models \neg Y$, so we can say: if an argument is valid, that means there is no structure $\mathbf{S}$ such that $\mathbf{S} \models X$ for all $X \in P$, and $\mathbf{S} \models \neg Y$. Again, this is just a formal way of saying it is impossible for the premises to be true but the conclusion to be false (or equivalently, it is impossible for the premises to be true, and the negation of the conclusion to also be true).

But note that now we really are talking about unsatisfiability! For what we just described may simply be put: the set $\{X_1, X_2, …, \neg Y\}$ is unsatisfiable. And this is, indeed, what validity boils down to. In particular, an argument is valid if, and only if its premises, together with the negation of its conclusion, are unsatisfiable. And again, all this just means that it is impossible for a valid argument to have true premises and a false conclusion. Thus:

Validity and tableau

From the above, you may already see how reasoning with sets of formulas is implemented in our system. With single formulas, we had that if every possible tree for $\neg X$ remained open, that must mean $\neg X$ is satisfiable (i.e., it is a tautology or contingent), which in turn ensures that $X$ is not a tautology. On the other hand, if there is a possible tree for $\neg X$ that closes (closes on all its branches), then $X$ is indeed a tautology, since its negation is not satisfiable. Similarly, but with sets of formulas, if a tree for $\{X_1, X_2, …, \neg Y\}$ closes at least once, then $\{X_1, X_2, …, \neg Y\}$ is not satisfiable, which in turn means that $\{X_1, X_2, ..\}$ entails $Y$. On the other hand, if no tree for $\{X_1, X_2, …, \neg Y\}$ closes, that means the set is satisfiable, and $\{X_1, X_2, …\}$ does not entail $Y$.

The only question is: how do we work with multiple formulas, when in the simpler case, we put the sole formula $\neg X$ at the root of the tree (when trying to prove $X$ is a tautology)? First, with arguments, we put the negation of the conclusion at the root of the tree. So if we are considering whether the set $S=\{X_1, X_2, …\}$ of premises is such that $S \vdash Y$, we put $\neg Y$ at the root of the tree.

The other change is more substantial. We introduce a very simple new rule into the system that enables us to inject any one of the premises at any part of our derivation. Thus:

Note that $X$ and $Y$ here are completely independent of one another. $X$ may be any formula that you happen to consider at any one point of your proof, and $Y$ can be any formula as long as it is one of the premises under consideration. Accordingly, the premise rule is radically different from all the previous rules, since it does not ‘depend’ on any formula at any one point of the tree. In other words, you can put any premise down at any one point of your derivation, and in fact, as many times as you want.

The relationship between the premise rule and all the other rules of our tableau system is similar to the relationship between the base rule and the productive rule(s) in our syntactic derivations.

Suppose you want to show that $\{X, X \rightarrow Y\} \vdash Y$. This is usually called Modus Ponens, and it is a valid argument form. In other words, for any choice of $X$, $Y$, it is true that $\{X, X \rightarrow Y\} \models Y$. So let’s show the corresponding fact syntactically.

As noted above, the first step here is to put the negation of the conclusion at the root of the tree derivation. Since $Y$ is the conclusion, the tree will start out as such:

Now unlike with tautologies, just having the negation of the conclusion gets us nowhere (if the conclusion is not itself a tautology). In fact, in this case, there is no rule you can use on $\neg Y$ to get further. On the other hand, what you can do is use the premise rule. There are two premises, so you have a choice. It is not always the case that all the premises are used, and in fact, the order in which they are used is also not predetermined, so there is a degree of freedom here.

Let’s start with the more complex premise:

Great! You should now see that you can use one of your other rules on the new formula. Thus:

You may have immediately noticed that the right side branch closes by the occurrence of $Y$ and $\neg Y$ on it. Thus, we have:

On the other hand, you might also see that the left hand side branch of the tree remains open, and there are no formulas left on which we might apply a rule. Thus, we have to look for another premise. (Not) incidentally, our other premise, $X$ is just what we need. In particular:

Accordingly, we can conclude that $\{X, X \rightarrow Y\} \vdash Y$.

Let’s look at a more complicated proof before it is your turn. Suppose you want to evaluate the following argument:

As a first step, like before, we put the negation of the conclusion at the root of our tree. Thus:

Note that we are negating the whole formula, so you have to provide the outer parentheses if they were omitted previously.

It is a good idea to break this down a bit more immediately, since it won’t branch.

As before, there are various ways to proceed, some shorter than others. In particular, we could start breaking down $Q \vee Z$. However, this would make the proof longer than necessary. Once you are more comfortable with how the system works, you will be able to see this.

For now, let’s proceed by adding $\neg \neg Y$ with our premise rule. We could immediately simplify it further, but for now, we will leave it as is. So we have:

Then, we can add the other premise to our tree, again, non-branching:

We now have a choice to branch. But doing the proof briefly in our head, we immediately see that if we branch to $X$ and $\neg Y$, our tree immediately closes by $\neg X$ and $\neg \neg Y$. On the other hand, if we branch to $Q$ and $Z$, nothing happens, and we still need to branch further to $X$ and $\neg Y$ to close the tree. And in fact, in the latter case, we have to do it twice, resulting in four branches in the end.

So the simplest way is to go immediately to:

Again, you can compare this to:

And in fact, if you branched immediately at the beginning as many times as possible, and applied every rule as many times as possible, you would have had this:

Now this may not look that bad on paper, but notice that the first proof had 7 occurrences of formulas, the second had 11, while the last one had 22! On the other hand, none of these proofs are incorrect. It is just that they become less and less elegant.

On soundness and completeness, again

Note that we can now reformulate our soundness and completeness claims from above in a stronger form. Previously, we had:

$$\models X \textit{ iff } \vdash X$$

Again, from left to right, this is completeness, and from right to left, this is soundness. But we also have a stronger version of this, with multiple formulas, as opposed to singular ones. In particular: $$A \models X \textit{ iff } A \vdash X$$ Or in words, $A$ semantically entails X iff $A$ syntactically entails X. And once again, from left to right, this is (strong) completeness, and from right to left, this is (strong) soundness (for zeroth-order logic).

We shall not prove this biconditional in this book, as it involves more advanced techniques than we are ready for. However, we can note one of its very interesting consequences.

Let’s negate both sides of the biconditional again, just as before. Then, we get: $$A \not\models X \textit{ iff } A \nvdash X$$ Again, we can try and unpack the two sides, and see what we get. First, if $A \nvdash X$, that means that $\neg X$ cannot have a closed tableau, no matter which members of $A$ are used in any of the attempted trees. In other words, all the trees starting with $\neg X$ will remain open, no matter how long they might be.

On the other side, we have that $A \not\models X$, i.e., that $A$ does not semantically entail $X$. Now previously, we defined semantic entailment in terms of unsatisfiability. In particular, $A$ semantically entails $X$ provided the set $A$ together with $\neg X$ form a set (precisely $A$ plus $\neg X$) that is unsatisfiable. Accordingly, $A$ does not semantically entail $X$ provided $A$ together with $\neg X$ is not unsatisfiable. Or in other words, $A$ together with $\neg X$ is satisfiable.

Putting the above two results together, we then get that $A$ together with $\neg X$ is satisfiable iff $\neg X$ does not have a closed tableau from premises $A$.