Struct BoundedArithmetic 

pub struct BoundedArithmetic {
    pub theory: String,
    pub base_theory: String,
    pub formula_class: String,
}

PA^ω conservativity results for bounded arithmetic.

Fields

theory: String

The theory name (e.g. “PA^ω”, “WKL_0”).

base_theory: String

The base theory it is conservative over (e.g. “PRA”).

formula_class: String

Formula class for which conservativity holds.

Implementations

impl BoundedArithmetic

pub fn paomega_over_pra() -> Self

PA^ω is Π^0_2-conservative over PRA.

Trait Implementations

impl Clone for BoundedArithmetic

fn clone(&self) -> BoundedArithmetic

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for BoundedArithmetic

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.