Second order logic question.

Question

I'm reading Michael Potter's book "Set Theory and its Philosophy" and where he's explaining why he chose to use first-order predicate calculus with identity instead of second order logic to reason about sets, there is this paragraph on page 13 where I need some clarification about what exactly he's saying about second order logic. The paragraph is as follows:

It is undoubtedly significant, however, that a formalization of first-order logic is available at all. This marks a striking contrast between the levels of logic, since in the second-order case only the formation rules are completely formalizable, not the inference rules: it is a consequence of Godel’s first incompleteness theorem that for each system of formal rules we might propose there is a second-order logical inference we can recognize as valid which is not justified by that system of rules.

My questions: 1) Whats do we mean by the formation rules and the inference rules of a logic? I.e. whats the difference between the two types of rules?

2) Whats meant by "...for each system of formal rules we might propose there is a second-order logical inference we can recognize as valid which is not justified by that system of rules." I.e. how do we recognize something as valid if its not justified by the logics system of rules?

Answer 1

The formation rules are the rules that tell us whether a sequence of symbols is a ("well-formed") formula.

The second-order logical inference referred to is the reasoning that tells us that the Gödel sentence constructed from the axioms and inference rules is in fact true in the natural numbers.

Answer 2

Here is the explanation of the second part. Suppose that we have any effective, sound set $I$ of finitary inference rules for a second-order set theory, say $\text{ZFC}^2$ for concreteness.

We can equally well view $I$ as a set of inference rules for a two-sorted theory $T$ in first-order semantics which has exactly the same syntax as $\text{ZFC}^2$. The only difference is that in this theory we cannot guarantee that the class variables quantify over all classes, as we can in second-order semantics. But from a point of view of syntax and provability, they are identical.

By the incompleteness theorem, the Gödel sentence $\phi$ of $T$ is true in the standard model of $T$, but not provable in $I$ (*). Therefore, $\phi$ is also true in the unique model of $\text{ZFC}^2$ in second-order semantics, because this is exactly the standard model of $T$. Hence $I$ was not a complete set of inference rules for $\text{ZFC}^2$ in second-order semantics, because there is a sentence $\phi$ that is true but is not provable in $\text{ZFC}^2$ using the rules in $I$.

The way that we recognize $\phi$ is true is the same way we recognize the Gödel sentence of any other true theory to be true. The Gödel sentence is just an arithmetical statement that says a certain proof does not exist, and indeed that proof does not exist under the assumptions we have already made at the outset of the proof.

(*): As it is usually stated, the incompleteness theorem only applies to differing theories with a fixed set of inference rules. However, the proof is easily generalized to allow not only an arbitrary effective consistent theory, but also an arbitrary effective sound set of finitary inference rules.

Answer 3

I would be happier if the last sentence in the quotation had said "inference that is valid" rather than "inference we can recognize as valid". The latter brings our recognition abilities into the picture, and disagreements can arise there. A formalist might well claim to be able to recognize as valid only those inferences that are provable in a certain formal system.

As Carl Mummert points out in an edit to his answer, his explanation depends on our knowing that the system $I$ (or equivalently $T$) is sound (or at least consistent), so it won't work for a formalist who insists on recognizing only what is deducible in $I$.

In contrast, if we just say that the inference is valid, rather than that we can recognize it as such, then Carl's explanation is fine. The formalist's refusal of recognition to certain correct statements doesn't make them incorrect. In somewhat more mathematical and less polemical form: It is a theorem of ZFC (and of far weaker systems) that the set of valid second-order inferences is not recursively enumerable and therefore cannot be generated by any recursive system of formal inference rules.

Answer 4

1) By "formation rules", he just means rules which tell you when a string of symbols counts as a well-formed formula or a sentence.

By "inference rules" he means like in a proof system. There are a number of different proofs systems available for first-order logic, e.g. Hilbert axiomatic systems, Fitch-style natural deduction systems, sequent calculi, etc. (I'm assuming you're familiar with some of these?) All of these systems are sound and (more importantly) complete for first-order semantics, i.e. a set of sentences $\Gamma$ has a model if and only if $\Gamma$ is consistent (i.e. there is no proof from some sentences of $\Gamma$ to a contradiction). However...

2) Second-order logic, by contrast, has no such proof system. Any sound proof system you propose for second-order logic will inherently be incomplete, i.e. there will be a set of sentences $\Gamma$ from which you cannot deduce a contradiction, yet which have no model. (Put another way: there are some $\Gamma$ and $\varphi$ such that $\Gamma \vDash \varphi$ but $\Gamma \not\vdash \varphi$.)

Potter's point here is just that there is some such set of sentences in second-order logic, which is both unsatisfiable yet consistent; it's not really a comment about what we can or can't recognize to be valid.