AntinomyWe are therefore confronted with a proposition which asserts its own unprovability. 15
14 Every epistemological antinomy can likewise be used for a similar undecidability proof.
(Gödel 1931:40)
...term often used in logic and epistemology, when describing a paradox or
unresolvable contradiction. https://www.newworldencyclopedia.org/entry/Antinomy
Gödel, Kurt 1931.
On Formally Undecidable Propositions of Principia Mathematica And Related Systems
https://mavdisk.mnsu.edu/pj2943kt/Fall% ... l-1931.pdf
On this basis we define a much more powerful F in a formal system having
its own unprovability operator: ⊬ This eliminates the need for the complexity
of arithmetization and diagonalization.
G := (F ⊬ G) means G is defined to be another name for (F ⊬ G)
https://en.wikipedia.org/wiki/List_of_logic_symbols
∃G ∈ F (G := (F ⊬ G))
There exists a G in F that proves its own unprovability in F
Within this much more powerful F a proof of G in F requires a sequence
of inference steps in F that prove that they themselves do not exist.