0

While employing induction method for proving, is deriving the string(formula) "Fn → Fn+1 " any different from showing that if Fn holds true, then so does Fn+1 ?

By showing I mean that we use the expression Fn or its consequence in order to derive Fn+1. It appears to me that both in the end mean the same thing -but I am not sure. Is there any difference meta-mathematically or proof theoretically? (However, it seems to me that when deriving the string(formula) "Fn → Fn+1 " we are operating at a meta level). If the latter can be shown to hold, is it always possible to "derive" the formula "Fn → Fn+1" ?

Improve this question
13
  • No difference... – Mauro ALLEGRANZA Oct 25 '20 at 14:00
  • @MauroALLEGRANZA "Fn→ Fn+1 " : Shouldn't this mean that this holds under "every interpretation"? – Ajax Oct 25 '20 at 14:06
  • Because I am deriving not Fn+1, but the string(formula) "Fn→ Fn+1 " itself... – Ajax Oct 25 '20 at 14:07
  • @MauroALLEGRANZA - (1) Sure, but keeping aside "amounts" to (saying that we have proved) P → Q. how does one go about deriving the string "P→ Q " itself? (2) Is that equivalent to deriving from empty set so that, ⊢ P→ Q ? – Ajax Oct 25 '20 at 16:11
  • Exactly........ – Mauro ALLEGRANZA Oct 25 '20 at 17:06
2

If you are referring to page 259-262 of Turing's paper, the proof that formula CFn is provable, for every n, is by induction.

It is a meta-theory proof, because it is about formulas and their derivability ("provability") in the formal system.

The proof is standard proof by Induction:

(i) Base case: CF0 is provable.

(ii) Induction step: formula CFn → CFn+1 is provable, for every n.

Thus, by Induction, we conclude that CFn is provable, for every n.

Now, the issue is: what is the exact meaning of "formula CFn is provable" ?

It is derivable in predicate calculus.

See page 259:

[...] to show that the Hilbert Entscheidungsproblem (the problem asks for an algorithm that considers, as input, a statement and answers "Yes" or "No" according to whether the statement is universally valid) can have no solution.

I propose, therefore, to show that there can be no general process for determining whether a given formula A of the functional calculus K [see David Hilbert's and Wilhelm Ackermann's Grundzüge der theoretischen Logik (1928), Ch.3] is provable, i.e. that there can be no machine which, supplied with any one A of these formulae, will eventually say whether A is provable.

Corresponding to each computing machine M we construct a formula Un(M) and we show that, if there is a general method for determining whether Un(M) is provable, then there is a general method for determining whether M ever prints 0.

Thus, trying to be more "formal", the result you are referring to amounts to (see "turnstile" symbol):

⊢K CFn, for every n,

where ⊢K CFn means:

"there is a derivation of formula CFn in functional calculus K."

Additional note: as said above, the induction is performed in the meta-theory, because it applies to formulas.

We have an infinite sequence of formulas: { CF0, CF1, ..., CFn, ...} and we consider the property P(n) := "formula CFn is provable (in functional calculus K)".

We prove that CF0 is provable, i.e. that P(0) holds, and we prove that: "if CFn is provable, then also CFn+1 is provable, for n whatever".

Thus, applying Mathematical Induction, we conclude that P(n) holds for every n, i.e. that:

"CFn is provable, for every n.

Turing writes "CFn → CFn+1 is provable" instead of "if CFn is provable, then also CFn+1 is provable".

There is no difference; in symbols, from ⊢K CFn and ⊢K CFn → CFn+1, by Modus ponens we have ⊢K CFn+1.

Improve this answer
5
  • Thank you for your answer. Indeed, Turing's paper is where I am having this doubt. I have one lingering doubt still. Shouldn't we write, in Induction Step: "(ii) Induction step: If CF(n), then CF(n+1) is provable, for every n." because saying that "formula CF(n) → CF(n+1) is provable, for every n" is technically wrong until we prove ⊢K CF(n), for every n (which only happens when the proof by induction terminates). (More strictly) we shouldn't because "formula CF(n) → CF(n+1) is provable, for every n" is equivalent to ⊢K CF(n), for every n? – Ajax Oct 26 '20 at 9:50
  • 1
    @Ajax - NOT EXACTLY. CF(n) is not the same as CF(n) → CF(n+1). The second one holds also if CF(n) is false (see truth table for the conditional (→) connective). – Mauro ALLEGRANZA Oct 26 '20 at 9:57
  • Yes! And this should clear things up: so in the context of this paper, statement "Induction Step: formula CF(n) → CF(n+1) is provable, for every n" is not the same as the meaning of "⊢K CF(n) → CF(n+1), for every n" ? – Ajax Oct 26 '20 at 10:24
  • 1
    @Ajax - NOT SURE TO UNDERSTAND. They are the same; see my answer. "CF(0) is provable (in functional calculus K)" means: "⊢K CF(0)". CF(n) → CF(n+1) is provable means "⊢K CF(n) → CF(n+1)" and "CF(n) is provable (in the functional calculus K), for every n" is "⊢K CF(n), for every n". – Mauro ALLEGRANZA Oct 26 '20 at 10:31
  • 1
    What you have to consider is that CF(n) is a formula where n is not a variable but an "index". Thus, we cannot write the formula (n)CF(n) because in the formal system variables range over "objects" and not formulas. This is why the induction is in the meta- (outside the formal system): because only in the meta- we cam speak of formulas (and not numbers). – Mauro ALLEGRANZA Oct 26 '20 at 10:33
2

A quasi-formal representation of mathematical induction can be given as the following:

enter image description here

The stage that we argue from an arbitrary k to its successor, though gives the impression of a logical pattern, is essentially arithmetical (compare this case to the sorites paradox, for instance). Mind you, if it were logical, its consequences would be far more reaching than a vindication of logicism.

Improve this answer
1
  • @Ajax I've taken your question on mathematical induction in a general setting by which we ordinarily obtain a material implication at an intermediate step. Each of these three statements, 'T1 → T2', ''T1 → T2 is provable', 'if T1 is provable then T2 is provable' belongs to a distinct logical level and their relationships are not immediate; but have to be shown in a Peano Arithmetic dependent way (as for the present case). See Chapter 2 (titled "Peano Arithmetic") of G. Boolos's "The Logic of Provability" for a thorough examination. – Tankut Beygu Oct 27 '20 at 10:24

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.