Project topics and materials
Get Complete Project Material File(s) Now! »
Logical axioms and rules and Boolean axioms
We begin by adapting the set of rules for the first-order Minimal predicate Logic from [111] and/or [10] 8 to the setting of program-extraction by the light (monotone) Dialectica interpretation (defined in Chapter 2). First of all we define the following two variable conditions which will be used to constrain the rules concerning the (ncm-)universal quantifier:
– VC (z) : the variable z does not occur free in any of the undischarged assumptions of the proof of the premise of the rule;
– VC (z, t) : the term t is “free for” z in the conclusion, i.e., no free variable of t gets quantified after substituting {z ←t} in the conclusion.
We also define an NCM – formula condition which is required to constrain the rule of Implication Introduction (abbreviated “Imp Intro”) which has that kind of contraction formula which is computationally relevant to the Light Dialec-tica (see below for this terminology). Such a restriction will be necessary in or-der to attain soundness of program-extraction by the light (monotone) Dialec-tica interpretation in Theorems 2.10 and respectively 2.12 from Chapter 2.
Definition 1.15 (The ncm−FC restriction) For some given formula A, if A contains (at least) a positive universal or a negative existential (regular) quan-tifier, then A does not contain any ncm quantifier. We abbreviate this “ncm – Formula Condition” restriction set on A by the shorter expression ncm−FC(A). Remark 1.16 (Rˆole of ncm−FC during LD-extraction) If the ncm−FC(A) restriction holds, then the LD-interpretation of A (see Definition 2.1) will have a quantifier-free base formula AD . Therefore AD will be decidable, cf. Propo-sition 1.35 / Lemma 1.36. If A is the formula-type of the (parcel) assumption variable u which is to be cancelled at some Imp Intro with LDR-contraction (see below), the decidability of AD will be strictly and unavoidably necessary for determining, according to actual values, which of the terms Light Dialec-tica realizing the multiple instances of A is chosen to Light Dialectica realize the new single implicative assumption A of the conclusion formula of such an Imp Intro. See Definition 2.6 and the proof of Theorem 2.10 for details.
Stability, Case Distinction, Decidability and Disjunction Introduction/Elimination
Notational Convention. For simplicity we here-on abbreviate at(tt) by T and at(ff) by F. We also abbreviate by ⌉A :≡ A → F the so-called “boolean negation” of the formula A. Lemma 1.27 The following hold in minimal logics ML, respectively IL0 :
ML ⊢ ∀q . q =o tt ↔ at(q) (1.10)
ML ⊢ ∀q . q =o ff ↔ (at(q) → F) ≡ ⌉at(q) (1.11)
ML ⊢ ∀q . ⌉at(q) → ¬at(q) (1.12)
ML ⊢ [ ∀q . ¬at(q) → ⌉at(q) ] ↔ (⊥ → F) (1.13)
IL0 ⊢ [ ∀q . ¬¬at(q) → at(q) ] ↔ (⊥ → F) (1.14)
Proof: Even without using AxBIA, (1.10), (1.11) and (1.12) are simply imme-diate from the definition (1.7) of =o , AxTRH and AxFLS. Also without AxBIA, at (1.13) the direction “←” follows immediately and the direction “→” fol-lows from AxTRH after setting q := tt. The direction “←” of (1.14) can only be proved by boolean induction AxBIA on q . Hence for q ≡ tt, ¬¬at(tt) → at(tt) follows from AxTRH. On the other hand, for q ≡ ff, ¬¬at(ff) → at(ff) rewrites as ((F → ⊥) → ⊥) → F which is immediately seen to be equivalent to ⊥ → F in minimal logic ML. This also proves the direction “→” of (1.14). ✷
Corollary 1.28 (Boolean/Logical Stability of atomic formulas) In the same lines of the above proof of (1.14) it immediately follows that: IL0 ⊢ ∀qo . ⌉⌉at(q) → at(q) (1.15) On the other hand, from (1.14) it immediately follows that IL ⊢ ∀qo . ¬¬at(q) → at(q) (1.16) where the axiom AxEFQ : ⊥ → F is strictly necessary in the proof of (1.16). Lemma 1.29 (Boolean/Logical Case Distinction on atomic formulas) The following hold in minimal logic IL0 for every formula A of F∃,nc :
IL0 ⊢ ∀qo. (q =o tt → A) ∧ (q =o ff → A) → A IL0 ⊢ ∀qo. (at(q) → A) ∧ (⌉at(q) → A) → A IL0 ⊢ ∀qo. (at(q) → A) ∧ (¬at(q) → A) → A.
The rules of Equality for booleans, naturals and all complex types
We are now at the point of introducing the axioms which give the (usual) behaviour of (higher-order extensional) equality, stressing from the beginning that extensionality must12 be restricted in the context of Dialectica interpre-tation. The extensionality axiom Eσ,τ : ∀zστ , xσ , yσ . x =σ y → zx =τ zy must not be derivable in our system. We here deviate from the system Z of Berger, Buchholz and Schwichtenberg which derives Eσ,τ and hence is fully exten-sional. But let us first present the more basic Reflexivity, Symmetry and Transitivity which we prefer to give directly at higher types and therefore we further prefer to introduce as rules:
REFτ : x =τ x (Reflexivity)
SYMτ : x =τ y ⊢ y =τ x (Symmetry)
TRZτ : x =τ y , y =τ z ⊢ x =τ z (Transitivity)
Although without computational content under Modified Realizability, the axiom versions of SYMτ and TRZτ would have required realizing terms under Dialectica interpretation for higher-order τ . We could have used only the ax-iom versions of REFι, SYMι and TRZι since higher-type Reflexivity, Symmetry and Transitivity can be deduced in pure Minimal Logic from the Reflexivity, Symmetry and respectively Transitivity of natural numbers. The latter are quantifier-free and hence realizer-free under both Realizability and Dialectica interpretations. We however chose the above presentation for the practical reason that proofs are shorter and no Dialectica realizers are needed for the rule versions of higher-order Symmetry and Transitivity.
Table of contents :
Introduction
Outline of the following sections
1 Arithmetical systems for G¨odel functionals
1.1 Languages, types, terms and formulas
1.2 Logical axioms and rules and Boolean axioms
1.2.1 Stability, Case Distinction, Decidability and Disjunction Introduction/Elimination
1.3 Weakly extensional Intuitionistic Arithmetics WeZ, WeZ∃, WeZnc and WeZ∃,nc
1.3.1 The “no-undischarged-assumptions” Induction Rule
1.3.2 The rules of Equality for all simple types
1.3.3 Equality axioms induced by the Conversion Relation →֒ 40
1.3.4 The definition of systems WeZ, WeZ∃, WeZnc and WeZ∃,nc . 40
1.3.5 Equivalence between three formulations of Induction . 42
1.4 Immediate extension of systems WeZnc and WeZ∃,nc
1.5 The monotonic intuitionistic Arithmetics WeZ∃ m and WeZ∃,nc+ m
1.6 The classical (monotonic) Arithmetics WeZnc,c+ and WeZ∃,nc,c+ m .
2 The light (monotone) functional Dialectica interpretation
2.1 The light G¨odel functional “Dialectica” interpretation
2.2 The light monotone functional “Dialectica” interpretation
2.3 Extensions of the light (monotone) Dialectica interpretation to extractions from fully classical proofs
2.4 Light Monotone Dialectica extractions from classical analytical
proofs by elimination-of-extensionality and ε-arithmetization .
3 Feasible systems of Arithmetic and Analysis
3.1 A poly-time Arithmetic/Analysis due to Oliva, Cook-Urquhart and Ferrreira
3.2 A polynomial bounded Arithmetic/Analysis due to Kohlenbach
3.2.1 Elimination of the non-standard analytical axiom F−
3.2.2 Verification in the full set-theoretic type structure
3.3 Our proposal for a feasible Arithmetic/Analysis system
4 Comparison with other techniques for extraction of exact realizers from non-intuitionistic proofs. Case Studies
4.1 The BBS refined A-translation
4.1.1 Theoretical comparison with the BBS technique
4.2 Berger’s hsh example
4.2.1 MinLog source code for Berger’s hsh example
4.3 The (semi-)classical Fibonacci proof
4.3.1 Motivation for treatment of Fibonacci in MinLog
4.3.2 The semi-classical Fibonacci proof in MinLog
4.3.3 The light functional “Dialectica” interpretation
4.3.4 A comparison of the three extraction techniques
4.4 Conclusions and future work
4.5 The integer square root example
5 Synthesis of moduli of uniform continuity by the LMD-interpretation in the proof-system MinLog
5.1 The minimal arithmetic HeExtEq proof in the computer-system MinLog
5.2 The MinLog machine majorant extraction
5.3 Machine results for the HeExtEq case-study
Conclusions
Bibliography
