Struct SecondOrderLogic 

pub struct SecondOrderLogic {
    pub full_comprehension: bool,
    pub with_induction: bool,
    pub system_name: String,
}

Describes a second-order logic system.

Fields

full_comprehension: bool

Whether comprehension axiom is full or restricted.

with_induction: bool

Whether the system includes induction.

system_name: String

The second-order system name.

Implementations

impl SecondOrderLogic

pub fn new( system_name: &str, full_comprehension: bool, with_induction: bool, ) -> Self

Create a new second-order logic descriptor.

pub fn z2() -> Self

Second-order arithmetic Z_2 (full second-order arithmetic).

pub fn aca0() -> Self

ACA_0: Arithmetical Comprehension Axiom (base system of second-order arithmetic).

pub fn interprets_pa(&self) -> bool

Whether this system interprets first-order PA (Peano Arithmetic).

pub fn is_categorical(&self) -> bool

Categoricity: second-order PA is categorical (all models are isomorphic).

pub fn is_complete(&self) -> bool

Incompleteness: by Gödel, Z_2 is incomplete if ω-consistent.

Trait Implementations

impl Clone for SecondOrderLogic

fn clone(&self) -> SecondOrderLogic

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for SecondOrderLogic

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

Formats the value using the given formatter.