michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Update Negation.lagda.md

Browse source 
At suggestion of Fredrik Nordvall Forsberg, replace "proof by contradiction" with "reductio ad absurdum".
This commit is contained in:
Philip Wadler 2020-07-23 12:12:43 +01:00 committed by GitHub
parent ada0f50e5d
commit dd32f8f6c6
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/plfa/part1/Negation.lagda.md
View file

@ -34,8 +34,8 @@ as implication of false:
¬_ : Set → Set
¬ A = A → ⊥
```
This is a form of _proof by contradiction_: if assuming `A` leads
to the conclusion `⊥` (a contradiction), then we must have `¬ A`.
This is a form of _reductio ad absurdum_: if assuming `A` leads
to the conclusion `⊥` (an absurdity), then we must have `¬ A`.
Evidence that `¬ A` holds is of the form