Realizability

<h2 id="example-kleenes-1945-realizability">Example: Kleene's 1945-realizability</h2>
<a href="/facts/Stephen_Cole_Kleene/sKSax2se">Kleene</a>'s original version of realizability uses natural numbers as realizers for formulas in <a href="/facts/Heyting_arithmetic/aBfjC0zg">Heyting arithmetic</a>. A few pieces of notation are required: first, an ordered pair (n,m) is treated as a single number using a fixed <a href="/facts/Primitive_recursive_function/4z97gRnl">primitive recursive</a> <a href="/facts/Pairing_function/RdKC15Mk">pairing function</a>; second, for each natural number n, φn is the <a href="/facts/Computable_function/dzwBlLGn">computable function</a> with index n. The following clauses are used to define a relation "n realizes A" between natural numbers n and formulas A in the language of Heyting arithmetic, known as Kleene's 1945-realizability relation:<a class="footnote-ref" id="fnref:2" href="#fn:2">2</a>

<ul><li>Any number n realizes an atomic formula s=t if and only if s=t is true. Thus every number realizes a true equation, and no number realizes a false equation.</li>
<li>A pair (n,m) realizes a formula A∧B if and only if n realizes A and m realizes B. Thus a realizer for a conjunction is a pair of realizers for the conjuncts.</li>
<li>A pair (n,m) realizes a formula A∨B if and only if the following hold: n is 0 or 1; and if n is 0 then m realizes A; and if n is 1 then m realizes B. Thus a realizer for a disjunction explicitly picks one of the disjuncts (with n) and provides a realizer for it (with m).</li>
<li>A number n realizes a formula A→B if and only if, for every m that realizes A, φn(m) realizes B. Thus a realizer for an implication corresponds to a computable function that takes any realizer for the hypothesis and produces a realizer for the conclusion.</li>
<li>A pair (n,m) realizes a formula (∃ x)A(x) if and only if m is a realizer for A(n). Thus a realizer for an existential formula produces an explicit witness for the quantifier along with a realizer for the formula instantiated with that witness.</li>
<li>A number n realizes a formula (∀ x)A(x) if and only if, for all m, φn(m) is defined and realizes A(m). Thus a realizer for a universal statement is a computable function that produces, for each m, a realizer for the formula instantiated with m.</li></ul>
With this definition, the following theorem is obtained:<a class="footnote-ref" id="fnref:3" href="#fn:3">3</a>

Let A be a sentence of Heyting arithmetic (HA). If HA proves A then there is an n such that n realizes A.
On the other hand, there are classical theorems (even propositional formula schemas) that are realized but which are not provable in HA, a fact first established by Rose.<a class="footnote-ref" id="fnref:4" href="#fn:4">4</a> So realizability does not exactly mirror intuitionistic reasoning.
Further analysis of the method can be used to prove that HA has the "<a href="/facts/Disjunction_and_existence_properties/18s8ll0e">disjunction and existence properties</a>":<a class="footnote-ref" id="fnref:5" href="#fn:5">5</a>

<ul><li>If HA proves a sentence (∃ x)A(x), then there is an n such that HA proves A(n)</li>
<li>If HA proves a sentence A∨B, then HA proves A or HA proves B.</li></ul>
More such properties are obtained involving <a href="/facts/Harrop_formula/7ICBu8K2">Harrop formulas</a>.

<h2 id="later-developments">Later developments</h2>
<a href="/facts/Georg_Kreisel/fejTurVu">Kreisel</a> introduced modified realizability, which uses <a href="/facts/Typed_lambda_calculus/g86GP4uK">typed lambda calculus</a> as the language of realizers. Modified realizability is one way to show that <a href="/facts/Markov%2527s_principle/Dmd1B0J8">Markov's principle</a> is not derivable in intuitionistic logic. On the contrary, it allows to constructively justify the principle of <a href="/facts/Independence_of_premise/wMJ8wjpS">independence of premise</a>:

(
 A
 →
 ∃
 x
 
 P
 (
 x
 )
 )
 →
 ∃
 x
 
 (
 A
 →
 P
 (
 x
 )
 )
 
 
 {\displaystyle (A\rightarrow \exists x\;P(x))\rightarrow \exists x\;(A\rightarrow P(x))}
 
.
Relative realizability<a class="footnote-ref" id="fnref:6" href="#fn:6">6</a> is an intuitionist analysis of <a href="/facts/Computable/VpnJUkPN">computable</a> or <a href="/facts/Computably_enumerable/lpzr8jHn">computably enumerable</a> elements of data structures that are not necessarily computable, such as computable operations on all real numbers when reals can be only approximated on digital computer systems.
Classical realizability was introduced by Krivine<a class="footnote-ref" id="fnref:7" href="#fn:7">7</a> and extends realizability to classical logic. It furthermore realizes axioms of <a href="/facts/Zermelo%25E2%2580%2593Fraenkel_set_theory/UYIsPbXw">Zermelo–Fraenkel set theory</a>. Understood as a generalization of <a href="/facts/Paul_Cohen/wMLaE3Vz">Cohen</a>’s <a href="/facts/Forcing_(mathematics)/3vMqqKcq">forcing</a>, it was used to provide new models of set theory.<a class="footnote-ref" id="fnref:8" href="#fn:8">8</a>
Linear realizability extends realizability techniques to <a href="/facts/Linear_logic/NmFxFRWh">linear logic</a>. The term was coined by Seiller<a class="footnote-ref" id="fnref:9" href="#fn:9">9</a> to encompass several constructions, such as <a href="/facts/Geometry_of_interaction/dCFdtjsJ">geometry of interaction</a> models,<a class="footnote-ref" id="fnref:10" href="#fn:10">10</a> <a href="/facts/Ludics/ezum1WTK">ludics</a>,<a class="footnote-ref" id="fnref:11" href="#fn:11">11</a> interaction graphs models.<a class="footnote-ref" id="fnref:12" href="#fn:12">12</a>

<h2 id="use-in-proof-mining">Use in proof mining</h2>
Realizability is one of the methods used in <a href="/facts/Proof_mining/5PkmkIHm">proof mining</a> to extract concrete "programs" from seemingly non-constructive mathematical proofs. Program extraction using realizability is implemented in some <a href="/facts/Proof_assistant/hjFGxLPn">proof assistants</a> such as <a href="/facts/Coq_(software)/7oBXgLCE">Coq</a>.

<h2 id="see-also">See also</h2>
<ul><li><a href="/facts/Curry%25E2%2580%2593Howard_correspondence/Q3eVu60u">Curry–Howard correspondence</a></li>
<li><a href="/facts/Dialectica_interpretation/WPfbFVmL">Dialectica interpretation</a></li>
<li><a href="/facts/Harrop_formula/7ICBu8K2">Harrop formula</a></li></ul>
<h2 id="notes">Notes</h2>

<ul><li>Birkedal, Lars; Jaap van Oosten (2000). <a href="https://www.staff.science.uu.nl/~ooste110/realizability/birkoost.ps.gz">Relative and modified relative realizability</a>.</li>
<li>Kreisel G. (1959). "Interpretation of Analysis by Means of Constructive Functionals of Finite Types", in: Constructivity in Mathematics, edited by A. Heyting, North-Holland, pp. 101–128.</li>
<li>Kleene, S. C. (1945). "On the interpretation of intuitionistic number theory". <a href="/facts/Journal_of_Symbolic_Logic/lfXVXcoy">Journal of Symbolic Logic</a>. 10 (4): 109–124. <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.2307%2F2269016">10.2307/2269016</a>. <a href="/facts/JSTOR_(identifier)/YTeVmaJ7">JSTOR</a> <a href="https://www.jstor.org/stable/2269016">2269016</a>.</li>
<li>Kleene, S. C. (1973). "Realizability: a retrospective survey" from Mathias, A. R. D.; Hartley Rogers (1973). Cambridge Summer School in Mathematical Logic : held in Cambridge/England, August 1–21, 1971. Berlin: Springer. <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 3-540-05569-X., pp. 95–112.</li>
<li>van Oosten, Jaap (2000). <a href="http://www.math.uu.nl/people/jvoosten/realizability/history.ps.gz">Realizability: An Historical Essay</a>.</li>
<li>Rose, G. F. (1953). <a href="https://doi.org/10.2307%2F1990776">"Propositional calculus and realizability"</a>. <a href="/facts/Transactions_of_the_American_Mathematical_Society/JmKtyCwK">Transactions of the American Mathematical Society</a>. 75 (1): 1–19. <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.2307%2F1990776">10.2307/1990776</a>. <a href="/facts/JSTOR_(identifier)/YTeVmaJ7">JSTOR</a> <a href="https://www.jstor.org/stable/1990776">1990776</a>.</li></ul>
<h2 id="external-links">External links</h2>
<ul><li><a href="http://www.math.uu.nl/people/jvoosten/realizability.html">Realizability</a> Collection of links to recent papers on realizability and related topics.</li></ul>

<h2 id="references">References</h2>

<ol>
<li id="fn:1">van Oosten 2000 <a href="#fnref:1" class="footnote-back-ref">↩</a></li>
<li id="fn:2">A. Ščedrov, "Intuitionistic Set Theory" (pp.263--264). From Harvey Friedman's Research on the Foundations of Mathematics (1985), Studies in Logic and the Foundations of Mathematics vol. 117. <a href="#fnref:2" class="footnote-back-ref">↩</a></li>
<li id="fn:3">van Oosten 2000, p. 7 <a href="#fnref:3" class="footnote-back-ref">↩</a></li>
<li id="fn:4">Rose 1953 <a href="#fnref:4" class="footnote-back-ref">↩</a></li>
<li id="fn:5">van Oosten 2000, p. 6 <a href="#fnref:5" class="footnote-back-ref">↩</a></li>
<li id="fn:6">Birkedal 2000 <a href="#fnref:6" class="footnote-back-ref">↩</a></li>
<li id="fn:7">Krivine, Jean-Louis (2001). "Typed lambda-calculus in classical Zermelo-Fraenkel set theory". Archive for Mathematical Logic. 40 (2): 189–205. <a href="/wiki/Archive_for_Mathematical_Logic" target="_blank">/wiki/Archive_for_Mathematical_Logic</a> <a href="#fnref:7" class="footnote-back-ref">↩</a></li>
<li id="fn:8">Krivine, Jean-Louis (2011). "Realizability algebras: a program to well order R". Logical Methods in Computer Science. 7. <a href="/wiki/Logical_Methods_in_Computer_Science" target="_blank">/wiki/Logical_Methods_in_Computer_Science</a> <a href="#fnref:8" class="footnote-back-ref">↩</a></li>
<li id="fn:9">Seiller, Thomas (2024). Mathematical Informatics (Habilitation thesis). Université Sorbonne Paris Nord. <a href="https://theses.hal.science/tel-04616661" target="_blank">https://theses.hal.science/tel-04616661</a> <a href="#fnref:9" class="footnote-back-ref">↩</a></li>
<li id="fn:10">Girard, Jean-Yves (1989). "Geometry of interaction 1: Interpretation of System F". Studies in Logic and the Foundations of Mathematics. 127: 221–260. <a href="#fnref:10" class="footnote-back-ref">↩</a></li>
<li id="fn:11">Girard, Jean-Yves (2001). "Locus Solum: from the rules of logic to the logic of rules". Mathematical Structures in Computer Science. 11: 301–506. <a href="#fnref:11" class="footnote-back-ref">↩</a></li>
<li id="fn:12">Seiller, Thomas (2016). "Interaction graphs: Full linear logic". Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science. <a href="/wiki/Symposium_on_Logic_in_Computer_Science" target="_blank">/wiki/Symposium_on_Logic_in_Computer_Science</a> <a href="#fnref:12" class="footnote-back-ref">↩</a></li>
</ol>

Realizability open-in-new

Realizability