Detrazione naturale: comprensione dell'eliminazione inferiore (¬)

Question

Sono nuovo alla deduzione naturale ea leggere su vari metodi online, mi sono imbattuto nella regola dell'eliminazione del fondo nel seguente Esempio .

Non capisco il passo nella riga 10.

All'ispezione, il mio pensiero iniziale sarebbe che l'assunzione di ¬P e P sia che sia vera è assurdo, quindi tutto può essere dedotto (in questo caso "P ').Tuttavia, se questo fosse il caso in cui ti fermeresti (questo sembra essere uno strumento troppo potente)?Quindi presumo che questa idea sia sbagliata.

Qualcuno potrebbe aiutarmi a capire la regola?

Nota : Sono arrivato a Stackexchange a causa della mancanza di risorse e informazioni specifiche online.

Answer 1

Di solito in pratica abbiamo saldato i due passi insieme e dici solo che da $ P $ e $ \ lnot p $ Qualsiasi cosa segue, ma in logica formale Questa è una combinazione di due regole di inferenza:

.
1. $ p $ e $ \ lnot p $ entrambi insieme comportano la falsyhood $ \ Bot $ ,
2. da $ \ bot $ Viene segue.

Queste sono precisamente linee 9 e 10 nella tua prova.

Prendiamo spesso $ \ lnot p $ per essere un'abbreviazione per $ P \ RightArrow \ Bot $ , nel qual caso la regola "da $ P $ e $ \ lnot p $ segue $ \ bot $ "è solo un caso speciale di modus ponens" da $ p $ e $ P \ RightArrow R $ Segue $ r $ ".