Concise introduction to first-order deductive system with free-variable formulas

246 Views Asked by At

In first-order logic, sentences are a subset of (well-formed) formulas, viz. those that do not have free variables. With most deductive systems in the literature, one may only prove sentences, but not formulas with free variables.

EDIT

Since some do not think this, let me quote from Language, Proof and Logic by Barker-Plummer, Barwise and Etchemendy:

Before getting down to the rules, though, we should emphasize that formal proofs in the system F contain only sentences, never wffs with free variables. This is because we want every line of a proof to make a definite claim. Wffs with free variables do not make claims, as we have noted. Some deductive systems do allow proofs containing formulas with free variables, where such variables are interpreted universally, but that is not how the system F works.

END OF EDIT

However the latter do exist, e.g. Henkin (1949), Tarski (1965), Kalish and Montague (1965). But these are very concise completeness proofs and hardly show object proofs. I am looking for a textbook (or a PDF of some logic course, etc.) where such a system is presented in more detail with examples. It does not have to be an introductory logic book (in fact, conciseness is preferred for everything other than the presentation of the deductive system).

(Such books are mentioned in this question, but without any specific examples.)

1

There are 1 best solutions below

2
On

With most deductive systems in the literature, one may only prove sentences, but not formulas with free variables.

I totally disagree with this claim. On the contrary, since sentences cannot be defined inductively and all deductive systems build the proof of a sentence in a inductive way, then by necessity deductive systems for first-order logic have to deal with formulas with free variables.

To prove a formula of the form $\forall x \, A(x)$ you typically prove $A(x)$ (where $x$ is a free variable in $A$) and then use the universal generalization rule to infer $\forall x \,A(x)$. Dually, as Mauro Allegranza correctly said in his comment to your question, any deduction system allows you to derive say $y = y$ (which is a formula with a free variable $y$) from $\forall x \, x = x$ (principle of universal instantiation).

More in general, take any derivation $\pi$ of some formula $A$ in propositional logic in any deductive system, in $\pi$ replace any occurrence of a propositional variable $p$ in $A$ with an atomic formula of first-order logic $P(x)$ and you get for free a derivation of a formula with free variables in first-order logic (without quantifiers).

I am looking for a textbook (or a PDF of some logic course, etc.) where such a system is presented in more detail with examples.

I suggest to study sequent calculus and natural deduction as deductive systems. They are deductive systems with many good properties and they deal with formulas with free variables in a natural way. Maybe natural deduction is more intuitive and accessible for a beginner.

In my opinion, for natural deduction, van Dalen's textbook and Chiswell & Hodeges' textbook are excellent references. Also, here you can find a lot of examples of derivations in natural deduction. In these examples, take a derivation whose last rule is $\forall_I$ (the universal generalization rule for natural deduction), drop the last rule and you get a derivation of a formula with a free variable.

I guess an accessible introduction to sequent calculus is Girard's textbook (Chapter 5), even if this is a bit for specialists.