New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

二重否定の除去の二重否定 #1599

Open

Seasawher opened this issue Feb 16, 2025 · 0 comments

Labels

コード例メモ

Member

Seasawher commented Feb 16, 2025 •

edited

Loading

タグ：命題論理、二重否定、直観主義、証明例

/-- 二重否定の除去の二重否定 -/
example (P : Prop) : ¬¬ (¬¬ P → P) := by
  intro h

  have : ¬ P := by
    intro hp
    suffices ¬¬P → P from by
      contradiction
    intro _
    assumption

  apply h
  intro hn2p
  contradiction

Seasawher added コード例メモ labels

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment