Закон двойного отрицания

[Виктор Викторов]

В книге А Чёрча «Введение в математическую логику» на странице 68 вводятся три аксиомы. Первые две как и обычно (например у Мендельсона) $[p\to [q\to p]]$ и $[[s\to [p\to q]]\to [[s\to p]\to [s\to q]]]$, но дальше вместо $[[\neg p\to \neg f]\to [[\neg p\to f]\to p]]$ говорится о законе двойного отрицания и написана весьма странная формула: $[[[p\to f]\to f]\to p]{.}$ Эта формула не является законом двойного отрицания и даже не есть тавтология. Я проверил английские издания, и там точно таже формула. Имелась ли в виду формула $[\neg \neg p\to p]{?}$ И можно ли, заменив $[[\neg p\to \neg f]\to [[\neg p\to f]\to p]]$ на $[\neg \neg p\to p]{,}$ построить что-нибудь разумное?

[Portnov]

Насколько я понял, это конструктивистское определение отрицания. Вместо $\neg p$ пишем $p\to f$, где $f$ — заведомо ложное утверждение (эквивалентность такого определения и обычного легко проверить хотя бы по таблице истинности). Рассуждения о природе отрицания и всяких разных определениях отрицания мне понравились у Карри в «Основаниях математической логики», там целая глава этим вопросам посвящена.

[Виктор Викторов]

Спасибо. Мне эта мысль пришла в голову, но я её отмел поскольку рядом $f$ используется как обыкновенное буквенное обозначение.