2
$\begingroup$

I asked a question some time ago that was down voted and subsequently deleted. Regardless of the rights and wrongs of that, I'd like to have a link to the question in my account because it contained information and debate that would be useful to hang on to. The question did appear to be there for about a month after it was publicly deleted, but it now seems to have disappeared altogether. Has it gone forever or can it be recovered?

$\endgroup$
5

1 Answer 1

2
$\begingroup$

So the question might have been what appears below. There was a longish string of comments below the question, and it was closed as "unclear what you're asking". If this is not what you were looking for, then you had better give at least some description or keywords.


"With typical hubris I thought I had a proof of the inference rule for induction starting from a construction of the natural numbers. But I now find on closer inspection that there's a glitch. My original question on mathematics stack exchange, and in particular my answer to the question at the foot of the post, has all of the background. The complete proof, including the glitch, can also be found here. I could give a further explanation now but I might just muddy the waters so it's best just to point the reader to the original post and then just highlight the glitch.

"The problem is with the following assertion which can be found in the second subproof of the proof for the main rule:

τ(s(k)) ⊢ T(k)::P(k)

"Whilst it is certainly true that T(k) should in some sense belong to the context τ(s(k)), it seems that I can't simply assert that it is a proof of P(k). Or can I?

"Update: As far as I understand it the aforementioned judgement τ(s(k)) ⊢ T(k)::P(k) within the subproof is actually fine because the definition of the context should be:

let τ(s(k))=σ,T(k)::P(k)

"Quite why this is permissible when (obviously) the judgement T(k)::P(k) hasn't itself been proven is something I am still not one hundred percent sure about. I would appreciate some clarification. There are some rambling comments of mine at the end but I'm not sure these are of much value.

"Update: There is a rather glib answer to the remaining question, namely is τ(s(k))=σ,T(k)::P(k) correct? The answer is that if τ(s(k)) were not defined in this way then theorem T(s(k)) would simply not verify."

$\endgroup$
1
  • 3
    $\begingroup$ Thank you. I think you can delete this, though, since I now have your link to the original question in your comment. $\endgroup$ Sep 19, 2017 at 13:48

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .