on math
Товарищи!
А кто читал Geometry of Interaction V: logic in the hyperfinite factor (Jean-Yves Girard) и может обьяснить ход мысли?
TLDR: люди ищут формализм, дуальный к традиционной математической нотации: «The aim of GoI is therefore to find a space where truth, commuting diagrams, etc. are no longer primitive and where dynamical processes (proof-search, rewriting, a.k.a. normalisation) are primitive»
Но эээ как же тяжело оно читается!
Занятные заметки оттуда:
Subjectivity has nothing to do with subjectivism; it is indeed its antidote. Let
us start with a famous example: Ptolemaic astronomy was the most «objec-
tive» science ever, allowing no room for the subject; however, it produced the
subjectivistic delirium of epicycles. Later on, Kepler, Galileo, were able to dis-
antangle this mess by restoring some subjectivity: observations are realtive to
a viewpoint, Earth.
A similar problem occurs in logic, especially when dealing with cognitive
questions: here the subject - the cognitive process - is part of the data. Take
the interesting remark that an absent information is false: a bank has no record
of its non-clients; handled subjectively, this works swell, since one can easily
determine whether or not the bank considers Mr. Girard as part of its clients.
The same idea, handled objectively, would amount at deciding whether or not
Mr. Girard is a client under, say, an assumed name, i.e., independently of any
cognitive process. The replacement of «I don’t know» by «one cannot know»,
i.e., «one cannot prove» led to those modern epicycles - non-monotonic logics,
closed world assumption, etc. -, which were refuted long before their invention
by incompleteness, which, in fine, exposes the limitations of a blunt objectivity.
A constructive9 approach thus requires to rebuild the objectivity by tak-
ing into account the subjective aspects of logic: after all, logic is about about
reasoning, language, etc. In contrast with the objectivistic fantasy known as
semantics.
For instance, formulas do no proceed from the sky; they proceed from their
own operationality. What can be internalised by means of the negation, which
thus takes in charge logical normativity: before refuting, negation forbids. This
idea of «negation as norm» was first implemented in ludics [9]: although the
expression has a game-theoretic flavour, ludics is strongly antagonistic to «game
semantics» which, as the name suggests, relies on a ready-made normativity,
thus missing the point.
GoI is even more radical, since it introduces a doubt - absent from ludics -
as to the underlying combinatoric universe. The idea being that, like in the
quantum world, logical artifacts interact «wavelike», but that questions like
truth are rather base-dependent, i.e., «measurement-like».
This approach can hardly be considered as subjectivistic. Typically, the
choice of a viewpoint is implicit in the statement of a problem: through the
decomposition of a formula into its significant subformulas - a decomposition
which suits our own analyticity, thus subjective. In practice, there will be a
preferred viewpoint - like in astronomy, the geocentric viewpoint -, but the
existence of other viewpoints - «non standard» ones, if the term were not too
heavily connoted - introduces unexpected possibilities of interpretation.
*9 Forget the sectarian connotation taken nowadays by this expression, which basically means
that object and subject must be constructed, do not preexist.
[9] J.-Y. Girard. Locus Solum. Mathematical Structures in Computer Sci-
ence, 11:301 - 506, 2001.
This entry was originally posted at http://wizzard.dreamwidth.org/381962.html. It has
comments. Please comment there using OpenID.
А кто читал Geometry of Interaction V: logic in the hyperfinite factor (Jean-Yves Girard) и может обьяснить ход мысли?
TLDR: люди ищут формализм, дуальный к традиционной математической нотации: «The aim of GoI is therefore to find a space where truth, commuting diagrams, etc. are no longer primitive and where dynamical processes (proof-search, rewriting, a.k.a. normalisation) are primitive»
Но эээ как же тяжело оно читается!
Занятные заметки оттуда:
Subjectivity has nothing to do with subjectivism; it is indeed its antidote. Let
us start with a famous example: Ptolemaic astronomy was the most «objec-
tive» science ever, allowing no room for the subject; however, it produced the
subjectivistic delirium of epicycles. Later on, Kepler, Galileo, were able to dis-
antangle this mess by restoring some subjectivity: observations are realtive to
a viewpoint, Earth.
A similar problem occurs in logic, especially when dealing with cognitive
questions: here the subject - the cognitive process - is part of the data. Take
the interesting remark that an absent information is false: a bank has no record
of its non-clients; handled subjectively, this works swell, since one can easily
determine whether or not the bank considers Mr. Girard as part of its clients.
The same idea, handled objectively, would amount at deciding whether or not
Mr. Girard is a client under, say, an assumed name, i.e., independently of any
cognitive process. The replacement of «I don’t know» by «one cannot know»,
i.e., «one cannot prove» led to those modern epicycles - non-monotonic logics,
closed world assumption, etc. -, which were refuted long before their invention
by incompleteness, which, in fine, exposes the limitations of a blunt objectivity.
A constructive9 approach thus requires to rebuild the objectivity by tak-
ing into account the subjective aspects of logic: after all, logic is about about
reasoning, language, etc. In contrast with the objectivistic fantasy known as
semantics.
For instance, formulas do no proceed from the sky; they proceed from their
own operationality. What can be internalised by means of the negation, which
thus takes in charge logical normativity: before refuting, negation forbids. This
idea of «negation as norm» was first implemented in ludics [9]: although the
expression has a game-theoretic flavour, ludics is strongly antagonistic to «game
semantics» which, as the name suggests, relies on a ready-made normativity,
thus missing the point.
GoI is even more radical, since it introduces a doubt - absent from ludics -
as to the underlying combinatoric universe. The idea being that, like in the
quantum world, logical artifacts interact «wavelike», but that questions like
truth are rather base-dependent, i.e., «measurement-like».
This approach can hardly be considered as subjectivistic. Typically, the
choice of a viewpoint is implicit in the statement of a problem: through the
decomposition of a formula into its significant subformulas - a decomposition
which suits our own analyticity, thus subjective. In practice, there will be a
preferred viewpoint - like in astronomy, the geocentric viewpoint -, but the
existence of other viewpoints - «non standard» ones, if the term were not too
heavily connoted - introduces unexpected possibilities of interpretation.
*9 Forget the sectarian connotation taken nowadays by this expression, which basically means
that object and subject must be constructed, do not preexist.
[9] J.-Y. Girard. Locus Solum. Mathematical Structures in Computer Sci-
ence, 11:301 - 506, 2001.
This entry was originally posted at http://wizzard.dreamwidth.org/381962.html. It has
comments. Please comment there using OpenID.