package coq-inconsequential_modus_ponens

  1. Overview
  2. No Docs
A Coq library about how redundant modus ponens is

Install

Dune Dependency

github.com Edit opam file Versions (2)

Authors

  1. V
    Veeti Eronen

Maintainers

  1. E
    eronenveeti174@gmail.com

Sources

1.0.6.tar.gz
sha256=cea9ebdc58043cc9d43226b620ab7b27809888813bd15d24f6241104de010217

Description

It shown with two interpretations of modus ponens that it's only true when one of two other propositional sentences unsuitable for deducing facts from others are true.

Tags

keyword:modus ponens category:Mathematics/Logic/Foundations date:2022-08-20

Published: 25 Sep 2022

Dependencies (1)

  1. coq >= "8.15"

Dev Dependencies

None

Used by

None

Conflicts

None