Home MATH 318 Friday, September 30, 2011

Friday, September 30, 2011 CC-BY-NC
The rules of formal logic

Maintainer: admin

1Introduction to formal logic

A formal proof is a finite collection of lines, each of which is a sequent (i.e. an expression of the form $\Phi_1, ... \Phi_n \vdash \Psi$, where each of $\Phi_1, ... \Phi_n, \Psi$ is a formula; $n=0$ is allowed), in a specific order and abiding by specific rules. Each line in a proof should either be valid by itself or should logically follow from one or more earlier lines.

2Structural rules

Let $\Gamma = \{ \Phi_1, ...\Phi_n \}$. We then have the following structural rules:

2.1Monotonicity

$$\frac{\Gamma \vdash \Psi}{\Gamma' \vdash \Psi}$$

provided $\Gamma \subseteq \Gamma'$ (so $\Gamma'$ is a superset of $\Gamma$). So we can always increase the number of premises and reach the same conclusion we reached in an earlier line, as long as the earlier line is valid. This is true even if a contradiction occurs among the premises - after all, by material implication, $\bot$ implies everything.

2.2Transitivity

$$\displaylines{\Gamma \vdash \Psi \\ \frac{\Gamma, \Phi \vdash \Psi}{\Gamma \vdash \Psi}}$$

So $\Phi$ is basically a lemma.

2.3Deduction

This one is really two rules, and is the only principle that is completely reversible.

$$\frac{\Gamma \vdash \Phi \to \Psi}{\Gamma, \Phi \vdash \Psi} \quad \text{ and } \quad \frac{\Gamma, \Phi \vdash \Psi}{\Gamma \vdash \Phi \to \Psi}$$

2.4Contradiction

Not completely necessary, but the more rules you have, the easier (and shorter) your proofs get. This rule is basically proof by contradiction - once you reach a contradictory conclusion, you know that the premises can't all be true.

$$\frac{\Gamma, \Phi \vdash \Psi \land \neg \Psi}{\Gamma \vdash \neg \Phi}$$

2.5Tautology

If $\Phi_1 \land ... \land \Phi_n \to \Psi$ is a tautology, then we can put $\Phi_1, ... \Phi_n \vdash \Psi$ in any line of any proof, no justification necessary.

These rules don't really tell us much about the reasoning, but it's a good idea to keep them explicit. Note: the order of things on the left side is unimportant, although keeping them consistent may be less confusing.

3Valuation within predicate logic

Valuation: a function $V: L_{\Sigma} \to \{\top, \bot\}$ with the same basic rules as in propositional logic so I'm not going to type them up again.

Note that there is nothing in the definition preventing $V(x = x) = \bot$ from being true, i.e. the definition of valuation says nothing about squality. So $x=x$ may be an axiom, but it is certainly not a tautology (or even a formula - we can't even make a truth table for this because there are no valuations). On the other hand, $Px \lor \neg Px$ is, where $P$ is a unary predicate symbol.

4Rules for quantifiers

4.1For-all elimination

You can put this in any line of a proof:

$$\forall x \Phi(x) \to \Phi(t)$$

"If it's true for anything, then it's true for any specific thing." Make sure to change the bound variable to something free, so you avoid a clash of variables.

Examples:

$$\forall x\exists y(\neg(x=y)) \to \exists y(\neg (x=y)) \,\checkmark$$

$$\forall x \exists y (\neg (x=y)) \to \exists y(\neg(0 = y))\, \checkmark$$

$$\forall x \exists y(\neg(x=y)) \to \exists y(\neg (x=SSz)) \,\checkmark$$

$$\forall x \exists y(\neg(x=y)) \to \exists y (\neg (y=y)) \,\times$$

$$\forall x \exists y (\neg(x=y)) \to \exists y (\neg(Sy=y)) \,\times$$

The last two are invalid because of the clash of variable thing.

More to come next lecture.