In the book Gödel's Proof by Ernest Nagel and James R. Newman, the authors insist that formal systems are to be considered as meaningless mechanical systems, which yield theorems by merely applying syntactic transformation rules on strings composed of meaningless symbols.

But then the authors proceed to give a proof of consistency for the logic of propositions from Principia Mathematica, and here's how they introduce their proof:

Our aim is to show that this set of axioms is not contradictory, that is, to prove "absolutely" that it is impossible by using the Transformation Rules to derive from the axioms a formula $S$ together with its formal negation $\sim{}S$.

My concern is: if we consider formal systems to only handle meaningless strings, how can we possibly say that the strings $S$ and $\sim{}S$ are mutually-incompatible assertions of our formal system, and that if both statements are theorems of our system then the system is inconsistent?

My intuition is that at this point, we're "jumping out" of the formal system, using external rules of inference instead of our formal system's rules, thus it's acceptable to use a model that interprets the $\sim{}$ sign as signifying logical negation, in which case $S$ and $\sim{}S$ are indeed logically incompatible.

But still, I find it difficult to accept this as a valid reasoning. Any insights to help my understanding?

  • $\begingroup$ When we are studying the "algebra" of strings and transformation rules, one can use all the tools of ordinary mathematics to prove theorems about that algebra. $\endgroup$ – André Nicolas Jun 25 '16 at 16:56
  • 2
    $\begingroup$ $S$ and $\sim{}S$ are not inherently mutually incompatible. However, the usual meaning of 'consistency' in a formal system is that you cannot get both $S$ and $\sim{}S$; I guess it comes down to definitions. $\endgroup$ – shardulc says Reinstate Monica Jun 25 '16 at 16:59
  • 5
    $\begingroup$ Both $S$ and $\neg S$ can still be regarded as "meaningless strings". The goal is, as stated, simply to prove that, for any $S$, the system cannot derive both $S$ and $\neg S$ — or, equivalently, given the system's rules of deduction, that the system doesn't derive every well-formed formula of propositional logic. $\endgroup$ – BrianO Jun 25 '16 at 17:02
  • $\begingroup$ Note also the fact that in 'formal logic', from $S$ and $\sim{}S$ together you can derive any theorem you wish. $\endgroup$ – shardulc says Reinstate Monica Jun 25 '16 at 17:02
  • 1
    $\begingroup$ Nagel and Newman are speaking (in the paraphrase above) too strongly. Most of the formal systems that we study are of interest precisely because their formulas are not meaningless. Similarly, the reason we would include a negation symbol in a formal language is because we want it to have a particular meaning. In general it rarely helps to think of formal languages as composed of entirely meaningless strings. $\endgroup$ – Carl Mummert Jun 26 '16 at 0:41

I have some set $S$ of strings over a certain alphabet, defined in a complicated way. There are two basic ways for $S$ to be uninteresting: maybe $S$ is empty, or maybe $S$ is the set of all strings. Taking $S$ to be the set of strings corresponding to theorems of (say) $PA$, clearly the former case doesn't happen; so you can think of the formalist interpretation of "consistency" as being "interestingness". Ignoring all possible semantic interpretations, $S$ just isn't very interesting if it consists of all strings.

Now we can prove theorems about what $S$ could be. For instance, one thing we can prove is if $\sigma$ and $\neg\sigma$ are in $S$ for some string $\sigma$, then every string is in $S$. And to argue this, we don't have to talk about the meaning of the strings at all.

Note that there is a separate question here: why is the set $S$ something we care about in the first place? This is where formalist responses get more complicated (disclaimer: I'm a formalist), but is orthogonal to your question.

OK, fine: we really shouldn't be talking about $S$ as a set of strings, but rather as a set of well-formed strings: that is, we have the set of all strings, and then the subset of all strings corresponding to wffs, and then inside that is $S$. (Or we can use a weird syntax where every string is well-formed.) But that's a really minor point.

| cite | improve this answer | |
  • $\begingroup$ What meaning do you use for "formalist" ? $\endgroup$ – DanielV Jun 27 '16 at 18:36

A proof system is usually called also calculus (like: propositional calculus) and we can handle it "mechanically", i.e. avoiding any interpretation.

Of course, it is "useful" because we can interpret it (for example, as a way to formalize logical arguments).

It is the same with the addition algorithm of elementary arithmetic: with it you can perform additions in a "mechanical" way, ignoring the fact that you are adding the balls contained into two boxes.

Having defined proof system as a set of rules for "manipulating" formulae, we define a derivability relation between formulae: $⊢$.

With it, we say that a set of formulae $Γ$ is consistent when $Γ⊬⊥$, where $⊥$ (the falsum) may be "instantiated" by every contradiction.

If the system has no $\bot$ symbol and has $\lnot$ symbol, we say that $Γ$ is inconsistent when both $Γ ⊢ \varphi$ and $Γ ⊢ \lnot \varphi$, for some formula $\varphi$.

If we want to avoid also $\lnot$, we say that $Γ$ is consistent when $Γ ⊢ \varphi$ for any formula $\varphi$.

We can prove that (for a "full" language) the above three conditions are equivalent.

When we interpret the formal system with the "usual" truth-functional semantics based on the truth tables for the conncetives, we define :

a formula $\varphi$ is a tautology if $[\varphi]_v =$ t for all valuations $v$


a formula $\varphi$ is a contradiction if $[\varphi]_v =$ f for all valuations $v$.

Under this "convention" we have :

$[\bot]_v =$ f, for all $v$ [thus: the falsum]


a formula $\varphi$ is a tautology iff $\lnot \varphi$ is a contradiction.

Thus, we have may instances of contradictory formulae, like :

$P \land \lnot P$ in propositional logic,

and :

$0=0 \land 0 \ne 0$ in the language of arithmetic.

Under the semantical interpretation, all are equivalent to $\bot$.

| cite | improve this answer | |
  • $\begingroup$ Thanks, but my question remains: if '[the falsum] may be "instantiated" by every contradiction', we still have to establish that having both $\sim{}S$ and $S$ as theorems is a contradiction. How do we do that? $\endgroup$ – TanguyP Jul 2 '16 at 11:46

A formal system is defined to be inconsistent if all formulae are provable, i.e., if every formula is a theorem. If (as in Nagel and Newman) the formal system includes the usual rules of propositional logic, then a system is inconsistent iff there is a formula $S$ such that both $S$ and $\lnot S$ are theorems (because by those rules you can derive any formula $T$ given $S$ and $\lnot S$). And it is then reasonable to follow Nagel and Newman and say that a system of axioms is "contradictory" to mean that it is "inconsistent". Nothing that I have just written relies on any assumption about the meaning of formulas. You introduced the idea of assertions being "mutually incompatible" and then drew an unjustified conclusion from that idea: you don't need to "jump outside the system" or use semantic arguments to prove that if $S$ and $\lnot S$ are provable then every formula is provable.

| cite | improve this answer | |
  • 2
    $\begingroup$ Of course, as soon as we talk about statements being provable or not, we are already working outside the formal system $\endgroup$ – Carl Mummert Jun 26 '16 at 0:40
  • $\begingroup$ Obviously you are making a metatheoretical statement when you say something is not provable. However, on my reading of the question, the OP think that you need to "jump outside the system" to prove $S \land \lnot S \Rightarrow T$, but this is not so: each instance of that formula is a theorem of the object theory. You only need to work outside the object theory to claim that all such instances are theorems. $\endgroup$ – Rob Arthan Jun 26 '16 at 20:08
  • $\begingroup$ Actually, my problem with Nagel and Newman's proof is that it is in the reverse order: as I understand it, they take as a starting point the fact that "consistent" is defined as "non-contradictory", then they somehow jump from "this set of axioms is non-contradictory" to "it is impossible to derive $S$ and $\sim{}S$ from the axioms" (I'm rephrasing a bit, but I think I'm doing justice to their actual words). Only then do they show that, if both $S$ and $\sim{}S$ are derivable, every wff is a theorem. They then find one wff which is not a theorem, therefore their system is consistent. $\endgroup$ – TanguyP Jul 2 '16 at 9:32
  • $\begingroup$ This is the best answer because the point is not really that both $S$ and $~S$ can be proved: some systems may not even have that concept. The point is that any consistent system has to have some formulæ that it can't prove. "$S$ and not-$S$" happens to be just one way of failing to fulfil that condition. $\endgroup$ – Martin Kochanski Jul 2 '16 at 12:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.