Formulas

Symbols

Fix a set of distinct symbols %$(,),=,\land ,\lor ,\rightarrow ,\leftrightarrow ,\lnot ,\forall ,\exists$%, plus infinitely many new (that is, different from any of the symbols so far mentioned) distinct symbols called variables. I shall use the greek letter nu, %$\nu$%, possibly with subscripts, as a metalinguistic variable to range over variables. I have included more symbols than is necessary: one can define %$\land$% from %$lnot$% and %$\lor$%, and many other simplifications are possible. That means that my definitions of formula and proof are unnecessarily long. I feel that it is useful for pedagogical purposes to see the redundant definitions given here.

Let the language %$\mathcal L$% be a set of (new) relation symbols and (new) constant symbols (I'm omitting function symbols for simplicity) with a number associated with each relation symbol (its number of places). The members of %$\mathcal L$% are called nonlogical symbols.

Formulas

The formulas of the language %$\mathcal L$% are defined recursively as follows:

1. A variable or a constant symbol followed by = followed by a variable or a constant symbol is a formula.
2. A relation symbol from %$\mathcal L$% followed by a list of variables and constant symbols from %$\mathcal L$% of length the number of places of the relation symbol is a formula.
3. If %$\phi$% and %$\psi$% are formulas of the language %$\mathcal L$%, then so are %$(\phi\land\psi )$%, %$(\phi\lor\psi )$%, %$(\phi\rightarrow\psi )$%, and %$(\phi\leftrightarrow\psi )$%.
4. If %$\phi$% is a formula of the language %$\mathcal L$%, then so is %$(\lnot\phi )$%.
5. If %$\phi$% is a formula of the language %$\mathcal L$% and %$\nu$% is a variable, then %$\forall\nu\phi$% and %$\exists\nu\phi$% are formulas of the language %$\mathcal L$%.

Free variables

If %$\theta$% is a formula of a language %$\mathcal L$%, then the set of free variables of %$\theta$%, %$\text{Fv}\theta$% is defined by recursion on the formation of %$\theta$% as follows:

If %$\theta$% is a formula of a language %$\mathcal L$% according to either of the first two clauses of the definition of a formula, then %$\text{Fv}\theta$% is just the set of variables that actually occur among the symbols in the formula %$\phi$%.

If %$\theta$% is formed from %$\phi$% and %$\psi$% according to the third clause of the definition of a formula, then %$\text{Fv}\theta =\text{Fv}\phi\cup\text{Fv}\psi$%, the union of the sets of free variables of the formulas from which %$\theta$% was formed.

If %$\theta$% is %$(\lnot\phi )$%, then %$\text{Fv}\theta =\text{Fv}\phi$%.

If %$\theta$% is a formula of a language %$\mathcal L$% according to the final clause of the definition of a formula formed from the formula %$\phi$$% and the variable %$\nu$%, then %$\text{Fv}\theta =\text{Fv}\phi \setminus\{\nu\}$%, the set of all the free variables of %$\phi$% except for %$\nu$%.

Sentences

A sentence of a language %$\mathcal L$% is a formula with no free variables. (That is, a formula %$\phi$% of a language %$\mathcal L$% is a sentence if %$\text{Fv}\phi =\varnothing$%.)

Substitution

If %$\theta$% is a formula of the language %$\mathcal L$%, %$\nu$% is a variable, and %$t$% is a variable or a constant symbol of the language %$\mathcal L$%, then %$\theta (\nu /t)$%, the formula obtained from %$\theta$% by substituting %$t$% for every free occurrence of %$\nu$% is defined as follows:

If %$\theta$% is a formula of a language %$\mathcal L$% according to either of the first two clauses of the definition of a formula, then %$\theta (\nu /t)$% is the formula obtained from %$\theta$% by replacing every occurrence of %$\nu$% in %$\theta$% by %$t$%.

If %$\theta$% is formed from %$\phi$% and %$\psi$% according to the third clause of the definition of a formula, then %$\theta (\nu /t)$% is the formula obtained from %$\theta$% by replacing %$\phi$% in the formation of %$\theta$% by %$\phi (\nu /t)$% and %$\psi$% by %$\psi (\nu /t)$%.

If %$\theta$% is %$(\lnot\phi )$%, then %$\theta (\nu /t)$% is %$(\lnot \phi (\nu /t))$%.

If %$\theta$% is a formula of a language %$\mathcal L$% according to the final clause of the definition of a formula formed from the formula %$\phi$$% and the variable %$\nu$%, then %$\theta (\nu /t)$% is %$\theta$% (that is, no substitution is performed).

If %$\theta$% is a formula of a language %$\mathcal L$% according to the final clause of the definition of a formula formed from the formula %$\phi$$% and the variable %$\mu$% and %$\mu$% is distinct from %$\nu$%, then %$\theta (\nu /t)$% is the formula obtained from %$\theta$% by substituting %$\phi (\nu /t)$% for %$\phi$% in the formation of %$\theta$%.

Substitutability

The variable %$\mu$% is substitutable for the variable %$\nu$% in the formula %$\theta$% if any of the following conditions obtains:

The formula %$\theta$% is a formula of a language %$\mathcal L$% according to either of the first two clauses of the definition of a formula.

The formula %$\theta$% is formed from %$\phi$% and %$\psi$% according to the third clause of the definition of a formula and the variable %$\mu$% is substitutable for the variable %$\nu$% in both of the formulas %$\phi$% and %$\psi$%.

The formula %$\theta$% is %$(\lnot\phi )$% and the variable %$\mu$% is substitutable for the variable %$\nu$% in the formula %$\phi$%.

The formula %$\theta$% is a formula of a language %$\mathcal L$% according to the final clause of the definition of a formula formed from the formula %$\phi$$% and the variable %$\nu$%.

The formula %$\theta$% is a formula of a language %$\mathcal L$% according to the final clause of the definition of a formula formed from the formula %$\phi$$% and the variable %$\mu$%, and %$\nu$% does not occur free in %$\theta$%.

The formula %$\theta$% is a formula of a language %$\mathcal L$% according to the final clause of the definition of a formula formed from the formula %$\phi$$% and a variable other than %$\mu$% or %$\nu$%, and the variable %$\mu$% is substitutable for the variable %$\nu$% in the formula %$\phi$%.

Theorems

Inference Rules

Fix a language %$\mathcal L$%. From now on, formula means formula of the language %$\mathcal L$% and so forth.

There are two rules of proof for each of the symbols %$\land ,\lor ,\lnot ,\rightarrow ,\leftrightarrow ,\forall ,\exists$%, an introduction rule that starts with formulas in which the symbol need not occur and concludes with a formula in which the symbol does occur and an elimination rule that starts with at least one formula in which the symbol does occur and ends with a formula in which the symbol does not occur. (The situation is actually a bit more complicated for negation, but I won't go into details.) There are also rules for equality and structural rules concerning deducibility.

Let %$\Gamma$% be a (possibly empty) set of formulas. I shall write, for example, %$\Gamma , \phi ,\psi$% for the set formed by adding %$\phi$% and %$\psi$% to %$\Gamma$%. Each rule takes the form that a single formula can be inferred from a set of formulas. When %$\phi$% can be inferred from %$\Gamma$%, we write %$\Gamma\vdash\phi$%, read %$\phi$% is deducible (or provable) from %$\Gamma$%. The metalinguistic variables %$\phi ,\psi ,\theta$% always range over all formulas.

%$\land$% introduction (%$\land$%I)

From %$\Gamma , \phi ,\psi$%, infer %$(\phi\land\psi )$%. Concisely, %$\Gamma , \phi ,\psi\vdash (\phi\land\psi )$%.

%$\land$% elimination (%$\land$%E)

%$\Gamma ,(\phi\land\psi )\vdash\phi$% and %$\Gamma ,(\phi\land\psi )\vdash\psi$%.

%$\lor$%I

%$\Gamma,\phi\vdash (\phi\lor\psi )$% and %$\Gamma,\phi\vdash (\psi\lor\phi )$%.

%$\lor$%E

If %$\Gamma,\phi\vdash\theta$% and %$\Gamma,\psi\vdash\theta$%, then %$\Gamma,(\phi\lor\psi )\vdash\theta$%.

%$\rightarrow$%I

If %$\Gamma,\phi\vdash\psi$%, then %$\Gamma\vdash (\phi\rightarrow\psi )$%.

%$\rightarrow$%E

If %$\Gamma\vdash\phi$% and %$\Gamma ,\psi\vdash\theta$% then %$\Gamma ,(\phi\rightarrow\psi )\vdash\theta$%.

%$\leftrightarrow$%I

If %$\Gamma\vdash (\phi\rightarrow\psi )$% and %$\Gamma\vdash (\psi\rightarrow\phi )$%, then %$\Gamma\vdash (\phi\leftrightarrow\psi )$%.

%$\leftrightarrow$%E

%$\Gamma , (\phi\leftrightarrow\psi )\vdash (\phi\rightarrow\psi )$% and %$\Gamma , (\phi\leftrightarrow\psi )\vdash (\psi\rightarrow\phi )$%.

%$\lnot$%I

If %$\Gamma ,\phi\vdash\psi$% and %$\Gamma ,\phi\vdash (\lnot\psi)$%, then %$\Gamma\vdash (\lnot\phi )$%.

%$\lnot$%E

If %$\Gamma ,(\lnot\phi )\vdash\psi$% and %$\Gamma ,(\lnot\phi )\vdash (\lnot\psi)$%, then %$\Gamma\vdash\phi$%.

%$\forall$%I

If %$\Gamma\vdash\phi$% and %$\nu$% is not a free variable of any member of %$\Gamma$%, then %$\Gamma\vdash\forall\nu\phi$%.

%$\forall$%E

%$\Gamma,\forall\nu\phi\vdash\phi (\nu /t)$%, where %$t$% is a constant symbol or a variable that is substitutable for %$\nu$% in %$\phi$%.

%$\exists$%I

%$\Gamma ,\phi (\nu /t)\vdash\exists\nu\phi$%, where %$t$% is a constant symbol or a variable that is substitutable for %$\nu$% in %$\phi$%.

%$\exists$%E

If %$\Gamma ,\exists\nu\phi\vdash\psi$%, then %$\Gamma ,\phi\vdash\psi$%, if %$\nu$% is not a free variable of any member of %$\Gamma$%.

Reflexivity of %$=$%

%$\Gamma\vdash t=t$%, where %$t$% is a constant symbol or a variable.

Transitivity of %$=$%

%$\Gamma , r=s,s=t\vdash r=t$%, where %$r$%, %$s$%, and %$t$% are constant symbols or variables.

Substitution

If %$\phi$% is a formula according to either of the first two clauses of the definition of a formula, %$s$% and %$t$% are variables or constant symbols, and %$\psi$% is obtained from %$\phi$% by replacing some occurrences of %$s$% by %$t$%, then %$\Gamma ,s=t,\phi\vdash\psi$%.

Thinning

If %$\Sigma$% is a set of formulas and %$\Gamma\vdash\phi$%, then %$\Gamma\cup\Sigma\vdash\phi$%.

Cut

If %$\Gamma\vdash\sigma$% for every %$\sigma$% in %$\Sigma$% and %$\Sigma\vdash\phi$%, then %$\Gamma\vdash\phi$%.

Proofs and theorems

A derivation (or proof) of %$\phi$% from %$\Gamma$% is a finite sequence of inferences %$\Sigma_{i}\vdash\phi_{i}$% such that the last one is %$\Gamma\vdash\phi$% and such that each %$\Sigma_{i}\vdash\phi_{i}$% is shown to be a legitimate inference using only the rules above and %$\Sigma_{j}\vdash\phi_{j}$% for %$j<i$%. A sentence %$\phi$% is derivable from %$\Gamma$% or is a theorem of %$\Gamma$% if there is a proof of %$\phi$% from %$\Gamma$% or, equivalently, if %$\phi$% is a member of the smallest set %$\Sigma$% such that %$\Gamma\subseteq\Sigma$% and, for any formula %$\sigma$% if %$$\Sigma\vdash\sigma$%, then %$\sigma\in\Sigma$%.

Consistency

A set %$\Gamma$% of formulas is inconsistent if there is a formula %$\psi$% such that %$\Gamma\vdash\phi$% and %$\Gamma\vdash (\lnot\phi )$%. A set %$\Gamma$% of formulas is consistent if it is not inconsistent.

-- ShaughanLavine - 03 May 2009