Stateful realizers for nonstandard analysis

2025-05-03 0 0 615.91KB 44 页 10玖币

侵权投诉

Logical Methods in Computer Science

Volume 19, Issue 2, 2023, pp. 7:1–7:44

https://lmcs.episciences.org/

Submitted Oct. 12, 2022

Published Apr. 25, 2023

STATEFUL REALIZERS FOR NONSTANDARD ANALYSIS

BRUNO DINIS aAND ´

ETIENNE MIQUEY b

aEscola de Ciˆencia e Tecnologia, Universidade de ´

Evora

e-mail address: bruno.dinis@uevora.pt

bAix-Marseille Universit´e, CNRS, I2M, Marseille, France

e-mail address: etienne.miquey@univ-amu.fr

Abstract.

In this paper we propose a new approach to realizability interpretations for

nonstandard arithmetic. We deal with nonstandard analysis in the context of (semi)

intuitionistic realizability, focusing on the Lightstone-Robinson construction of a model

for nonstandard analysis through an ultrapower. In particular, we consider an extension

of the

-calculus with a memory cell, that contains an integer (the state), in order to

indicate in which slice of the ultrapower

the computation is being done. We pay

attention to the nonstandard principles (and their computational content) obtainable in

this setting. In particular, we give non-trivial realizers to Idealization and a non-standard

version of the LLPO principle. We then discuss how to quotient this product to mimic the

Lightstone-Robinson construction.

1. Introduction

In this paper we propose a new approach to realizability interpretations for nonstandard

arithmetic. On the one hand, we deal with nonstandard analysis in the context of (semi)

intuitionistic realizability. On the other hand, we focus on Lightstone and Robinson’s

construction of a model for nonstandard analysis through an ultrapower [

LR75

]. This paper

is an extended version of [

DM21

]. The main novelties here are in Section 4.4, where we

establish a connection with evidenced frames [

CMT21

], and in Section 6, where we give a

realizer for a nonstandard version of the Lesser Limited Principle of Omniscience (LLPO).

We also now have a better understanding of why performing a quotient leads to some

counter-intuitive properties (cf. Section 7).

Throughout the history of mathematics, inﬁnitesimals were crucial for the intuitive

development of mathematical knowledge by authors such as Archimedes, Stevin, Fermat,

Key words and phrases: realizabiliy, nonstandard arithmetic, stateful computations, ultraﬁlters, glueing.

The authors would like to thank Alexandre Miquel for suggesting several ideas at the root of this work and

Valentin Blot and Mikhail Katz, as well as the anonymous reviewers of [

DM21

], for their accurate remarks

and suggestions. The ﬁrst author was supported by FCT - Funda¸c˜ao para a Ciˆencia e a Tecnologia, and the

research centers CMAFcIO - Centro de Matem´atica, Aplica¸c˜oes Fundamentais e Investiga¸c˜ao Operacional

and CIMA - Centro de Investiga¸c˜ao em Matem´atica e Aplica¸c˜oes – under the projects UIDB/04561/2020,

UIDP/04561/2020 and UIDP/04674/2020.

LOGICAL METHODS

IN COMPUTER SCIENCE DOI:10.46298/LMCS-19(2:7)2023 © B. Dinis and É. Miquey

Creative Commons

7:2 B. Dinis and ´

E. Miquey Vol. 19:2

Leibniz, Euler and Cauchy, to name but a few (see e.g. [

KS13

BBE+18

BBG+20

]). In

particular, in Leibniz’s Calculus one may recognize calculation rules – sometimes called the

Leibniz rules [

Lut87

Cal92

DvdB19

] – which correspond to heuristic intuitions for how the

inﬁnitesimals should operate under calculations: the sum and product of inﬁnitesimals is

inﬁnitesimal, the product of a limited number (i.e. not inﬁnitely large) with an inﬁnitesimal

is inﬁnitesimal,...

In [

Rob61

Rob66

] Robinson showed that, in the setting of model theory, it is possible

to extend usual mathematical sets (

, etc.) witnessing the existence of new elements,

the so-called nonstandard individuals. In this way, it is possible to deal consistently with

inﬁnitesimal and inﬁnitely large numbers via ultraproducts and ultrapowers, in a way that

is consistent with the Leibniz rules. Since the extended structures are nonstandard models

of the original structures, this new setting was dubbed nonstandard analysis.

These constructions are meant to simplify doing mathematics: notions like limits or

continuity can for instance be given a simpler form in nonstandard analysis. Later in

the 70s, Nelson developed a syntactical approach to nonstandard analysis, introducing in

particular three key principles: Idealization, Standardization and Transfer [

Nel77

]. The

validity of these principles for constructive mathematics has been studied in diﬀerent

settings, in particular, following some pioneer work by Moerdijk, Palmgren and Avigad

[

Moe95

MP97

Avi05

] in nonstandard intuitionistic arithmetic, several recent works, inspired

by Nelson’s approach, lead to interpretations of nonstandard theories in intuitionistic

realizability models [BBS12, DF17, HvdB17, DG18].

The very ﬁrst ideas of realizability are to be found in the Brouwer-Heyting-Kolmogorov

interpretation [

Hey34

Kol32

], which identiﬁes evidences and computing proofs (the realizers).

Realizability was designed by Kleene to interpret the computational content of the proofs

of Heyting arithmetic [

Kle45

], and was later extended to more expressive frameworks

[

G¨o58

Kre51

Kri09

]. While the Curry-Howard isomorphism focuses on a syntactical

correspondence between proofs and programs, realizability rather deals with the (operational)

semantics of programs: a realizer of a formula

is a program which computes adequately

with the speciﬁcation that

provides. As such, realizability constitutes a technique to

develop new models of a wide class of theories (from Heyting arithmetic to Zermelo-Fraenkel

set theory), whose algebraic structures has been studied in [vO08, Kri16, Miq20].

With the development of his classical realizability, Krivine evidences the fact that

extending the

-calculus with new programming instructions may result in getting new

reasoning principles:

call/cc

to get classical logic [

Gri90

Kri09

quote

for dependent choice

[

Kri01

], etc. In this paper, we follow this path to show how the addition of a monotonic

reference allows us to get a realizability interpretation for nonstandard analysis. The

realizability interpretation proposed here can be understood as a computational interpretation

of the ultraproduct construction in [

LR75

], where the value of the reference indicates the

slice of the product in which the computation takes place. In particular, we obtain a realizer

for the Idealization principle whose computational behaviour increases the reference in the

manner of a diagonalization process. Our setting turns out to be semi-intuitionistic since it

allows to deduce a rather non-trivial realizer for a nonstandard version of the nonconstructive

Lesser Limited Principle of Omniscience [BR87].

Outline.

We start this paper by recalling the main ideas of the ultraproduct construction

(Section 2) and the deﬁnition of a standard realizability interpretation for second-order

Heyting arithmetic (Section 3). We then introduce stateful computations and our notion of

Vol. 19:2 STATEFUL REALIZERS FOR NONSTANDARD ANALYSIS 7:3

realizability with slices in Section 4. We also show that our stateful interpretation induces

an evidenced frame thus providing a connection with the usual algebraic tools to deal with

realizability interpretations. As shown in Section 5 and Section 6, this interpretation provides

us with realizers for several nonstandard reasoning principles. We discuss the possibility of

taking a quotient for this interpretation in Section 7. We conclude the paper in Section 8

with a comparison to related work and with some questions left for future work.

2. The ultrapower construction

The main contribution of this paper consists in deﬁning a realizability interpretation to

give a computational content to the ultrapower construction of Robinson and Lightstone

in [

LR75

]. We shall begin by brieﬂy explaining how this construction works in the realm of

model theory.

Let us start by recalling some deﬁnitions.

Deﬁnition 2.1. Let Ibe a set. We say that F ⊂ P(I) is a ﬁlter over Iif:

(i)Fis non empty and ∅/∈ F (non triviality)

(ii) for all F1, F2∈ F,F1∩F2∈ F (closure under intersection)

(iii) for any F, G ∈ P(I), if F∈ F and F⊂G, then G∈ F (upwards closure)

An ultraﬁlter is a ﬁlter

such that for any

F∈ P

(

), either

or its complement

are in

For instance, the set of coﬁnite subsets of

deﬁnes the so-called Fr´echet ﬁlter, which is

not an ultraﬁlter since it contains neither the set of even natural numbers nor the set of odd

natural numbers. Nonetheless, it is well-known that any ﬁlter

over an inﬁnite set

contained in an ultraﬁlter

over

: this is the so-called ultraﬁlter principle. An ultraﬁlter

that contains the Fr´echet ﬁlter is called a free ultraﬁlter. The existence of free ultraﬁlters

was proved by Tarski in 1930 [Tar30] and is in fact a consequence of the Axiom of Choice.

Deﬁnition 2.2.

Given two sets

and

and an ultraﬁlter

over

, we can deﬁne an

equivalence relation

∼

over

u∼

=Uv,{i∈I

vi}∈U

. We write

VI/U

for the

set obtained by performing a quotient on the set

by this equivalence relation, which is

called an ultrapower.

Consider a theory

(say ZFC) and its language

, for which we assume the existence

of a model

. The goal is to build a nonstandard model

M∗

of the theory

that validates

new principles. Let us denote by

the set which interprets individuals in

, and let us

ﬁx a free ultraﬁlter

over

. Roughly speaking, the new model

M∗

is deﬁned as the

ultrapower

MN/U

. Individuals are interpreted by functions in

while the validity of a

relation R(x1, ..., xk) (where the xiare interpreted by fi, for i∈ {1, ..., k}) is deﬁned by

M∗R(f1, ..., fk) iﬀ {n∈N:MR(f1(n), ..., fk(n))}∈U.

We can now extend the language with a new predicate

(

) to express that

is standard.

Standard elements are deﬁned as the ones that, with respect to

∼

, are equivalent to constant

functions, i.e.

M∗st

(

) if and only if there exists

p∈N

such that

{n∈N

(

) =

p}∈U

M∗st(f) iﬀ ∃p∈N.{n∈N:f(n) = p} ∈ U.

Formulas that involve this new predicate are called external, while formulas of the original

language Lare called internal.

7:4 B. Dinis and ´

E. Miquey Vol. 19:2

Lightstone and Robinson’s construction relies on the well-known

o´s ’ theorem [

Lo60

]

which states that if

is an internal formula (with parameters in

), then

M∗ϕ

if and

only

{n∈N

Mϕn} ∈ U

, where

ϕn

refers to the formula

whose parameters have

been replaced by their values in

. This construction indeed deﬁnes a model of

which

satisﬁes other relevant properties, namely Transfer, Idealization and Standardization. As a

consequence of

o´s ’ theorem, to see that an internal formula

(

) holds for all elements,

it is enough to see that it holds for all standard elements: this is the Transfer principle.

In our setting, Idealization amounts to a diagonalization process: it is for instance easy to

see that if one deﬁnes

n7→ n

(where we, with abuse of notation, write

for both the

natural number

and its interpretation in

), then

M∗∀x.

(

)

→x < δ

). Finally,

Standardization is a sort of “comprehension scheme” which states that we can specify subsets

of standard sets by giving a membership criterion for standard elements (by means of an

internal formula).

3. Realizability in a nutshell

3.1.

Heyting second-order arithmetic.

We start by introducing the terms and formulas

of Heyting second-order arithmetic (HA2), for which we follow Miquel’s presentation [

Miq11a

Second-order formulas are build on top of ﬁrst-order arithmetical expressions, by means

of logical connectives, ﬁrst- and second-order quantiﬁcations and primitive predicates. We

use upper case letters for second-order variables and lower case letters for ﬁrst-order ones.

We use a primitive predicate

Nat

(

) to denote that

is a natural number (0 then has type

Nat

(0) and the term s

has type

Nat

(

)) provided that

has type

Nat

(

)). We consider

the usual

-calculus terms extended with pairs, projections (written

πi

), natural numbers

and a recursion operator:

1st-order expressions e::= x|0|S(e)|f(e1, . . . , en)

Formulas A, B ::= Nat(e)|X(e1, . . . , en)|A→B|A∧B

| ∀x.A | ∃x.A | ∀X.A | ∃X.A

Terms t, u ::= x|0|s|rec |λx.t |t u |(t, u)|π1(t)|π2(t)

where

Nn→N

is any arithmetical function. We write Λ for the set of all closed

-terms.

Note that we did not include disjunctions as formulae. In fact, for most of our purposes,

disjunctions are not needed. The only exception is Section 6 where we interpret a nonstandard

version of the Lesser Limited Principle of Omniscience. It is however possible to include

disjunctions all the way but, since this would mostly only add some unnecessary technicalities

to all our proofs, we delay the introduction of disjunction until Section 6.

To simplify the use of existential quantiﬁers, as in [

Miq11a

], we introduce a congruence

relation on formulas deﬁned by the following rules

(∃x.A)→B∼

=∀x.(A→B) (∃X.A)→B∼

=∀X.(A→B) (3.1)

This congruence relation allows us to, given any typed term, to (re)type it with any formula

congruent to the original one. In particular, this means that we do not need the elimination

rules for the existential quantiﬁers, which results in a simpliﬁed type system. This type

system, which is given in Figure 1, corresponds to the usual rules of natural deduction. The

reader may observe that we do not give computational content to quantiﬁcations.

Vol. 19:2 STATEFUL REALIZERS FOR NONSTANDARD ANALYSIS 7:5

Natural numbers Γ`0 : Nat(0) (0) Γ`s:∀N

x.Nat(S(x)) (S)

Γ`rec :∀Z.Z(0) →(∀N

y.(Z(y)→Z(S(y)))) → ∀N

x.Z(x)(rec)

Logical rules (x:A)∈Γ

Γ`x:A(Ax)Γ`t:A→BΓ`u:A

Γ`t u :B(→E)

Γ, x :A`t:B

Γ`λx . t :A→B(→I)Γ`t:AΓ`u:B

Γ`(t, u) : A∧B(∧I)Γ`t:A∧B

Γ`π1(t) : A(∧1

Γ`t:A∧B

Γ`π2(t) : B(∧2

E)Γ`t:A[x:= n]

Γ`t:∃x.A (∃1

I)Γ`t:∀x.A

Γ`t:A[x:= n](∀1

Γ`t:A x /∈F V (Γ)

Γ`t:∀x.A (∀1

I)Γ`t:A[X(x1, . . . , xn) := B]

Γ`t:∃X.A (∃2

Γ`t:∀X.A

Γ`t:A[X(x1, . . . , xn) := B](∀2

E)Γ`t:A X /∈F V (Γ)

Γ`t:∀X.A (∀2

I)Γ`t:A0A∼

=A0

Γ`t:A(∼

Figure 1: Type system

In the sequel, we make use of the following usual abbreviations:

sn+10,s(sn0)

n,sn0

>,∃X.X

⊥,∀X.X

¬A,A→ ⊥

e=e0,∀Z.(Z(e)→Z(e0))

∀N

x.A ,∀x.(Nat(x)→A)

∃N

x.A ,∃x.(Nat(x)∧A)

It is well-known that the above deﬁnition of equality (often called Leibniz law) enjoys

the usual expected properties (reﬂexivity, symmetry, transitivity) and allows to perform

substitution of equal terms. The quantiﬁcations

∀N

x.A

and

∃N

x.A

are often said to be

relativized to natural numbers.

The one-step (weak) reduction over terms is deﬁned by the following rules:

(λx.t)u βt[u/x]rec u0u10βu0rec u0u1(st)βu1t(rec u0u1t)

π1(t, u)βt π2(t, u)βu

We write

→β

for the congruent reﬂexive-transitive closure of

β

. The reduction

→β

is known

to be conﬂuent, type-preserving and normalizing on typed terms [Bar92].

3.2.

Realizability interpretation of HA2.

In this subsection we deﬁne the realizability

interpretation of the type system deﬁned in Figure 1, in which formulas are interpreted as

saturated sets of terms, i.e. as sets of closed terms

S⊆

Λ such that

t→βt0

and

t0∈S

imply

that

t∈S

. We write

SAT

to denote the set of all saturated sets and, given a formula

, we

call truth value its realizability interpretation.

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

LogicalMethodsinComputerScienceVolume19,Issue2,2023,pp.7:17:44https://lmcs.episciences.org/SubmittedOct.12,2022PublishedApr.25,2023STATEFULREALIZERSFORNONSTANDARDANALYSISBRUNODINISaANDETIENNEMIQUEYbaEscoladeCi^enciaeTecnologia,UniversidadedeEvorae-mailaddress:bruno.dinis@uevora.ptbAix-MarseilleUn...

展开>> 收起<<

Stateful realizers for nonstandard analysis.pdf

共44页,预览5页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

Stateful realizers for nonstandard analysis

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: