# Decidability of quantified propositional intuitionistic logic and S4 on trees of height and arity ≤ ω

Zach, Richard. 2004. “Decidability of Quantified Propositional Intuitionistic Logic and S4 on Trees of Height and Arity ≤ω.” Journal of Philosophical Logic 33 (2): 155–64. https://doi.org/10.1023/B:LOGI.0000021744.10237.d0.

Quantified propositional intuitionistic logic is obtained from propositional intuitionistic logic by adding quantifiers $$\forall p$$, $$\exists p$$, where the propositional variables range over upward-closed subsets of the set of worlds in a Kripke structure. If the permitted accessibility relations are arbitrary partial orders, the resulting logic is known to be recursively isomorphic to full second-order logic (Kremer, 1997). It is shown that if the Kripke structures are restricted to trees of at height and width at most $$\omega$$, the resulting logics are decidable. This provides a partial answer to a question by Kremer. The result also transfers to modal S4 and some Gödel-Dummett logics with quantifiers over propositions.

# Hilbert’s “Verunglückter Beweis,” the first epsilon theorem, and consistency proofs

Zach, Richard. 2004. “Hilbert’s ‘Verunglückter Beweis’, the First Epsilon Theorem, and Consistency Proofs.” History and Philosophy of Logic 25 (2): 79–94. https://doi.org/10.1080/01445340310001606930.

In the 1920s, Ackermann and von Neumann, in pursuit of Hilbert’s Programme, were working on consistency proofs for arithmetical systems. One proposed method of giving such proofs is Hilbert’s epsilon-substitution method. There was, however, a second approach which was not reflected in the publications of the Hilbert school in the 1920s, and which is a direct precursor of Hilbert’s first epsilon theorem and a certain ‘general consistency result’ due to Bernays. An analysis of the form of this so-called ‘failed proof’ sheds further light on an interpretation of Hilbert’s Program as an instrumentalist enterprise with the aim of showing that whenever a ‘real’ proposition can be proved by ‘ideal’ means, it can also be proved by ‘real’, finitary means.