Displaying 21 – 40 of 515

Showing per page

A Note on Negative Tagging for Least Fixed-Point Formulae

Dilian Gurov, Bruce Kapron (2010)

RAIRO - Theoretical Informatics and Applications

Proof systems with sequents of the form U ⊢ Φ for proving validity of a propositional modal μ-calculus formula Φ over a set U of states in a given model usually handle fixed-point formulae through unfolding, thus allowing such formulae to reappear in a proof. Tagging is a technique originated by Winskel for annotating fixed-point formulae with information about the proof states at which these are unfolded. This information is used later in the proof to avoid unnecessary unfolding, without...

A note on Δ₁ induction and Σ₁ collection

Neil Thapen (2005)

Fundamenta Mathematicae

Slaman recently proved that Σₙ collection is provable from Δₙ induction plus exponentiation, partially answering a question of Paris. We give a new version of this proof for the case n = 1, which only requires the following very weak form of exponentiation: " x y exists for some y sufficiently large that x is smaller than some primitive recursive function of y".

Currently displaying 21 – 40 of 515