Re: [isabelle] A proof for existential

Hi John,

your lemma does not follow from your axioms, even after fixing your typos. I guess you meant your axioms to be

ax1: "EX x. ALL y. x ~= y --> h x > h y" and
ax2: "EX x. (ALL y. x ~= y --> h x > h y) --> g x = 0"

Take g(x) = 1 and h(x) = if x = 0 then 1 else 2.
Then g and h satisfy both ax1 and ax2:
Take x=0 for the existential quantifier in ax1 and take x=1 for the existential in ax2 (with y=0 for the universal quantifier).


Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Gebäude 50.41, Raum 023
76131 Karlsruhe

Telefon: +49 721 608-8352
Fax: +49 721 608-8457
E-Mail: andreas.lochbihler at
KIT - Universität des Landes Baden-Württemberg und nationales Großforschungszentrum in der Helmholtz-Gemeinschaft

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.