Table of Contents

1.

Nechť x nemá v A volný výskyt

A ↔ (∀x)A

Důkaz

Budu dokazovat dvě implikace

|- A→(∀x)A a |- (∀x)A→A

Vyjdu z v1

|- A→A

Podle věty o zavedení obecného kvantifikátoru

|- A→(∀x)A

Vyjdu ze schematu specifikace

|- (∀x)A→Ax[t]

Za t dosadím x

|- (∀x)A→A

QED

2.

Nechť x nemá v A volný výskyt

(∃x)A↔A

Důkaz

Stejně jako v předchozím případě budu dokazovat dvě implikace

(∃x)A→A a A→(∃x)A

Vyjdu z

|- A→A

Podle věty o zavedení existenčního kvantifikátoru

|- (∃x)A→A

Podle pravidla substituce

|- Ax[t]→(∃x)A

Za t dosadím x

|- A→(∃x)A

QED

 
a_-_x_a.txt · Last modified: 2006/05/02 16:34 by 85.160.17.55
 
Recent changes RSS feed Creative Commons License Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki