Constructive Proofs of some Positivstellensätze for Compact Semialgebraic Subsets of ℝ d

2013 ◽  
Vol 158 (2) ◽  
pp. 410-418 ◽  
Author(s):  
Gennadiy Averkov
Keyword(s):  
Constructive Proofs

scholarly journals Feasibly constructive proofs of succinct weak circuit lower bounds

2020 ◽  
Vol 171 (2) ◽  
pp. 102735
Author(s):  
Moritz Müller ◽  
Ján Pich
Keyword(s):  
Lower Bounds ◽  
Circuit Lower Bounds ◽  
Constructive Proofs

scholarly journals Strongly uniform bounds from semi-constructive proofs

2006 ◽  
Vol 141 (1-2) ◽  
pp. 89-107 ◽  
Author(s):  
Philipp Gerhardy ◽  
Ulrich Kohlenbach
Keyword(s):  
Uniform Bounds ◽  
Constructive Proofs

scholarly journals Boundary Topological Entanglement Entropy in Two and Three Dimensions

2021 ◽  
Author(s):  
Jacob C. Bridgeman ◽  
Benjamin J. Brown ◽  
Samuel J. Elman
Keyword(s):  
General Property ◽  
Entanglement Entropy ◽  
Quantum Correlations ◽  
Three Dimensions ◽  
Topological Phases ◽  
Fusion Categories ◽  
Special Cases ◽  
Constructive Proofs ◽  
And Algebra ◽  
Topological Entanglement Entropy

AbstractThe topological entanglement entropy is used to measure long-range quantum correlations in the ground space of topological phases. Here we obtain closed form expressions for the topological entropy of (2+1)- and (3+1)-dimensional loop gas models, both in the bulk and at their boundaries, in terms of the data of their input fusion categories and algebra objects. Central to the formulation of our results are generalized $${\mathcal {S}}$$ S -matrices. We conjecture a general property of these $${\mathcal {S}}$$ S -matrices, with proofs provided in many special cases. This includes constructive proofs for categories up to rank 5.

Interpretations of Kleene's metamathematical predicate Γ ∣ a in intuitionistic arithmetic

1965 ◽  
Vol 30 (2) ◽  
pp. 140-154 ◽  
Author(s):  
T. Thacher Robinson
Keyword(s):  
Predicate Calculus ◽  
Sufficient Condition ◽  
Necessary And Sufficient Condition ◽  
Recursive Functions ◽  
Finite Sequences ◽  
Constructive Proofs ◽  
Necessary And Sufficient ◽  
Intuitionistic Arithmetic

Let Pp, Pd, and N be the intuitionistic systems of prepositional calculus, predicate calculus, and elementary arithmetic, respectively, described in [3].Kleene [4] introduces a metamathematical predicate Γ ∣ A for each of the systems Pp, Pd, and N, where Γ ranges over finite sequences of wffs, and A ranges over wffs, of that system. In the case of N, if Γ is consistent, then ‘ Γ ∣ A’ is essentially the result of deleting all references to recursive functions from the metamathematical predicate ‘A is realizable-(Γ ⊦)’ described in [3], pp. 502–503.Through use of this predicate, Kleene [4] obtains elegant constructive proofs of the following results for N:Metatheorem 0.1. If B ∨ C is a closed theorem of N, then ⊦ B or ⊦ C.Metatheorem 0.2. If (∃a)D(a) is a closed theorem of N, then there is a numeral n such that ⊦D(n).Metatheorem 0.3. If A is a closed wff of N, then A ∣ A is a necessary and sufficient condition that, for all closed B, C, (∃a)D(a) inN:(0.3.1) ⊦ A ⊃ B ∨ C implies ⊦ A ⊃ B or ⊦A ⊃ Cand(0.3.2) ⊦A ⊃ (∃)D(a) implies there is a numeral n such that ⊦ A ⊃ D(n).

scholarly journals Stirling Permutations, Cycle Structure of Permutations and Perfect Matchings

10.37236/5318 ◽  
2015 ◽  
Vol 22 (4) ◽  
Author(s):  
Shi-Mei Ma ◽  
Yeong-Nan Yeh
Keyword(s):  
Perfect Matchings ◽  
Maximal Elements ◽  
Cycle Structure ◽  
Constructive Proofs

In this paper we provide constructive proofs that the following three statistics are equidistributed: the number of ascent plateaus of Stirling permutations of order $n$, a weighted variant of the number of excedances in permutations of length $n$ and the number of blocks with even maximal elements in perfect matchings of the set $\{1,2,3,\ldots,2n\}$.

scholarly journals Proof Theory and Computational Analysis

1997 ◽  
Vol 4 (30) ◽  
Author(s):  
Ulrich Kohlenbach
Keyword(s):  
Proof Theory ◽  
Computational Analysis ◽  
Numerical Data ◽  
Expressive Power ◽  
Rates Of Convergence ◽  
Uniform Bounds ◽  
Survey Paper ◽  
Constructive Proofs ◽  
Polynomial Bounds ◽  
The Relationship

In this survey paper we start with a discussion how functionals of finite type can be used for the proof-theoretic extraction of numerical data (e.g. effective<br />uniform bounds and rates of convergence) from non-constructive proofs in numerical analysis. We focus on the case where the extractability of polynomial bounds is guaranteed.<br />This leads to the concept of hereditarily polynomial bounded analysis (PBA). We indicate the mathematical range of PBA which turns out to be surprisingly large. Finally we discuss the relationship between PBA and so-called feasible analysis<br />FA. It turns out that both frameworks are incomparable. We argue in favor of the thesis that PBA offers the more useful approach for the purpose of extracting mathematically interesting bounds from proofs. In a sequel of appendices to this paper we indicate the expressive power of PBA.

Sign in / Sign up

Export Citation Format

Share Document