Struct ConservationResult 

pub struct ConservationResult {
    pub stronger: BigFiveSystem,
    pub weaker: BigFiveSystem,
    pub formula_class: &'static str,
    pub reference: &'static str,
}

A conservation result: stronger is formula_class-conservative over weaker.

Fields

stronger: BigFiveSystem

The stronger system (e.g. WKL₀).

weaker: BigFiveSystem

The weaker system (e.g. RCA₀).

formula_class: &'static str

The class of formulas for which conservation holds.

reference: &'static str

Authors and year of result.

Implementations

impl ConservationResult

pub fn wkl0_over_rca0() -> Self

WKL₀ is Π¹_1-conservative over RCA₀ (Friedman 1976, Simpson).

pub fn aca0_over_pa() -> Self

ACA₀ is conservative over PA for first-order sentences (well-known).

pub fn atr0_over_aca0() -> Self

ATR₀ is Π¹_2-conservative over ACA₀.

pub fn is_valid_direction(&self) -> bool

Verify the direction: stronger ≥ weaker in the Big Five ordering.

Trait Implementations

impl Clone for ConservationResult

fn clone(&self) -> ConservationResult

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ConservationResult

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

Formats the value using the given formatter.