You can subscribe to this list here.
2003 
_{Jan}

_{Feb}

_{Mar}

_{Apr}

_{May}

_{Jun}

_{Jul}

_{Aug}
(12) 
_{Sep}
(8) 
_{Oct}
(20) 
_{Nov}
(21) 
_{Dec}
(3) 

2004 
_{Jan}
(16) 
_{Feb}
(11) 
_{Mar}
(26) 
_{Apr}
(15) 
_{May}
(17) 
_{Jun}
(10) 
_{Jul}
(3) 
_{Aug}
(4) 
_{Sep}
(11) 
_{Oct}

_{Nov}
(11) 
_{Dec}
(8) 
2005 
_{Jan}
(16) 
_{Feb}
(18) 
_{Mar}
(22) 
_{Apr}
(23) 
_{May}
(17) 
_{Jun}
(22) 
_{Jul}
(10) 
_{Aug}
(9) 
_{Sep}
(13) 
_{Oct}
(26) 
_{Nov}
(26) 
_{Dec}
(31) 
2006 
_{Jan}
(29) 
_{Feb}
(35) 
_{Mar}
(20) 
_{Apr}
(23) 
_{May}
(35) 
_{Jun}
(17) 
_{Jul}
(18) 
_{Aug}
(11) 
_{Sep}
(18) 
_{Oct}
(12) 
_{Nov}
(16) 
_{Dec}
(27) 
2007 
_{Jan}
(27) 
_{Feb}
(22) 
_{Mar}
(15) 
_{Apr}
(38) 
_{May}
(26) 
_{Jun}
(24) 
_{Jul}
(8) 
_{Aug}
(20) 
_{Sep}
(21) 
_{Oct}
(23) 
_{Nov}
(20) 
_{Dec}
(24) 
2008 
_{Jan}
(16) 
_{Feb}
(19) 
_{Mar}
(24) 
_{Apr}
(54) 
_{May}
(24) 
_{Jun}
(21) 
_{Jul}
(20) 
_{Aug}
(12) 
_{Sep}
(19) 
_{Oct}
(28) 
_{Nov}
(26) 
_{Dec}
(34) 
2009 
_{Jan}
(22) 
_{Feb}
(15) 
_{Mar}
(20) 
_{Apr}
(33) 
_{May}
(27) 
_{Jun}
(30) 
_{Jul}
(23) 
_{Aug}
(13) 
_{Sep}
(21) 
_{Oct}
(19) 
_{Nov}
(29) 
_{Dec}
(22) 
2010 
_{Jan}
(36) 
_{Feb}
(30) 
_{Mar}
(58) 
_{Apr}
(38) 
_{May}
(36) 
_{Jun}
(35) 
_{Jul}
(22) 
_{Aug}
(8) 
_{Sep}
(40) 
_{Oct}
(27) 
_{Nov}
(29) 
_{Dec}
(23) 
2011 
_{Jan}
(31) 
_{Feb}
(39) 
_{Mar}
(30) 
_{Apr}
(49) 
_{May}
(38) 
_{Jun}
(27) 
_{Jul}
(11) 
_{Aug}
(13) 
_{Sep}
(20) 
_{Oct}
(28) 
_{Nov}
(23) 
_{Dec}
(18) 
2012 
_{Jan}
(36) 
_{Feb}
(39) 
_{Mar}
(61) 
_{Apr}
(71) 
_{May}
(188) 
_{Jun}
(117) 
_{Jul}
(132) 
_{Aug}
(153) 
_{Sep}
(32) 
_{Oct}
(44) 
_{Nov}
(64) 
_{Dec}
(56) 
2013 
_{Jan}
(85) 
_{Feb}
(36) 
_{Mar}
(44) 
_{Apr}
(130) 
_{May}
(47) 
_{Jun}
(33) 
_{Jul}
(34) 
_{Aug}
(25) 
_{Sep}
(20) 
_{Oct}
(49) 
_{Nov}
(20) 
_{Dec}
(39) 
2014 
_{Jan}
(38) 
_{Feb}
(61) 
_{Mar}
(83) 
_{Apr}
(56) 
_{May}
(42) 
_{Jun}
(37) 
_{Jul}
(24) 
_{Aug}
(16) 
_{Sep}
(28) 
_{Oct}
(33) 
_{Nov}
(21) 
_{Dec}
(22) 
2015 
_{Jan}
(12) 
_{Feb}
(43) 
_{Mar}
(46) 
_{Apr}
(36) 
_{May}
(57) 
_{Jun}
(29) 
_{Jul}
(19) 
_{Aug}
(21) 
_{Sep}
(17) 
_{Oct}
(20) 
_{Nov}
(77) 
_{Dec}
(30) 
2016 
_{Jan}
(20) 
_{Feb}
(39) 
_{Mar}
(53) 
_{Apr}
(32) 
_{May}
(47) 
_{Jun}
(53) 
_{Jul}
(24) 
_{Aug}

_{Sep}

_{Oct}

_{Nov}

_{Dec}

From: <Michael.N<orrish@da...>  20160725 00:43:13

If you use the most recent working version of HOL (get it via git), then your Holmake processes will be multicore on a pertheory basis (i.e., where the theorygraph of dependencies permits it, Holmake will cause theories to build concurrently). There is currently no support for concurrent execution within a single session. Michael From: hamed nemati <hn_nemati1985@...> ReplyTo: hamed nemati <hn_nemati1985@...> Date: Monday, 25 July 2016 at 03:37 To: "Norrish, Michael (Data61, Canberra City)" <Michael.Norrish@...>, "holinfo@..." <holinfo@...> Subject: Re: [Holinfo] EVAL(tac conv rule) Dear Michael, Thanks for your reply, I managed to solve the problem. As a complementary question, I wonder if HOL4 can use more than one core for its computations. Regards, Hamed Nemati On Sunday, July 24, 2016 5:39 AM, "Michael.Norrish@..." <Michael.Norrish@...> wrote: One approach would be to define constants that do the abbreviation for you. Then you should recast the theorems/definitions that EVAL is using to also use those new constants. I'm afraid there isn't any code already around that automatically detects repeated subterms, so you'd have to write some custom SML to get exactly the behaviour you want. Michael From: hamed nemati <hn_nemati1985@...> ReplyTo: hamed nemati <hn_nemati1985@...> Date: Sunday, 24 July 2016 at 02:59 To: HOLinfo List <holinfo@...> Subject: [Holinfo] EVAL(tac conv rule) Dear All, I would be very grateful if someone can help me with the following issue, When I am applying (RESTR_) EVAL(TAC/ CONV / RULE etc.) to evaluate a term I get a very huge result which has subterms repeat several times inside. Is there any smarter version of EVAL(tac conv rule) which avoids expanding the same subterms repeatedly by for example abbreviating them. This would decrease evaluation time and make the evaluated term much shorter. Regards, Hamed Nemati 
From: hamed nemati <hn_nemati1985@ya...>  20160724 17:37:43

Dear Michael,Thanks for your reply, I managed to solve the problem. As a complementary question, I wonder if HOL4 can use more than one core for its computations. Regards,Hamed Nemati On Sunday, July 24, 2016 5:39 AM, "Michael.Norrish@..." <Michael.Norrish@...> wrote: #yiv7118188152  filtered {panose1:0 0 0 0 0 0 0 0 0 0;}#yiv7118188152 filtered {fontfamily:Calibri;panose1:2 15 5 2 2 2 4 3 2 4;}#yiv7118188152 filtered {fontfamily:HelveticaNeue;}#yiv7118188152 p.yiv7118188152MsoNormal, #yiv7118188152 li.yiv7118188152MsoNormal, #yiv7118188152 div.yiv7118188152MsoNormal {margin:0cm;marginbottom:.0001pt;fontsize:12.0pt;}#yiv7118188152 a:link, #yiv7118188152 span.yiv7118188152MsoHyperlink {color:#0563C1;textdecoration:underline;}#yiv7118188152 a:visited, #yiv7118188152 span.yiv7118188152MsoHyperlinkFollowed {color:#954F72;textdecoration:underline;}#yiv7118188152 span.yiv7118188152EmailStyle17 {fontfamily:Calibri;color:windowtext;}#yiv7118188152 span.yiv7118188152msoIns {textdecoration:underline;color:teal;}#yiv7118188152 .yiv7118188152MsoChpDefault {fontsize:10.0pt;}#yiv7118188152 filtered {margin:72.0pt 72.0pt 72.0pt 72.0pt;}#yiv7118188152 div.yiv7118188152WordSection1 {}#yiv7118188152 One approach would be to define constants that do the abbreviation for you. Then you should recast the theorems/definitions that EVAL is using to also use those new constants. I'm afraid there isn't any code already around that automatically detects repeated subterms, so you'd have to write some custom SML to get exactly the behaviour you want. Michael From: hamed nemati <hn_nemati1985@...> ReplyTo: hamed nemati <hn_nemati1985@...> Date: Sunday, 24 July 2016 at 02:59 To: HOLinfo List <holinfo@...> Subject: [Holinfo] EVAL(tac conv rule) Dear All, I would be very grateful if someone can help me with the following issue, When I am applying (RESTR_) EVAL(TAC/ CONV / RULE etc.) to evaluate a term I get a very huge result which has subterms repeat several times inside. Is there any smarter version of EVAL(tac conv rule) which avoids expanding the same subterms repeatedly by for example abbreviating them. This would decrease evaluation time and make the evaluated term much shorter. Regards, Hamed Nemati 
From: <Michael.N<orrish@da...>  20160724 03:38:54

One approach would be to define constants that do the abbreviation for you. Then you should recast the theorems/definitions that EVAL is using to also use those new constants. I'm afraid there isn't any code already around that automatically detects repeated subterms, so you'd have to write some custom SML to get exactly the behaviour you want. Michael From: hamed nemati <hn_nemati1985@...> ReplyTo: hamed nemati <hn_nemati1985@...> Date: Sunday, 24 July 2016 at 02:59 To: HOLinfo List <holinfo@...> Subject: [Holinfo] EVAL(tac conv rule) Dear All, I would be very grateful if someone can help me with the following issue, When I am applying (RESTR_) EVAL(TAC/ CONV / RULE etc.) to evaluate a term I get a very huge result which has subterms repeat several times inside. Is there any smarter version of EVAL(tac conv rule) which avoids expanding the same subterms repeatedly by for example abbreviating them. This would decrease evaluation time and make the evaluated term much shorter. Regards, Hamed Nemati 
From: hamed nemati <hn_nemati1985@ya...>  20160723 17:01:26

Dear All,I would be very grateful if someone can help me with the following issue, When I am applying (RESTR_) EVAL(TAC/ CONV / RULE etc.) to evaluate a term I get a very huge result which has subterms repeat several times inside. Is there any smarter version of EVAL(tac conv rule) which avoids expanding the same subterms repeatedly by for example abbreviating them. This would decrease evaluation time and make the evaluated term much shorter. Regards,Hamed Nemati 
From: Thomas Melham <thomas.melham@ba...>  20160723 08:58:17

Dear Dwi, This is classic HOL stuff  see this old paper<https://www.cl.cam.ac.uk/techreports/UCAMCLTR91.pdf>; or my thesis<http://dx.doi.org/10.1017/CBO9780511569845>;. I suspect that floatingpoint verification directly in HOL, at least for circuits of any size, will be quite challenging. However, David Russinoff<http://dblp.org/pid/53/70>; does this kind of thing quite regularly in ACL2, so it’s certainly possible. All best regards, Tom On 23/07/2016, 05:01, "dwi.teguh51" <dwi.teguh51@...<mailto:dwi.teguh51@...>> wrote: Dear all, Hi, I'm Dwi, a newbie in HOL Now I'm still learning and exploring hardware verification especially about floating point for my master thesis. I want to try the verification at the gate level. Is anyone ever tried to specify or modeling the basic logic gates (AND, OR, NOT, etc.) in HOL or HOL Light? Is there any related library I can explore? Thank you. Best Regards, Dwi  What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic patterns at an interfacelevel. Reveals which users, apps, and protocols are consuming the most bandwidth. Provides multivendor support for NetFlow, JFlow, sFlow and other flows. Make informed decisions using capacity planning reports.http://sdm.link/zohodev2dev _______________________________________________ holinfo mailing list holinfo@...<mailto:holinfo@...> https://lists.sourceforge.net/lists/listinfo/holinfo 
From: dwi.teguh51 <dwi.teguh51@ui...>  20160723 04:20:31

Dear all, Hi, I'm Dwi, a newbie in HOL Now I'm still learning and exploring hardware verification especially about floating point for my master thesis. I want to try the verification at the gate level. Is anyone ever tried to specify or modeling the basic logic gates (AND, OR, NOT, etc.) in HOL or HOL Light? Is there any related library I can explore? Thank you. Best Regards, Dwi 
From: Sebastian Gerwinn <sgerwinn@tc...>  20160720 07:11:57

======================================================================== FORMATS'16  Call for participation 14th international conference on Formal Modeling and Analysis of Timed Systems (joint with CONCUR'16 and QEST'16) Québec City, Canada, 2426 August http://formats16.lsv.fr/ ======================================================================== FORMATS'16 will take place in Québec City, Canada, from 24 to 26 August 2016. It is colocated with the conferences CONCUR'16 and QEST'16 (which start on 23 August 2016), and with the workshops EXPRESS/SOS (22 August 2016) and TRENDS (27 August 2016). Invited speakers, in collaboration with CONCUR and QEST:  Scott A. Smolka (State University of New York, Stony Brook) Ufuk Topcu (University of Texas, Austin) Oleg Sokolsky (University of Pennsylvania) FORMATS'16 program:  http://formats16.lsv.fr/?page_id=240 Registration:  You can register from the CONCUR website: http://www.concur2016.ulaval.ca/registration_and_venue/ (Earlyregistration fees until 22 July) 
From: Peter Schueller <peter.schuller@ma...>  20160715 13:49:42

(Apologies if you receive multiple copies of this email. Please distribute to interested parties.)  ICLP DC 2016 Twelfth ICLP Doctoral Student Consortium to be held in New York City, USA, 18 October 2016 http://dciclp16.cs.bath.ac.uk/  The ICLP Doctoral Consortium (DC) is the twelfth doctoral consortium to be held as part of the 32nd International Conference on Logic Programming (ICLP 2016). The DC will take place during ICLP 2016 in New York City, USA. It provides a forum for doctoral students working in areas related to logic and constraint programming, with a particular emphasis to students interested in pursuing a career in academia. The DC gives students the opportunity to present and discuss their research and to obtain feedback from peers as well as worldrenowned experts. ** Target Audience ** The DC is designed for students currently enrolled in a Ph.D. program, though we are also open to exceptions (e.g., students currently in a Master's program and interested in doctoral studies). Students at any stage in their doctoral studies are encouraged to apply for participation in the DC. Applicants are expected to conduct research in areas related to logic and constraint programming; topics of interest include (but are not limited to):  Theoretical Foundations of Logic and Constraint Logic Programming  Sequential and Parallel Implementation Technology  Static and Dynamic Analysis, Abstract Interpretation, Compilation Technology, Verification  Logicbased Paradigms (e.g., Answer Set Programming, Concurrent Logic Programming, Inductive Logic Programming)  Innovative Applications of Logic Programming  Logic Programming and Nonmonotonic Reasoning  Logic Programming and Causality  Logic Programming Systems Submissions by students who have presented their work at previous ICLP DC editions are allowed, but should occur only if there are substantial changes or improvements to the student's work. The DC allows participants to interact with established researchers and fellow students, through presentations, questionanswer sessions, panel discussions, and invited presentations. The Doctoral Consortium will provide the possibility to reflect  through short activities, information sessions, and discussions  on the process and lessons of research and life in academia. Each participant will give a short, critiqued, research presentation. ** Application Process ** An application for participation in the ICLP DC 2016 consists of a cover letter, a research summary, and a letter of recommendation (e.g., from your supervisor). All applications must be in English and submitted electronically via EasyChair by 17 July 2016. Detailed submission instructions are provided at the ICLP DC 2016 website: http://dciclp16.cs.bath.ac.uk/ <http://dciclp15.cs.bath.ac.uk/>; The DC program committee will select participants based on their anticipated contribution to the DC objectives. Students will be selected based on clarity and completeness of their submission package, relevance of their research area w.r.t. the focus of ICLP, stage of research, recommendation letter, and evidence of promise towards a successful career in research and academia, such as published papers or technical reports. The works accepted for presentation at the DC will be published in conjunction with the ICLP proceedings. Updates follow as soon as we have more information regarding this. There will be some financial support available to students who attend the DC. The details will be announced soon. ** Important Dates ** Application Submission: 17 July 2016 Acceptance Notification: 1 August 2016 Cameraready Version: 14 August 2016 Doctoral Consortium: 18 October 2016 ** Organization **  Program Committee: Martin Gebser, Aalto Jose F. Morales, IMDEA Software Research Institute Ekaterina Komendantskaya, School of Computing, University of Dundee Fabio Fioravanti, University of ChietiPescara Francesco Ricca, Department of Mathematics University of Calabria Frank Valencia, LIX, Ecole Polytechnique Takehide Soh, Information Science and Technology Center, Kobe University  Program Chairs: Marina De Vos, University of Bath (M.D.Vos@...) Neda Saeedloei, University of Minnesota Duluth (nsaeedlo@...) Website: http://dciclp16.cs.bath.ac.uk/ 
From: JAMES P. (366409) <p.366409@sw...>  20160715 12:58:43

Registration for WADT 2016 is now open. Early registration ends on: Monday, July 18, 2016. Note that we can offer a number of reduced rate places for students / young researchers to attend WADT'16, who are not registered as an author for a paper. These places are limited to early registration. Link: http://cs.swan.ac.uk/wadt16/ When Sep 21, 2016  Sep 24, 2016 Where Gregynog, UK Submission Deadline June 17, 2016 (extended) Notification July 3, 2016 (extended) Final Version Due July 15, 2016 AIMS AND SCOPE The algebraic approach to system specification encompasses many aspects of the formal design of software systems. Originally born as formal method for reasoning about abstract data types, it now covers new specification frameworks and programming paradigms (such as objectoriented, aspectoriented, agentoriented, logic and higherorder functional programming) as well as a wide range of application areas (including information systems, concurrent, distributed and mobile systems). The workshop will provide an opportunity to present recent and ongoing work, to meet colleagues, and to discuss new ideas and future trends. TOPICS OF INTEREST Typical, but not exclusive topics of interest are:  Foundations of algebraic specification  Other approaches to formal specification, including process calculi and models of concurrent, distributed and mobile computing  Specification languages, methods, and environments  Semantics of conceptual modelling methods and techniques  Modeldriven development  Graph transformations, term rewriting and proof systems  Integration of formal specification techniques  Formal testing and quality assurance, validation, and verification INVITED SPEAKERS  Alessio Lomuscio (London, UK)  Till Mossakowski (Magdeburg, Germany)  John Tucker (Swansea, UK) WORKSHOP FORMAT AND LOCATION The workshop will take place over four days, Wednesday to Saturday, at Gregynog Hall in Wales, UK (http://www.gregynog.org). Participants should arrive on Tuesday evening, the workshop will end on Saturday with lunch. Presentations will be selected on the basis of submitted abstracts. IMPORTANT DATES Submission deadline for abstracts: June 17, 2016 (extended) Notification of acceptance: July 3, 2016 (extended) Early registration: July 3, 2016 (delayed) Final abstract due: July 15, 2016 Workshop in Gregynog: September 2124, 2016 SUBMISSIONS The scientific programme of the workshop will include presentations of recent results and ongoing research. The presentations will be selected by the Steering Committee on the basis of submitted abstracts according to originality, significance and general interest. The abstracts must be up to two pages long including references. If a longer version of the contribution is available, it can be made accessible on the web and referenced in the abstract. The abstracts have to be submitted electronically via the EasyChair system. PROCEEDINGS After the workshop, authors will be invited to submit full papers for the refereed proceedings. All submissions will be reviewed; selection will be based on originality, soundness and significance of the presented ideas and results. The proceedings will be published as a volume of Lecture Notes in Computer Science (Springer). SPONSORSHIP The workshop takes place under the auspices of IFIP WG 1.3. WADT STEERING COMMITTEE Andrea Corradini (Italy) Jose Fiadeiro (UK) Rolf Hennicker (Germany) HansJorg Kreowski (Germany) Till Mossakowski (Germany) Fernando Orejas (Spain) Francesco ParisiPresicce (Italy) Markus Roggenbach (UK) [chair] Grigore Rosu (United States) Andrzej Tarlecki (Poland) ORGANIZING COMMITTEE Phillip James (UK) Markus Roggenbach (UK) CONTACT INFORMATION Email: M.Roggenbach@... Homepage: http://cs.swan.ac.uk/wadt16/ 
From: Abid Rauf <abid.rauf@se...>  20160712 07:27:16

Dear All, Thankyou to Sir John Harrison for providing valuable help with the Definition. Also thanks to Mr. Marks Adam for highlighting the type difference. I am having the following type checking issue with my goal in the Matrix theory of HOLLight. It seems that left hand side and right hand side dont have similar types. I would appreciate if someone can please help me out with the change in definition or change in writing the goal or any other suggestion to get rid of this error. let horz_conct1 = new_definition `(horz_conct1:real^N^M>real^P^M>real^((N,P)finite_sum)^M) A B = lambda a b . if (b<=dimindex(:N)) then (A$a$b) else (B$a$(b(dimindex(:N))))`;; Now if i want to prove that g`!(A:real^N^M) (B:real^P^M) (C:real^Q^M). horz_conct1 (horz_conct1 A B) (C)= horz_conct1 (A) (horz_conct1 B C)`;; The types for the left hand side and right hand side were: `:real^((N,P)finite_sum,Q)finite_sum^M` (with type vars N, P, Q, M) `:real^(N,(P,Q)finite_sum)finite_sum^M` (with type vars N, P, Q, M) it gives following error Exception: Failure "typechecking error (initial type assignment)". So the definition is accepted but the proof goal using the function gives the problem. Best Regards, Abid Rauf Ph.D Scholar (CS) & RA SAVe Labs, School of Electrical Engineering and Computer Science (SEECS), National University of Science and Technology (NUST), H12, Islamabad, Pakistan On Mon, Jul 4, 2016 at 5:28 AM, <holinforequest@...> wrote: > Send holinfo mailing list submissions to > holinfo@... > > To subscribe or unsubscribe via the World Wide Web, visit > https://lists.sourceforge.net/lists/listinfo/holinfo > or, via email, send a message with subject or body 'help' to > holinforequest@... > > You can reach the person managing the list at > holinfoowner@... > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of holinfo digest..." > > > Today's Topics: > > 1. Re: A question about the definition of the function in HOL4 > (Ramana Kumar) > 2. Matrix Definition Query (Abid Rauf) > 3. Type checking issue (Abid Rauf) > 4. Re: Matrix Definition Query (John Harrison) > 5. Re: Type checking issue (Mark Adams) > > >  > > Message: 1 > Date: Thu, 30 Jun 2016 23:17:10 +1000 > From: Ramana Kumar <Ramana.Kumar@...> > Subject: Re: [Holinfo] A question about the definition of the > function in HOL4 > To: Ada <956066427@...> > Cc: holinfo <holinfo@...> > MessageID: > <CAMej= > 26cFzGL+f9eSjUxwE6saO5NttK6hrDjEkCouZfKFWVhQ@...> > ContentType: text/plain; charset="utf8" > > Hi Ada, > > It still looks like you might be mixing up ML and HOL. Are you trying to > define an ML function, or a HOL function? > > In ML, the conjunction of two Boolean expressions can be formed using the > "andalso" operator. > Now, maybe you already defined /\ like this, and gave it infix status: > > infix /\; > fun op /\ (a, b) = a andalso b; > > Then I would expect your definition to work. > > But please note that this is a definition in ML. If you want to make a > definition in HOL, use Define. > For example: > > val ccdd_def = Define`ccdd a b c d = if ((a = b) /\ (c = d)) then T else > F`; > > Cheers, > Ramana > > > On 30 June 2016 at 22:51, Ada <956066427@...> wrote: > > > Hi,guys > > I am working with HOL4. > > I defined a function in HOL4,like following > >  fun ccdd a b c d = if ((a = b) /\ (c = d)) then true else false; > > It responded that: > > ! Toplevel input: > > ! fun ccdd a b c d = if ((a = b) /\ (c = d)) then true else false; > > ! ^^^^^^^ > > ! Type clash: expression of type > > ! bool > > ! cannot have type > > ! 'a > 'b > > I can't understand it. > > Who know the reason? > > Thanks! > > > > > > >  > > Attend Shape: An AT&T Tech Expo July 1516. Meet us at AT&T Park in San > > Francisco, CA to explore cuttingedge tech and listen to tech luminaries > > present their vision of the future. This family event has something for > > everyone, including kids. Get more information and register today. > > http://sdm.link/attshape > > _______________________________________________ > > holinfo mailing list > > holinfo@... > > https://lists.sourceforge.net/lists/listinfo/holinfo > > > > >  next part  > An HTML attachment was scrubbed... > >  > > Message: 2 > Date: Fri, 1 Jul 2016 11:45:28 +0500 > From: Abid Rauf <abid.rauf@...> > Subject: [Holinfo] Matrix Definition Query > To: holinfo@... > MessageID: > < > CAMYogGWwzZss31WSUtPmGJhSdPOaDxVOLMRFrUYhxAw0cnjeg@...> > ContentType: text/plain; charset="utf8" > > Dear All, > > I have a Query about Matrices. Can i write a definition in HOL light which > takes two matrices of dimensions real^N^M and real^Q^P and after a certain > operation output a vector with dimension real^(N*Q)^(M*P). > I was going through the theory and found finite_sum, which is the addition > of dimensions, but here i need product or multiplication of dimensions. Can > anyone help me out please. > > Best Regards, > Abid Rauf > Ph.D Scholar (CS) & RA SAVe Labs, > School of Electrical Engineering and Computer Science (SEECS), > National University of Science and Technology (NUST), H12, Islamabad, > Pakistan >  next part  > An HTML attachment was scrubbed... > >  > > Message: 3 > Date: Sat, 2 Jul 2016 14:30:43 +0500 > From: Abid Rauf <abid.rauf@...> > Subject: [Holinfo] Type checking issue > To: holinfo@... > MessageID: > <CAMYogGVCtZm0= > i_DnT7TGcz_j7t8BoYFTCn381S4Vue7KLCatg@...> > ContentType: text/plain; charset="utf8" > > Dear All, > > I am having the following type checking issue with a definition in the > Matrix theory of HOLLight. It seems the double application of the function > leads to an unknown dimension of the matrix, which is causing the problem. > I would appreciate if someone can please help me out with us. > > let horz_conct1 = new_definition > `(horz_conct1:real^N^M>real^P^M>real^((N,P)finite_sum)^M) A B = lambda > a b . > if (b<=dimindex(:N)) > then (A$a$b) else (B$a$(b(dimindex(:N))))`;; > > Now if i want to prove that > > g`!(A:real^N^M) (B:real^P^M) (C:real^Q^M). horz_conct1 (horz_conct1 A B) > (C)= horz_conct1 (A) (horz_conct1 B C)`;; > > it gives following error > > Exception: Failure "typechecking error (initial type assignment)". > So the definition is accepted but the proof goal using the function gives > the problem. > > > Best Regards, > Abid Rauf > Ph.D Scholar (CS) & RA SAVe Labs, > School of Electrical Engineering and Computer Science (SEECS), > National University of Science and Technology (NUST), H12, Islamabad, > Pakistan >  next part  > An HTML attachment was scrubbed... > >  > > Message: 4 > Date: Sat, 02 Jul 2016 17:08:59 +0100 > From: John Harrison <John.Harrison@...> > Subject: Re: [Holinfo] Matrix Definition Query > To: Abid Rauf <abid.rauf@...> > Cc: holinfo@... > MessageID: <E1bJNTY0003jz0J@...> > > > Hi Abid, > >  I was going through the theory and found finite_sum, which is the > addition >  of dimensions, but here i need product or multiplication of dimensions. > Can >  anyone help me out please. > > I think the following should work  I should probably add it to the > system > as it might be useful for others too. > > let finite_prod_tybij = > let th = prove > (`?x. x IN 1..(dimindex(:A) * dimindex(:B))`, > EXISTS_TAC `1` THEN REWRITE_TAC[IN_NUMSEG; LE_REFL] THEN > MESON_TAC[LE_1; DIMINDEX_GE_1; MULT_EQ_0]) in > new_type_definition "finite_prod" > ("mk_finite_prod","dest_finite_prod") th;; > > let FINITE_PROD_IMAGE = prove > (`UNIV:(A,B)finite_prod>bool = > IMAGE mk_finite_prod (1..(dimindex(:A)*dimindex(:B)))`, > REWRITE_TAC[EXTENSION; IN_UNIV; IN_IMAGE] THEN > MESON_TAC[finite_prod_tybij]);; > > let DIMINDEX_HAS_SIZE_FINITE_PROD = prove > (`(UNIV:(M,N)finite_prod>bool) HAS_SIZE (dimindex(:M) * dimindex(:N))`, > SIMP_TAC[FINITE_PROD_IMAGE] THEN > MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN > ONCE_REWRITE_TAC[DIMINDEX_UNIV] THEN REWRITE_TAC[HAS_SIZE_NUMSEG_1] > THEN > MESON_TAC[finite_prod_tybij]);; > > let DIMINDEX_FINITE_PROD = prove > (`dimindex(:(M,N)finite_prod) = dimindex(:M) * dimindex(:N)`, > GEN_REWRITE_TAC LAND_CONV [dimindex] THEN > REWRITE_TAC[REWRITE_RULE[HAS_SIZE] DIMINDEX_HAS_SIZE_FINITE_PROD]);; > > John. > > > >  > > Message: 5 > Date: Mon, 04 Jul 2016 01:28:35 +0100 > From: Mark Adams <mark@...> > Subject: Re: [Holinfo] Type checking issue > To: Abid Rauf <abid.rauf@...> > Cc: holinfo@... > MessageID: <cde8a22147d81eb6fcab205d4031c4c3@...> > ContentType: text/plain; charset="usascii" > > Hello Abid, > > The term quotation fails type checking simply because the types of LHS > and RHS of the equality are different: > > `:real^((N,P)finite_sum,Q)finite_sum^M` (with type vars N, P, Q, M) > > `:real^(N,(P,Q)finite_sum)finite_sum^M` (with type vars N, P, Q, M) > > As I understand it (I may be wrong here), there is no way of getting the > HOL type system to let you express this associativity property about > 'horz_conct1'. If you want to express these kinds of properties, I > think you need to define your function in a different way, not using > types like this. > > Mark. > > On 02/07/2016 10:30, Abid Rauf wrote: > > > Dear All, > > > > I am having the following type checking issue with a definition in the > Matrix theory of HOLLight. It seems the double application of the function > leads to an unknown dimension of the matrix, which is causing the problem. > I would appreciate if someone can please help me out with us. > > > > let horz_conct1 = new_definition > > `(horz_conct1:real^N^M>real^P^M>real^((N,P)finite_sum)^M) A B = lambda > a b . > > if (b<=dimindex(:N)) > > then (A$a$b) else (B$a$(b(dimindex(:N))))`;; > > > > Now if i want to prove that > > > > g`!(A:real^N^M) (B:real^P^M) (C:real^Q^M). horz_conct1 (horz_conct1 A B) > (C)= horz_conct1 (A) (horz_conct1 B C)`;; > > > > it gives following error > > > > Exception: Failure "typechecking error (initial type assignment)". > > > > So the definition is accepted but the proof goal using the function > gives the problem. > > > > Best Regards, > > > > Abid Rauf > > Ph.D Scholar (CS) & RA SAVe Labs, > > School of Electrical Engineering and Computer Science (SEECS), > > National University of Science and Technology (NUST), H12, Islamabad, > Pakistan > > >  > > Attend Shape: An AT&T Tech Expo July 1516. Meet us at AT&T Park in San > > Francisco, CA to explore cuttingedge tech and listen to tech luminaries > > present their vision of the future. This family event has something for > > everyone, including kids. Get more information and register today. > > http://sdm.link/attshape > > _______________________________________________ > > holinfo mailing list > > holinfo@... > > https://lists.sourceforge.net/lists/listinfo/holinfo >  next part  > An HTML attachment was scrubbed... > >  > > >  > Attend Shape: An AT&T Tech Expo July 1516. Meet us at AT&T Park in San > Francisco, CA to explore cuttingedge tech and listen to tech luminaries > present their vision of the future. This family event has something for > everyone, including kids. Get more information and register today. > http://sdm.link/attshape > >  > > _______________________________________________ > holinfo mailing list > holinfo@... > https://lists.sourceforge.net/lists/listinfo/holinfo > > > End of holinfo Digest, Vol 122, Issue 1 > **************************************** > 
Dear Members of the Research Community, After a very fruitful debate with Russell O'Connor (who provided the proof of Goedel's First Incompleteness Theorem in Coq) I would like to correct and update some of my earlier publications. Also, with the kind permission of Russell O'Connor, his definitions for carrying out Goedel's First Incompleteness Theorem in Peter B. Andrews' logic Q0, an improved variant of Church's type theory, including a sample proof for a case of theorem V, are attached at the end of this email. Andrews' logic Q0 is specified in [Andrews, 2002, pp. 210215; Andrews, 1986, pp. 161165]. A short description is available online at [Andrews, 2014]: http://plato.stanford.edu/archives/spr2014/entries/typetheorychurch/#ForBasEqu Finally, a comparison of the proofs of Goedel's First Incompleteness Theorem by Russell O'Connor (in Coq) and Lawrence C. Paulson (in Isabelle) is undertaken in order to foster the understanding of the proof. The type system implemented by O'Connor is particularly well suited for demonstrating the three different language levels in the proof. Kind regards, Ken Kubota I. Corrections 1. The critique of a presentation of Goedel's First Incompleteness Theorem in my 2013 article [Kubota, 2013] applies to that particular presentation only, but not to the original publication of Goedel's First Incompleteness Theorem [Gödel, 1931]. Since the work with the criticized presentation is a standard work on higherorder logic, and the author of that work is usually extremely precise and accurate, I did not expect the criticized presentation to substantially differ from Goedel's original proof. 2. The hypothesis in my 2015 article [Kubota, 2015] that there is a significant difference in the results between axiomatic (Hilbertstyle) deductive systems (called "object logics" in the article) and natural deduction systems (called "metalogics" in the article) cannot be upheld. In summary, although some presentations of Goedel's First Incompleteness Theorem fail, this doesn't seem to apply to Goedel's original proof, nor does it apply to the formalized (mechanized) proofs provided by Russell O'Connor (in Coq) and others. The result of the formal proof can be interpreted in the sense that there is a formula (having the form of a sentence) that is neither provable nor refutable, but calling this "incompleteness" depends on a specific philosophical view, the semantic approach (model theory). If one doesn't share the semantic view, Goedel's theorem, although it seems formally correct, doesn't have the philosophical relevance often associated with it. II. Summary of the Proof 1. Mathematical (formal) part a) Goedel begins with the introduction of a number of definitions supposed to represent the form of a mathematical proof using mathematical (arithmetic) means, up to the last definition "Bew" (for "beweisbare Formel", i.e., "provable formula"). b) In theorem V, Goedel shows that each relation R (with the property of being primitive recursive) is definable within the logistic system by syntactical means (i.e., provability) only, in other words, for each R, there is an r (with the free variables u_1, ..., u_n), such that R(x_1, ..., x_n) > Bew( Sb(r, u_1, Z(x_1), ..., u_n, Z(x_n)) ) where Z is the numeral function, which returns the number in the language of the embedded language when supplying a (natural) number of the logistic system in which the proof is undertaken. The proof is of a rather technical nature and quite lengthy, and, unfortunately, in his presentation Goedel only sketched the idea. For an example, see the attached presentation by Russell O'Connor. c) Newer presentations refer to a fixedpoint theorem called the diagonal lemma (or diagonalization lemma), which is rather implicit in Goedel's original proof. It can be used to construe a formula with the form of a sentence (a booleanvalued wellformed formula with no free variables) g of the embedded language, such that (simplified) ~Bew(g) and ~Bew(not g). For an excellent introduction to the diagonal lemma, see [Raatikainen, 2015], available online at http://plato.stanford.edu/archives/spr2015/entries/goedelincompleteness/sup2.html In order to use the least amount of prerequisites, one may consider Goedel's proof of the (simplified) formula ~Bew(g) /\ ~Bew(not g) as a purely formal proof, where the definition of "Bew" is simply an abbreviation of a more complex numbertheoretic wellformed formula. However, for establishing the philosophical meaning associated with Goedel's First Incompleteness Theorem, namely incompleteness, two philosophical assumptions are necessary. 2. Philosophical part I: Correctness of definitions The first philosophical assumption is the correspondence of the definitions up to "Bew" with the form of mathematical proofs. Although it is obvious that the definitions do establish a proper representation of mathematical proofs, this fact goes beyond the formal part. For example, a proof verification system (or proof assistant) may prove ~Bew(g) /\ ~Bew(not g) as a formal theorem, showing that, given the definitions, this theorem can be obtained. But the software does not verify whether the definitions actually match the form of mathematical proofs; this task is left to the reader. Goedel himself emphasizes that the definability of (primitive) recursive relations in the system P is expressed by theorem V "_without_ reference to any interpretation of the formulas of P" [Gödel, 1931, p. 606, emphasis in the original]. Goedel speaks of yielding "an isomorphic image of the system PM in the domain of arithmetic, and all metamathematical arguments can just as well be carried out in this isomorphic image." [Gödel, 1931, p. 597, fn. 9] The isomorphism itself, however, can only be seen from top, from the metaperspective, i.e., from outside of the logistic system in which the proof is undertaken. A direct reference of the formal system to its own propositions is not possible. Accordingly, O'Connor distinguishes between a Goedel quote function and a Goedel numbering (or encoding) function, saying that propositions are "opaque". The Goedel numbering (or encoding) function "G isn't a function from propositions to natural numbers. It is supposed to be a function from *syntactic* formulas to natural numbers and the type of syntactic formulas is completely different from the type of propositions. Computations over syntactic formulas can inspect the intension[al] structure of the formula, but propositions are opaque and no such computation is possible." [Russell O'Connor, email to Ken Kubota, February 8, 2016] The same consideration was made by the author when mentioning the "nondefinability of the Goedel encoding function" previously at https://lists.cam.ac.uk/pipermail/clisabelleusers/2016January/msg00029.html By verifying the definitions (which is not a purely mathematical / formal task) one then can reasonably state that "Bew" can be interpreted as "provable", and that there is a formula with the form of a sentence (a proposition with no free variables) that is neither provable nor refutable. 3. Philosophical part II: The semantic approach Assuming 1. the correctness of the formal proof, and 2. the correctness of the definitions, the result obtained so far is that a wellformed formula exists, or more specifically, a formula of the form of an arithmetic proposition exists, which can neither be proven nor refuted. Following the semantic approach, according to which meaning is obtained by an interpretation in some kind of metatheory, either "g" or "not g" must be true, hence there must be a true but unprovable theorem. This discrepancy between syntax (provability) and semantics (truth, meaning) is what is commonly called "incompleteness". The implicit assumption made here and not discussed in the original publication of Goedel's First Incompleteness Theorem in [Gödel, 1931] is the use of the semantic approach (also called modeltheoretic approach). In his completeness essay published a year earlier, Goedel already makes use of the modeltheoretic approach in which semantic evaluation is performed by substitution at a metalevel, without explicitly pointing out the use of a specific philosophical assumption: "A formula of this kind is said to be valid (tautological) if a true proposition results from every substitution of specific propositions and functions for X, Y, Z, ... and F(x), G(x,y), ..., respectively [...]." [Gödel, 1930, p. 584, fn. 3] In order to speak of "incompleteness", an expectation of "completeness" is necessary, which is generally defined as the provability of all true propositions. Hence, incompleteness is only possible if semantics (meaning) differs from syntax, as is the case with model theory (the semantic approach). But the semantic approach itself is a specific philosophical view and not inherent in mathematics. If one, like the author, does not share the semantic approach, but a purely syntactic approach, such that meaning in mathematics is obtained by syntactical inference only (and the few rules of inference have their legitimation in philosophy, outside of formal logic and mathematics), then by definition there is no distinction between syntax and semantics. In summary, if one assumes the philosophical assumption of the semantic approach, then there is mathematical (arithmetic) incompleteness. But if one doesn't, Goedel's First Incompleteness Theorem only shows that there is a formula with the form of a wellformed (arithmetic) proposition which is neither provable nor refutable, but may also be considered meaningless. Not every wellformed formula (proposition) necessarily has to have a meaning, if one doesn't follow the semantic approach. "Mathematics is liquid" is grammatically correct, but nonsense. In philosophy, it is a wellestablished fact that sentences may have the (outward) form of a meaningful proposition without being meaningful. Hence, without the philosophical assumption of the semantic view or a similar approach, Goedel's First Incompleteness Theorem loses its philosophical significance. III. The Proofs by Russell O'Connor (in Coq) and Lawrence C. Paulson (in Isabelle) A particularly elegant formulation of Goedel's First Incompleteness Theorem was presented by Russell O'Connor using the proof assistant Coq, as he takes advantage of "type safety by coding using an inductive type" [Russell O'Connor, email to Ken Kubota, February 13, 2016], such that all three language levels use a different type. A short description is given in [O'Connor, 2006] available online at http://arxiv.org/pdf/cs/0505034v2.pdf The formal proof is available at http://www.lix.polytechnique.fr/coq/pylons/contribs/view/Goedel/trunk O'Connor uses different types for the three different levels of language: L1: type "prop" L2: type "Formula" (which may contain expressions of type "Term") L3: type "nat" The first language level (L1) is the language in which the proof is undertaken, expressed by propositions (type "prop"). The second language level (L2) is the embedded logic to be represented, expressed by syntactic formulae (type "Formula"). The third language level (L3) are the Goedel numbers obtained by encoding syntactic formulae (L2) using the Goedel numbering (or encoding) function, expressed by natural numbers (type "nat"). For example, the elimination of the implication can be expressed by "Lemma impE : forall (T : System) (f g : Formula), SysPrf T (impH g f) > SysPrf T g > SysPrf T f." http://www.lix.polytechnique.fr/coq/pylons/contribs/files/Goedel/trunk/Goedel.LNN.html with the predicate "SysPrf" corresponding to Goedel's "Bew", expressing the provability of a L2 formula p in a theory T by "SysPrf T p". The L1 expression is: "forall (T : System) (f g : Formula), SysPrf T (impH g f) > SysPrf T g > SysPrf T f". A L2 expression is: "impH g f" (which would be written as "g > f" at the L1 level). The Goedel numbering (or encoding) function accepts an argument of L2, and returns a number of L3: "Fixpoint codeFormula (f : Formula) : nat := match f with  fol.equal t1 t2 => cPair 0 (cPair (codeTerm t1) (codeTerm t2))  fol.impH f1 f2 => cPair 1 (cPair (codeFormula f1) (codeFormula f2))  fol.notH f1 => cPair 2 (codeFormula f1)  fol.forallH n f1 => cPair 3 (cPair n (codeFormula f1))  fol.atomic R ts => cPair (4+(codeR R)) (codeTerms _ ts) end." http://www.lix.polytechnique.fr/coq/pylons/contribs/files/Goedel/trunk/Goedel.code.html The numeral function accepts a number of L3 and returns the corresponding term that can be part of a L2 formula: "Fixpoint natToTerm (n : nat) : Term := match n with  O => Zero  S m => Succ (natToTerm m) end." http://www.lix.polytechnique.fr/coq/pylons/contribs/files/Goedel/trunk/Goedel.LNN.html For example, the number 3 is mapped to Succ(Succ(Succ(Zero))). The final result is: "Theorem Goedel'sIncompleteness1st : wConsistent T > exists f : Formula, ~ SysPrf T f /\ ~ SysPrf T (notH f) /\ (forall v : nat, ~ In v (freeVarFormula LNN f))." http://www.lix.polytechnique.fr/coq/pylons/contribs/files/Goedel/trunk/Goedel.goedel1.html So if the theory is (omega)consistent, then a proposition exists (that does not contain any free variables) which is neither provable nor refutable. Another formulation of Goedel's First Incompleteness Theorem was presented by Lawrence C. Paulson using the Isabelle proof assistant software. Descriptions are given in [Paulson, 2014] and [Paulson, 2015], linked at http://www.cl.cam.ac.uk/~lp15/papers/Formath/ and available online at http://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedellogicmine.pdf http://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedelar.pdf The formal proof is available at https://www.isaafp.org/browser_info/current/AFP/Incompleteness/ The proof by Paulson is carried out in his proof assistant software Isabelle, which is implemented as a logical framework (a metalogic), such that a fourth language level (the metalogic) is involved. On the basis of this metalogic (Isabelle/Pure), different object logics can be implemented such as set theory (Isabelle/ZF) or type theory (Isabelle/HOL). Hence, the four language levels of Paulson's proof are: L0: type "prop" of Isabelle/Pure (the logical framework / metalogic) L1: type "bool" of Isabelle/HOL (the object logic) L2: type "fm" (for formula) of HF set theory (which may contain expressions of type "tm") L3: type "tm" (for term) of HF set theory However, since the purpose of the logical framework or metalogic (L0) is only the implementation of several object logics such as the type theory / higherorder logic HOL (L1), the metalogic has no significance, and for the purpose of verifying Goedel's proof and comparing its different formulations, one may abstract from (i.e., ignore) it. The proof could be carried out within a direct implementation of HOL (without a logical framework / metalogic) also. Particularly misleading to those not familiar with the Isabelle software can be the turnstile symbol (⊢) as defined by Paulson in the context of Goedel's proof only: "inductive hfthm :: "fm set => fm => bool" (infixl "⊢" 55)" https://www.isaafp.org/browser_info/current/AFP/Incompleteness/SyntaxN.html The turnstile is introduced as an infix operator in a L1 expression, accepting a set of L2 formulae as first (left) operand, and a L2 formula as second (right) operand, denoting the predicate hfthm (for theorem of HF set theory) defined inductively directly afterwards. Usually in literature (e.g., [Andrews, 2002]), the right operand is an expression of the main language (L1), such that the turnstile is an operator of the metamathematical level (which one would have to place at L0, although it would functionally differ from a logical framework). Paulson's Goedel numbering (or encoding) function does not return numbers, but type "tm" (for term) of L3, which are more likely to be confused with L2: "class quot = fixes quot :: "'a => tm" ("⌈_⌉") instantiation tm :: quot begin definition quot_tm :: "tm => tm" where "quot_tm t = quot_dbtm (trans_tm [] t)" instance .. end [...] instantiation fm :: quot begin definition quot_fm :: "fm => tm" where "quot_fm A = quot_dbfm (trans_fm [] A)" instance .. end" https://www.isaafp.org/browser_info/current/AFP/Incompleteness/Coding.html Paulson: "It is essential to remember that [in Paulson's formulation of the proof] Gödel encodings are terms (having type tm), not sets or numbers." http://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedelar.pdf (p. 16) The final result is: "text{*Gödel's first incompleteness theorem: If consistent, our theory is incomplete.*} theorem Goedel_I: assumes "¬ {} ⊢ Fls" obtains δ where "{} ⊢ δ IFF Neg (PfP ⌈δ⌉)" "¬ {} ⊢ δ" "¬ {} ⊢ Neg δ" "eval_fm e δ" "ground_fm δ" " https://www.isaafp.org/browser_info/current/AFP/Incompleteness/Goedel_I.html Paulson's definition of the turnstile symbol (⊢) corresponds to O'Connor's predicate "SysPrf", which allows to express provability of L2 sentences within L1. Paulson's definition of the predicate "PfP" corresponds to O'Connor's predicate "codeSysPf", which allows to express provability of L3 sentences within L2. The statement "{} ⊢ δ IFF Neg (PfP ⌈δ⌉)" is an instance of the diagonal lemma using the construction "not provable" ("Neg (PfP [...])") as the lemma's property, which corresponds to that in O'Connor's definition of G: "Definition G := let (a,_) := FixPointLNN (notH codeSysPf) 0 in a." http://www.lix.polytechnique.fr/coq/pylons/contribs/files/Goedel/trunk/Goedel.goedel1.html The statements "¬ {} ⊢ δ" and "¬ {} ⊢ Neg δ" express that neither the proposition nor its negation are provable. The turnstile (⊢) denotes a predicate defined on the basis of the language of the logic in which the proof is undertaken. In contrast to O'Connor, Paulson also performs a semantic evaluation: The statement "eval_fm e δ" says that the proposition evaluates to true. The statement "ground_fm δ" ensures, like in O'Connor's proof, that the proposition does not contain any free variables. Despite Paulson's claim that "the availability of this formal proof (which can be surveyed by anybody who has a suitable computer and a copy of the Isabelle software) can help to demystify the incompleteness theorems" http://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedellogicmine.pdf (p. 1) his presentation has a number of disadvantages. In order to fully understand Paulson's proof, including the language levels and the type system involved, Paulson's articles are insufficient. Especially the description of the type system of both metalogic and object logic is fragmented into a number of occurrences across various documentation files of the software, making it extremely tedious to obtain all the information necessary to fully understand the formalized (mechanized) proof for anyone who is not very familiar with the proof assistant software used, even with advanced knowledge in formalizing (mechanizing) proofs. Not only would one expect a short introduction into the language levels, including the type system involved, but the articles concentrate on technical implementation details rather than the basic idea of the proof. The type "tm" occurs at two different language levels (L2 and L3), resulting in a higher ambiguity. The notation would require introduction, as a predicate is written as a symbol. Intermediary results, such as an instance of the diagonal lemma, and the additional semantic evaluation make the final result less readable in comparison to O'Connor's, who focuses on the nonprovability and nonrefutability of the proposition like Goedel in his original proof in theorem VI [cf. Gödel, 1931, p. 607 ff.]. Moreover, the formulation of the diagonal lemma is given as a special instance only, but not in the general form. Due to the "elimination of the pseudofunction K_i" http://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedelar.pdf (p. 23) his formulation of the diagonal lemma (and its application in Goedel's First Incompleteness Theorem) lacks the explicit use of the numeral function, yielding the following formulation: "lemma diagonal: obtains δ where "{} ⊢ δ IFF α(i::=⌈δ⌉)" "supp δ = supp α  {atom i}" " https://www.isaafp.org/browser_info/current/AFP/Incompleteness/Goedel_I.html Only the encoding function (⌈...⌉) is explicit in Paulson's formulation, whereas in O'Connor's formulation not only the Goedel encoding function (codeFormula), but also the numeral function (natToTermLNT) is present: "Lemma FixPointLNT : forall (A : Formula) (v : nat), {B : Formula  SysPrf PA (iffH B (substituteFormula LNT A v (natToTermLNT (codeFormula B)))) /\ [...]" http://www.lix.polytechnique.fr/coq/pylons/contribs/files/Goedel/trunk/Goedel.fixPoint.html Without crediting Wikipedia with scientific credibility, we shall take advantage of the symbolic notation used for the Goedel encoding function (#) and the numeral function (°): "Then T proves [...] p <> F(°#(p)), which is the desired result." [The Greek character 'psi' was replaced by 'p'.] https://en.wikipedia.org/w/index.php?title=Diagonal_lemma&oldid=702789841#Proof In both cases quoted above, first the Goedel numbering or encoding function (#/codeFormula), then the numeral function (°/natToTermLNT) is applied. IV. Possible Objections to the Formalized (Mechanized) Proofs Due to their nature, formalized (mechanized), i.e., computer verified proofs are unlikely to contain mistakes. But two conceptual issues require discussion, as they are tacitly assumed. 1. The semantic approach (model theory) Some proof assistants use methods of inference that rely on the semantic approach, specifically on the notion of satisfiability. These methods include resolution, which regularly makes use of unification and skolemization. If one does not share the semantic approach, but wants to rely on syntactical inference only, some skepticism may arise against theorems obtained by using these methods. However, since no unexpected results are known by the use of the current proof assistants, most likely an equivalent method exists by which the results can be obtained using syntactical means only. 2. The introduction of types with the BackusNaur form (BNF) Most of the current proof assistants allow the introduction of mathematical types by use of the BackusNaur form (BNF), which in computer science is the method of specifying an element of a formal language corresponding to inductive definitions in mathematics. For example, O'Connor defines the type of syntactic formulae "Formula" as follows: "Inductive Formula : Set :=  equal : Term > Term > Formula  atomic : forall r : Relations L, Terms (arity L (inl _ r)) > Formula  impH : Formula > Formula > Formula  notH : Formula > Formula  forallH : nat > Formula > Formula." http://www.lix.polytechnique.fr/coq/pylons/contribs/files/Goedel/trunk/Goedel.fol.html In an email to the author, Paulson, who designed the Isabelle proof assistant software, basically argued that newer type systems should be more expressive than Church's simple type theory which uses combinations of iota (i) and omicron (o) only. Although this is, of course, correct, the explanation is not sufficient for justifying this specific mode, namely BNF, of type introduction. The legitimacy of mathematical types depends on logical properties. For example, types must not be empty, since otherwise the logistic system is rendered inconsistent. Thus, the use of the BackusNaur form, which historically was introduced to specify grammars, is not appropriate for replacing mathematical reasoning. Types were invented by Bertrand Russell in order to avoid the paradoxes and therefore have logical properties (e.g., being nonempty) which should be subject to proof, but not be a matter of arbitrary declaration. Nevertheless, other means may be used to express the same, such that the use of the BackusNaur form is not essential to the proofs obtained by it. V. Some Remarks on the Semantic Approach In his article "The Semantic or ModelTheoretic View of Theories and Scientific Realism" available online at http://www3.nd.edu/~achakra1/downloads/semantic_view.pdf Anjan Chakravartty emphasizes that according to the syntactic view, a theory "is identified with a particular linguistic formulation" [Chakravartty, 2001, p. 325]. In contrast, the semantic view aims at "independence on behalf of theories from language" [Chakravartty, 2001, p. 326]. Obviously, Paulson and his Isabelle software follow the semantic approach. In his essays describing the proof [Paulson, 2014; Paulson, 2015], the semantic approach remains a tacit assumption given as granted, as the notion of incompleteness depends on it. On the basis of Isabelle's logical framework Isabelle/Pure, variants of both axiomatic set theory and type theory, i.e., a formulation of ZermeloFraenkel set theory (Isabelle/ZF) and a polymorphic version of Church's simple type theory (Isabelle/HOL), are implemented without opting or showing preference for one. In some sense, O'Connor is more careful, as he doesn't refer to the general notion of incompleteness, but only to "arithmetic incompleteness" or "essential incompleteness of [...] the language of arithmetic" [O'Connor, 2006, p. 15]. The problem reduces to a very specific phenomenon: "Goedel's theorem is more than the exist[ ]ance of a wff of type 'o' that is neither provable nor refutable. That goal is easy ((iota x : Nat . F) = 0) : o This wff above is neither provable nor refutable in Q0 (or both provable and refutable in the unlikely case Q0 is inconsistent.) The point of the incompleteness theorem is that there is an *arith[ ]metic* formula that is neither provable nor refutable, specifically a Pi1 arithmetic formula." [Russell O'Connor, email to Ken Kubota, February 19, 2016] "The emphasis on syntactical inference exists already hidden in the œuvre of Andrews. After stating that the semantic approach is only 'appealing' (but not definitely necessary), he then suggests to 'focus on trying to understand what there is about the syntactic structures of theorems that makes them valid.' '[S]imply checking each line of a truth table is not really very enlightening' [Andrews, 1989, pp. 257 f.]." [Kubota, 2013, p. 15] VI. Acknowledgements I would like to thank Russell O'Connor for providing the attached definitions and the sample proof as well as for granting permission for publication, for our interesting discussion, and for granting permission for the quotes used in this article to be published. References Andrews, Peter B. (1986), An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Orlando: Academic Press. Andrews, Peter B. (2002), An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Second edition. Dordrecht / Boston / London: Kluwer Academic Publishers. ISBN 1402007639. DOI: 10.1007/9789401599344. Andrews, Peter B. (2014), "Church's Type Theory". In: Stanford Encyclopedia of Philosophy (Spring 2014 Edition). Ed. by Edward N. Zalta. Available online at http://plato.stanford.edu/archives/spr2014/entries/typetheorychurch/ (July 2, 2016). Chakravartty, Anjan (2001), "The Semantic or ModelTheoretic View of Theories and Scientific Realism". In: Synthese 127, pp. 325345. DOI: 10.1023/A:1010359521312. Available online at http://www3.nd.edu/~achakra1/downloads/semantic_view.pdf (June 30, 2016). Gödel, Kurt (1930), "The completeness of the axioms of the functional calculus of logic". In: Heijenoort, Jean van, ed. (1967), From Frege to Gödel: A Source Book in Mathematical Logic, 18791931. Cambridge, Massachusetts: Harvard University Press, pp. 582591. Gödel, Kurt (1931), "On formally undecidable propositions of Principia mathematica and related systems I". In: Heijenoort, Jean van, ed. (1967), From Frege to Gödel: A Source Book in Mathematical Logic, 18791931. Cambridge, Massachusetts: Harvard University Press, pp. 596616. Kubota, Ken (2013), On Some Doubts Concerning the Formal Correctness of Gödel's Incompleteness Theorem. Berlin: Owl of Minerva Press. ISBN 9783943334043. DOI: 10.4444/100.101. See: http://dx.doi.org/10.4444/100.101 Kubota, Ken (2015), Gödel Revisited. Some More Doubts Concerning the Formal Correctness of Gödel's Incompleteness Theorem. Berlin: Owl of Minerva Press. ISBN 9783943334067. DOI: 10.4444/100.102. See: http://dx.doi.org/10.4444/100.102 O'Connor, Russell (2006), "Essential Incompleteness of Arithmetic Verified by Coq" (2nd version). Available online at http://arxiv.org/pdf/cs/0505034v2.pdf (June 29, 2016). DOI: 10.1007/11541868_16. Paulson, Lawrence C. (2014), "A MachineAssisted Proof of Gödel's Incompleteness Theorems for the Theory of Hereditarily Finite Sets". In: Review of Symbolic Logic 7, pp. 484498. DOI: 10.1017/S1755020314000112. Available online at http://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedellogicmine.pdf (June 30, 2016). Paulson, Lawrence C. (2015), "A Mechanised Proof of Gödel's Incompleteness Theorems using Nominal Isabelle". In: Journal of Automated Reasoning 55, pp. 137. DOI: 10.1007/s1081701593228. Available online at http://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedelar.pdf (June 30, 2016). Raatikainen, Panu (2015), "Supplement: The Diagonalization Lemma". In: Stanford Encyclopedia of Philosophy (Spring 2015 Edition). Ed. by Edward N. Zalta. Available online at http://plato.stanford.edu/archives/spr2015/entries/goedelincompleteness/sup2.html (June 30, 2016). ____________________ Ken Kubota doi: 10.4444/100 http://dx.doi.org/10.4444/100 ________________________________________________________________________________ SampleProofTheoremV by Russell O'Connor ________________________________________________________________________________ [In the following, all occurrences of "substitueFormula" were replaced by "substituteFormula".] [...] formal proof of a statement like (1) forall R exists r forall x PRR1(R) > [ Rx > [ proofB[Sb(r,u,Z(x))] ] ] but done in Q0 instead of informal mathematics. However, to get us started we can just try proving a single instance of this more general theorem in Q0. (2) exists r forall x PRR1([\x.x>1]) > [ [\x.x>1]x > [ proofB[Sb(r,u,Z(x))] ] ] The sad bit is that this single instance is much much easier to prove directly than the general theorem is, so my proof of the single instance probably won't be too illuminating. First, let me partially formalize statement (1) in Q0. PRR1 : (Nat > o) > o PRR1 := ... to be defined later ... PR1isExpressible : o PR1isExpressible forall R : Nat > o. PRR1(R) => exists r \in FormulaSet. exists u \in Nat. forall x \in NatSet. (R x => proves RA (substituteFormula r (at u (natToTerm x)))) /\ (~R x => proves RA (not (substituteFormula r (at u (natToTerm x))))) (everything else should be defined [below]) The simpler instance is stated in Q0 as follows GT1isExpressible : o GT1isExpressible := exists r \in FormulaSet. exists u \in Nat. forall x \in NatSet. (x > 1 => proves RA (substituteFormula r (at u x))) /\ (~x > 1 => proves RA (not (substituteFormula r (at u (natToTerm x))))) /\ Unfortu[na]tely I've lopped off the PRR1 bit which is probably what inter[e]sted you, because now the proof is too easy. Take r to be (some 1 (equal (var 0) (plus (var 1) (succ (succ zero))))) Take u to be 0. Let x be any value in NatSet. We need to show that (a) (x > 1) => proves RA (substituteFormula (some 1 (equal (var 0) (plus (var 1) (succ (succ zero))))) (at 0 (natToTerm x)))) and (b) ~(x < 1) => proves RA (not (substituteFormula (some 1 (equal (var 0) (plus (var 1) (succ (succ zero))))) (at 0 (natToTerm x)))) First thing I'd like to note is that we can use the definition of substituteFormula to prove that (substituteFormula (some 1 (equal (var 0) (plus (var 1) (succ (succ zero))))) (at 0 (natToTerm x)))) = (some 0 (equal (natToTerm x) (plus (var 0) (succ (succ zero))))) I also need a lemma that says (forall x \in NatSet. freeVarTerm (natToTerm x) = empty) This reduces our goal to (a) (x > 1) => proves RA (some 0 (equal (natToTerm x) (plus (var 0) (succ (succ zero))))) and (b) ~(x < 1) => proves RA (not (some 0 (equal (natToTerm x) (plus (var 0) (succ (succ zero)))))) Let's do (b) first because it is easier. We know x \in NatSet and that ~(x < 1) holds. So x = 0 or x = 1. Suppose x = 0. Then we have to prove goal: (proves RA (not (some 0 (equal (natToTerm 0) (plus (var 0) (succ (succ zero)))))) Using a lemma that natToTerm 0 = zero we can reduce this proving goal: (proves RA (not (some 0 (equal zero (plus (var 0) (succ (succ zero)))))) expanding the definition of some we get goal: (proves RA (not (not (all 0 (not (equal zero (plus (var 0) (succ (succ zero)))))))) Using a lemma that says that forall f \in FormulaSet. (proves RA (not (not f)))=(proves RA f) we can reduce this to showing goal: (proves RA (all 0 (not (equal zero (plus (var 0) (succ (succ zero)))))))) So we can reduce or goal to goal: (proves RA (not (equal zero (plus (var 0) (succ (succ zero))))))) One of the formulas in LA is all 1 (all 2 (impl (equal (var 1) (var 2)) (impl (all 0 (not (equal zero (var 1)))) (all 0 (not (equal zero (var 2))))))) so we know that (proves RA all 1 (all 2 (impl (equal (var 1) (var 2)) (impl (all 0 (not (equal zero (var 1)))) (all 0 (not (equal zero (var 2)))))))) from the universal instantiation lemma which says forall f \in FormulaSet. forall n \in NatSet. forall t \in TermSet. proves RA (all n f) => proves RA (substituteFormula f (at n t)) we can conclude (proves RA (impl (equal (succ (plus (var 0) (succ zero)))) (plus (var 0) (succ (succ zero)) (impl (all 0 (not (equal zero (succ (plus (var 0) (succ zero))) (all 0 (not (equal zero (plus (var 0) (succ (succ zero))) One of the axioms of RA is (all 0 (all 1 (equal (plus (var 0) (succ (var 1))) (succ (plus (var 0) (var 1)))))) So by using the universal [i]nstantiation theorem we get (proves RA (equal (plus (var 0) (succ (succ zero))) (succ (plus (var 0) (succ zero)))) We have another lemma that says forall t \in TermSet. forall s \in TermSet. (proves RA (equal t s))=(proves RA (equal s t)) which lets us deduce that (proves RA (equal (succ (plus (var 0) (succ zero))) (plus (var 0) (succ (succ zero))))) So by the modus ponens closure property that defines proves, we can conclude that (proves RA (impl (all 0 (not (equal zero (succ (plus (var 0) (succ zero))) (all 0 (not (equal zero (plus (var 0) (succ (succ zero)))) Another axiom of RA is all 0 (not (equal (succ (var 0)) zero)) So that plus universal instantiation lets us show that (proves RA (not (equal (succ (plus (var 0) (succ zero))) zero))) And another lemma that says forall t \in TermSet. forall s \in TermSet. (proves RA (not (equal t s)))=(proves RA (not (equal s t))) so we can conclude that (proves RA (not (equal zero (succ (plus (var 0) (succ zero)))))) Buy the universal gen[er]alization lemma we conclude (proves RA (all 0 (not (equal zero (succ (plus (var 0) (succ zero))))))) Using the modus ponens closure property that defines proves we can conclude t[ha]t (proves RA (all 0 (not (equal zero (plus (var 0) (succ (succ zero)))) which was our goal. [...] I'll let you do the case where x = 1. Now back to part (a) goal: (x > 1) => proves RA (some 0 (equal (natToTerm x) (plus (var 0) (succ (succ zero))))) Assuming that x > 1 that means there is some y \in NatSet such that x = S (S y) So this reduces our goal to goal: proves RA (some 0 (equal (natToTerm (S (S y))) (plus (var 0) (succ (succ zero))))) We can prove that (natToTerm (S (S y))) = succ (succ (natToTerm y)), so our goal is further reduced to goal: proves RA (some 0 (equal (succ (succ (natToTerm y))) (plus (var 0) (succ (succ zero))))) [...] the rest of the p[r]oof [...] to basical[l]y goes like this: You can show (proves RA (equal (succ (succ (natToTerm y))) (plus (natToTerm y) (succ (succ zero)))) and from this you can prove taht (proves RA (some 0 (equal (succ (succ (natToTerm y))) (plus (var 0) (succ (succ zero))))) which is the desired result. At some point you have to use induction on 'y' to do these sorts of proofs, but you might be able to get away without induction here because we were lucky. ________________________________________________________________________________ ExtendedIncompletenessInQ0 by Russell O'Connor ________________________________________________________________________________ // Define Computably Enumerable (aka recursively enumerable) predicates. CESet : (Nat > o) > o CESet := \p. exists f \in PRF2Set. p = (\n. exists m:Nat. 0 < f n m) // Standard Model interpT : (Nat > Nat) > Term > Nat interpT := \v. TermR_(Nat) v 0 (\t. S) (\t. \s. \n, \m. n + m) (\t. \s. \n. \m. n * m) interpF : (Nat > Nat) > Formula > o interpF := \v. \f. FormulaR_((Nat > Nat) > o) (\t. \s. \v. interpT v t = interpT v s) (\v. F) (\f. \g. \r. \s. \v. r v /\ s v) (\f. \g. \r. \s. \v. r v => s v) (\f. \n. \r. \s. \v. forall m \in NatSet. r (\x. if x = n then m else v x)) isTrue : Formula > o isTrue := \f. f \in FormulaSet /\ freeVarFormula f = empty /\ interpF (\x. x) f // Statement of essential incompleteness of arithmetic ExtendedEssentialIncompletenessOfRA : o ExtendedEssentialIncompletenessOfRA := forall t : Theory. (t c= FormulaSet /\ RA c= proves t /\ (proves t) \in CESet) => exists g \in FormulaSet. freeVarFormula g = empty /\ ((proves t g \/ proves t (not g)) => proves t = FormulaSet) /\ (~(isTrue g) => proves t = FormulaSet) ________________________________________________________________________________ PrimitiveRecursiveFunctions by Russell O'Connor ________________________________________________________________________________ // We will make use of some object of type Nat that are not in NatSet top : Nat top := \p : (i > o). T bottom : Nat bottom := \p : (i > o). F // Lists of natural numbers are countable, so we code them with natural numbers. // Type Definition ListNat := nat nil : ListNat nil := 0 cons : Nat > ListNat > ListNat cons := \x. \l. 1 + pair x l ListNatSet : ListNat > o ListNatSet := \l. forall p : ListNat > o. (p nil /\ forall n \in NatSet. forall k. p k => p (cons n k)) => p l ListNatR_a : a > (Nat > ListNat > a > a) > ListNat > a ListNatR_a := \n. \c. \r. iota x : a. forall w : ListNat > a > o. (w nil n /\ (forall n \n NatSet. forall l : ListNat. forall y : a. w l y => w (cons n l) (c n l y)) ) => w r x length : ListNat > Nat length := ListNatR_(Nat) 0 (\h. \t. S) // Returns an error, repres[en]ted by bottom, when passed nil head : ListNat > Nat head := if (nil=l) then bottom else iota h : Nat. exists t \in ListNatSet. (cons h t)=l // Returns an error, repres[en]ted by bottom, when passed nil tail : ListNat > ListNat tail := if (nil=l) then bottom else iota t : ListNat. exists h \in NatSet. (cons h t)=l allList : (Nat > o) > ListNat > o allList := \p. ListNatR_o T (\n. \l. \r. p n /\ r) lookup : ListNat > Nat > Nat lookup := ListNatR_(Nat > Nat) (\n. bottom) (\h. \t. \r. \n. R (\m. \z. r m) h) // A type for primitive recursive programs (source code) // The number of primitive recursive programs is countable, so we will represent them with natural numbers. // Type Definition PrimRecProg := Nat // Type Definition ListPrimRecProg := ListNat // the program that takes no input and outputs 0 zeroP : PrimRecProg zeroP := 0 // the program that takes one input and outputs the successor of the input succP : PrimRecProg succP := 1 // the program that takes n inputs and returns the kth input. piP : Nat > Nat > PrimRecProg piP := \n. \k. 2 + 3*(pair n k) // the composition of m programs each taking n inputs and with program taking m inputs to make a program that takes n inputs. composeP : PrimRecProg > ListPrimRecProg > PrimRecProg composeP := \p. \lp. 2 + 3*(pair n lp) + 1 // the combin[a]tion of one program taking n inputs (base case), f, and // a second programming taking n + 2 inputs (recur[s]ive case), g, and // combining them by primitive recursion to make a program, h, that takes n + 1 inputs. // where h(0,x1,x2...xn) = f(x1,x2...xn) and h(S n,x1,x2...xn) = g(n,h(n,x1,x2...xn),x1,x2...xn) primRecP : PrimRecProg > PrimRecProg > PrimRecProg primRecP := \f. \g. 2 + 3*(pair f g) + 2 // Not all programs are well defined. The combinators have to take the programs that have the correct number of parameters and such. // Here we define the set of well formed programs accepting n inputs. primRecProgSet : Nat > PrimRecProg > o primRecProgSet := \n. \p. forall (w : Nat > PrimRecProg > o). (w 0 zeroP /\ w 1 succP /\ (forall n \in NatSet. forall k \in NatSet. k < n. w n (pi n k)) /\ (forall n \in NatSet. forall m \in NatSet. forall q : PrimRecProg. forall qs : ListPrimRecProg. (w m q /\ allList (w n) qs) => w n (composeP q qs)) /\ (forall n \in NatSet. forall f : PrimRecProg. forall g : PrimRecProg. (w n f /\ w (S (S n)) g) => w (S n) (primRecP f g)) ) => w n p //Now we give semantics to primitive recursive programs by writing an interpreter for them. //This inte[r]preter needs to produce functions that take n arguments for various n, but we cannot write this directly in Q0. //We cheat by writing functions that operate on ListNat and expect n elements in the list. //We make note of the arity of the function by returning the arity when passed the value "top" which is of type Nat, but isn't a member of NatSet. interpret : PrimRecProg > ListNat > Nat interpret := \p. \a. if (a = top) then (iota r : Nat. primRecProgSet r p) else (iota r : List > Nat. forall w : PrimRecProg > (List > Nat) > o. (w zeroP (\l. 0) /\ w succP (\l. S (head l)) /\ (forall n \in NatSet. forall k \in NatSet. k < n => w (piP n k) (\l. lookup l k)) /\ (forall n \in NatSet. forall m \in NatSet. forall q \in primRecProgSet m. forall iq : ListNat > Nat. forall qs : ListPrimRecProg. forall iqs : ListNat > ListNat. (forall i \in NatSet. i < length qs => lookup qs i \in primRecProgSet n) => (w q iq /\ (forall i \in NatSet. i < length qs => w (lookup qs i) (\l. lookup (iqs l) i))) => w (composeP q qs) (\l. iq (iqs l))) /\ (forall n \in NatSet. forall f \in primRecProgSet n. forall if : ListNat > Nat. forall g \in primRecProgSet (S (S n)). forall ig : ListNat > Nat. (w f if /\ w g ig) => w (primRecP f g) (\l. R (\n. \z. g (cons n (cons z (tail l)))) (f (tail l)) (head l))) ) => w p r) l // Now we can state what it means for every primitive recursive function to be repre[se]n[ ]table by an arith[ ]metic formula. PRFRepresentable : o PRFRepr[e]sentable : forall n \in NatSet. forall p \in primRecProgSet n. exists f \in FormulaSet. (forall i \in NatSet. i \in freeVarFormula f => i < (S n)) /\ (forall l \in ListNatSet. length l = n => forall y \in NatSet. (proves RA (substituteFormula f (\i. natToTerm (lookup (cons y l) i)))) <=> interpret p l=y) // We can specialize the above general theorem to the case of Primitive Recursive Functions of 2 argume[nt]s PRF2Set : (nat > nat > nat) > o PRF2Set := \f. exists p \in primRecProgSet 2. forall x \in NatSet. forall y \in NatSet. interpret p (cons x (cons y nill)) = f x y. // We can state as a corollary of PRFRepr[e]sentable that every member of PRF2Set is representable by an arith[ ]metic formula. PRF2Representable : o PRF2Representable : forall f \in PRF2Set. exists f \in FormulaSet. (forall i \in NatSet. i \in freeVarFormula f => i < 3) /\ (forall x \in NatSet. forall y \in NatSet. forall z \in NatSet. (proves RA (substituteFormula f (\i. natToTerm (if i=0 then z else if i=1 then x else if i=2 then y else 0)))) <=> f x y=z) ________________________________________________________________________________ IncompletenessOfArithmeticInQ0 by Russell O'Connor ________________________________________________________________________________ // Section: Primitive // 'a' stands for any type Q_a : a > a > o iota : (i > o) > i // Section: Logic // Notation A = B := Q A B // Notation A <=> B := Q_o A B T : o T := Q_o = Q_o F : o F := \x : o. T = \x : o. x // Notation forall x : a. A := (\x : a. T) = (\x : a. A) // Notation A /\ B := (\g : o > o > o. g T T) = (\g : o > o > o. g A B) // Notation A => B := A = (A /\ B) // Notaton ~A := A = F // Notation A \/ B := ~(~A /\ ~B) // Notation exists x : a. A := ~(forall x : a. ~A) // Notation A =/= B := ~(A = B) // Recursive Notation iota x : i. A := iota (\x. A) iota x : o. A := (\x. x) = (\x. A) iota f : a > b. A := \x : a. iota z : b. exists f : a > b. A /\ f x = z //Notation if A then B else C := iota x. (A /\ x = B) \/ (~A /\ x = C) // Section: sets / predicates //Notation A \in B := B A //Notation A \notin B := ~(A \in B) //Notation {A} := Q A //Notation A \intersect B := \x. x \in A /\ x \in B //Notation A \union B := \x. x \in B \/ x \in B //Notation A c= B := \x. x \in A => x \in B //Notation A \ B := A \intersect (\x. x \notin B) //Notation (usually i occurs in A) { A  i < B } := \x. exists i \in B. x = A //Notation forall x \in A. B := forall x. x \in A => B //Notation exists x \in A. B := exists x. x \in A /\ B empty_a : a > o empty_a := \x. F BigUnion_a : ((a > o) > o) > a > o BigUnion_a := \p. \a. exists s \in p. a \in s // Section: Natural numbers. // Type defintion Nat := (i > o) > o 0 : Nat 0 := Q (\x. F) S : Nat > Nat S := \n. \p. exists x. p x /\ n (\y. y =/= x /\ p y) NatSet : Nat > o NatSet := \n. forall p : Nat > o. (p 0 /\ forall m : Nat. p m => p (S m)) => p n R : (Nat > Nat > Nat) > Nat > Nat > Nat R := \h. \g. \n. iota m : Nat. forall w : Nat > Nat > o. (w 0 g /\ forall x : Nat. forall y : Nat. w x y => w (s x) (h x y)) => w n m 1 : Nat 1 := S 0 2 : Nat 2 := S 1 3 : Nat 3 := S 2 4 : Nat 4 := S 3 //Notation A + B := R (\x. S) A B //Notation A * B := R (\x. \y. (A + y)) 0 B triangle : Nat > Nat triangle := R (\x. \y. (S x) + y) 0 pair : Nat > Nat > Nat pair := \n. \m. triangle (n + m) + m //Notation A <= B := exists n \in NatSet . A + n = B //Notation mu n. A := iota n : Nat. n \in NatSet /\ n \in A /\ forall m \in A. n <= m // Section: Syntactic Logic // Type defintion Term := Nat var : Nat > Term var := \n. 1 + 4*n zero : Term zero := 0 succ : Term > Term succ := \t. 1 + 4*t + 1 plus : Term > Term > Term plus := \t. \s. 1 + 4*(pair t s) + 2 mult : Term > Term > Term mult := \t. \s. 1 + 4*(pair t s) + 3 TermSet : Term > o TermSet := \t. forall p : Term > o. ((forall n \in NatSet. p (var n)) /\ p zero /\ (forall t : Term. p t => p (succ t)) (forall t : Term. forall s : Term. (p t /\ p s) => p (plus t s)) /\ (forall t : Term. forall s : Term. (p t /\ p s) => p (mult t s)) ) => p t TermR_a : (Nat > a) > a > (Term > a > a) > (Term > Term > a > a > a) > (Term > Term > a > a > a) > Term > a TermR_a := \v. \z. \c. \p. \m. \r. iota x : a. forall w : Term > a > o. ((forall n \in NatSet. w (var n) (v n)) /\ w zero z /\ (forall t : Term. forall y : a. w t y => w (succ t) (c t y)) /\ (forall t : Term. forall s : Term. forall y : a. forall z : a. (w t y /\ w s z) => w (plus t s) (p t s y z)) /\ (forall t : Term. forall s : Term. forall y : a. forall z : a. (w t y /\ w s z) => w (mult t s) (m t s y z)) ) => w r x freeVarTerm : Term > Nat > o freeVarTerm := TermR_(Nat > o) (\n. {n}) empty (\t. \p. p) (\t. \s. \p. \q. p \union q) (\t. \s. \p. \q. p \union q) subTerm : Term > (Nat > Term) > Term subTerm := \r. \l. TermR_(Term) l zero (\t. succ) (\t. \s. plus) (\t. \s. mult) r at :: Nat > Term > Nat > Term at := \n. \t. \m. if m = n then t else (var m) // Type definition Formula := Nat equal : Term > Term > Formula equal := \t. \s. 1 + 4*(pair t s) falsum : Formula falsum := 0 conj : Formula > Formula > Formula conj := \f. \g. 1 + 4*(pair f g) + 1 impl : Formula > Formula > Formula impl := \f. \g. 1 + 4*(pair f g) + 2 all : Nat > Formula > Formula all := \n. \f. 1 + 4*(pair n f) + 3 FormulaSet : Formula > o FormulaSet := \f. forall p : Formula > o. ((forall t \in Term. forall s \in Term. p (equal t s)) /\ p falsum /\ (forall f : Formula. forall g : Formula. (p f /\ p g) => p (conj f g)) /\ (forall f : Formula. forall g : Formula. (p f /\ p g) => p (impl f g)) /\ (forall n \in NatSet. forall f : Formula. p f => p (all n f)) ) => p f not : Formula > Formula not := \f. impl f falsum disj : Formula > Formula > Formula disj := \f. \g. not (conj (not f) (not g)) iff : Formula > Formula > Formula iff := \f. \g. conj (impl f g) (impl g f) some : Nat > Formula > Formula some := \n. \f. not (all n (not f)) FormulaR_a : (Term > Term > a) > a > (Formula > Formula > a > a > a) > (Formula > Formula > a > a > a) > (Formula > Nat > a > a) > Formula > a FormulaR_a := \e. \m. \c. \i. \l. \r. iota x : a. forall w : Formula > a > o. ((forall t \in TermSet. forall s \in TermSet. w (equal t s)) /\ w falsum m /\ (forall f : Formula. forall g : Formula. forall y : a. forall z : a. (w f y /\ w g z) => w (conj f g) (c f g y z)) /\ (forall f : Formula. forall g : Formula. forall y : a. forall z : a. (w f y /\ w g z) => w (impl f g) (i f g y z)) /\ (forall n \in NatSet. forall f : Formula. forall y : a. w f y => w (all n f) (l f n y)) ) => w r x freeVarFormula : Formula > Nat > o freeVarFormula := FormulaR_(Nat > o) (\t. \s. freeVarTerm t \union freeVarTerm s) empty (\f. \g. \p. \q. p \union q) (\f. \g. \p. \q. p \union q) (\f. \n. \p. p \ {n}) fresh : (Nat > o) > Nat fresh := \p. mu x. ~p x subFormula : Formula > (Nat > Term) > Formula subFormula := FormulaR_((Nat > Term) > Formula) (\t. \s. \l. equal (subTerm t l) (subTerm s l)) (\l. falsum) (\f. \g. \r. \s. \l. conj (r l) (s l)) (\f. \g. \r. \s. \l. impl (r l) (s l)) (\f. \n. \r. \l. (\z. all z (r (\m. if m = n then var z else l m))) (fresh (BigUnion {freeVarTerm (l i)  i < freeVarFormula f}))) // Type definition Theory := Formula > o // Close a set of formulas under universal generalization. gen :: (Formula > o) > Theory gen := \q. \f. forall p : Formula > o. (q c= p /\ (forall n \in NatSet. forall g : Formula. p g => p (all n g))) => p f // Logical Axioms for syntactic formulas LA : Theory LA := gen (\f. (exists a \in FormulaSet. exists b \in FormulaSet. f = impl a (impl b a)) \/ (exists a \in FormulaSet. exists b \in FormulaSet. exists c \in FormulaSet. f = impl (impl a (impl b c)) (impl (impl a b) (impl a c))) \/ (exists a \in FormulaSet. exists b \in FormulaSet. f = impl (conj a b) a) \/ (exists a \in FormulaSet. exists b \in FormulaSet. f = impl (conj a b) b) \/ (exists a \in FormulaSet. exists b \in FormulaSet. f = impl a (impl b (conj a b))) \/ (exists a \in FormulaSet. f = impl falsum a) \/ (exists a \in FormulaSet. exists b \in FormulaSet. f = impl (impl (impl a b) a) a) \/ (exists n \in NatSet. exists. a \in FormulaSet. exists t \in TermSet. f = impl (all n a) (subFormula a (at n t))) \/ (exists n \in NatSet. exists. a \in FormulaSet. exists b \in FormulaSet. f = impl (all n (impl a b)) (impl (all n a) (all n b))) \/ (exists n \in NatSet. exists. a \in FormulaSet. n \notin freeVarFormula a /\ f = impl a (all n a)) \/ (exists n \in NatSet. f = equal (var n) (var n)) \/ (exists n \in NatSet. exists m \in NatSet. exists z \in NatSet. exists a \in FormulaSet. f = impl (equal (var n) (var m)) (impl (subFormula a (at z (var n))) (subFormula a (at z (var m)))))) // Close a set of formulas under modus ponens proves : Theory > Formula > o proves := \t. \f. forall p : Formula > o. (t c= p /\ LA c= p /\ (forall f : Formula. forall g : Formula. (p f /\ p (impl f g)) => p g)) => p f // Section Goedel // Axioms of Robinson Arithmetic RA : Theory RA := \f. f = all 0 (not (equal (succ (var 0)) zero)) \/ f = all 0 (all 1 (impl (equal (succ (var 0)) (succ (var 1))) (equal (var 0) (var 1)))) \/ f = all 0 (or (equal (var 0) zero) (some 1 (equal (var 0) (succ (var 1))))) f = all 0 (equal (plus (var 0) zero) (var 0)) \/ f = all 0 (all 1 (equal (plus (var 0) (succ (var 1))) (succ (plus (var 0) (var 1))))) \/ f = all 0 (equal (mult (var 0) zero) zero) \/ f = all 0 (all 1 (equal (mult (var 0) (succ (var 1))) (plus (mult (var 0) (var 1)) (var 0)))) natToTerm : Nat > Term natToTerm := R (\x. succ) zero codeTerm : Term > Nat codeTerm : TermR_(Nat) (\n. 1 + 4*n) 0 (\t. \n. 1 + 4*n + 1) (\t. \s. \n. \m. 1 + 4*(pair n m) + 2) (\t. \s. \n. \m. 1 + 4*(pair n m) + 3) codeFormula : Formula > Nat codeFormula : FormulaR_(Nat) (\t. \s. 1 + 4*(pair (codeTerm t) (codeTerm s))) 0 (\f. \g. \n. \m. 1 + 4*(pair n m) + 1) (\f. \g. \n. \m. 1 + 4*(pair n m) + 2) (\f. \n. \m. 1 + 4*(pair n m) + 3) quotF : Formula > Term quotF := \f. natToTerm (codeFormula f) expressableF : (Formula > o) > Theory > o expressableF := \p. \t. exists n \in NatSet. exists f \in FormulaSet. {n} = freeVarFormula f /\ (forall m \in p => proves t (subFormula f (at n (quotF m)))) /\ (forall m \in Formula. m \notin p => proves t (not (subFormula f (at n (quotF m))))) // Statement of the diagona[l] lemma: https://en.wikipedia.org/wiki/Diagonal_lemma diagonal_lemma : o diagonal_lemma := forall t : Theory. (t c= FormulaSet /\ RA c= proves t) => forall n \in natSet. forall f \in FormulaSet. exists g \in FormulaSet. freeVarFormula g = freeVarFormula f \ {n} /\ (proves t (iff g (subFormula f (at n (quotF g))))) // Statement of essential incompleteness of (Robins[ ]on) arithmetic EssentialIncompletenessOfRA : o EssentialIncompletenessOfRA := forall t : Theory. (t c= FormulaSet /\ RA c= proves t /\ expressibleF t t) => exists g \in FormulaSet. freeVarFormula g = empty /\ ((proves t g \/ proves t (not g)) => proves t = FormulaSet) ________________________________________________________________________________ 
From: Heiko Becker <s9hhbeck@st...>  20160706 09:45:17

Hello Petros and Marco, thank you for your replies. With your help I was able to finish the subgoal. Regards, Heiko On 07/05/2016 04:59 PM, Petros Papapanagiotou wrote: > Hello Keiko, > > > On 05/07/2016 11:02, Heiko Becker wrote: >> The script I used is: >> >> e (ONCE_REWRITE_TAC[eval_exp_CASES]);; >> e (INTRO_TAC "!eps env v val; cases");; >> e (REMOVE_THEN "cases" (DESTRUCT_TAC "var  const  bin"));; >> (* Var case *) >> e (REMOVE_THEN "var" (DESTRUCT_TAC "@v2. var_eq val_eq"));; >> e (SUBGOAL_TAC "v_eq_v2" `v = v2` [REMOVE_THEN "var_eq" (MP_TAC) THEN >> ONCE_REWRITE_TAC[injectivity "exp"]]);; >> e (DISCH_TAC);; >> e (EXPAND_TAC "v2");; >> e (ONCE_REWRITE_TAC[ASSUME `v = v2`]); >> >> Since the last two tactics do not change the goal in any way my >> questions in this case are: >> >> 1) How can I use the assumption 1 and rewrite it inside my goal? > > Do you mean to rewrite the assumption itself or use the assumption to > rewrite the goal? > The former can be accomplished with RULE_ASSUM_TAC (REWRITE_RULE > [...]). This will rewrite all assumptions (there are more complicated > ways that allow more control). > For the latter you can use ASM_REWRITE_TAC. For simple variable > substitutions you can also use FIRST_X_ASSUM SUBST1_TAC. > > >> 2) Is there an easier way of closing the proof, since I already derived >> the goal I have? > > The problem is in your SUBGOAL_TAC step. When you introduce the > subgoal `v = v2`, HOL Light does not know the context of v and v2 so > it assigns them variable types. The resulting subgoal is unprovable. > Instead you can use: > > e(SUBGOAL_TAC "v_eq_v2" `v:num = v2` [... > > (The answer to your 3rd question may help with such problems in the > future.) > > There is a number of other ways to deal with this proof. For example: > > e (RULE_ASSUM_TAC (REWRITE_RULE[injectivity "exp"]) THEN > ASM_REWRITE_TAC[]);; > > > >> 3) (A little unrelated) Can I make HOLLight annotate all terms in my >> goal with their derived type? >> > > This snippet* has come in handy in numerous occasions: > > let print_varandtype fmt tm = > let hop,args = strip_comb tm in > let s = name_of hop > and ty = type_of hop in > if is_var hop & args = [] then > (pp_print_string fmt "("; > pp_print_string fmt s; > pp_print_string fmt ":"; > pp_print_type fmt ty; > pp_print_string fmt ")") > else fail() ;; > > let show_types,hide_types = > (fun () > install_user_printer ("Show Types",print_varandtype)), > (fun () > try delete_user_printer "Show Types" > with Failure _ > failwith ("hide_types: "^ > "Types are already hidden."));; > > * Slightly modified from original source: > https://code.google.com/archive/p/flyspeck/wikis/TipsAndTricks.wiki#Investigating_Types > > Use "show_types();;" to make HOL Light print out the types of all > variables. > Use "hide_types();;" to restore the original behaviour. > > Hope this helps. > > Regards, > Petros > > > >> >>  >> >> let binop_IND, binop_REC = define_type >> "binop = Plus  Sub  Mult  Div ";; >> (* >> Define an evaluation function for binary operators. >> *) >> let eval_binop = new_recursive_definition binop_REC >> `(eval_binop Plus v1 v2 = v1 + v2) /\ >> (eval_binop Sub v1 v2 = v1  v2) /\ >> (eval_binop Mult v1 v2 = v1 * v2) /\ >> (eval_binop Div v1 v2 = v1 / v2)`;; >> >> let exp_IND, exp_REC= define_type >> "exp = Var num >>  Const V >>  Binop binop exp exp";; >> >> let perturb = define `(perturb:real>real>real) = \r e. r * ((&1) + >> e)`;; >> new_type_abbrev ("env_ty",`:num>real`);; >> >> let eval_exp_RULES, eval_exp_IND, eval_exp_CASES = >> new_inductive_definition >> `(!eps env v. >> eval_exp eps env (Var v) (env v)) /\ >> (!eps env n delta. >> abs delta <= eps ==> >> eval_exp eps env (Const n) (perturb n delta)) /\ >> (!eps env b e1 e2 v1 v2 delta. >> eval_exp eps env e1 v1 /\ >> eval_exp eps env e2 v2 /\ >> abs delta <= eps ==> >> eval_exp eps env (Binop b e1 e2) (perturb (eval_binop b v1 v2) >> delta))`;; >> >> >>  >> >> Attend Shape: An AT&T Tech Expo July 1516. Meet us at AT&T Park in San >> Francisco, CA to explore cuttingedge tech and listen to tech luminaries >> present their vision of the future. This family event has something for >> everyone, including kids. Get more information and register today. >> http://sdm.link/attshape >> _______________________________________________ >> holinfo mailing list >> holinfo@... >> https://lists.sourceforge.net/lists/listinfo/holinfo >> > 
From: Marco Maggesi <maggesi@ma...>  20160705 15:04:25

Dear Heiko, I see two main problem in your proof: 1. When you open the subgoal, you have to be sure about the types of your terms. I.e., here you have to add the annotation :num beside v or v2: e (SUBGOAL_TAC "v_eq_v2" `v:num = v2` [REMOVE_THEN "var_eq" (MP_TAC) THEN ONCE_REWRITE_TAC[injectivity "exp"]]);; 2. About your proof strategy, you surely want to make use of injectivity and distinctness of constructors. This is what I would do in this case: g `!eps env v val. eval_exp eps env (Var v) val ==> val = env v`;; e (REPEAT GEN_TAC);; e (ONCE_REWRITE_TAC[eval_exp_CASES]);; (* Use distinctness of constructors. *) e (REWRITE_TAC[distinctness "exp"]);; (* Use injectivity of constructors. *) e (REWRITE_TAC[injectivity "exp"]);; (* Now you can easy conclude with MESON_TAC, or, if you wish, with. *) e (DISCH_THEN STRUCT_CASES_TAC);; e REFL_TAC;; Marco 20160705 12:02 GMT+02:00 Heiko Becker <s9hhbeck@...>: > Hello everyone, > > I have another question on HOLLight. This time I am stuck with some > rewriting in a proof. > > I have defined an inductive type and want to prove an "inversion" lemma > for it: > > g `!eps env v val. > eval_exp eps env (Var v) val ==> val = env v`;; > > I have been able to do the proof until I arrive at a subgoal which I > think is easy to proof but I cannot find the appropriate tactic to do it: > > val it : xgoalstack = 1 subgoal (4 total) > > 0 [`val = env v2`] (val_eq) > 1 [`v = v2`] > > `v = v2` > > The script I used is: > > e (ONCE_REWRITE_TAC[eval_exp_CASES]);; > e (INTRO_TAC "!eps env v val; cases");; > e (REMOVE_THEN "cases" (DESTRUCT_TAC "var  const  bin"));; > (* Var case *) > e (REMOVE_THEN "var" (DESTRUCT_TAC "@v2. var_eq val_eq"));; > e (SUBGOAL_TAC "v_eq_v2" `v = v2` [REMOVE_THEN "var_eq" (MP_TAC) THEN > ONCE_REWRITE_TAC[injectivity "exp"]]);; > e (DISCH_TAC);; > e (EXPAND_TAC "v2");; > e (ONCE_REWRITE_TAC[ASSUME `v = v2`]); > > Since the last two tactics do not change the goal in any way my > questions in this case are: > > 1) How can I use the assumption 1 and rewrite it inside my goal? > > 2) Is there an easier way of closing the proof, since I already derived > the goal I have? > > 3) (A little unrelated) Can I make HOLLight annotate all terms in my > goal with their derived type? > > I have added my formalization below. > > > Thank you (once again) in advance. > > Best regards, > > Heiko > > >  > > let binop_IND, binop_REC = define_type > "binop = Plus  Sub  Mult  Div ";; > (* > Define an evaluation function for binary operators. > *) > let eval_binop = new_recursive_definition binop_REC > `(eval_binop Plus v1 v2 = v1 + v2) /\ > (eval_binop Sub v1 v2 = v1  v2) /\ > (eval_binop Mult v1 v2 = v1 * v2) /\ > (eval_binop Div v1 v2 = v1 / v2)`;; > > let exp_IND, exp_REC= define_type > "exp = Var num >  Const V >  Binop binop exp exp";; > > let perturb = define `(perturb:real>real>real) = \r e. r * ((&1) + e)`;; > new_type_abbrev ("env_ty",`:num>real`);; > > let eval_exp_RULES, eval_exp_IND, eval_exp_CASES = new_inductive_definition > `(!eps env v. > eval_exp eps env (Var v) (env v)) /\ > (!eps env n delta. > abs delta <= eps ==> > eval_exp eps env (Const n) (perturb n delta)) /\ > (!eps env b e1 e2 v1 v2 delta. > eval_exp eps env e1 v1 /\ > eval_exp eps env e2 v2 /\ > abs delta <= eps ==> > eval_exp eps env (Binop b e1 e2) (perturb (eval_binop b v1 v2) > delta))`;; > > > >  > Attend Shape: An AT&T Tech Expo July 1516. Meet us at AT&T Park in San > Francisco, CA to explore cuttingedge tech and listen to tech luminaries > present their vision of the future. This family event has something for > everyone, including kids. Get more information and register today. > http://sdm.link/attshape > _______________________________________________ > holinfo mailing list > holinfo@... > https://lists.sourceforge.net/lists/listinfo/holinfo > 
From: Petros Papapanagiotou <pe.p@ed...>  20160705 14:59:44

Hello Keiko, On 05/07/2016 11:02, Heiko Becker wrote: > The script I used is: > > e (ONCE_REWRITE_TAC[eval_exp_CASES]);; > e (INTRO_TAC "!eps env v val; cases");; > e (REMOVE_THEN "cases" (DESTRUCT_TAC "var  const  bin"));; > (* Var case *) > e (REMOVE_THEN "var" (DESTRUCT_TAC "@v2. var_eq val_eq"));; > e (SUBGOAL_TAC "v_eq_v2" `v = v2` [REMOVE_THEN "var_eq" (MP_TAC) THEN > ONCE_REWRITE_TAC[injectivity "exp"]]);; > e (DISCH_TAC);; > e (EXPAND_TAC "v2");; > e (ONCE_REWRITE_TAC[ASSUME `v = v2`]); > > Since the last two tactics do not change the goal in any way my > questions in this case are: > > 1) How can I use the assumption 1 and rewrite it inside my goal? Do you mean to rewrite the assumption itself or use the assumption to rewrite the goal? The former can be accomplished with RULE_ASSUM_TAC (REWRITE_RULE [...]). This will rewrite all assumptions (there are more complicated ways that allow more control). For the latter you can use ASM_REWRITE_TAC. For simple variable substitutions you can also use FIRST_X_ASSUM SUBST1_TAC. > 2) Is there an easier way of closing the proof, since I already derived > the goal I have? The problem is in your SUBGOAL_TAC step. When you introduce the subgoal `v = v2`, HOL Light does not know the context of v and v2 so it assigns them variable types. The resulting subgoal is unprovable. Instead you can use: e(SUBGOAL_TAC "v_eq_v2" `v:num = v2` [... (The answer to your 3rd question may help with such problems in the future.) There is a number of other ways to deal with this proof. For example: e (RULE_ASSUM_TAC (REWRITE_RULE[injectivity "exp"]) THEN ASM_REWRITE_TAC[]);; > 3) (A little unrelated) Can I make HOLLight annotate all terms in my > goal with their derived type? > This snippet* has come in handy in numerous occasions: let print_varandtype fmt tm = let hop,args = strip_comb tm in let s = name_of hop and ty = type_of hop in if is_var hop & args = [] then (pp_print_string fmt "("; pp_print_string fmt s; pp_print_string fmt ":"; pp_print_type fmt ty; pp_print_string fmt ")") else fail() ;; let show_types,hide_types = (fun () > install_user_printer ("Show Types",print_varandtype)), (fun () > try delete_user_printer "Show Types" with Failure _ > failwith ("hide_types: "^ "Types are already hidden."));; * Slightly modified from original source: https://code.google.com/archive/p/flyspeck/wikis/TipsAndTricks.wiki#Investigating_Types Use "show_types();;" to make HOL Light print out the types of all variables. Use "hide_types();;" to restore the original behaviour. Hope this helps. Regards, Petros > >  > > let binop_IND, binop_REC = define_type > "binop = Plus  Sub  Mult  Div ";; > (* > Define an evaluation function for binary operators. > *) > let eval_binop = new_recursive_definition binop_REC > `(eval_binop Plus v1 v2 = v1 + v2) /\ > (eval_binop Sub v1 v2 = v1  v2) /\ > (eval_binop Mult v1 v2 = v1 * v2) /\ > (eval_binop Div v1 v2 = v1 / v2)`;; > > let exp_IND, exp_REC= define_type > "exp = Var num >  Const V >  Binop binop exp exp";; > > let perturb = define `(perturb:real>real>real) = \r e. r * ((&1) + e)`;; > new_type_abbrev ("env_ty",`:num>real`);; > > let eval_exp_RULES, eval_exp_IND, eval_exp_CASES = new_inductive_definition > `(!eps env v. > eval_exp eps env (Var v) (env v)) /\ > (!eps env n delta. > abs delta <= eps ==> > eval_exp eps env (Const n) (perturb n delta)) /\ > (!eps env b e1 e2 v1 v2 delta. > eval_exp eps env e1 v1 /\ > eval_exp eps env e2 v2 /\ > abs delta <= eps ==> > eval_exp eps env (Binop b e1 e2) (perturb (eval_binop b v1 v2) > delta))`;; > > >  > Attend Shape: An AT&T Tech Expo July 1516. Meet us at AT&T Park in San > Francisco, CA to explore cuttingedge tech and listen to tech luminaries > present their vision of the future. This family event has something for > everyone, including kids. Get more information and register today. > http://sdm.link/attshape > _______________________________________________ > holinfo mailing list > holinfo@... > https://lists.sourceforge.net/lists/listinfo/holinfo >  Petros Papapanagiotou, Ph.D. CISA, School of Informatics The University of Edinburgh Email: pe.p@...  The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. 
From: Heiko Becker <s9hhbeck@st...>  20160705 10:04:50

Hello everyone, I have another question on HOLLight. This time I am stuck with some rewriting in a proof. I have defined an inductive type and want to prove an "inversion" lemma for it: g `!eps env v val. eval_exp eps env (Var v) val ==> val = env v`;; I have been able to do the proof until I arrive at a subgoal which I think is easy to proof but I cannot find the appropriate tactic to do it: val it : xgoalstack = 1 subgoal (4 total) 0 [`val = env v2`] (val_eq) 1 [`v = v2`] `v = v2` The script I used is: e (ONCE_REWRITE_TAC[eval_exp_CASES]);; e (INTRO_TAC "!eps env v val; cases");; e (REMOVE_THEN "cases" (DESTRUCT_TAC "var  const  bin"));; (* Var case *) e (REMOVE_THEN "var" (DESTRUCT_TAC "@v2. var_eq val_eq"));; e (SUBGOAL_TAC "v_eq_v2" `v = v2` [REMOVE_THEN "var_eq" (MP_TAC) THEN ONCE_REWRITE_TAC[injectivity "exp"]]);; e (DISCH_TAC);; e (EXPAND_TAC "v2");; e (ONCE_REWRITE_TAC[ASSUME `v = v2`]); Since the last two tactics do not change the goal in any way my questions in this case are: 1) How can I use the assumption 1 and rewrite it inside my goal? 2) Is there an easier way of closing the proof, since I already derived the goal I have? 3) (A little unrelated) Can I make HOLLight annotate all terms in my goal with their derived type? I have added my formalization below. Thank you (once again) in advance. Best regards, Heiko  let binop_IND, binop_REC = define_type "binop = Plus  Sub  Mult  Div ";; (* Define an evaluation function for binary operators. *) let eval_binop = new_recursive_definition binop_REC `(eval_binop Plus v1 v2 = v1 + v2) /\ (eval_binop Sub v1 v2 = v1  v2) /\ (eval_binop Mult v1 v2 = v1 * v2) /\ (eval_binop Div v1 v2 = v1 / v2)`;; let exp_IND, exp_REC= define_type "exp = Var num  Const V  Binop binop exp exp";; let perturb = define `(perturb:real>real>real) = \r e. r * ((&1) + e)`;; new_type_abbrev ("env_ty",`:num>real`);; let eval_exp_RULES, eval_exp_IND, eval_exp_CASES = new_inductive_definition `(!eps env v. eval_exp eps env (Var v) (env v)) /\ (!eps env n delta. abs delta <= eps ==> eval_exp eps env (Const n) (perturb n delta)) /\ (!eps env b e1 e2 v1 v2 delta. eval_exp eps env e1 v1 /\ eval_exp eps env e2 v2 /\ abs delta <= eps ==> eval_exp eps env (Binop b e1 e2) (perturb (eval_binop b v1 v2) delta))`;; 
From: Heiko Becker <s9hhbeck@st...>  20160704 14:45:16

Hello Petros, thank you for your fast answer. Your tactic worked perfectly. Regards, Heiko On 07/04/2016 03:20 PM, Petros Papapanagiotou wrote: > Hello Heiko, > > Try: > e (REWRITE_TAC[distinctness "test"]);; > > HOL Light automatically produces distinctness theorems for inductive > types, accessed through the "distinctness" function. > > > Regards, > Petros > > > On 04/07/2016 13:36, Heiko Becker wrote: >> On 07/04/2016 02:34 PM, Heiko Becker wrote: >> >>> Hello everyone, >>> >>> >>> suppose I have an inductive type as follows: >>> >>> let test_IND, test_CASES = >>> define_type >>> "test = Foo num >>> Bar int ";; >>> >>> Can someone explain to me how I can derive a contradiction given >>> equality as in the goal below? >>> >>> g `Foo 1 = Bar (&1) ==> F`;; >>> >>> Thanks in advance. >>> >>> Best regards, >>> >>> >>> Heiko >>> >> Forgot to add: >> I want to do the proof in HOLLight. Sorry the double post. >> >> Best regards. >> >>  >> >> Attend Shape: An AT&T Tech Expo July 1516. Meet us at AT&T Park in San >> Francisco, CA to explore cuttingedge tech and listen to tech luminaries >> present their vision of the future. This family event has something for >> everyone, including kids. Get more information and register today. >> http://sdm.link/attshape >> _______________________________________________ >> holinfo mailing list >> holinfo@... >> https://lists.sourceforge.net/lists/listinfo/holinfo >> > 
From: Petros Papapanagiotou <pe.p@ed...>  20160704 13:20:40

Hello Heiko, Try: e (REWRITE_TAC[distinctness "test"]);; HOL Light automatically produces distinctness theorems for inductive types, accessed through the "distinctness" function. Regards, Petros On 04/07/2016 13:36, Heiko Becker wrote: > On 07/04/2016 02:34 PM, Heiko Becker wrote: > >> Hello everyone, >> >> >> suppose I have an inductive type as follows: >> >> let test_IND, test_CASES = >> define_type >> "test = Foo num >> Bar int ";; >> >> Can someone explain to me how I can derive a contradiction given >> equality as in the goal below? >> >> g `Foo 1 = Bar (&1) ==> F`;; >> >> Thanks in advance. >> >> Best regards, >> >> >> Heiko >> > Forgot to add: > I want to do the proof in HOLLight. Sorry the double post. > > Best regards. > >  > Attend Shape: An AT&T Tech Expo July 1516. Meet us at AT&T Park in San > Francisco, CA to explore cuttingedge tech and listen to tech luminaries > present their vision of the future. This family event has something for > everyone, including kids. Get more information and register today. > http://sdm.link/attshape > _______________________________________________ > holinfo mailing list > holinfo@... > https://lists.sourceforge.net/lists/listinfo/holinfo >  Petros Papapanagiotou, Ph.D. CISA, School of Informatics The University of Edinburgh Email: pe.p@...  The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. 
From: Heiko Becker <s9hhbeck@st...>  20160704 12:38:36

On 07/04/2016 02:34 PM, Heiko Becker wrote: > Hello everyone, > > > suppose I have an inductive type as follows: > > let test_IND, test_CASES = > define_type > "test = Foo num > Bar int ";; > > Can someone explain to me how I can derive a contradiction given > equality as in the goal below? > > g `Foo 1 = Bar (&1) ==> F`;; > > Thanks in advance. > > Best regards, > > > Heiko > Forgot to add: I want to do the proof in HOLLight. Sorry the double post. Best regards. 
From: Heiko Becker <s9hhbeck@st...>  20160704 12:36:39

Hello everyone, suppose I have an inductive type as follows: let test_IND, test_CASES = define_type "test = Foo num Bar int ";; Can someone explain to me how I can derive a contradiction given equality as in the goal below? g `Foo 1 = Bar (&1) ==> F`;; Thanks in advance. Best regards, Heiko 
From: Mark Adams <mark@pr...>  20160704 00:28:44

Hello Abid, The term quotation fails type checking simply because the types of LHS and RHS of the equality are different: `:real^((N,P)finite_sum,Q)finite_sum^M` (with type vars N, P, Q, M) `:real^(N,(P,Q)finite_sum)finite_sum^M` (with type vars N, P, Q, M) As I understand it (I may be wrong here), there is no way of getting the HOL type system to let you express this associativity property about 'horz_conct1'. If you want to express these kinds of properties, I think you need to define your function in a different way, not using types like this. Mark. On 02/07/2016 10:30, Abid Rauf wrote: > Dear All, > > I am having the following type checking issue with a definition in the Matrix theory of HOLLight. It seems the double application of the function leads to an unknown dimension of the matrix, which is causing the problem. I would appreciate if someone can please help me out with us. > > let horz_conct1 = new_definition > `(horz_conct1:real^N^M>real^P^M>real^((N,P)finite_sum)^M) A B = lambda a b . > if (b<=dimindex(:N)) > then (A$a$b) else (B$a$(b(dimindex(:N))))`;; > > Now if i want to prove that > > g`!(A:real^N^M) (B:real^P^M) (C:real^Q^M). horz_conct1 (horz_conct1 A B) (C)= horz_conct1 (A) (horz_conct1 B C)`;; > > it gives following error > > Exception: Failure "typechecking error (initial type assignment)". > > So the definition is accepted but the proof goal using the function gives the problem. > > Best Regards, > > Abid Rauf > Ph.D Scholar (CS) & RA SAVe Labs, > School of Electrical Engineering and Computer Science (SEECS), > National University of Science and Technology (NUST), H12, Islamabad, Pakistan >  > Attend Shape: An AT&T Tech Expo July 1516. Meet us at AT&T Park in San > Francisco, CA to explore cuttingedge tech and listen to tech luminaries > present their vision of the future. This family event has something for > everyone, including kids. Get more information and register today. > http://sdm.link/attshape > _______________________________________________ > holinfo mailing list > holinfo@... > https://lists.sourceforge.net/lists/listinfo/holinfo 
From: John Harrison <John.H<arrison@cl...>  20160702 16:09:08

Hi Abid,  I was going through the theory and found finite_sum, which is the addition  of dimensions, but here i need product or multiplication of dimensions. Can  anyone help me out please. I think the following should work  I should probably add it to the system as it might be useful for others too. let finite_prod_tybij = let th = prove (`?x. x IN 1..(dimindex(:A) * dimindex(:B))`, EXISTS_TAC `1` THEN REWRITE_TAC[IN_NUMSEG; LE_REFL] THEN MESON_TAC[LE_1; DIMINDEX_GE_1; MULT_EQ_0]) in new_type_definition "finite_prod" ("mk_finite_prod","dest_finite_prod") th;; let FINITE_PROD_IMAGE = prove (`UNIV:(A,B)finite_prod>bool = IMAGE mk_finite_prod (1..(dimindex(:A)*dimindex(:B)))`, REWRITE_TAC[EXTENSION; IN_UNIV; IN_IMAGE] THEN MESON_TAC[finite_prod_tybij]);; let DIMINDEX_HAS_SIZE_FINITE_PROD = prove (`(UNIV:(M,N)finite_prod>bool) HAS_SIZE (dimindex(:M) * dimindex(:N))`, SIMP_TAC[FINITE_PROD_IMAGE] THEN MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN ONCE_REWRITE_TAC[DIMINDEX_UNIV] THEN REWRITE_TAC[HAS_SIZE_NUMSEG_1] THEN MESON_TAC[finite_prod_tybij]);; let DIMINDEX_FINITE_PROD = prove (`dimindex(:(M,N)finite_prod) = dimindex(:M) * dimindex(:N)`, GEN_REWRITE_TAC LAND_CONV [dimindex] THEN REWRITE_TAC[REWRITE_RULE[HAS_SIZE] DIMINDEX_HAS_SIZE_FINITE_PROD]);; John. 
From: Abid Rauf <abid.rauf@se...>  20160702 09:30:57

Dear All, I am having the following type checking issue with a definition in the Matrix theory of HOLLight. It seems the double application of the function leads to an unknown dimension of the matrix, which is causing the problem. I would appreciate if someone can please help me out with us. let horz_conct1 = new_definition `(horz_conct1:real^N^M>real^P^M>real^((N,P)finite_sum)^M) A B = lambda a b . if (b<=dimindex(:N)) then (A$a$b) else (B$a$(b(dimindex(:N))))`;; Now if i want to prove that g`!(A:real^N^M) (B:real^P^M) (C:real^Q^M). horz_conct1 (horz_conct1 A B) (C)= horz_conct1 (A) (horz_conct1 B C)`;; it gives following error Exception: Failure "typechecking error (initial type assignment)". So the definition is accepted but the proof goal using the function gives the problem. Best Regards, Abid Rauf Ph.D Scholar (CS) & RA SAVe Labs, School of Electrical Engineering and Computer Science (SEECS), National University of Science and Technology (NUST), H12, Islamabad, Pakistan 
From: Stephan Merz <stephan.merz@lo...>  20160701 14:03:05

Dear colleagues, the VTSA summer school may be of interest to the interactive theorem proving community. Also note that it takes place in the week following ITP 2016, and that Liège, Belgium, is easily reached from Nancy, France. I would be most obliged if you could pass on this announcement to interested students and colleagues. Best regards, Stephan Merz ====================================================== Summer School on Verification Technology, Systems & Applications http://www.mpiinf.mpg.de/vtsa16/ The 9th edition of the Summer School on Verification Technology, Systems and Applications (VTSA) will be organized by the University of Liège, in cooperation with Inria Nancy  Grand Est, MaxPlanckInstitut für Informatik Saarbrücken, Université du Luxembourg, and Universität KoblenzLandau. The school will take place from August 29th to September 2nd, 2016 at the Montefiore Institute in Liège, Belgium. The following speakers have accepted to give courses at VTSA 2016:  Hubert Comon: Communication security: Formal models and proofs  Thomas Eiter: Answer set programming and extensions  Jean Krivine: Executable knowledge representation in systems biology: The rulebased approach  Tobias Nipkow: Introduction to interactive proof with Isabelle/HOL  Ruzica Piskac: SMTbased verification of heapmanipulating Programs Participation is free (except for travel and accommodation costs) and open to anybody holding at least a bachelor degree or equivalent in computer science; it includes the lectures, daily coffee and lunchbreaks, and a school dinner. Attendance is limited to 40 participants. Please apply electronically by sending to vtsa16@...:  a onepage CV,  an application letter explaining your interest in the school and your experience in the area,  a copy of your bachelor certificate (or equivalent or a more significant certificate). The deadline for application is July 12th, 2016. Notification of acceptance will be given by July 15th, 2016. Full details are available at http://www.mpiinf.mpg.de/vtsa16/ 
From: Abid Rauf <abid.rauf@se...>  20160701 06:45:38

Dear All, I have a Query about Matrices. Can i write a definition in HOL light which takes two matrices of dimensions real^N^M and real^Q^P and after a certain operation output a vector with dimension real^(N*Q)^(M*P). I was going through the theory and found finite_sum, which is the addition of dimensions, but here i need product or multiplication of dimensions. Can anyone help me out please. Best Regards, Abid Rauf Ph.D Scholar (CS) & RA SAVe Labs, School of Electrical Engineering and Computer Science (SEECS), National University of Science and Technology (NUST), H12, Islamabad, Pakistan 
From: Ramana Kumar <Ramana.K<umar@cl...>  20160630 13:17:40

Hi Ada, It still looks like you might be mixing up ML and HOL. Are you trying to define an ML function, or a HOL function? In ML, the conjunction of two Boolean expressions can be formed using the "andalso" operator. Now, maybe you already defined /\ like this, and gave it infix status: infix /\; fun op /\ (a, b) = a andalso b; Then I would expect your definition to work. But please note that this is a definition in ML. If you want to make a definition in HOL, use Define. For example: val ccdd_def = Define`ccdd a b c d = if ((a = b) /\ (c = d)) then T else F`; Cheers, Ramana On 30 June 2016 at 22:51, Ada <956066427@...> wrote: > Hi,guys > I am working with HOL4. > I defined a function in HOL4,like following >  fun ccdd a b c d = if ((a = b) /\ (c = d)) then true else false; > It responded that: > ! Toplevel input: > ! fun ccdd a b c d = if ((a = b) /\ (c = d)) then true else false; > ! ^^^^^^^ > ! Type clash: expression of type > ! bool > ! cannot have type > ! 'a > 'b > I can't understand it. > Who know the reason? > Thanks! > > >  > Attend Shape: An AT&T Tech Expo July 1516. Meet us at AT&T Park in San > Francisco, CA to explore cuttingedge tech and listen to tech luminaries > present their vision of the future. This family event has something for > everyone, including kids. Get more information and register today. > http://sdm.link/attshape > _______________________________________________ > holinfo mailing list > holinfo@... > https://lists.sourceforge.net/lists/listinfo/holinfo > > 