Current set of HOOO axioms

[bvssvni]

excm = excluded middle axiom (classical/decidable proposition)

Axioms:

• a^b => (a^b)^c (pow_lift constructive)
• (a => b)^c => (a^c => b^c)^true (tauto_hooo_imply constructive)
• (a ⋁ b)^c => (a^c ⋁ b^c)^true (tauto_hooo_or constructive)

Proof cases:

• a^b => (a^b)^c (pow_lift constructive axiom)
• (□a)^b == (□(a^b))^true (some are invalid)
  • ((¬a)^b) => (¬(a^b))^true (tauto_hooo_not invalid)
  • (¬(a^b))^true => (¬a)^b (tauto_hooo_rev_not proof requires excm for a)
• (□a)^b == □(a^b) (some are invalid)
  • ((¬a)^b) => ¬(a^b) (hooo_not invalid)
  • ¬(a^b) => (¬a)^b (hooo_rev_not proof requires excm for a)
• (a □ b)^c == (a^c □ b^c)^true (some are invalid)
  • (a => b)^c => (a^c => b^c)^true (tauto_hooo_imply constructive axiom)
  • (a^c => b^c)^true => (a => b)^c (tauto_hooo_rev_imply invalid)
  • (a ⋀ b)^c => (a^c ⋀ b^c)^true (tauto_hooo_and constructive proof)
  • (a^c ⋀ b^c)^true => (a ⋀ b)^c (tauto_hooo_rev_and constructive proof)
  • (a ⋁ b)^c => (a^c ⋁ b^c)^true (tauto_hooo_or constructive axiom)
  • (a^c ⋁ b^c)^true => (a ⋁ b)^c (tauto_hooo_rev_or constructive proof)
  • (a == b)^c => (a^c == b^c)^true (tauto_hooo_eq constructive proof)
  • (a^c == b^c)^true => (a == b)^c (tauto_hooo_rev_eq constructive proof)
  • (¬(a == b))^c => (¬(a^c == b^c))^true (tauto_hooo_neq invalid)
  • (¬(a^c == b^c))^true => (¬(a == b))^c (tauto_hooo_rev_neq proof requires excm for a, b)
  • (¬(b => a))^c => (¬(b^c => a^c))^true (tauto_hooo_nrimply invalid)
  • (¬(b^c => a^c))^true => (¬(b => a))^c (tauto_hooo_rev_nrimply proof requires excm for a, b)
• c^(a □ b) == (c^a □[¬] c^b)^true (some requires excm, some are invalid)
  • c^(a => b) => (¬(c^b => c^a))^true (tauto_hooo_dual_imply invalid)
  • (¬(c^b => c^a))^true => c^(a => b) (tauto_hooo_dual_rev_imply classical proof)
  • c^(a ⋀ b) => (c^a ⋁ c^b)^true (tauto_hooo_dual_and classical proof)
  • (c^a ⋁ c^b)^true => c^(a ⋀ b) (tauto_hooo_dual_rev_and constructive proof)
  • c^(a ⋁ b) => (c^a ⋀ c^b)^true (tauto_hooo_dual_or constructive proof)
  • (c^a ⋀ c^b)^true => c^(a ⋁ b) (tauto_hooo_dual_rev_or constructive proof)
  • c^(a == b) => (¬(c^a == c^b))^true (tauto_hooo_dual_eq invalid)
  • (¬(c^a == c^b))^true => c^(a == b) (tauto_hooo_dual_rev_eq classical proof)
  • c^(¬(a == b)) => (c^a == c^b)^true (tauto_hooo_dual_neq classical proof)
  • (c^a == c^b)^true => c^(¬(a == b)) (tauto_hooo_dual_rev_neq proof requires excm for a, b, see #627)
  • c^(¬(b => a)) => (c^a => c^b)^true (tauto_hooo_dual_nrimply classical proof)
  • (c^a => c^b)^true => c^(¬(b => a)) (tauto_hooo_dual_rev_nrimply proof requires excm for a, b)
• (a □ b)^c == (a^c □ b^c) (some are invalid)
  • (a => b)^c => (a^c => b^c) (hooo_imply constructive proof)
  • (a^c => b^c) => (a => b)^c (hooo_rev_imply invalid)
  • (a ⋀ b)^c => (a^c ⋀ b^c) (hooo_and constructive proof)
  • (a^c ⋀ b^c) => (a ⋀ b)^c (hooo_rev_and constructive proof)
  • (a ⋁ b)^c => (a^c ⋁ b^c) (hooo_or constructive proof)
  • (a^c ⋁ b^c) => (a ⋁ b)^c (hooo_rev_or constructive proof)
  • (a == b)^c => (a^c == b^c) (hooo_eq constructive proof)
  • (a^c == b^c) => (a == b)^c (hooo_rev_eq classical proof)
  • (¬(a == b))^c => ¬(a^c == b^c) (hooo_neq invalid)
  • ¬(a^c == b^c) => (¬(a == b))^c (hooo_rev_neq proof requires excm for a, b)
  • (¬(b => a))^c => ¬(b^c => a^c) (hooo_nrimply invalid)
  • ¬(b^c => a^c) => (¬(b => a))^c (hooo_rev_nrimply proof requires excm for a, b)
• c^(a □ b) == (c^a □[¬] c^b) (some requires excm, some are invalid)
  • c^(a => b) => ¬(c^b => c^a) (hooo_dual_imply invalid)
  • ¬(c^b => c^a) => c^(a => b) (hooo_dual_rev_imply classical proof)
  • c^(a ⋀ b) => (c^a ⋁ c^b) (hooo_dual_and classical proof (see comment))
  • (c^a ⋁ c^b) => c^(a ⋀ b) (hooo_dual_rev_and constructive proof)
  • c^(a ⋁ b) => (c^a ⋀ c^b) (hooo_dual_or constructive proof)
  • (c^a ⋀ c^b) => c^(a ⋁ b) (hooo_dual_rev_or constructive proof)
  • c^(a == b) => ¬(c^a == c^b) (hooo_dual_eq invalid)
  • ¬(c^a == c^b) => c^(a == b) (hooo_dual_rev_eq classical proof)
  • c^(¬(a == b)) => (c^a == c^b) (hooo_dual_neq classical proof)
  • (c^a == c^b) => c^(¬(a == b)) (hooo_dual_rev_neq classical proof, see #627)
  • c^(¬(b => a)) => (c^a => c^b) (hooo_dual_nrimply classical proof)
  • (c^a => c^b) => c^(¬(b => a)) (hooo_dual_rev_nrimply classical proof)