Email Gateway (Mar 07 2021 at 11:01): Email Gateway (Mar 07 2021 at 11:01):From: "Jens-D. Doll" <jens.doll@live.de>
Hello everyone,
is there a common sense about how a proof has to be structured? Does
there exist a formal grammar or a mathematical structure for it? Can
coherence* be formalized?
Happy reasoning,
Jens
*from philosophy of science
Email Gateway (Mar 07 2021 at 18:27):From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>
Dear Jens,
you may want to have a look in Chapter 6 of the Isabelle manual
https://isabelle.in.tum.de/doc/isar-ref.pdf
where there are some details about common proof structures, e.g. proof
by induction,
proof by cases, proof by contradiction etc.-- in Isar there exist some
standard
ways for structuring these.
I'm not sure if this answers your question though.
Best wishes,
Angeliki
Email Gateway (Mar 08 2021 at 17:17):From: "Jens-D. Doll" <jens.doll@live.de>
Hello Angeliki,
the basic types of proofs is not enough. I imagine a formal expression
over these types, which tells me if a certain sequence or hierarchy is
allowed. For instance a sequence of two proofs by contradiction is not
allowed?!
Jens
Last updated: Jan 04 2025 at 20:18 UTC