Taking out LK parts from a proof in Peano arithmetic

1986 ◽  
Vol 51 (3) ◽  
pp. 682-700 ◽  
Author(s):  
Tsuyoshi Yukami
Keyword(s):  
Natural Number ◽  
Peano Arithmetic ◽  
Function Symbol ◽  
Maximum Length

Let PA be Peano arithmetic with function symbols′, + and ·. The length of a proof P, denoted by lh(P), is the maximum length of threads of P (for the term ‘thread’, see [T, p. 14]). For a formula A and a natural number m, PA ⊢mA denotes the fact that there is a proof in PA of A whose length is less than or equal to m. PA ⊢ A denotes the fact that there is a proof in PA of A.G. Kreisel conjectured that the following proposition holds.“Let m be a natural number and A(a) be a formula. If for each natural number n, then PA ⊢ ∀xA(x)”.Let PA1 be the corresponding system with + and · replaced by ternary predicates and axioms saying that these predicates represent functions. Parikh [P] proved the following proposition which is obtained from Kreisel's conjecture by replacing PA by PA1.Proposition. Let A(a) be a formula in PA1and m be a natural number. Assume thatfor each natural number n. Then PA1 ⊢ ∀xA(x).The reason why Parikh's method succeeds is the fact that the only function symbol ′ in PA1 is unary. So his method fails for PA.To solve this conjecture for PA, we must make syntactical investigation into proofs in PA of formulas of the form A() with length ≤ m. Even if lengths of proofs are less than or equal to m, depths of occurrences of bound variables in induction axiom schemata or equality axiom schemata in proofs are not always bounded.

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 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.…

scholarly journals The Frontier of Time: The Concept of Quantum Information

2020 ◽  
Author(s):  
Vasil Dinev Penchev
Keyword(s):  
Quantum Mechanics ◽  
Quantum Information ◽  
Natural Number ◽  
Set Theory ◽  
Peano Arithmetic ◽  
Axiom Of Choice ◽  
The Axiom Of Choice ◽  
Infinite Set ◽  
In Virtue Of

A concept of formal transcendentalism is utilized. The fundamental and definitive property of the totality suggests for “the totality to be all”, thus, its externality (unlike any other entity) is contained within it. This generates a fundamental (or philosophical) “doubling” of anything being referred to the totality, i.e. considered philosophically. Thus, that doubling as well as transcendentalism underlying it can be interpreted formally as an elementary choice such as a bit of information and a quantity corresponding to the number of elementary choices to be defined. This is the quantity of information defined both transcendentally and formally and thus, philosophically and mathematically. If one defines information specifically, as an elementary choice between finiteness (or mathematically, as any natural number of Peano arithmetic) and infinity (i.e. an actually infinite set in the meaning of set theory), the quantity of quantum information is defined. One can demonstrate that the so-defined quantum information and quantum information standardly defined by quantum mechanics are equivalent to each other. The equivalence of the axiom of choice and the well-ordering “theorem” is involved. It can be justified transcendentally as well, in virtue of transcendental equivalence implied by the totality. Thus, all can be considered as temporal as far anything possesses such a temporal counterpart necessarily. Formally defined, the frontier of time is the current choice now, a bit of information, furthermore interpretable as a qubit of quantum information.

Predicative Fragments of Frege Arithmetic

2004 ◽  
Vol 10 (2) ◽  
pp. 153-174 ◽  
Author(s):  
Øystein Linnebo
Keyword(s):  
Natural Number ◽  
Order Theory ◽  
Peano Arithmetic ◽  
Two Dimensions ◽  
Second Order ◽  
Order Logic ◽  
The Other ◽  
Hume’S Principle ◽  
Important Exception ◽  
Second Order Logic

AbstractFrege Arithmetic (FA) is the second-order theory whose sole non-logical axiom is Hume's Principle, which says that the number of Fs is identical to the number of Gs if and only if the Fs and the Gs can be one-to-one correlated. According to Frege's Theorem, FA and some natural definitions imply all of second-order Peano Arithmetic. This paper distinguishes two dimensions of impredicativity involved in FA—one having to do with Hume's Principle, the other, with the underlying second-order logic—and investigates how much of Frege's Theorem goes through in various partially predicative fragments of FA. Theorem 1 shows that almost everything goes through, the most important exception being the axiom that every natural number has a successor. Theorem 2 shows that the Successor Axiom cannot be proved in the theories that are predicative in either dimension.

scholarly journals Choice, Infinity, and Negation: Both Set-Theory and Quantum-Information Viewpoints to Negation

2020 ◽  
Author(s):  
Vasil Dinev Penchev
Keyword(s):  
Hilbert Space ◽  
Quantum Mechanics ◽  
Quantum Information ◽  
Natural Number ◽  
Set Theory ◽  
Peano Arithmetic ◽  
Complex Hilbert Space ◽  
Heyting Arithmetic ◽  
Infinite Set

The concepts of choice, negation, and infinity are considered jointly. The link is the quantity of information interpreted as the quantity of choices measured in units of elementary choice: a bit is an elementary choice between two equally probable alternatives. “Negation” supposes a choice between it and confirmation. Thus quantity of information can be also interpreted as quantity of negations. The disjunctive choice between confirmation and negation as to infinity can be chosen or not in turn: This corresponds to set-theory or intuitionist approach to the foundation of mathematics and to Peano or Heyting arithmetic. Quantum mechanics can be reformulated in terms of information introducing the concept and quantity of quantum information. A qubit can be equivalently interpreted as that generalization of “bit” where the choice is among an infinite set or series of alternatives. The complex Hilbert space can be represented as both series of qubits and value of quantum information. The complex Hilbert space is that generalization of Peano arithmetic where any natural number is substituted by a qubit. “Negation”, “choice”, and “infinity” can be inherently linked to each other both in the foundation of mathematics and quantum mechanics by the meditation of “information” and “quantum information”.

Theories very close to PA where Kreisel's Conjecture is false

2007 ◽  
Vol 72 (1) ◽  
pp. 123-137 ◽  
Author(s):  
Pavel Hrubeš
Keyword(s):  
Natural Number ◽  
Function Symbol ◽  
Unary Predicate

AbstractWe give four examples of theories in which Kreisel's Conjecture is false: (1) the theory PA(-) obtained by adding a function symbol minus, ‘—’, to the language of PA, and the axiom ∀x∀y∀z (x − y = z) ≡ (x = y + z ∨ (x < y ∧ z = 0)); (2) the theory L of integers; (3) the theory PA(q) obtained by adding a function symbol q (of arity ≥ 1) to PA, assuming nothing about q; (4) the theory PA(N) containing a unary predicate N(x) meaning ‘x is a natural number’. In Section 6 we suggest a counterexample to the so called Sharpened Kreisel's Conjecture.

scholarly journals Constructive truth and falsity in Peano arithmetic

2020 ◽  
Author(s):  
Hirohiko Kushida
Keyword(s):  
Natural Number ◽  
Peano Arithmetic ◽  
Logic Of Proofs ◽  
Logical Status ◽  
Reflection Principles

Abstract Artemov (2019, The provability of consistency) offered the notion of constructive truth and falsity of arithmetical sentences in the spirit of Brouwer–Heyting–Kolmogorov semantics and its formalization, the logic of proofs. In this paper, we provide a complete description of constructive truth and falsity for Friedman’s constant fragment of Peano arithmetic. For this purpose, we generalize the constructive falsity to $n$-constructive falsity in Peano arithmetic where $n$ is any positive natural number. Based on this generalization, we also analyse the logical status of well-known Gödelean sentences: consistency assertions for extensions of PA, the local reflection principles, the ‘constructive’ liar sentences and Rosser sentences. Finally, we discuss ‘extremely’ independent sentences in the sense that they are classically true but neither constructively true nor $n$-constructively false for any $n$.

Seed Width to Pod Width Ratio for Identification of Green Soybean Pods that have Attained Maximum Length and Width 1

Crop Science ◽  
1982 ◽  
Vol 22 (3) ◽  
pp. 463-466
Author(s):  
S. Rodriguez de Cianzio ◽  
S. J. Frank ◽  
W. R. Fehr
Keyword(s):  
Maximum Length ◽  
Width Ratio ◽  
Seed Width

scholarly journals Modal Structuralism with Theoretical Terms

Erkenntnis ◽  
2021 ◽  
Author(s):  
Holger Andreas ◽  
Georg Schiemer
Keyword(s):  
Philosophy Of Mathematics ◽  
Formal Semantics ◽  
Peano Arithmetic ◽  
Theoretical Terms ◽  
Structural Interpretation ◽  
Oxford University ◽  
Structuralist Approach ◽  
Modal Semantics ◽  
Oxford University Press

AbstractIn this paper, we aim to explore connections between a Carnapian semantics of theoretical terms and an eliminative structuralist approach in the philosophy of mathematics. Specifically, we will interpret the language of Peano arithmetic by applying the modal semantics of theoretical terms introduced in Andreas (Synthese 174(3):367–383, 2010). We will thereby show that the application to Peano arithmetic yields a formal semantics of universal structuralism, i.e., the view that ordinary mathematical statements in arithmetic express general claims about all admissible interpretations of the Peano axioms. Moreover, we compare this application with the modal structuralism by Hellman (Mathematics without numbers: towards a modal-structural interpretation. Oxford University Press: Oxford, 1989), arguing that it provides us with an easier epistemology of statements in arithmetic.

A 73dB-A Audio VCO-ADC based on a Maximum Length Sequence Generator in 130nm CMOS

2021 ◽  
pp. 1-1
Author(s):  
Carlos Perez ◽  
Andres Quintero ◽  
Pedro Amaral ◽  
Andreas Wiesbauer ◽  
L. Hernandez
Keyword(s):  
Maximum Length ◽  
Sequence Generator
Sign in / Sign up

Export Citation Format

Share Document