Skip to main content
added 83 characters in body
Source Link
Joel David Hamkins
  • 236.2k
  • 44
  • 777
  • 1.4k

Let me assume that you also include the axioms $\vdash A$ whenever $A$ is a logical axiom, for some fixed standard proof system using modus ponens as the only inference rule. And let me also assume that we have induction in the language including $\vdash$.

It now follows easily by induction on proofs in that system that whenever $S$ is provable in PA, then your theory proves $\vdash S$.

Indeed, since the induction on proofs can be undertaken internally to the theory, we get that your theory proves the universal claim $$\forall S, \text{ if }S\text{ is provable in PA, then }\vdash S.$$

And since strong provability implies provability, the answer is yes, every instance of your implication is provable in your theory. (But I find strong provability to be a red herring here.)

If you don't include the logical axioms in your theory, then it will break this argument, but furthermore it would be questionable whether your theory in that case was expressing a useful concept about provability.

Let me assume that you also include the axioms $\vdash A$ whenever $A$ is a logical axiom, for some fixed standard proof system using modus ponens as the only inference rule.

It now follows easily by induction on proofs in that system that whenever $S$ is provable in PA, then your theory proves $\vdash S$.

Indeed, since the induction on proofs can be undertaken internally to the theory, we get that your theory proves the universal claim $$\forall S, \text{ if }S\text{ is provable in PA, then }\vdash S.$$

And since strong provability implies provability, the answer is yes, every instance of your implication is provable in your theory. (But I find strong provability to be a red herring here.)

If you don't include the logical axioms in your theory, then it will break this argument, but furthermore it would be questionable whether your theory in that case was expressing a useful concept about provability.

Let me assume that you also include the axioms $\vdash A$ whenever $A$ is a logical axiom, for some fixed standard proof system using modus ponens as the only inference rule. And let me also assume that we have induction in the language including $\vdash$.

It now follows easily by induction on proofs in that system that whenever $S$ is provable in PA, then your theory proves $\vdash S$.

Indeed, since the induction on proofs can be undertaken internally to the theory, we get that your theory proves the universal claim $$\forall S, \text{ if }S\text{ is provable in PA, then }\vdash S.$$

And since strong provability implies provability, the answer is yes, every instance of your implication is provable in your theory. (But I find strong provability to be a red herring here.)

If you don't include the logical axioms in your theory, then it will break this argument, but furthermore it would be questionable whether your theory in that case was expressing a useful concept about provability.

added 43 characters in body
Source Link
Joel David Hamkins
  • 236.2k
  • 44
  • 777
  • 1.4k

Let me assume that you also include the axioms $\vdash A$ whenever $A$ is a logical axiom, for some fixed standard proof system using modus ponens as the only inference rule.

It now follows easily by induction on proofs in that system that whenever $S$ is provable in PA, then $\vdash S$.

Since strong provability implies provability, the answer is yes, every instance of your implication is provable in your theory proves $\vdash S$.

Indeed, since the induction on proofs can be undertaken in PAinternally to the theory, we get that your theory proves the universal claim $$\forall S, \text{ if }S\text{ is provable in PA, then }\vdash S.$$ So

And since strong provability implies provability, the answer is yes, every instance of your implication is provable in your theory. (butBut I find strong provability isto be a red herring here).)

If you don't include the logical axioms in your theory, then it will break this argument, but furthermore it would be questionable whether your theory in that case was expressing a useful concept about provability.

Let me assume that you also include the axioms $\vdash A$ whenever $A$ is a logical axiom, for some fixed standard proof system using modus ponens as the only inference rule.

It now follows easily by induction on proofs in that system that whenever $S$ is provable in PA, then $\vdash S$.

Since strong provability implies provability, the answer is yes, every instance of your implication is provable in your theory.

Indeed, since the induction on proofs can be undertaken in PA, we get that your theory proves the universal claim $$\forall S, \text{ if }S\text{ is provable in PA, then }\vdash S.$$ So the answer is yes (but strong provability is a red herring here).

If you don't include the logical axioms, then it will break this argument, but furthermore it would be questionable whether your theory in that case was expressing a useful concept about provability.

Let me assume that you also include the axioms $\vdash A$ whenever $A$ is a logical axiom, for some fixed standard proof system using modus ponens as the only inference rule.

It now follows easily by induction on proofs in that system that whenever $S$ is provable in PA, then your theory proves $\vdash S$.

Indeed, since the induction on proofs can be undertaken internally to the theory, we get that your theory proves the universal claim $$\forall S, \text{ if }S\text{ is provable in PA, then }\vdash S.$$

And since strong provability implies provability, the answer is yes, every instance of your implication is provable in your theory. (But I find strong provability to be a red herring here.)

If you don't include the logical axioms in your theory, then it will break this argument, but furthermore it would be questionable whether your theory in that case was expressing a useful concept about provability.

Source Link
Joel David Hamkins
  • 236.2k
  • 44
  • 777
  • 1.4k

Let me assume that you also include the axioms $\vdash A$ whenever $A$ is a logical axiom, for some fixed standard proof system using modus ponens as the only inference rule.

It now follows easily by induction on proofs in that system that whenever $S$ is provable in PA, then $\vdash S$.

Since strong provability implies provability, the answer is yes, every instance of your implication is provable in your theory.

Indeed, since the induction on proofs can be undertaken in PA, we get that your theory proves the universal claim $$\forall S, \text{ if }S\text{ is provable in PA, then }\vdash S.$$ So the answer is yes (but strong provability is a red herring here).

If you don't include the logical axioms, then it will break this argument, but furthermore it would be questionable whether your theory in that case was expressing a useful concept about provability.