Markov's rule vs. Markov's principle
Thomas Streicher
> says that in Martin-Lof type theory if Sigma |- ~~Exist x. t[x] = s[x],
> then Sigma |- Exists x. t[x] = s[x]. Is this enough to give Pi_2
> conservation of MLTT + MP over MLTT? Is MLTT is strong enough to
> formalize Tait's theorem?
What Palmgren shows is that MLTT is closed under Markov's rule. This,
of course doesn't entail Markov's Principle.
But it suffices to give Pi_2 conservation of MLTT + MP over MLTT since the
negative translation of MLTT + MP is provable in MLTT.
Thomas
roco...@theorem.ca
So I believe that we have satified Martin's request for a sytem (MLTT)
which is (presumably) strong enough to prove Tait's theorem that system T
is normalizing and is conservative under the addition of MP for Pi_2
statemets (in fact it appears to be conservative under the addition of EM
for PI_2 statements).
Thus Tait's proof must contain an algorithm for normalizing system T that
only uses bounded recursion.
--
Russell O'Connor <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''
Thomas Streicher
> which is (presumably) strong enough to prove Tait's theorem that system T
> is normalizing and is conservative under the addition of MP for Pi_2
> statemets (in fact it appears to be conservative under the addition of EM
> for PI_2 statements).
it depends on what you mean by MLTT
of course, for Goedelian reasons
MLTT cannot prove strong normalisation for its own term language
but if MLT has W-types and/or universes one can prove strong normalisation
of Goedel's T in it
however, with W-types one cannot formulate Tait's proof but has to use
\varepsilon_0 induction
having universes available one can use formalize Tait's argument
one needs a universe just for being able to define a T of type
(\sigma:SType) Tm(\sigma) -> Prop
by recusrion on SType (the set of simple types over N)
Thomas