Re: intuitionist logic

In intuitionistic logic
not not not a iff not a.
How ?

Fitch-style proof:

1 | ~~~A hyp
2 || A hyp
3 ||| ~A hyp
4 ||| A 2, reit
5 || ~~A 3-4, ~ int
6 || ~~~A 1, reit
7 | ~A 2-6, ~ int
8 ~~~A -> ~A 1-7, -> int

1 | ~A hyp
2 || ~~A hyp
3 || ~A 1, reit
4 |~~~A 2-3, ~ int
5 ~A -> ~~~A 1-4, -> int

============== j-c ====== @ ====== purr . demon . co . uk ==============
Jack Campin: 11 Third St, Newtongrange EH22 4PU, Scotland | tel 0131 660 4760
<http://www.purr.demon.co.uk/jack/> for CD-ROMs and free | fax 0870 0554 975
stuff: Scottish music, food intolerance, & Mac logic fonts | mob 07800 739 557
.

Quantcast