∀LP (LP ↔ ~⊢LP)
If LP was a theorem this contradicts its assertion: ~⊢LP
If ~LP was a theorem this contradicts its assertion: ⊢LP
Formalization followed by Simple English intuition
(0) ∀x True(x) ↔ φ(x) // Tarski (1933) Formal correctness of True
(1) ∀x True(x) ↔ ⊢x // x can be proven True from known facts.
(2) ∀x ~True(x) ↔ ~⊢x // x cannot be proven True from known facts.
(3) ∀x False(x) ↔ ⊢~x // x can be proven False from known facts.
∀x (Logic_Sentence(x) ↔ (True(x) ∨ False(x)) ↔ (⊢x ∨ ⊢~x))
Axiom An axiom is a proposition regarded as self-evidently true without proof. (Weisstein 2018). An Axiom from math is comparable to an established fact in English. To anchor the notion of Math(Axiom) and English(Fact) we can think of both of these as expressions of language that have been defined to have the semantic property of Boolean True.
Rules-of-Inference show how to correctly transform some expressions of language into other expressions of language.
Theorems are expressions of language proven entirely on the basis of Axioms, and Rules-of-Inference. (Mendelson 2015: 28). When the above definition of Axiom is used as the basis Theorems can be construed as the conclusions of sound deductive inference.
Copyright 2018 by Pete Olcott
Mendelson, Elliott 2015 Introduction to Mathematical logic Sixth edition
1.4 An Axiom System for the Propositional Calculus page 28
Weisstein, Eric W. 2018 “Axiom.” From MathWorld–A Wolfram Web Resource. http://mathworld.wolfram.com/Axiom.html