Brain Retrieved

Having put aside my other intellectual enterprises to do an abstract for the ITP workshop, I came up with nothing, despite being very keen at the outset and spending three weeks tussling with the problem.

I think too much of my thinking in this area is speculative and philosophical, and the small core of relevant technical detail got simpler and less substantial the more I thought about it.

The abstract deadline is today, so I have finally thrown in the towel.
I now need to think a bit before picking up some other threads.

RBJ

Well Founded Set Theoretic Truth

In the course of failing to come up with an abstract for the upcoming ITP workshop in Cambridge, I came across something I think rather nice which is only to be found in the overheads of the last talk I gave on X-Logic.

So I thought I would post it here, to give it a better home.

First just a few words of context.

I am unusual in considering the most important role for set theory to be its role as a foundation for abstract semantics.
From this point of view it is unfortunate that mathematical logic (where set theory belongs) has a negative attitude towards semantics, and tolerates a situation  in which set theory has no definite semantics (or at least, no single generally agreed semantics, there are many possibilities).

Anyway, I came up with a neat semantics for set theory as follows.
This is a definition for the truth conditions of sentences in set theory.
It assumes understood the notion of truth in an interpretation.

• a well-founded set is a definite collection of well-founded sets
  
• an interpretation of set theory is a transitive well-founded set
  
• a sentence is false if the collection of interpretations in which it is true is definite
  
• a sentence is true if the collection of interpretations in which it is false is definite
  

This is what I wrote about this at the time.

This semantics:

• is maximally rich (large cardinal axioms are true)
  
• is definite (CH has a truth value, particular facts about cardinal arithmetic have truth values)
  
• makes ZFC neither true nor false
  
• is not limited to first order languages (will work for infinitary set theory)
  
• is self defining (conjecture)
  

This probably all needs explaining in much greater detail, I will follow up with a bit more explanation.

RBJ

Brain Hijacked

Just at the point when I am trying, almost deperately, to get movement on my X-Logic and an associated informal analytic meta-methodology, an opportunity to engage with the Theorem Proving community comes up which I can't ignore.

Workshop on Trusted Extensions of Interactive Theorem Provers


The workshop is August 11-12 2010, in Cambridge, (England!) and abstracts for contributed talks have to be in by 28 June.
I intend to submit an abstract for a talk on X-Logic.  (I have already talked about X-Logic at the Computer Labs in Cambridge, but things have moved on since then).

At the heart of X-Logic is a system assurance/trust/authority (not sure which words to use) tags which is partly inspired by the problems of trust that arise in interworking between interactive theorem provers and other software (but also by a long list of other related problems).
X-Logic is now at the heart of my thinking about analytic methods appropriate for use in philosophy (and elsewhere). Alternatively, it is a label for the formal side of my methodological thinking.

The timescales are short, so it is likely to hijack my brain between now and the event (if my abstract were accepted, otherwise up to the point of its being declined!).

Though I will be pre-occupied with getting my story straight for the workshop, I hope there will be plenty of room for discussion about the impact of X-Logic on my philosphical projects, including the Carnap/Grice conversation, and my other thing.  I will be posting on this at the X-Logic blog, and probably something at Carnap Corner, The Eternal City, and maybe other places too.

Watch these spaces.

RBJ