The limit lemma in fragments of arithmetic
The recursion theoretic limit lemma, saying that each function with a graph is a limit of certain function with a graph, is provable in .
On sequent calculi for intuitionistic propositional logic
The well-known Dyckoff's 1992 calculus/procedure for intuitionistic propositional logic is considered and analyzed. It is shown that the calculus is Kripke complete and the procedure in fact works in polynomial space. Then a multi-conclusion intuitionistic calculus is introduced, obtained by adding one new rule to known calculi. A simple proof of Kripke completeness and polynomial-space decidability of this calculus is given. An upper bound on the depth of a Kripke counter-model is obtained.
Arithmetical classification of the set of all provably recursive functions
The set of all indices of all functions provably recursive in any reasonable theory is shown to be recursively isomorphic to , where is -complete set.
A sentence that is difficult to interpret
Degrees of interpretability
Page 1