Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userClassical Mathematics for a Constructive World
134
0
0.0
(
0
)
Added by
Russell O'Connor
Publication date
2010
fields
Informatics Engineering
and research's language is
English
Authors
Russell OConnor
Ask ChatGPT about the research
No Arabic abstract
Interactive theorem provers based on dependent type theory have the flexibility to support both constructive and classical reasoning. Constructive reasoning is supported natively by dependent type theory and classical reasoning is typically supported by adding additional non-constructive axioms. However, there is another perspective that views constructive logic as an extension of classical logic. This paper will illustrate how classical reasoning can be supported in a practical manner inside dependent type theory without additional axioms. We will see several examples of how classical results can be applied to constructive mathematics. Finally, we will see how to extend this perspective from logic to mathematics by representing classical function spaces using a weak value monad.
rate research
Read More
We show that numerous distinctive concepts of constructive mathematics arise automatically from an antithesis translation of affine logic into intuitionistic logic via a Chu/Dialectica construction. This includes apartness relations, complemented subsets, anti-subgroups and anti-ideals, strict and non-strict order pairs, cut-valued metrics, and apartness spaces. We also explain the constructive bifurcation of some classical concepts using the choice between multiplicative and additive affine connectives. Affine logic and the antithesis construction thus systematically constructivize classical definitions, handling the resulting bookkeeping automatically.
We study a conservative extension of classical propositional logic distinguishing between four modes of statement: a proposition may be affirmed or denied, and it may be strong or classical. Proofs of strong propositions must be constructive in some sense, whereas proofs of classical propositions proceed by contradiction. The system, in natural deduction style, is shown to be sound and complete with respect to a Kripke semantics. We develop the system from the perspective of the propositions-as-types correspondence by deriving a term assignment system with confluent reduction. The proof of strong normalization relies on a translation to System F with Mendler-style recursion.
Proposed initially from a practical circumstance, the traveling salesman problem caught the attention of numerous economists, computer scientists, and mathematicians. These theorists were instead intrigued by seeking a systemic way to find the optimal route. Many attempts have been made along the way and all concluded the nonexistence of a general algorithm that determines optimal solution to all traveling salesman problems alike. In this study, we present proof for the nonexistence of such an algorithm for both asymmetric (with oriented roads) and symmetric (with unoriented roads) traveling salesman problems in the setup of constructive mathematics.
In this paper we provide two new semantics for proofs in the constructive modal logics CK and CD. The first semantics is given by extending the syntax of combinatorial proofs for propositional intuitionistic logic, in which proofs are factorised in a linear fragment (arena net) and a parallel weakening-contraction fragment (skew fibration). In particular we provide an encoding of modal formulas by means of directed graphs (modal arenas), and an encoding of linear proofs as modal arenas equipped with vertex partitions satisfying topological criteria. The second semantics is given by means of winning innocent strategies of a two-player game over modal arenas. This is given by extending the Heijltjes-Hughes-Stra{ss}burger correspondence between intuitionistic combinatorial proofs and winning innocent strategies in a Hyland-Ong arena. Using our first result, we provide a characterisation of winning strategies for games on a modal arena corresponding to proofs with modalities.
We present a formalisation in Agda of the theory of concurrent transitions, residuation, and causal equivalence of traces for the pi-calculus. Our formalisation employs de Bruijn indices and dependently-typed syntax, and aligns the proved transitions proposed by Boudol and Castellani in the context of CCS with the proof terms naturally present in Agdas representation of the labelled transition relation. Our main contributions are proofs of the diamond lemma for the residuals of concurrent transitions and a formal definition of equivalence of traces up to permutation of transitions. In the pi-calculus transitions represent propagating binders whenever their actions involve bound names. To accommodate these cases, we require a more general diamond lemma where the target states of equivalent traces are no longer identical, but are related by a braiding that rewires the bound and free names to reflect the particular interleaving of events involving binders. Our approach may be useful for modelling concurrency in other languages where transitions carry metadata sensitive to particular interleavings, such as dynamically allocated memory addresses.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
