Realizability algebras: a program to well order R

Details Realizability algebras: a program to well order R Realizability algebras: a program to well order R

2010-05-13

arxiv.org/abs/1005.2395v4

LMCS 7 (3:2) 2011

Computer Science

Logic in Computer Science

Scientific paper

10.2168/LMCS-7(3:2)2011

The theory of classical realizability is a framework in which we can develop the proof-program correspondence. Using this framework, we show how to transform into programs the proofs in classical analysis with dependent choice and the existence of a well ordering of the real line. The principal tools are: The notion of realizability algebra, which is a three-sorted variant of the well known combinatory algebra of Curry. An adaptation of the method of forcing used in set theory to prove consistency results. Here, it is used in another way, to obtain programs associated with a well ordering of R and the existence of a non trivial ultrafilter on N.

Affiliated with

Also associated with

No associations

Rating

Realizability algebras: a program to well order R does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Realizability algebras: a program to well order R, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Realizability algebras: a program to well order R will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-641232