4 citations · 5 across the 5 of their papers we have counts for
6 papers · 1 filter
On the computational content of Zorn's lemma
Thomas Powell
We give a computational interpretation to an abstract instance of Zorn's lemma formulated as a wellfoundedness principle in the language of arithmetic in all finite types. This is…
An algorithmic approach to the existence of ideal objects in commutative algebra
Thomas Powell, Peter M Schuster, Franziskus Wiesnet
The existence of ideal objects, such as maximal ideals in nonzero rings, plays a crucial role in commutative algebra. These are typically justified using Zorn's lemma, and thus pos…
Dependent choice as a termination principle
Thomas Powell
We introduce a new formulation of the axiom of dependent choice that can be viewed as an abstract termination principle, which generalises the recursive path orderings used to esta…
Sequential algorithms and the computational content of classical proofs
Thomas Powell
We develop a correspondence between the theory of sequential algorithms and classical reasoning, via Kreisel's no-counterexample interpretation. Our framework views realizers of th…
Computational interpretations of classical reasoning: From the epsilon calculus to stateful programs
Thomas Powell
The problem of giving a computational meaning to classical reasoning lies at the heart of logic. This article surveys three famous solutions to this problem - the epsilon calculus,…
Applying Gödel's Dialectica Interpretation to Obtain a Constructive Proof of Higman's Lemma
Thomas Powell
We use Gödel's Dialectica interpretation to analyse Nash-Williams' elegant but non-constructive "minimal bad sequence" proof of Higman's Lemma. The result is a concise constructive…