3 ms·

Hi Ethn! Existence of the [Gödel 1931] proposition I'mUnprovable is inconsistent with the following theorem to the effect that theorems can be used in proofs:

Hi Ethn! Existence of the [Gödel 1931] proposition I'mUnprovable is inconsistent with the following theorem to the effect that theorems can be used in proofs: ⊢∀[Proposition Ψ] (⊢Ψ)⇒Ψ

mike00632 6y ago
For a statement so short it would be easy to avoid using jargon...
- ProfHewitt 6y ago
  The following theorem says that every theorem can be used in another proof: ⊢∀[Proposition Ψ] (⊢Ψ)⇒Ψ The above theorem is completely standard mathematical notation.
  - vfclists 6y ago
    What character set or input method is used in creating this mathmatical characters?
- ProfHewitt 6y ago
  Just to be clear ⊢∀[Proposition Ψ] (⊢Ψ)⇒Ψ is not jargon. Instead, it is standard mathematics.
  - mike00632 6y ago
    It absolutely is jargon. The fact that you explained it by saying it's "mathematics" instead of "English" suggests as much. Jargon means that it's technical language specific to a field and not used in everyday vernacular. What you wrote can't even be typed on a standard keyboard. It's jargon. I'm pointing it out because its use is not so innocent. Jargon is often used to obfuscate meaning, especially when it means something that would otherwise be easy to say plainly.
kazinator 6y ago
Axioms can be used in proofs, and they are not provable. If a proposition is not provable, yet raises no issues if regarded as true, then it can be added as an axiom and used in theorems.
- ProfHewitt 6y ago
  It turns out that for powerful theories of Computer Science, there must exist infinitely many propositions that are inferentially undecidable, that is, can be neither proved nor disproved. However, the propositions cannot be specified constructively and so are not very interesting. Currently, there seem to be no propositions interesting to practical Computer Science that are provably inferentially undecidable.

Hi Ethn! Existence of the [Gödel 1931] proposition I'mUnprovable is inconsistent with the following theorem to the effect that theorems can be used in proofs: ⊢∀[Proposition Ψ] (⊢Ψ)⇒Ψ

mike00632 6y ago

For a statement so short it would be easy to avoid using jargon...

ProfHewitt 6y ago
The following theorem says that every theorem can be used in another proof: ⊢∀[Proposition Ψ] (⊢Ψ)⇒Ψ The above theorem is completely standard mathematical notation.
- vfclists 6y ago
  What character set or input method is used in creating this mathmatical characters?
ProfHewitt 6y ago
Just to be clear ⊢∀[Proposition Ψ] (⊢Ψ)⇒Ψ is not jargon. Instead, it is standard mathematics.
- mike00632 6y ago
  It absolutely is jargon. The fact that you explained it by saying it's "mathematics" instead of "English" suggests as much. Jargon means that it's technical language specific to a field and not used in everyday vernacular. What you wrote can't even be typed on a standard keyboard. It's jargon. I'm pointing it out because its use is not so innocent. Jargon is often used to obfuscate meaning, especially when it means something that would otherwise be easy to say plainly.

kazinator 6y ago

Axioms can be used in proofs, and they are not provable. If a proposition is not provable, yet raises no issues if regarded as true, then it can be added as an axiom and used in theorems.

ProfHewitt 6y ago
It turns out that for powerful theories of Computer Science, there must exist infinitely many propositions that are inferentially undecidable, that is, can be neither proved nor disproved. However, the propositions cannot be specified constructively and so are not very interesting. Currently, there seem to be no propositions interesting to practical Computer Science that are provably inferentially undecidable.