online course in combined logic coming up - late summer

[Mark Tarver]

I'm now completing a new online course designed to introduce logic and much of discrete maths in a new way.  If you've battled a bit with Shen and sequent calculus, then you might enjoy this course because it teaches logic through sequent calculus and should make you more confident in using it. The course is quite unique in its kind, because it focuses on logic at the intersection of three important disciplines - philosophy, mathematics and computer science and shows the connections to logic in all three areas.  

So if you are a student in one of these areas, you'll learn a lot of the topology of the subject and how these areas link together. The course is derived from my discrete maths course at Stony Brook.  There is an accompanying text Logic, Proof and Computation 2nd edition  (extensively revised from a version I bashed out in one month years ago) coming out - priced between £10-15 for those who want it.  

The topics covered include formal language theory, truth-tables, propositional and first-order logic, identity and Boolean algebra dealt from within sequent based reasoning.   All the proofs are driven by a provedit! program written in Shen (no pen and paper needed). The formalisation taught actually reflects the reasoning needed to tackle more advanced proofs in mathematics and I discuss the use of indirect proof, how to pose lemmas, how to prune dead assumptions, discriminating safe inference rules from unsafe ones and recognising dead ends which need to be abandoned.   

In computing, the course touches on material such as the use of the Sheffer stroke function and its reflection in NAND gates; building a simple circuit from logic gates and the relation of SAT solvers to propositional calculus.  

Later, after first-order logic, we cover set theory, mentioning ZF but we use a version called AFST (abstraction free set theory) which is a fragment of set theory designed for machine-assisted proof in basic set theory and you get to produce machine-assisted proofs of some foundational theorems of set theory.  We study tuples, relations and functions and based on this we look at Codd's Relational Algebra - the basis for MySQL and a host of RDBMS. 

After that, we look at the Peano axioms for arithmetic and induction and we look at solving inductive problems.   I use the heuristics developed by Boyer and Moore to teach you how to tackle inductive proofs and prove functional programs correct. We learn this in the context of reasoning about Shen programs.  Note, the course does not require facility with Shen, but one lecture, on the automation of machine proof through tactics, introduces the ideas of Robin Milner through very simple Shen.

The later lectures cover Turing machines and the strategy for proving undecidability using a proof of the undecidability first-order logic as an example.   We close on a reconstruction of Godel's Incompleteness Theorem using a Shen program as an example (much less complex than Godel's pre-computer approach of 80+ years ago).  

There is a lot of philosophy embedded in the text.  You learn the distinction between minimal logic and intuitionistic logic, the case for paraconsistent logic and what it is.  Also anti-realism in mathematics in response to the Continuum Hypothesis.  Russell's Paradox and responses to it,  Cantor's proof and responses to it, logicism, conventionalism and formalism as philosophies of mathematics.  Also the formalisation of English, Russell's Theory of Definite Descriptions, Davidson's work on formalising action sentences and the challenges to formalisation (paradoxes of material implication etc) from Strawson and Austin.  We conclude by looking at Lucas on the implications of Godel's Incompleteness Theorem for artificial intelligence.

This is a quite unique course; nothing quite like it is taught in CS departments.  Years ago, I campaigned for an M.Sc. in Combined Logic in which computational, mathematical and philosophical logic was integrated into one degree.  The course is really the foundation course for such an M.Sc.  So if you've ever wanted a magical mystery tour of some of the greatest thinkers of the C20 in these three disciplines, this is for you.

I'll flag this up again when the course is about to commence.

Mark 

[Raoul Duke]

this sounds very cool.

[Artella Coding]

Wow! That sounds really interesting. Will definitely be buying a copy of the book.

--
You received this message because you are subscribed to the Google Groups "Shen" group.
To unsubscribe from this group and stop receiving emails from it, send an email to qilang+un...@googlegroups.com.
To post to this group, send email to qil...@googlegroups.com.
Visit this group at http://groups.google.com/group/qilang.
For more options, visit https://groups.google.com/d/optout.

[Shaun Gilchrist]

I am definitely interested - will it be video based?

[Bruno Deferrari]

Me too.

--
BD

[Mark Tarver]

Yes it will; I begin creating the videos next month.

Mark

[Mark Tarver]

To amplify; the course is based on the UK semester standard of 20 1 hour lectures.

Mark

[Samuel Chase]

@Dr. Tarver, I'm interested! :-)

[Federico Brubacher]

I'm interested too

[Greg Spurrier]

I'm definitely interested in this. If I can swing the monetary and time commitment at the time it's offered, I'll likely participate. At the very least, I intend to purchase the book when it is available.

Greg

[Rafael Turner]

Beautiful. Don't forget to please send out a link for registration, description, and examples when you are ready. :) 

Are you going to cover SMT as well? 

[Jacob]

Seems like it will be pretty cool.  How will it be delivered?  Will the course be part of some online freebie school like coursera or will this be a youtube series?

[Mark Tarver]

It won't be a freebie course; I can't afford such gestures!   It may appear on Uedemy.   LPC would make a great foundation course for an MSc in Combined Logic.    The M.Sc. course I envisaged 20 years ago looked like this:

Computing, Maths, Philosophy

LPC - foundation course

Logic Programming and Expert Systems

Automated Reasoning

Philosophical Logic

Deviant and Extended Logics

Formal Methods

Functional Programming and Type Theory

Axiomatic Set Theory and Model Theory

Category Theory

However the complete incapacity of the professor in charge - a complete egg plant who was only interested in cranking out boring papers for his CV - meant that the course never happened. I think since then better departments have done this.

I'm adding material on free logic and Turing machines to LPC.

Mark

[Frank Colcord]

Hi, did you ever do this course? Is there an archive? How much did you charge? 

I'm looking for a course to learn more about Robin Milner's work.

I found your statement through google "introduces the ideas of Robin Milner through very simple Shen."

I was going to buy your book, but found it's only paperback. Can I buy an electronic copy somewhere?

I've read through some of your web pages. Perhaps you don't have much respect for Milner's work. 

I wonder what resources you would suggest for someone interested in learning how to reason clearly about systems, concurrency and communicating agents.

Frank

[Mark Tarver]

I started to do it and stopped because it was rather boring for me.  Not because the material was boring, but because I'd covered it fairly well in LPC and really all one needed to do was to work through the book.    So I was just repeating myself.  I rather like doing things which I don't fully understand which might seem odd to some.  

Oh, I have a lot of respect for Milner.  I met him over 30 years ago when he was head of the LFCS.  LPC has a chapter devoted to his ideas.  But generally when I present ideas they are reconstructions of what people did because what I want to communicate is the essence of what I consider their contribution to be.  So what I present is a reconstruction of Milner's ideas about tactics.   Likewise the final chapter on Godel is heavily reconstructed because I want to show how simple it is to reproduce Godel's ideas in a new way on the computer w.o. Godel numbering and other stuff that is traditionally taught.

So if you want to read what these men had to say w.o. any intervening interpretation then follow the recommended reading in the book list.  Milner's CCS and the Edinburgh LCF text are probably the main texts to follow.    

I never do e-copies of my books.   LPC is not expensive though.   

Mark

[fuzzy wozzy]

what about intensional logic / intensional programming?
unless you're familiar with it to the point of finding it boring, it might suit shen well,
being that it was developed via dataflow languages like lucid, esterel, etc,
I don't really know what it is or how it works, something to do with reactive programming maybe,
it's used in areas that require extreme exactness of calculation with very little margin of error
or none allowed, since shen is known to do dataflow well, at least that's the impression overall...

[fuzzy wozzy]

https://wiki.haskell.org/Lucid

[Frank Colcord]

Thanks for letting me know. I'll buy the book. I much prefer ebooks since I travel a lot.

The Milner book I'm trying to understand is 'the space and motion of communicating agents'. 

It looks as if I'll need to read his previous texts first.

[fuzzy wozzy]

I don't really want to say this, but as everyone knows, every programming language has its proponents and
advocates as well the naysayers and whatnot, but some say that functional reactive programming will the future
of programming be... now, I have no clue based on what evidence they can make such claims, but perhaps
some shenturians can enlighten me on this, even better if with demo versions of shen code, I personally had always
thought and believed that code generation with macros were the key to the easy transition to the future programming,
but who's to say that one can only choose one or the other and not bake the cake it and eat it too, maybe the future
of programming encompass any and all of the above, in other words, code generating macros where the codes are
functional reactive ones... one can hope

[fuzzy wozzy]

gabriel ditu wrote a book, creating translucid,
there's a web-enabled interpreter,

http://translucid.web.cse.unsw.edu.au/tlweb