Module prop::hooo_traits

Traits showing what would happen with alternative axioms for HOOO Exponential Propositions.

Traits

• ConstructiveHoooRevNot
  Shows that a constructive hooo_rev_not would not allow theories.
• ConstructivePowNot
  Shows that a constructive pow_not would make theories collapse to up(a).
• GlobalTautoHoooRevImply
  Shows that a global tauto_hooo_rev_imply axiom would collapse power to implication.
• HoooDualEq
  Shows that a hooo_dual_eq axiom would be absurd.
• HoooDualImply
  Shows that a hooo_dual_imply axiom would be absurd.
• HoooNRImply
  Shows that a hooo_nrimply axiom would be absurd.
• HoooNeq
  Shows that a hooo_neq axiom would be absurd.
• HoooNot
  Shows that a hooo_not axiom would be absurd.
• HoooRevImply
  Shows that a tauto_hooo_rev_imply axiom would collapse power to implication.
• Lob
  Shows that Löb’s theorem is absurd in the model of Modal Logic derived from HOOO EP.
• TautoHoooDualImply
  Shows that a hooo_dual_imply axiom would be absurd.
• TautoHoooNRImply
  Shows that a tauto_hooo_nrimply axiom would be absurd.
• TautoHoooNeq
  Shows that a tauto_hooo_neq axiom would be absurd.
• TautoHoooNot
  Shows that tauto_hooo_not axiom would be absurd.
• TautoHoooRevImply
  A tauto_hooo_rev_imply axiom.