2
$\begingroup$

I have preoccupied myself some with very weak set theories that suffice to interpret Robinson Arithmetic, as in this question Is Extensionality needed for the incompleteness of very weak set theories?. May we have confidence that the theory SU, which has the axioms for empty set and for universal set and for adjunction as well as the rules $\vdash\hspace{-2pt}\alpha(a)\Leftrightarrow\hspace{2pt}\vdash\hspace{-2pt} a\notin\{x|\lnot\alpha(x)\}$ and $\vdash\hspace{-2pt}\alpha(a)\Leftrightarrow\hspace{2pt}\vdash\hspace{-2pt} a\in\{x|\alpha(x)\}$ is consistent or even omega consistent in an appropriate sense? Does SU still support its own coding to get a Godelian provability predicate for SU?

SU has all set terms and we presuppose an underlying theory of identity by having the Leibnizian-Russellian definition of $a=b$ as $\forall u(a\in u\rightarrow b\in u)$ and the axiom schema $\vdash\forall x, y(x=y\rightarrow(\alpha(x)\rightarrow\alpha(y)))$.

P.S. The appropriate omega consistency I want is that if $\vdash\alpha(t)$ for all terms $t$ then $\nvdash\exists x\lnot\alpha(x)$.

Improve this question
$\endgroup$
16
  • 1
    $\begingroup$ I don't quite understand the additional axiom in SU - is "$\{x: \neg \alpha(x)\}$" actually a term in your language? If not, what exactly is it shorthand for? (For example, are you saying that there is a set of all $x$ such that $\neg\alpha(x)$?) Also, what assumptions are you willing to make - e.g. if SU is consistent relative to ZFC, are you happy? $\endgroup$
    – Noah Schweber
    Commented Mar 11, 2016 at 23:58
  • 1
    $\begingroup$ The addition you are alluding to comprise inference rules and not axioms. Yes, $\{x|\lnot\alpha(x)\}$ is a term. In fact, all terms $\{x|\alpha(x)\}$ are terms of SU. I would believe that SU is consistent relative to much weaker theories than $ZFC$, but any result is of interest. $\endgroup$
    – Frode Alfson Bjørdal
    Commented Mar 12, 2016 at 0:10
  • 3
    $\begingroup$ OK, then I am worried your theory is inconsistent: you have a term $\{x: \neg (x\in x)\}$! Now, you don't have an axiom scheme saying $\forall x[\alpha(x)\iff x\in \{x: \alpha(x)\}]$, so we don't immediately hit a contradiction - but at this point I wouldn't be surprised if there is a contradiction. $\endgroup$
    – Noah Schweber
    Commented Mar 12, 2016 at 0:14
  • 1
    $\begingroup$ May terms $\lbrace x \mid \alpha(x) \rbrace$ contain parameters? $\endgroup$
    – Andrej Bauer
    Commented Mar 12, 2016 at 7:53
  • 2
    $\begingroup$ I think the worry about inconsistency comes from the fact that changing your inference rule to the axiom $\forall a . (\alpha(a) \Leftrightarrow a \not\in \lbrace x \mid \lnot \alpha(x) \rbrace)$ opens the road to Russell's paradox. $\endgroup$
    – Andrej Bauer
    Commented Mar 12, 2016 at 8:01

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .