Variable IIReadonly

Type Declaration

• • (formulas: PropFormula[]): PropFormula[]

  • Applies the rule of Implication Introduction.

    Given a proven formula F and an arbitrary formula G, it derives the implication G => F.

    This rule allows the introduction of implications in Hilbert-style calculus, enabling the creation of conditional statements from established facts.

    Parameters

    • formulas: PropFormula[]

      An array containing [provenFormula, newFormula]. - provenFormula: The formula that has been proven - newFormula: The arbitrary formula to be the antecedent

    Returns PropFormula[]

    The implication (newFormula => provenFormula)

    Throws

    if implication creation is not applicable.