Breadcrumb
A constructive naive set theory, a truth predicate and the omega-rule
Thu 10 January 2013, 17:00
Shunsuke Yatabe
Kyoto University
Organisers: Philip Welch, Peter Holy
ABSTRACT
It is known that naive set theories do not imply a contradiction in
contraction-free logics. Their significance is that they prove a fixed
point theorem: for any formula $\varphi(x,\cdots, y)$, we can
construct a term $\theta$ such that $(\forall x)[x\in
\theta\equiv\varphi(x,\cdots, \theta)]$. This allows us to define sets
circularly. For example, we can define the set of natural numbers
$\omega$: $(\forall x) [ x\in\omega\equiv[ x=\bar{0} \,\vee \,
(\exists y)[y\in\omega\otimes x={\bf suc} (y)]]]$. Similarly, we can
define a total truth predicate {\bf Tr} which satisfies the full form
of Tarskian schema.
However, the details of such circularly defined sets are not
well-known. Let us focus on $\omega$: in this talk, we prove that a
careless extension of {\bf CONS}, constructive naive set theory
within Full Lambek predicate calculus with exchange and weakening
rule ${\bf Flew}$\froall$ (which is a intuitionistic predicate logic
minus the contraction rule), by adding an infinitary rule implies a
contradiction:
{\bf Theorem}
A strong version of $\omega$-rule, which is an infinitary rule saying
$\omega$ consists of numerals only (roughly
$\omega=\bigcup_{n\in\NN}\{\bar{n}\}$), implies a contradiction in
$\FLST$.
The proof is done by simulating Girard's ! operator by using {\bf Tr}.
This is a partial and negative answer to the claim of the
standardness of $\omega$ in {\bf CONS}: the $\omega$-rule implies the
$\omega$-consistency, i.e. if $\varphi(\bar{n})$ holds for any {\it
numeral} $\bar{n}$ then $\forall x \varphi(x)$ holds for any
$\varphi(x)$, and it involves that the theory with the rule has a
standard model, i.e. any natural number in that model is a numeral.