advancedresearch/prop

Issues

• Proper handling of monic and epic functions in `id` and `comp` module

  #1734 opened a year ago by bvssvni
  0

• Change to solution semantics for the imaginary inverse

  #1728 opened a year ago by bvssvni
  0

• Is `fun::id::to_qu` (`a => ~a`) too strong?

  #1635 opened 2 years ago by bvssvni
  3

• Add `fun::bool_alg::FEqb`

  #951 opened 2 years ago by bvssvni
  1

• Figure out whether `~inv(f)` requires `f` to be total

  #1600 opened 2 years ago by bvssvni
  0

• Make `FId` take type argument

  #1348 opened 2 years ago by bvssvni
  1

• `path_semantics::ty_tr` is too strong

  #1487 opened 2 years ago by bvssvni
  1

• `fun::path_inv` is too strong (`~inv(f) ⋀ (f : x -> y) ⋀ (x -> y) => (y -> x)`)

  #1445 opened 2 years ago by bvssvni
  1

• Naming of successor function

  #1441 opened 2 years ago by bvssvni
  0

• Naming of addition and multiplication

  #1438 opened 2 years ago by bvssvni
  0

• Unsoundness in `fun::subst_id` (`a[b := a] == a`)

  #1309 opened 2 years ago by bvssvni
  0

• Potential unsoundness in `fun::fnat::para_pre_zero` (`(n : nat) ⋀ (0 == n + 1) => false`)

  #1312 opened 2 years ago by bvssvni
  4

• Interfacing with normal Rust code

  #1270 opened 2 years ago by bvssvni
  0

• `pow_not_e` collapses `theory(a)` to `up(a)`

  #855 opened 2 years ago by bvssvni
  0

• Boolean algebra operators must be commutative

  #784 opened 2 years ago by bvssvni
  1

• Create "fun" module for functional programming as propositions

  #764 opened 2 years ago by bvssvni
  0

• Create "mid" module for Middle Exponential Propositions

  #755 opened 2 years ago by bvssvni
  0

• Current set of HOOO axioms

  #502 opened 2 years ago by bvssvni
  0

• Add traits for alternative HOOO EP axioms

  #720 opened 2 years ago by bvssvni
  0

• `hooo_rev_imply` is too strong (`(a^c => b^c) => (a => b)^c`)

  #640 opened 2 years ago by bvssvni
  0

• `tauto_hooo_rev_imply` is too strong (`(a^c => b^c)^true => (a => b)^c`)

  #664 opened 2 years ago by bvssvni
  0

• `hooo_rev_eq` is only used with decidable propositions

  #704 opened 2 years ago by bvssvni
  0

• Change axiom schemes

  #641 opened 2 years ago by bvssvni
  0

• Dual axiom scheme of HOOO EP makes exponential propositions decidable

  #548 opened 2 years ago by bvssvni
  2

• `hooo_dual_imply` is too strong (`c^(a => b) => ¬(c^b => c^a)`)

  #579 opened 2 years ago by bvssvni
  2

• `hooo_dual_rev_neq` should require excluded middle for `A, B`

  #627 opened 2 years ago by bvssvni
  1

• `hooo_dual_eq` is too strong (`c^(a == b) => ¬(c^a == c^b)`)

  #620 opened 2 years ago by bvssvni
  1

• Remove HOOO axiom by `not[not] <=> not`

  #476 opened 2 years ago by bvssvni
  2

• `hooo_nrimply` is too strong (`(¬(b => a))^c => ¬(b^c => a^c)`)

  #618 opened 2 years ago by bvssvni
  1

• `hooo_neq` is too strong (`(¬(a == b))^c => ¬(a^c == b^c)`)

  #616 opened 2 years ago by bvssvni
  1

• Make Avatar Modal Logic use `¬¬a` instead of `false^(false^a))`

  #611 opened 2 years ago by bvssvni
  0

• Does Avatar Modal Logic make sense?

  #559 opened 2 years ago by bvssvni
  1

• Prove `hooo::tauto_from_para_transitivity` (challenge)

  #522 opened 2 years ago by bvssvni
  2

• Fix error in comment to `para_to_or`

  #506 opened 2 years ago by bvssvni
  0

• `a^(b ⋀ c) => (a^b)^c` (hooo::pow_rev_lower) is too strong

  #505 opened 2 years ago by bvssvni
  1

• `a => a^b` (hooo::pow_uni) is too strong

  #499 opened 2 years ago by bvssvni
  6

• Introduce SProp trait for `!~a == ~!a`

  #491 opened 2 years ago by bvssvni
  1

• Open problem: Prove `¬◇a => ⊥^a` constructively or prove it is impossible to prove

  #458 opened 2 years ago by bvssvni
  1

• Use 1-avatar for `◇a`

  #468 opened 2 years ago by bvssvni
  0

• Rename EP to EL for "Existential Logic"

  #358 opened 2 years ago by bvssvni
  0

• Rename `tauto` module to `hooo`

  #413 opened 2 years ago by bvssvni
  0

• Add `uniform(a) ⋁ false^uniform(a)` as HOOO axiom

  #408 opened 2 years ago by bvssvni
  0

• Add `(a^true == b^true) == (false^a == false^b)` as HOOO axiom

  #407 opened 2 years ago by bvssvni
  0

• Use `T, F` instead of `True, False`

  #409 opened 2 years ago by bvssvni
  1

• Use `not . eq` as dual of `eq` in `tauto` module

  #394 opened 2 years ago by bvssvni
  1

• Use `false^!(a == b)` for Leibniz equality

  #395 opened 2 years ago by bvssvni
  0

• Add type alias for `!a == !!b` for type theoretic existential philosophy

  #343 opened 2 years ago by bvssvni
  2

• Check `hom_eq(2, a, b) == ((a ~~ b) | (a ~!~ b))`

  #367 opened 2 years ago by bvssvni
  0

• Add support for substitution by equality of tautological identity

  #342 opened 2 years ago by bvssvni
  0

• Add `AProp` trait

  #319 opened 2 years ago by bvssvni
  0