Sciweavers

APAL
2010
66views more  APAL 2010»
13 years 3 months ago
Strong normalization results by translation
We prove the strong normalization of full classical natural deduction (i.e. with conjunction, disjunction and permutative conversions) by using a translation into the simply typed...
René David, Karim Nour
APAL
2010
129views more  APAL 2010»
13 years 3 months ago
Kripke models for classical logic
We introduce a notion of Kripke model for classical logic for which we constructively prove soundness and cut-free completeness. We discuss the meaning of the new notion and its a...
Danko Ilik, Gyesik Lee, Hugo Herbelin
APAL
2010
114views more  APAL 2010»
13 years 3 months ago
Classical predicative logic-enriched type theories
A logic-enriched type theory (LTT) is a type theory extended with a primitive mechanism for forming and proving propositions. We construct two LTTs, named LTT0 and LTT 0, which we...
Robin Adams, Zhaohui Luo
APAL
2010
69views more  APAL 2010»
13 years 3 months ago
Relativized Grothendieck topoi
In this paper we define a notion of relativization for higher order logic. We then show that there is a higher order theory of Grothendieck topoi such that all Grothendieck topoi ...
Nathanael Leedom Ackerman
APAL
2010
90views more  APAL 2010»
13 years 3 months ago
Canonical extensions for congruential logics with the deduction theorem
We introduce a new and general notion of canonical extension for algebras in the algebraic counterpart AlgS of any finitary and congruential logic S. This definition is logic-base...
Mai Gehrke, Ramon Jansana, Alessandra Palmigiano
APAL
2010
67views more  APAL 2010»
13 years 3 months ago
Projective mad families
Using almost disjoint coding we prove the consistency of the existence of a 1 2 definable -mad family of infinite subsets of (resp. functions from to ) together with b = 2 = 2.
Sy-David Friedman, Lyubomyr Zdomskyy
APAL
2010
88views more  APAL 2010»
13 years 3 months ago
Nonstandard arithmetic and recursive comprehension
First order reasoning about hyperintegers can prove things about sets of integers. In the author's paper Nonstandard Arithmetic and Reverse Mathematics, Bulletin of Symbolic L...
H. Jerome Keisler
APAL
2010
97views more  APAL 2010»
13 years 3 months ago
Beyond Borel-amenability: Scales and superamenable reducibilities
We analyze the degree-structure induced by large reducibilities under the Axiom of Determinacy. This generalizes the analysis of Borel reducibilities given in [1], [6] and [5] e.g...
L. Motto Ros
APAL
2010
73views more  APAL 2010»
13 years 3 months ago
Totality in arena games
Pierre Clairambault, Russ Harmer