Philosophy Now Forum

Let □ be the operator "it is provable in ZFC".
Let 'P' mean that the Continuum Hypothesis is the case.
Take the following Natural Deduction argument in GL provability logic:

1.□(~□P→(□P→P) Theorem Intro. (Prop. Logic)
2.□(~□~P→(□~P→~P)) Theorem Intro. (Prop. Logic)
3.□~□P→□(□P→P) 1, Distribution
4.□~□~P→□(□~P→~P) 2, Distribution
5.□(□P→P)→□P Löb's Rule
6.□(□~P→~P)→□~P Löb's Rule
7.□~□P ∧ □~□~P Theorem Intro. (Independence of the Continuum Hypothesis from ZFC)
8.(□~□P ∧ □~□~P)→(□P ∧ □~P) Theorem Intro. (Prop. Logic)
9.□(P ∧ ~P) 7,8 Modus Ponens; Theorem Intro. (System K)

Is this kind of result already known? What does it mean? Is it just equivalent to Gödel's Theorems? Any feedback would be appreciated!

1. All logical systems require axioms.

2. These axioms are unproven except through the proofs in which they are used.

3. The proof justifies the axiom and the axiom justifies the proof.

4. Proof and axiom, as circular, thus become interchangeable: a proof is an axiom and an axiom is a proof.

5. This interchangeability, as equivocation, results in obscurity as it is self-referencing therefore the axiom is no longer the axiom and the proof is no longer the proof as both become indefinite.

6. Axioms/proofs are only that which are accepted to deal with this indefiniteness, thus logic requires intuition.

7. Intuition thus expands the circle of axiom=proof to axiom=proof=intuition.

8. However intuition is not universal as the axiom=proof would not have to be taught if it where such.

9. In the equivocation of "axiom=proof=intuition" the intuition not being universal necessitates the axiom/proof as not universal.

10. This absence of universality necessitates a multiplicity of logics, all of which may not agree.

11. This absence of agreement in logics results in the axiom of "Logic" being obscure.