*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] How to create a new algebra based on 3 valued logic*From*: Gottfried Barrow <igbi at gmx.com>*Date*: Tue, 23 Sep 2014 13:00:12 -0500*In-reply-to*: <BAY167-W2774DB24A490D4EF1813B1B6B00@phx.gbl>*References*: <541D8E4A.2000407@informatik.tu-muenchen.de>, <541FE190.6090902@inf.ethz.ch> <BAY167-W2774DB24A490D4EF1813B1B6B00@phx.gbl>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 14-09-23 08:58, Lee Martin CCNP wrote: > I guess a 3 valued logic table > http://www.mapleprimes.com/questions/202431-How-To-Construct-A-Table-For-Base-10 > if succeed to create 3 operator table for base 10, > is it possible to develop a new algebra in Isabelle and proof it ? Lee, I assume you're working in Isabelle/HOL, with an entry point of importing Complex_Main, and not extending HOL with any axioms of your own. SHORT ANSWER PART 1: HOL is a logic, with a defined set of axioms (all of which are not clearly made known to users in the Isabelle literature), and as with mathematics in general, you are free to define algebraic operations, but what you can or cannot prove is dependent on your definitions, and on the HOL axioms. SHORT ANSWER PART 2 (the global law of spheres of mathematical influence) : a) In general, our proofs about math that are of interest to us, are of no interest to others, and b) if the math we're interested in is of no great, practical value, not only are others not interested in any proofs about such math, they're most likely not interested in the math. SHORT ANSWER PART 3: Back to part 1, and with part 2 in mind, it's up to you to show what can or cannot be done in Isabelle/HOL, for what hasn't been done in Isabelle/HOL, for what you're interested in. SHORT ANSWER PART 4: The above explains my approach, based on my past observations of the culture of mathematics. But even big time players, in all cultures, have a hard time getting people interested in what they're doing. Google, with millions of dollars in funding, couldn't get people very much interested in Google+, and as people got bored with Myspace, they will most likely get bored with Facebook. That's the short answer. I'll leave off the long answer, involving my opinions about marketing, and how marketing is generally necessary to draw people into what we are doing, and what we are interested in. Personally, what I have in mind is dance, trance, and disco, where the disco will hopefully be kept to a minimum, especially the display of gold chains, by means of leaving unbuttoned the top three buttons of a yellow, polyester shirt. But even trance can be risky. It's not that my professional reputation can be tarnished, since I have no professional reputation. It's that if one has heard 4 measures of trance, one has heard 4 hours of trance, which we could rephrase as the Law of Trance, "If one has heard 4 measures of trance, one has heard 4 hours of trance." Regards, GB

**References**:**[isabelle] Usability Lifting and Transfer***From:*Florian Haftmann

**Re: [isabelle] Usability Lifting and Transfer***From:*Andreas Lochbihler

**[isabelle] How to create a new algebra based on 3 valued logic***From:*Lee Martin CCNP

- Previous by Date: [isabelle] How to create a new algebra based on 3 valued logic
- Next by Date: [isabelle] proof document with conference style
- Previous by Thread: [isabelle] How to create a new algebra based on 3 valued logic
- Next by Thread: [isabelle] New AFP entry: The Sturm-Tarski Theorem
- Cl-isabelle-users September 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list