A library in Rust for theorem proving with Intuitionistic Propositional Logic.

AdvancedResearch

Last update: Jan 3, 2023

Related tags

Utilities prop

Overview

Prop

Propositional logic with types in Rust.

A library in Rust for theorem proving with Intuitionistic Propositional Logic. Supports theorem proving in Classical Propositional Logic.

Used in research on Path Semantics
Brought to you by the AdvancedResearch Community
Join us on Discord!

Abbreviations:

IPL: Intuitionistic/Constructive Propositional Logic
PL: Classical Propositional Logic
PSC: Path Semantical Intuitionistic/Constructive Propositional Logic
PSL: Path Semantical Classical Propositional Logic

Motivation

Path Semantics extends dependent types with normal paths and is also used to extend Classical Propositional Logic with multiple levels of propositions. It is also used to explore higher dimensional mathematics. A popular research subject in Path Semantics is Avatar Extensions.

When researching, in some cases it is useful to figure out whether a proof is provable in classical logic, but not in constructive logic. This requires comparing proofs easily.

This library uses a lifting mechanism for making it easier to produce proofs in classical logic and compare them to proofs in constructive logic.

Design

This library contains:

Prop: Propositions that might or might not be decidable (constructive logic)
DProp: Decidable propositions (classical logic)
LProp: Like Prop, but with path semantics (path semantical constructive logic)
DLProp: Like DProp, but with path semantics (path semantical classical logic)
Automatic lifting of Excluded Middle to decidable propositions
Double Negation for proofs of Prop
Formalization of the core axiom of Path Semantics
Tactics organized in modules by constructs (e.g. and or imply)

Due to first-order logic requiring dependent types, which is not yet supported in Rust, this library is limited to zeroth-order logic (propositional logic).

Examples

use prop::*;

fn proof(f: Imply, a: A) -> B {
    imply::modus_ponens(f, a)
}

Notice that there is no DProp used here, which means that it is a constructive proof.

use prop::*;

fn proof(f: Imply, Not>) -> Imply {
   imply::rev_modus_tollens(f)
}

Here, DProp is needed because rev_modus_tollens needs Excluded Middle. This limits the proof to decidable propositions.

Path Semantics

Path Semantics is an extremely expressive language for mathematical programming. It uses a single core axiom, which models semantics of symbols.

Basically, mathematical languages contain a hidden symmetry due to use of symbols. Counter-intuitively, symbols are not "inherently" in logic.

One way to put it, is that the symbols "themselves" encode laws of mathematics. The hidden symmetry can be exploited to prove semantics and sometimes improve performance of automated theorem provers.

For example, path Semantics can be used to boost performance of brute force theorem proving in Classical Propositional Logic on Type-hierarchy-like problems. For more information, see the blog post Improving Brute Force Theorem Proving.

For more information, see the Path Semantics Project.

Comments

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

It is possible to prove the following:

/// `(a == a^true)^true`. pub fn proof<A: Prop>(_: True) -> Eq<A, Tauto<A>> { (Rc::new(move |a| pow_uni(a)), Rc::new(move |tauto_a| tauto_a(True))) }

This should not be provable, because it collapses tautologies in HOOO Exponential Propositions into ordinary propositions.
hard

opened by bvssvni 6

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

pub fn proof<A: Prop, B: Prop>( pow_ba: Pow<B, A>, pow_bna: Pow<B, Not<A>> ) -> False { pow_rev_not(pow_bna)(pow_ba) } pub fn proof2() -> False { fn f(_: Or<True, Not<True>>) -> True {True} let (a, b) = hooo_dual_or(f); proof(a, b) }

Here, hooo_dual_or has a trusted proof:

/// `c^(a ⋁ b) => (c^a ⋀ c^b)`. pub fn hooo_dual_or<A: Prop, B: Prop, C: Prop>( x: Pow<C, Or<A, B>> ) -> And<Pow<C, A>, Pow<C, B>> { (pow_transitivity(Left, x.clone()), pow_transitivity(Right, x)) }

The only weakness is hooo_dual_imply, used in pow_rev_not:

/// `a^(¬b) => ¬a^b`. pub fn pow_rev_not<A: Prop, B: Prop>(x: Pow<A, Not<B>>) -> Not<Pow<A, B>> { let y = hooo_dual_imply(x); Rc::new(move |pow_a_b| { y(pow_a_b.map_any()) }) }
hard

opened by bvssvni 2

Dual axiom scheme of HOOO EP makes exponential propositions decidable

The dual axiom scheme of HOOO EP is too strong and should only be allowed for decidable propositions.

c^(a □ b) == (c^a □[¬] c^b)

The reason for this is the that following is provable using the S5 Modal Logic:

/// `◇a => □a`. pub fn pos_to_nec<A: Prop>(x: Pos<A>) -> Nec<A> { let x: Para<Not<A>> = pow_not(pos_to_npara(x)); let x: Not<Not<Para<Not<A>>>> = not::double(x); let x: Not<Pos<Not<A>>> = imply::in_left(x, |x| pos_to_npara(x)); nposn_to_nec(x) }

From this, it should be possible to prove theory(a) => false. Using hooo::program, one can then prove a^true | false^a for all a.

The reminding proof is to show that decidable propositions have this property:

(a | !a)^true a^true | (!a)^true a^true | false^true
hard

opened by bvssvni 2

Prove `hooo::tauto_from_para_transitivity` (challenge)

I will give 200 USD to the first person that can prove (⊥^(a == b) ∧ ⊥^(b == c)) => (a == c)^⊤.

It is currently believed that proving the contradiction is impossible, but if somebody does it, then the reward will be equal.

The proof, if found, will be added to hooo::tauto_from_para_transitivity.

Currently, there are only 4 axioms for HOOO Exponential Propositions, see https://github.com/advancedresearch/prop/issues/502. Finding this proof will reduce to a set of 3 axioms.
information

opened by bvssvni 2

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

Currently, one can prove the following:

pub fn proof<A: Prop>() -> False { let a: Pow<A, False> = fa(); let b: Pow<Not<A>, False> = fa(); hooo_not()(b)(a) }
hard

opened by bvssvni 2

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

See https://github.com/advancedresearch/prop/issues/620

Since hooo_dual_eq is too strong, a new constructive proof is desirable for hooo_dual_rev_neq.

A such proof exists if excluded middle is required for A, B. This is required due to or::from_de_morgan being used in the proof.

I think this proof is acceptable, given that the only reference to hooo_dual_rev_neq is in tauto_from_para_transitivity which requires excluded middle.
hard

opened by bvssvni 1

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

It is possible to prove the old pow_uni in the following way:

/// `a => b^a`. pub fn pow_uni<A: Prop, B: Prop>(a: A) -> Pow<A, B> { fn h<A: Prop, B: Prop>((_, a): And<B, A>) -> A {a} pow_rev_lower(h)(a) }

As figured out in https://github.com/advancedresearch/prop/issues/499, this can be used to prove:

/// `(a == a^true)^true`. pub fn proof<A: Prop>(_: True) -> Eq<A, Tauto<A>> { (Rc::new(move |a| pow_uni(a)), Rc::new(move |tauto_a| tauto_a(True))) }
draft discussion

opened by bvssvni 1

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

Currently, the proof ¬◇a => ⊥^a requires a do be decidable, which means it only holds in classical logic. See modal::npos_to_para. This will be available in v0.27.

The problem is whether this is possible to do constructively or not.

This requires proving ¬◇a => ⊥^a constructively or ⊥^((¬◇a => ⊥^a)^⊤) constructively (or similar) in Prop.
discussion

opened by bvssvni 1

`PureSeshatism` is a tautology

Using imply::modus_tollens, one can show that PureSeshatism is a tautology in IPL.

This was not discovered at first since PureSeshatism was designed initially without the symbolic distinction assumption. https://github.com/advancedresearch/prop/issues/164

Later, when a problem was discovered with PureSeshatism (https://github.com/advancedresearch/prop/issues/180), it was thought that imply::modus_tollens was non-constructive. Actually, it is imply::rev_modus_tollens that is non-constructive and this was confused with imply::modus_tollens.

PureSeshatism should be removed.
easy

opened by bvssvni 1

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

Currently, Avatar Modal Logic uses false^(false^a). However, it turns out that this equals ¬¬a.

By using ¬¬a, it might be possible to reduce dependence on HOOO Exponential Propositions.
draft discussion

opened by bvssvni 0

Does Avatar Modal Logic make sense?

In the last update (v0.33), I moved the old "modal" module to "ava_modal" and renamed it "Avatar Modal Logic" to avoid confusion with the new S5 Modal Logic.

The reason Avatar Modal Logic was derived the way it is, was because HOOO EP was too strong. However, now that some dual axioms requires excluded middle, it is a good to revisit Avatar Modal Logic and rethinking the design.

The idea behind Avatar Modal Logic might be sound, but it is not necessarily that the current design is the best one.

In particular, I am concerned about how decidability interacts with the API.
discussion

opened by bvssvni 1

Current set of HOOO axioms

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)

draft information

opened by bvssvni 0

Use 1-avatar for `◇a`

Currently, with ◇a == ⊥^(⊥^a), it is possible to prove ¬◇a == ◇¬a.

By wrapping ◇a in a new-type (1-avatar), it is possible to prevent proving ¬◇a == ◇¬a.

The relation between HOOO and Modal Logic becomes like the relation between Möbius Topologies and Hypercubes in Avatar Extensions. See section about Avatar Semantics.
draft discussion

opened by bvssvni 0

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

From lecture by Jean Louis Krivine: https://www.youtube.com/watch?v=HT9F5QDQOEg 1:06:31

The idea is to use an exponential proposition in place of Leibniz equality:

false^!(a == b)

Krivine seems to introduce a special inequality symbol.

I am guessing the form as exponential proposition.
draft discussion

opened by bvssvni 0