scholarly journals An application of graphical enumeration to PA

2003 ◽  
Vol 68 (1) ◽  
pp. 5-16
Author(s):  
Andreas Weiermann
Keyword(s):  
Normal Form ◽  
Asymptotic Analysis ◽  
Natural Number ◽  
Proof Theory ◽  
Peano Arithmetic ◽  
First Order ◽  
Primitive Recursive Arithmetic ◽  
Independence Result ◽  
Primitive Recursive

AbstractFor α less than ε0 let Nα be the number of occurrences of ω in the Cantor normal form of α. Further let ∣n∣ denote the binary length of a natural number n, let ∣n∣h denote the h-times iterated binary length of n and let inv(n) be the least h such that ∣n∣h ≤ 2. We show that for any natural number h first order Peano arithmetic, PA, does not prove the following sentence: For all K there exists an M which bounds the lengths n of all strictly descending sequences 〈α0, …, αn〉 of ordinals less than ε0 which satisfy the condition that the Norm Nαi of the i-th term αi is bounded by K + ∣i∣ · ∣i∣i.As a supplement to this (refined Friedman style) independence result we further show that e.g., primitive recursive arithmetic, PRA, proves that for all K there is an M which bounds the length n of any strictly descending sequence 〈α0, …, αn〉 of ordinals less than ε0 which satisfies the condition that the Norm Nαi of the i-th term αi is bounded by K + ∣i∣ · inv(i). The proofs are based on results from proof theory and techniques from asymptotic analysis of Polya-style enumerations.Using results from Otter and from Matoušek and Loebl we obtain similar characterizations for finite bad sequences of finite trees in terms of Otter's tree constant 2.9557652856.…

A result on implications of Σ1-sentences and its application to normal form theorems

1981 ◽  
Vol 46 (3) ◽  
pp. 634-642
Author(s):  
Jean-Yves Girard ◽  
Peter Päppinghaus
Keyword(s):  
Normal Form ◽  
Reflection Principle ◽  
The Other ◽  
Other Hand ◽  
Primitive Recursive Arithmetic ◽  
Incompleteness Theorems ◽  
False Premise ◽  
Primitive Recursive ◽  
Gödel’S Incompleteness Theorems

In this paper we are concerned with the formal provability of certain true implications of Σ1-sentences. Old completeness and incompleteness results already give some information about this. For example by Σ1-completeness of PRA (primitive recursive arithmetic) every true implication of the form D → E, where D is a Σ0-sentence and E a Σ1-sentence, or D a Σ1-sentence and E a true Σ1-sentence, is provable in PRA. On the other hand, by Gödel's incompleteness theorems one can define for every suitable theory S a false Σ1-sentence Ds such that for every false Σ0-sentence E the true implication Ds → E is not provable in S, but is provable in PRA + Cons. So one sees that for a suitable fixed conclusion the provability of true implications of Σ1-sentences depends on the content of the premise.Now we ask, if and how for a suitable fixed premise the provability of true implications of Σ1-sentences depends on the conclusion. As remarked above, by Σ1-completeness of PRA this question is settled, if the premise is true. For a false premise it is answered in § 1 as follows: Let D be a false Σ1-sentence, S an extension of PRA, and S+ ≔ PRA + IAΣ1 + RFNΣ1S). Depending on D and S one can define a Σ1-sentence Es such that S+ ⊢ D → Es, but S ⊬ D → Es provided that S+ is not strong enough to refute D. (IAΣ1 denotes the scheme of the induction axiom for Σ1-formulas, and RFNΣ1(S) the uniform Σ1-reflection principle for S.)

scholarly journals UNFOLDING FINITIST ARITHMETIC

2010 ◽  
Vol 3 (4) ◽  
pp. 665-689 ◽  
Author(s):  
SOLOMON FEFERMAN ◽  
THOMAS STRAHM
Keyword(s):  
Peano Arithmetic ◽  
Primitive Recursive Arithmetic ◽  
Primitive Recursive

The concept of the (full) unfolding $\user1{{\cal U}}(S)$ of a schematic system $S$ is used to answer the following question: Which operations and predicates, and which principles concerning them, ought to be accepted if one has accepted $S$? The program to determine $\user1{{\cal U}}(S)$ for various systems $S$ of foundational significance was previously carried out for a system of nonfinitist arithmetic, $NFA$; it was shown that $\user1{{\cal U}}(NFA)$ is proof-theoretically equivalent to predicative analysis. In the present paper we work out the unfolding notions for a basic schematic system of finitist arithmetic, $FA$, and for an extension of that by a form $BR$ of the so-called Bar Rule. It is shown that $\user1{{\cal U}}(FA)$ and $\user1{{\cal U}}(FA + BR)$ are proof-theoretically equivalent, respectively, to Primitive Recursive Arithmetic, $PRA$, and to Peano Arithmetic, $PA$.

On the No-Counterexample Interpretation

1999 ◽  
Vol 64 (4) ◽  
pp. 1491-1511 ◽  
Author(s):  
Ulrich Kohlenbach
Keyword(s):  
Normal Form ◽  
Formal System ◽  
Modus Ponens ◽  
Peano Arithmetic ◽  
Order Type ◽  
Cut Elimination ◽  
Substitution Method ◽  
Functional Interpretation ◽  
First Order ◽  
Definition Of

AbstractIn [15], [16] G. Kreisel introduced the no-counterexample interpretation (n.c.i.) of Peano arithmetic. In particular he proved, using a complicated ε-substitution method (due to W. Ackermann), that for every theorem A (A prenex) of first-order Peano arithmetic PA one can find ordinal recursive functionals of order type < ε0 which realize the Herbrand normal form AH of A.Subsequently more perspicuous proofs of this fact via functional interpretation (combined with normalization) and cut-elimination were found. These proofs however do not carry out the no-counterexample interpretation as a local proof interpretation and don't respect the modus ponens on the level of the nocounterexample interpretation of formulas A and A → B. Closely related to this phenomenon is the fact that both proofs do not establish the condition (δ) and—at least not constructively—(γ) which are part of the definition of an ‘interpretation of a formal system’ as formulated in [15].

scholarly journals The optimality of induction as an axiomatization of arithmetic

1983 ◽  
Vol 48 (1) ◽  
pp. 182-184 ◽  
Author(s):  
Daniel Leivant
Keyword(s):  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Primitive Recursive Arithmetic ◽  
Image Position ◽  
Primitive Recursive ◽  
Universal Closure

By induction for a formula φ we mean the schema(where the terms in brackets are implicitly substituted for some fixed variable, with the usual restrictions). Let be the schema IAφ for φ in Πn (i.e. ); similarly for . Each instance of is Δn+2, and each instance of is Σn+1 Thus the universal closure of an instance α is Πn+2 in either case. Charles Parsons [72] proved that and are equivalent over Z0, where Z0 is essentially Primitive Recursive Arithmetic augmented by classical First Order Logic [Parsons 70].Theorem. For each n > 0 there is a Πn formula π for whichis not derivable in Z0from(i) true Πn+1sentences; nor even(ii) Πn+1sentences consistent withZ0.

The Natural Numbers

2018 ◽  
Author(s):  
Øystein Linnebo
Keyword(s):  
Natural Number ◽  
Peano Arithmetic ◽  
Number Sequence ◽  
Natural Numbers ◽  
Ordinal Numbers ◽  
Cardinal Numbers

How are the natural numbers individuated? That is, what is our most basic way of singling out a natural number for reference in language or in thought? According to Frege and many of his followers, the natural numbers are cardinal numbers, individuated by the cardinalities of the collections that they number. Another answer regards the natural numbers as ordinal numbers, individuated by their positions in the natural number sequence. Some reasons to favor the second answer are presented. This answer is therefore developed in more detail, involving a form of abstraction on numerals. Based on this answer, a justification for the axioms of Dedekind–Peano arithmetic is developed.

scholarly journals Extensions in graph normal form

2020 ◽  
Author(s):  
Michał Walicki
Keyword(s):  
Normal Form ◽  
Fixed Points ◽  
Propositional Logic ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Special Cases

Abstract Graph normal form, introduced earlier for propositional logic, is shown to be a normal form also for first-order logic. It allows to view syntax of theories as digraphs, while their semantics as kernels of these digraphs. Graphs are particularly well suited for studying circularity, and we provide some general means for verifying that circular or apparently circular extensions are conservative. Traditional syntactic means of ensuring conservativity, like definitional extensions or positive occurrences guaranteeing exsitence of fixed points, emerge as special cases.

A reduction class containing formulas with one monadic predicate and one binary function symbol

1976 ◽  
Vol 41 (1) ◽  
pp. 45-49
Author(s):  
Charles E. Hughes
Keyword(s):  
Normal Form ◽  
Predicate Symbol ◽  
Conjunctive Normal Form ◽  
Function Symbol ◽  
Predicate Calculus ◽  
Binary Function ◽  
First Order ◽  
The Matrix ◽  
Reduction Class ◽  
Order Predicate Calculus

AbstractA new reduction class is presented for the satisfiability problem for well-formed formulas of the first-order predicate calculus. The members of this class are closed prenex formulas of the form ∀x∀yC. The matrix C is in conjunctive normal form and has no disjuncts with more than three literals, in fact all but one conjunct is unary. Furthermore C contains but one predicate symbol, that being unary, and one function symbol which symbol is binary.

scholarly journals Relations between Abs-Normal NLPs and MPCCs. Part 2: Weak Constraint Qualifications

2021 ◽  
Vol Volume 2 (Original research articles>) ◽  
Author(s):  
Lisa C. Hegerhorst-Schultchen ◽  
Christian Kirches ◽  
Marc C. Steinbach
Keyword(s):  
Normal Form ◽  
Optimization Problems ◽  
Constraint Qualifications ◽  
Inequality Constraints ◽  
First Order ◽  
Nonlinear Programs ◽  
Mathematical Programs ◽  
Ongoing Effort ◽  
Equality And Inequality Constraints ◽  
Smooth Optimization

This work continues an ongoing effort to compare non-smooth optimization problems in abs-normal form to Mathematical Programs with Complementarity Constraints (MPCCs). We study general Nonlinear Programs with equality and inequality constraints in abs-normal form, so-called Abs-Normal NLPs, and their relation to equivalent MPCC reformulations. We introduce the concepts of Abadie's and Guignard's kink qualification and prove relations to MPCC-ACQ and MPCC-GCQ for the counterpart MPCC formulations. Due to non-uniqueness of a specific slack reformulation suggested in [10], the relations are non-trivial. It turns out that constraint qualifications of Abadie type are preserved. We also prove the weaker result that equivalence of Guginard's (and Abadie's) constraint qualifications for all branch problems hold, while the question of GCQ preservation remains open. Finally, we introduce M-stationarity and B-stationarity concepts for abs-normal NLPs and prove first order optimality conditions corresponding to MPCC counterpart formulations.

Uniqueness, definability and interpolation

1988 ◽  
Vol 53 (2) ◽  
pp. 554-570 ◽  
Author(s):  
Kosta Došen ◽  
Peter Schroeder-Heister
Keyword(s):  
Proof Theory ◽  
Interpolation Theorem ◽  
Order Logic ◽  
First Order Logic ◽  
General Notion ◽  
Structural Part ◽  
First Order ◽  
First Case ◽  
Additional Constant ◽  
Special Case

This paper is meant to be a comment on Beth's definability theorem. In it we shall make the following points.Implicit definability as mentioned in Beth's theorem for first-order logic is a special case of a more general notion of uniqueness. If α is a nonlogical constant, Tα a set of sentences, α* an additional constant of the same syntactical category as α and Tα, a copy of Tα with α* instead of α, then for implicit definability of α in Tα one has, in the case of predicate constants, to derive α(x1,…,xn) ↔ α*(x1,…,xn) from Tα ∪ Tα*, and similarly for constants of other syntactical categories. For uniqueness one considers sets of schemata Sα and derivability from instances of Sα ∪ Sα* in the language with both α and α*, thus allowing mixing of α and α* not only in logical axioms and rules, but also in nonlogical assumptions. In the first case, but not necessarily in the second one, explicit definability follows. It is crucial for Beth's theorem that mixing of α and α* is allowed only inside logic, not outside. This topic will be treated in §1.Let the structural part of logic be understood roughly in the sense of Gentzen-style proof theory, i.e. as comprising only those rules which do not specifically involve logical constants. If we restrict mixing of α and α* to the structural part of logic which we shall specify precisely, we obtain a different notion of implicit definability for which we can demonstrate a general definability theorem, where a is not confined to the syntactical categories of nonlogical expressions of first-order logic. This definability theorem is a consequence of an equally general interpolation theorem. This topic will be treated in §§2, 3, and 4.

Sign in / Sign up

Export Citation Format

Share Document