Pravidlo zavedení existenčního kvantifikátoru

Nechť proměnná x není volná ve formuli B a nechť |- A→B

Potom |- (∃x)A→B

Důkaz

Předpoklad je

|- A→B

Dle v5 výrokové logiky (a tedy zároveň predikátové) a modus ponens

   A->B     (A->B)->(¬B->¬A)
  ---------------------------
           ¬B->¬A

|- ¬B→¬A

Dále použiju pravidlo zavední obecného kvantifikátoru a v4 výrokové logiky (s tou v4 si nejsem úplně jistý, že to takto jde - snad věta o ekvivalenci??)

|- ¬B→¬¬(∀x)¬A

To lze bez újmy na čemkoliv přepsat jako

|- ¬B→¬(∃x)A

A poslední krok je použití A3 a modus ponens

   ¬B->¬(∃x)A     ( ¬B->¬(∃x)A )->( (∃x)A->B )
  ----------------------------------------------
                   (∃x)A->B

|- (∃x)A→B