Pravidlo zavedení obecného kvantifikátoru

Nechť proměnná x nemá ve formuli A volný výskyt a nechť |- A→B.

Potom |- A→(∀x)B

Důkaz

Předpokládám

|- A→B

Dle pravidla generalizace

|- (∀x)(A→B)

Nyní použiju schéma přeskoku a modus ponens

   (∀x)(A->B)     (∀x)(A->B)->(A->(∀x)B)
  ---------------------------------------
               A->(∀x)B

(vím z předpokladů věty, že x nemá v A volný výskyt)

|- A→(∀x)B

QED

 
pravidlo_zavedeni_obecneho_kvantifikatoru.txt · Last modified: 2006/04/30 15:51 by 85.160.7.160
 
Recent changes RSS feed Creative Commons License Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki