Description: This minimal implicational calculus tautology is used in the following
argument: When ph , ps , ch , th , ta are replaced respectively by
( ph -> F. ) , F. , ph , F. , F. , the antecedent becomes
-. -. ( -. -. ph -> ph ) , that is, the double negation of the
stability of ph . If that statement were provable in minimal
calculus, then, since F. plays no particular role in minimal calculus,
also the statement with ps in place of F. would be provable. The
corresponding consequent is ( ( ( ps -> ph ) -> ps ) -> ps ) , that
is, the non-intuitionistic Peirce law. Therefore, the double negation of
the stability of any formula is not provable in minimal calculus.
However, it is provable both in intuitionistic calculus (see
iset.mm/bj-nnst) and in classical refutability calculus (see
bj-peircestab ). (Contributed by BJ, 30-Nov-2023)(Revised by BJ, 30-Jul-2024)(Proof modification is discouraged.)