Strong negation in the Theory of Computable Functionals TCF
2025-04-24
0
0
507.25KB
28 页
10玖币
侵权投诉
Logical Methods in Computer Science
Volume 21, Issue 2, 2025, pp. 1:1–1:28
https://lmcs.episciences.org/
Submitted May 30, 2023
Published Apr. 04, 2025
STRONG NEGATION IN THE
THEORY OF COMPUTABLE FUNCTIONALS TCF
NILS K ¨
OPP AND IOSIF PETRAKIS
aLudwig-Maximilians Universit¨at, Theresienstr. 39, 80333, M¨unchen
e-mail address: koepp@math.lmu.de
bUniversit`a di Verona, Strada le Grazie 15, 37134, Verona
e-mail address: iosif.petrakis@univr.it
Abstract.
We incorporate strong negation in the theory of computable functionals
TCF
,
a common extension of Plotkin’s PCF and G¨odel’s system T, by defining simultaneously
strong negation
AN
of a formula
A
and strong negation
PN
of a predicate
P
in
TCF
. As a
special case of the latter, we get strong negation of an inductive and a coinductive predicate
of
TCF
. We prove appropriate versions of the Ex falso quodlibet and of double negation
elimination for strong negation in
TCF
. We introduce the so-called tight formulas of TCF
i.e., formulas implied by the weak negation of their strong negation, and the relative tight
formulas. We present various case-studies and examples, which reveal the naturality of our
definition of strong negation in
TCF
and justify the use of TCF as a formal system for a
large part of Bishop-style constructive mathematics.
1. Introduction
In constructive (and classical) logic negation
¬A
of a formula
A
is defined in a negative way
as the implication
A→ ⊥
, where
⊥
denotes “falsum”. Constructively though,
¬A
has a
weak behaviour, as the negation of a conjunction
¬
(
A∧B
) does not generally imply the
disjunction
¬A∨ ¬B
, and similarly the negation of a universal formula
¬∀xA
(
x
) does not
generally imply the existential formula
∃x¬A
(
x
). Even if
A
and
B
are stable i.e.,
¬¬A→A
and
¬¬B→B
, we only get
¬
(
A∧B
)
⊢ ¬¬
(
¬A∨ ¬B
) and
¬∀xA
(
x
)
⊢ ¬¬∃x¬A
(
x
), where
⊢
is the derivability relation in minimal logic. For this reason,
¬A
is called the weak negation
of
A
, which, according to Rasiowa [
Ras74
], p. 276, is not constructive, exactly due to its
aforementioned behaviour.
In contrast to weak negation, and in analogy to the use of a strong “or” and “exists” in
constructive logic, Nelson [
Nel49
] introduced the strong negation
∼A
of
A
. Following Kleene’s
recursive realisability, Nelson developed constructive arithmetic with strong negation and
showed that it has the same expressive power as Heyting arithmetic. Within Nelson’s
realisability, the equivalences
∼
(
A∧B
)
⇔ ∼A∨ ∼ B
and
∼∀xA
(
x
)
⇔ ∃x∼A
(
x
) are
realisable. In axiomatic presentations of constructive logic with strong negation (
CLSN
)
(see [
Ras74
,
Gur77
]) these equivalences are axiom schemes. In most formalisations of
CLSN
,
Key words and phrases: higher-order computability, constructive mathematics, strong negation.
LOGICAL METHODS
IN COMPUTER SCIENCE DOI:10.46298/LMCS-21(2:1)2025
© N. Köpp and I. Petrakis
CC
⃝Creative Commons
1:2 N. K¨
opp and I. Petrakis Vol. 21:2
but not in all (see system N4 in [
AN84
]), strong negation
∼A
implies weak negation
¬A
.
Markov [
Mar50
] expressed weak negation through strong negation and implication as follows:
¬A
:=
A→ ∼A.
Rasiowa [
Ras74
] went even further, introducing a strong implication
A⇒B
, defined through the standard “weak” implication
→
and strong negation as follows:
A⇒B
:= (
A→B
)
∧
(
∼B→ ∼A
)
.
The various aspects of the model theory of
CLSN
are
developed in many papers (see e.g., [Gur77, Aka88, SV08b, SV08a]).
The critique of weak negation in intuitionistic logic and later constructive mathematics
(
CM
) goes back to Kolmogorov [
Kol
], it motivated Johanssen to develop minimal logic [
Joh37
]
and Griss to consider negationless mathematics [
Gri46
] altogether. Despite the use of
weak negation in Brouwer’s intuitionistic mathematics (
INT
) and Bishop’s constructive
mathematics (
BISH
), both, Brouwer and Bishop, developed a positive and strong approach
to many classically negatively defined concepts. An apartness relation
̸
=
X
on a set (
X,
=
X
)
is strong counterpart to the weak negation
¬
(
x
=
Xx′
) of its equality, strong complement
A̸=
:=
{x∈X| ∀a∈A
(
x̸
=
Xa
)
}
of a subset
A
of
X
is the positive version of its standard,
weak complement
1Ac
:=
{x∈X| ∀a∈A
(
¬
(
x
=
Xa
))
}
, inhabited sets are strong, non-empty
sets, and so on. Recently, Shulman [
Shu22
] showed that most of these strong concepts of
BISH
“arise automatically from an “antithesis” translation of affine logic into intuitionistic
logic via a “Chu/Dialectica construction”. Motivated by this work of Shulman, and in
relation to a reconstruction of the theory of sets underlying
BISH
(see [
Pet20b
,
Pet21
,
Pet22
]
and [
PW22
,
MWP24
]), the second author develops (in a work in progress) a treatment of
strong negation within
BISH
, arriving in a heuristic method for the definition of these strong
concepts of
BISH
similar to Shulman’s. For that, the equivalences occurring in the axiom
schemata related to strong negation in
CLSN
become the definitional clauses of the recursive
definition of ∼A, with respect to the inductive definition of formulas Ain BISH.
This idea of a recursive definition of strong negation is applied here to the formal
theory of computable functionals
TCF
, developed mainly by Schwichtenberg in [
SW12
].
TCF
is a common extension of Plotkin’s PCF and G¨odel’s system T, it uses, in contrast to
Scott’s LCF, non-flat free algebras as semantical domains for the base types, and for higher
types its intended model consists of the computable functions on partial continuous objects
(see [
SW12
], Chapter 7). Furthermore, it accommodates inductively and coinductively
defined predicates and its underlying logic is minimal.
TCF
is the theoretical base of
the proof assistant Minlog [
Sch24
] with which the extraction of computational content of
formalised proofs is made possible. A significant feature of
TCF
is its relation to
CM
, as
many parts of
BISH
have already been formalised in
TCF
and implemented in Minlog (see
e.g., [Sch09, Sch22, Sch23]).
A novelty of the definition of strong negation
AN
of a formula
A
of
TCF
is its extension,
by the first author, to inductive and coinductive predicates. Moreover, the analysis of strong
negation in the informal system of non-inductive
2
, constructive mathematics
BISH
given by
1
In this case
A
is considered to be an extensional subset of
X
i.e., it is defined by separation on
X
with
respect to an extensional property on X.
2
Bishop’s informal system of constructive mathematics BISH can be seen as a system that does not
accommodate inductive definitions. Although the inductive definitions of Borel sets and of the least function
space generated by a set of real-valued functions on a set are found in [
Bis67
], Bishop’s original measure
theory was replaced later by the Bishop-Cheng measure theory that avoids the inductive definition of Borel
sets, and the theory of function spaces was never elaborated by Bishop (it was developed by the second
author much later). It is natural to consider the extension BISH
∗
of BISH as Bishop’s informal system of
constructive mathematics with inductive definitions given by rules with countably many premises.
Vol. 21:2 STRONG NEGATION IN TCF 1:3
the second author is reflected and extended here in the study of strong negation within the
formal system
TCF
, as results and concepts of the former are translated and extended in
the latter. We structure this paper as follows:
•
In Section 2 we briefly describe
TCF
: its predicates and formulas, its derivations and
axioms, Leibniz equality, and weak negation.
•
In Section 3 strong negation
AN
of a formula
A
of
TCF
is defined by recursion on the
definition of formulas of
TCF
. This definition is extended to the definition of strong
negation
PN
of a predicate
P
of
TCF
(Definition 3.2). As a special case of the latter, we
get strong negation of an inductive and a coinductive predicate of TCF .
•
In Section 4 we prove some fundamental properties of
AN
in
TCF
. Among others,
we show an appropriate version of the Ex-falso-quodlibet (Lemma 4.3) and of double
negation elimination shift for strong negation (Theorem 4.6). We also explain why there
is no uniform way to define
AN
(Proposition 4.11), and we incorporate Rasiowa’s strong
implication in
TCF
. Finally, we show that weak and strong negation are classically
equivalent (using Lemma 4.3 and Lemma 4.15).
•
Motivated by the concept of a tight apartness relation in
CM
, in Section 5 we introduce
the so-called tight formulas of
TCF
i.e., the formulas
A
of
TCF
for which the implication
¬
(
AN
)
→A
is derivable in minimal logic. As in the partial setting of
TCF
very few
non-trivial formulas are tight, the introduced notion of relative tightness is studied (see
Proposition 5.5 and Lemma 5.6).
•
In Section 6 some important case-studies and examples are considered that reveal the
naturality of our main Definition 3.2. Furthermore, they justify the use of
TCF
as a
formal system for a large part of
BISH
, since the use of strong negation in
TCF
reflects
accurately the seemingly ad hoc definitions of strong concepts in BISH.
2. The Theory of Computable Functionals TCF
In this section we describe the theory of computable functionals
TCF
. For all notions and
results on
TCF
that are used here without further explanation or proof, we refer to [
SW12
].
The term-system of TCF, T
+
, is an extension of G¨odels T. Namely, the simple types
are enriched with free algebras
ι
, generated by a list of constructors, as extra base types.
Particularly, we have the usual strictly positive data-types, for example
N:=⟨0:N,S:N_N⟩, α ×β:=⟨[,] : α_β_α×β⟩.
Moreover, nesting into already defined algebras with parameters is allowed e.g., given lists
L
(
α
) and boole
B
, the finitely branching boolean-labelled and number-leafed trees is defined
via the algebra Twith constructors
Leaf :N_T,Branch :L[α/T]×B_T.
The term-system T
+
is simple-typed lambda-calculus. The constants are constructors or
program constants
D
:
⃗ρ _τ
, defined by a system of consistent left-to-right computation
rules. Particularly, we have recursion and corecursion operators
Rι
respectively,
coRι
, and
the destructor
Dι
for any free algebra
ι
. In that sense, it is regarded as an extension of
G¨odels T. In general terms are partial and if needed, computational properties e.g., totality
have to be asserted by proof.
1:4 N. K¨
opp and I. Petrakis Vol. 21:2
Definition 2.1 (Types and terms).We assume countably many distinct type-variable-names
α, β, γ, ξ
and term-variable-names
xρ, yρ
for every type
ρ
. Then we inductively define
Y
and
T+by the following rules:
ρ, σ, τ ∈ Y ::=α, β, γ, ξ ρ_σι:=⟨Ci:⃗ρi[β/ι]_ι⟩i<k,
t, s ∈T+::=xρ, yρ(λxρtσ)ρ_σ(tρ_σsρ)σC⃗ρi→ι
iD⃗ρ_τ.
•
For a constructor
Ci
:
⃗ρi
[
β/ι
]
_ι
we require that
β
occurs at most strictly positive in all
its k < |⃗ρi|argument-types ρik (β)
•
A program constant
D
:
⃗ρ _σ
is introduced by
i < k
computation rules
DP⃗ρ
i
:=
tσ
i
, where
Pi
is a constructor pattern namely, a list of term expressions built up using only variables
and constructors.
•Consistency is ensured, by requiring that there is no unification for Pi, Pj, if i̸=j.
• Y
and T
+
are closed under substitution and types, respectively terms are viewed as
equivalent with respect to bound renaming. Terms are identified according to beta
equivalence (λxt)s=t[x/s] and computation rules.
Example 2.2. We have the following algebras:
B:=⟨f:B,t:B⟩(boole),
L(α):=⟨[ ] : L(α),:: : α_L(α)_L(α)⟩(lists).
For the algebra
N
we also use roman numerals e.g.,
1
=
S0
. We introduce a program constant
natbin
:
N_N_L
[
B
], such that
natbin n m
computes a binary representation of
n
+ 2
m
and it is defined by the following rules:
nbin 0 0 = [ ],
nbin 0 Sk=f:: (nbin Sk0),
nbin 1 k=t:: (nbin k0),
nbin SSn k =nbin nSk.
For non-nested algebras with nullary constructor, the total terms are finite expressions
consisting only of constructors. For the type N, total terms are exactly of the form
0,S0,...,(S· · · S
|{z}
ntimes
)0, . . . .
Similar, cototal terms are all finite or infinite constructors-expressions. For the type of unary
natural number, the only non-total, cototal term is
∞=SSS · · · ,
which has the property
∞
=
S∞
. For lists of natural numbers,
L
(
N
), there are (countably)
many non-total and cototal terms, e.g., constant infinite lists n:n:· · · , or
1:2:3:4· · · ,2:3:5:· · · : (n−th prime) : ((n+ 1)(−th prime) · · · .
To assert properties of programs i.e., totality or correctness, we need the corresponding
formulas. E.g., the intended domain of
nbin
above are all finite natural numbers. Formally
we introduce a predicate TNwith
0∈TN,∀n(n∈TN→((Sn)∈TN)),
Vol. 21:2 STRONG NEGATION IN TCF 1:5
and it is the smallest predicate with this property i.e.,
0∈P→ ∀n∈TN(n∈P→(Sn)∈P)→TN⊆P.
Generally, formulas and predicates of TCF are structurally parallel to types and algebras,
though with additional term-dependency. Namely, we introduce inductive and co-inductive
predicates as least respectively, greatest fixed-point of clauses i.e., formulas of the form
∀⃗x(A0→ · · · → Ak−1→X⃗
t) which are also called clauses.
Formulas are generated by universal quantification
∀
and implication
→
. The logical
connectives ∧,∨and ∃are special cases of inductive predicates, but here, for the clarity of
the presentation, we prefer to introduce them as primitives.
Definition 2.3 (Predicates and formulas).We assume countably many predicate-variables
X
for any arity
⃗ρ
. We simultaneously define formulas
A, B ∈ F
and predicates
P, Q ∈ P
by
the following rules:
P::=X{⃗x |A}I:=µX⃗
KJ:=νX⃗
K,
F::=P⃗
tA⋄B⋄∈{→,∧,∨} ∇xA∇∈{∀,∃}.
•
Sometimes variable-dependencies will be emphasized by writing the variable-name, in
parantheses, directly behind an expression e.g., νY⃗
K(Y).
•I:=µX⃗
Kdenotes the least fix-point closed under the clauses ⃗
K.
•
J
:
=
νX⃗
K
denotes the greatest fixed-point closed under the clauses
⃗
K
A clause or
introductory rule
Ki
(
X
) of a fixed-point must be a closed formula of the form
Ki
=
∀⃗x
(
⃗
Ai
(
X
)
→X⃗
ti
), where
X
occurs at most strictly positive in all premises
Aik
(
X
) and
⃗
ti:⃗ρ a list of terms.
•
We refer to
{⃗x⃗σ |A
(
⃗x
)
}
, where
⃗x
are exactly the free term-variables of
A
, as a com-
prehension term. It is a predicate of arity
⃗σ
and we identify the formulas
{⃗x |A}⃗y
and
A[⃗x/⃗y].
•
Term and type-substitution extends to predicates. Formulas and predicates are closed
under (admissible) simultaneous substitutions for type-, term- and predicate-variables.
Given two predicates P, Q of the same arity, we use the following abbreviations.
P∩Q:={⃗x |P ⃗x ∧Q⃗x}, P ∪Q:={⃗x |P ⃗x ∨Q⃗x},
P⊆Q:=∀⃗x(P ⃗x →Q⃗x).
Furthermore, for any formula or predicate, we associate the following collections of predicate
variables:
•at most strictly positive: SP(·),
•strictly positive and free: PP(·),
•strictly negative and free: NP(·),
•freely occurring: FP(·).
摘要：
展开>>
收起<<
LogicalMethodsinComputerScienceVolume21,Issue2,2025,pp.1:1–1:28https://lmcs.episciences.org/SubmittedMay30,2023PublishedApr.04,2025STRONGNEGATIONINTHETHEORYOFCOMPUTABLEFUNCTIONALSTCFNILSK¨OPPANDIOSIFPETRAKISaLudwig-MaximiliansUniversit¨at,Theresienstr.39,80333,M¨unchene-mailaddress:koepp@math.lmu.de...
声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！
相关推荐
-
【词汇变形总汇】2025高考词汇变形总汇 - 教师版VIP免费
2024-12-06 3 -
【超简37页】新课标高考英语考纲3500词汇VIP免费
2024-12-06 4 -
《高考英语3500词详解》（WORD版）VIP免费
2024-12-06 13 -
《高考英语3500词详解》VIP免费
2024-12-06 11 -
高中英语-[教师版]80天通关高考3500词汇VIP免费
2024-12-06 12 -
高中人教选修7课文逐句翻译VIP免费
2024-12-06 7 -
高中人教选修7课文原文及翻译VIP免费
2024-12-06 13 -
高中人教必修4课文逐句翻译VIP免费
2024-12-06 7 -
高中人教必修4课文原文及翻译VIP免费
2024-12-06 13 -
高考英语核心高频688词汇VIP免费
2024-12-06 10
分类：图书资源
价格：10玖币
属性：28 页
大小：507.25KB
格式：PDF
时间：2025-04-24
作者详情
相关内容
-
3-专题三 牛顿运动定律 2-教师专用试题
分类：中学教育
时间：2025-04-07
标签：无
格式：DOCX
价格：5.9 玖币
-
2-专题二 相互作用 2-教师专用试题
分类：中学教育
时间：2025-04-07
标签：无
格式：DOCX
价格：5.9 玖币
-
6-专题六 机械能 2-教师专用试题
分类：中学教育
时间：2025-04-07
标签：无
格式：DOCX
价格：5.9 玖币
-
4-专题四 曲线运动 2-教师专用试题
分类：中学教育
时间：2025-04-08
标签：无
格式：DOCX
价格：5.9 玖币
-
5-专题五 万有引力与航天 2-教师专用试题
分类：中学教育
时间：2025-04-08
标签：无
格式：DOCX
价格：5.9 玖币
渝公网安备50010702506394
