Email Gateway (Aug 18 2022 at 16:11): Email Gateway (Aug 18 2022 at 16:11):From: John Munroe <munddr@gmail.com>
Hello
For the following:
axiomatization
c :: real
where
ax1 : "c > 0"
lemma "EX z. c = z"
sorry
Can the quantifier be proved by instantiation only? Perhaps, this
question logically follows: is there an expression y such that apply
(rule exI [where x=y])?
Thank you for the help.
John
Email Gateway (Aug 18 2022 at 16:11):From: Joachim Breitner <mail@joachim-breitner.de>
Hello,
I’m not sure what you mean, but maybe this is it?
lemma "EX z. c = z"
apply (rule exI[of _ c])
apply (rule refl);
done
Greetings,
Joachim
signature.asc
Email Gateway (Aug 18 2022 at 16:11):From: munddr@gmail.com
Thanks for the replies. I'm trying to not prove it by reflexivity, but
instead by instantiating z to an expression that follows from ax1. Such an
expression should probably say that "a real that is greater than 0", but I
can't quite see how that can be expressed.
Thanks
John
Email Gateway (Aug 18 2022 at 16:11):From: munddr@gmail.com
Thanks for the replies. I'm trying to not prove it by reflexivity, but
instead by instantiating z to an expression that follows from ax1. Such an
expression should probably say that "a real that is greater than 0", but I
can't quite see how that can be expressed.
Thanks
John
Last updated: Apr 26 2024 at 16:20 UTC