Re: [isabelle] Formalizing Turing machine


I read a bit about proof theory. So if I want to prove from premises
P_1, ..., P_k one can derive conclusion C and I used the induction
principle (IND) in the proof, I'm actually showing that P_1, ..., P_k,
IND entail C instead of just P_1, ..., P_k entail C. And usually for a
problem whether Q_1, ..., Q_j entail D, we are actually showing Q_1,
..., Q_j, ZFC entail D.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.