Kevin T. Kelly
Department of Philosophy
Carnegie Mellon University
Syntax is about linguistic form. It makes no reference to interpretation or meaning. Semantics concerns interpretation. Syntactic considerations include well-formedness, substitution, and rules of proof. Such matters may be heuristically guided by intended interpretations, but they are all specifiable independently of such interpretations.
Individual variables {x0, ..., xn, ...}.
Relational constants {=} (optional).
Propositional constants {_|_}.
Connectives {--->, v, &}.
Quantifiers {A, E}. (These will have to do in HTML).
-P = (P ---> _|_).
(Ex)P = -(Ax)-P.
(Q <---> R) = (Q ---> R) & (R ---> Q)
Individual constants {c0, ..., cn, ...}.
Function symbols {f0, ..., fn, ...}.
Predicate symbols {P0, ..., Pn, ...}.
Propositional variables {p0, ..., pn, ...}.
mapping a that assigns natural numbers to predicates and function symbols.
Interpretation: a(Pn) = the number of arguments Pn is suppoed to take.
You may think of constants as 0-ary functions and propositional variables as 0-ary predicates.
The set of terms is the least set closed under the following conditions:
ci is a term.
xi is a term.
If a(fi ) = n, and t1, ..., tn are terms, then fi (t1, ..., tn) is a term.
The set of formulas of L is the least set closed under the following conditions:
qi is a formula.
If t, t' are terms, then (t = t') is a formula.
If a(Pi) = n and t1, ..., tn are terms, then Pi (t1, ..., tn) is a formula. (such formulas are atomic).
If Q, R are formulas and # is a connective then (Q # R) is a formuila.
If Q are formulas then (Axi)Q is a formula.
Example of what we want: substitutions should not be made on bound variables.
((Ax)(P(x) ---> Q(x)) & Q(x))[t/x] = ((Ax)(P(x) ---> Q(x)) & Q(t)).
The concept is formally defined by recursion on the syntax of L. Since the syntax of L is defined in two inductions, the recursive definition must follow both, starting with terms and ending with formulas.
Let x, y, z be variables and f be a function symbol. Define:
a[x/y] = a.
z[x/y] = x if y =z and z[x/y] = z otherwise.
f(t1, ..., tn)[x/y] = f(t1[x/y], ..., tn[x/y]).
Let p be a propositional variable, P be a predicate symbol and # be a connective. Define:
p[x/y] = p.
(t = t')[x/y] = (t[x/y] = t'[x/y]).
P(t1, ..., tn)[x/y] = P(t1[x/y], ..., tn[x/y]).
(Q # R)[x/y] = (Q[x/y] # R[x/y]).
((Az)Q)[x/y] = (Az)Q if y = z and ((Az)Q)[x/y] = (Az)(Q[x/y]).
The idea: in the formula ((Ax)(P(x) ---> S(x)) & Q(x)), the variable x occurs once free (in Q(x)) and once bound (in S(x)). Thus, a variable can both occur free and occur bound in the same formula.
Abbreviation:
FV(x, Q) = some occurrence of x is free in Q.
not FV(x, a)..
FV(x, y) <===> x = y.
FV(x, f(t1, ..., tn) = FV(x, t1) v... v FV(x, tn).
not FV(x, p).
not FV(x, _|_).
FV(x, P(t1, ..., tn)) <===> FV(x, t1) v... v FV(x, tn).
FV(x, Q # R) = FV(x, Q) v FV(x, R).
FV(x, AyQ) <===> FV(x, Q) & not (x = y).
The idea: would substituting t in for x in Q lead to variables occurring in t becoming bound by quantifiers occurring already in Q. Such substitutions would lead to spurious inferences in our proof system so they must be excluded by a syntactic criterion.
To save writing, abbreviate
t is free for x in Q = FF(t, x, Q).
This concept doesn't need a separate recursion on terms because it calls FV. Define:
FF(t, x, p).
FF(t, x, _|_).
FF(t, x, P(t1, ..., tn)).
FF(t, x, (Q # R)) <===> FF(t, x, Q) & FF(t, x, R).
FF(t, x, (AyQ)) <===> FF(t, x, Q) & not (FV(x, t) and FV(x, Q)).
Sorry, I have to write the rules sideways. The marginal line is now an underline. I will let P, Q, R range over formulas of L in this section.
-P abbreviates (P ---> _|_)
(Ex)P abbreviates -(Ax)-P
[ _|_ ]"everything introduction"
from _|_, you may conclude P.
[& I]
from available P, Q, you may conclude (P & Q).
[v I]
from available P, you may conclude (P v Q).
from available Q, you may conclude (P v Q).
[---> I] "conditional proof"
from a subproof P ...Q, that uses only P together with available formulas, you may conclude (P ---> Q) and then you must make P ...Q unavailable.
[& E]
from available (P & Q), you may conclude P.
from available (P & Q), you may conclude Q.
[v E] "case argument"
from available (P v Q), a subproof P ...R, using only P and available formulas and a subproof Q...R, using only available formulas, you may conclude R and then make P ...R, and Q...R, unavailable.
[---> I] "modus ponens"
from available (P ---> Q) and from available P, you may conclude Q.
[- E] "reductio ad absurdum"
from a subproof -P... _|_, (underlined bottom loses its bottom) you may conclude P and then make -P... _|_ unavailable.
Note: the classical inference is
Notice that the "not" is elminated. The other version, which introduces "not"...
...is intuitionistic:
Subproof lines are on the side. Line numbers are given to show which available premises were used. Remember that you aren't allowed to use anything next to a line when the line stops! Notice that this example has two nested subproofs.
[A I] "universal generalization"
If x is not free in any uncancelled hypothesis on which Q depends and if Q is available, then you may conclude (Ax)Q. A hypothesis is a formula at the top of a vertical line.
The motivation for this rule is that any valid inference that works for arbitrary variable x must work for any term whatsoever since we "know" nothing special about x that would have aided the proof. If the restriction is violated, things can go very wrong.
[A E] "universal instantiation"
If t is free for x in Q and if (Ax)Q is available then you may conclude Q[t/x].
The motivation for this rule is that if you know (Ax)Q, you know Q holds of everything, so why not conclude Q[t/x]?
But this can go very wrong if t has a free variable that becomes bound when t is substituted into Q. Then you end up making some sort of general claim you didn't intend. For example:
[E I] "existential generalization"
If t is free for x in Q and Q[t/x] is available then you may conclude (Ex)Q.
This rule may be justified in terms of the other rules.
Suppose t is free for x in Q(x) and suppose that Q(t) occurs so far in a derivation. We may continue the proof as follows (I'm going to start using the intuitionistic derived rule [- I]).
[E E] "existential instantiation"
If x does not occur free in Q and (Ex)P is available and there is a subderivation P ... Q depending on available hypotheses in which x does not occur free, then you may conclude Q. A hypothesis is a formula at the top of a vertical line.
This rule also follows from the othes. Suppose x does not occur free in Q and (Ex)P(x) is available and there is a subderivation P(x) ... Q depending on available formulas in which x does no occur free. Then we may continue to argue as follows:
you may always conclude x = x.
if x = y is available, you may conclude y = x.
if x = y and y = z are available, you may conclude x = z.
if x1 = y1, ..., xn = yn, are all available, you may conclude t(x1, ..., xn) = t'(x1, ..., xn).
if x1 = y1, ..., xn = yn, Q(x1, ..., xn) are all available, you may conclude Q(x1, ..., xn).
Intuitionistic logic allows all of the above rules, including the quantifier rules, except for [- E].
Let S be a set of formulas and let Q be a formula.
We say that S |- Q <===> there exists a classical natural deduction derivation from formulas in S to Q.
If intuitionistic derivability is intended you can write |-i.
Say that S |= Q just in case every interpretation making each element of S true (this is a semantic concept) also makes Q true. We refer to |= as the semantic entailment relation. Let S be a subset of L, and let Q be a formula of L without free variables.
Soundness Theorem: S |- Q ===> S |= Q.
I.e., every deriviation is truth preserving.
Completeness Theorem (Gödel): S |= Q ===> S |- Q.
I.e., every truth preserving inference has a deriviation.
These results are proved in 80-310 and will be assumed in this class without proof.