Finite sum-product logic.
Formally self-referential propositions for cut free classical analysis and related systems [Book]
Fragments of complete extensions of PA and McDowell-Specker's theorem.
From Foundations to Science: Justifying and Unwinding Proofs
Functions provably total in
Functorial bounds for cut elimination in L... .I.
Functorial bounds for cut elimination in L.. .II.
Further applications of ultra-conservative ...-rules.
Geometric and higher order logic in terms of abstract Stone duality.
Geometrické upotřebení některých pouček o determinantech. [I.]
Geometrické upotřebení některých pouček o determinantechGeometric application of some theorems on determinants. [II.]
Gilt das Lemma von König "konstruktiv"?
Gödel et la thèse de Turing
Cet article porte sur la discussion par Gödel de la thèse de Turing. Pour l’essentiel, nous présentons des notes inédites conservées dans les Archives Gödel, qui apportent des éléments nouveaux sur la relation ambiguë de Gödel à Turing. La première section examine la position qu’avait Gödel avant 1937 sur la possibilité d’une définition de la calculabilité. La deuxième concerne directement l’interprétation par Gödel de la thèse de Turing. Dans plusieurs passages, antérieurs à 1937, Gödel qualifie...
Gödel's diagonalization technique and related properties of theories
Goldbach conjecture.
Goodstein's function.
Herbrand consistency and bounded arithmetic
We prove that the Gödel incompleteness theorem holds for a weak arithmetic Tₘ = IΔ₀ + Ωₘ, for m ≥ 2, in the form Tₘ ⊬ HCons(Tₘ), where HCons(Tₘ) is an arithmetic formula expressing the consistency of Tₘ with respect to the Herbrand notion of provability. Moreover, we prove , where is HCons relativised to the definable cut Iₘ of (m-2)-times iterated logarithms. The proof is model-theoretic. We also prove a certain non-conservation result for Tₘ.
Hercules and Hydra
Hercules and Hydra, a game on rooted finite trees