How to extend the semantic tableaux and cut-free versions of the second incompleteness theorem almost to Robinson's arithmetic q

2002 ◽  
Vol 67 (1) ◽  
pp. 465-496 ◽  
Author(s):  
Dan E. Willard
Keyword(s):  
Axiom System ◽  
Incompleteness Theorem ◽  
Semantic Tableaux ◽  
The Standard Model ◽  
Natural Extensions ◽  
Consistent Extension ◽  
Infinite Cardinality ◽  
Axiom Systems ◽  
A Minor ◽  
Open Question

AbstractLet us recall that Raphael Robinson's Arithmetic Q is an axiom system that differs from Peano Arithmetic essentially by containing no Induction axioms [13], [18]. We will generalize the semantic-tableaux version of the Second Incompleteness Theorem almost to the level of System Q. We will prove that there exists a single rather long Π1 sentence, valid in the standard model of the Natural Numbers and denoted as V. such that if α is any finite consistent extension of Q + V then α will be unable to prove its Semantic Tableaux consistency. The same result will also apply to axiom systems α with infinite cardinality when these infinite-sized axiom systems satisfy a minor additional constraint, called the Conventional Encoding Property.Our formalism will also imply that the semantic-tableaux version of the Second Incompleteness Theorem generalizes for the axiom system IΣ0, as well as for all its natural extensions. (This answers an open question raised twenty years ago by Paris and Wilkie [15].)

Self-verifying axiom systems, the incompleteness theorem and related reflection principles

2001 ◽  
Vol 66 (2) ◽  
pp. 536-596 ◽  
Author(s):  
Dan E. Willard
Keyword(s):  
Reflection Principle ◽  
Incompleteness Theorem ◽  
Semantic Tableaux ◽  
Total Function ◽  
Reflection Principles ◽  
Axiom Systems ◽  
Weak Axiom

AbstractWe will study several weak axiom systems that use the Subtraction and Division primitives (rather than Addition and Multiplication) to formally encode the theorems of Arithmetic. Provided such axiom systems do not recognize Multiplication as a total function, we will show that it is feasible for them to verify their Semantic Tableaux, Herbrand, and Cut-Free consistencies. If our axiom systems additionally do not recognize Addition as a total function, they will be capable of recognizing the consistency of their Hilbert-style deductive proofs. Our axiom systems will not be strong enough to recognize their Canonical Reflection principle, but they will be capable of recognizing an approximation of it, called the “Tangibility Reflection Principle”. We will also prove some new versions of the Second Incompleteness Theorem stating essentially that it is not possible to extend our exceptions to the Incompleteness Theorem much further.

scholarly journals An exploration of the partial respects in which an axiom system recognizing solely addition as a total function can verify its own consistency

2005 ◽  
Vol 70 (4) ◽  
pp. 1171-1209 ◽  
Author(s):  
Dan E. Willard
Keyword(s):  
Modus Ponens ◽  
Axiom System ◽  
Incompleteness Theorem ◽  
Deduction System ◽  
Total Function ◽  
Boundary Case ◽  
Axiom Systems

AbstractThis article will study a class of deduction systems that allow for a limited use of the modus ponens method of deduction. We will show that it is possible to devise axiom systems α that can recognize their consistency under a deduction system D provided that: (1) α treats multiplication as a 3-way relation (rather than as a total function), and that (2) D does not allow for the use of a modus ponens methodology above essentially the levels of Π1 and Σ1 formulae.Part of what will make this boundary-case exception to the Second Incompleteness Theorem interesting is that we will also characterize generalizations of the Second Incompleteness Theorem that take force when we only slightly weaken the assumptions of our boundary-case exceptions in any of several further directions.

On the available partial respects in which an axiomatization for real valued arithmetic can recognize its consistency

2006 ◽  
Vol 71 (4) ◽  
pp. 1189-1199 ◽  
Author(s):  
Dan E. Willard
Keyword(s):  
Incompleteness Theorem ◽  
Floating Point ◽  
Floating Point Arithmetic ◽  
Axiom Systems ◽  
Sufficient Strength ◽  
Point Arithmetic

AbstractGödel's Second Incompleteness Theorem states axiom systems of sufficient strength are unable to verify their own consistency. We will show that axiomatizations for a computer's floating point arithmetic can recognize their cut-free consistency in a stronger respect than is feasible under integer arithmetics. This paper will include both new generalizations of the Second Incompleteness Theorem and techniques for evading it.

scholarly journals INSTANTIAL NEIGHBOURHOOD LOGIC

2016 ◽  
Vol 10 (1) ◽  
pp. 116-144 ◽  
Author(s):  
JOHAN VAN BENTHEM ◽  
NICK BEZHANISHVILI ◽  
SEBASTIAN ENQVIST ◽  
JUNHUA YU
Keyword(s):  
Fine Structure ◽  
Normal Form ◽  
Axiom System ◽  
Topological Spaces ◽  
Relational Semantics ◽  
Basic Model ◽  
Semantic Tableaux ◽  
Dynamic Logics ◽  
A Current

AbstractThis paper explores a new language of neighbourhood structures where existential information can be given about what kind of worlds occur in a neighbourhood of a current world. The resulting system of ‘instantial neighbourhood logic’ INL has a nontrivial mix of features from relational semantics and from neighbourhood semantics. We explore some basic model-theoretic behavior, including a matching notion of bisimulation, and give a complete axiom system for which we prove completeness by a new normal form technique. In addition, we relate INL to other modal logics by means of translations, and determine its precise SAT complexity. Finally, we discuss proof-theoretic fine-structure of INL in terms of semantic tableaux and some expressive fine-structure in terms of fragments, while discussing concrete illustrations of the instantial neighborhood language in topological spaces, in games with powers for players construed in a new way, as well as in dynamic logics of acquiring or deleting evidence. We conclude with some coalgebraic perspectives on what is achieved in this paper. Many of these final themes suggest follow-up work of independent interest.

scholarly journals Matroids, Cyclic Flats, and Polyhedra

2021 ◽  
Author(s):  
◽  
Kadin Prideaux
Keyword(s):  
Polynomial Time ◽  
Solution Space ◽  
Axiom System ◽  
Linear Program ◽  
Integral Points ◽  
The Matrix ◽  
Axiom Systems

<p>Matroids have a wide variety of distinct, cryptomorphic axiom systems that are capable of defining them. A common feature of these is that they are able to be efficiently tested, certifying whether a given input complies with such an axiom system in polynomial time. Joseph Bonin and Anna de Mier, rediscovering a theorem first proved by Julie Sims, developed an axiom system for matroids in terms of their cyclic flats and the ranks of those cyclic flats. As with other matroid axiom systems, this is able to be tested in polynomial time. Distinct, non-isomorphic matroids may each have the same lattice of cyclic flats, and so matroids cannot be defined solely in terms of their cyclic flats. We do not have a clean characterisation of families of sets that are cyclic flats of matroids. However, it may be possible to tell in polynomial time whether there is any matroid that has a given lattice of subsets as its cyclic flats. We use Bonin and de Mier’s cyclic flat axioms to reduce the problem to a linear program, and show that determining whether a given lattice is the lattice of cyclic flats of any matroid corresponds to finding integral points in the solution space of this program, these points representing the possible ranks that may be assigned to the cyclic flats. We distinguish several classes of lattice for which solutions may be efficiently found, based upon the nature of the matrix of coefficients of the linear program, and of the polyhedron it defines, and then identify families of lattice that belong to those classes. We define operations and transformations on lattices of sets by examining matroid operations, and examine how these operations affect membership in the aforementioned classes. We conjecture that it is always possible to determine, in polynomial time, whether a given collection of subsets makes up the lattice of cyclic flats of any matroid.</p>

Pure Proof Theory Aims, Methods and Results: Extended Version of Talks Given at Oberwolfach and Haifa

1996 ◽  
Vol 2 (2) ◽  
pp. 159-188 ◽  
Author(s):  
Wolfram Pohlers
Keyword(s):  
Mathematical Logic ◽  
Computer Science ◽  
Proof Theory ◽  
Axiom System ◽  
Theoretical Research ◽  
Cut Elimination ◽  
Extended Version ◽  
Consistency Proof ◽  
Exciting Field ◽  
Axiom Systems

Apologies. The purpose of the following talk is to give an overview of the present state of aims, methods and results in Pure Proof Theory. Shortage of time forces me to concentrate on my very personal views. This entails that I will emphasize the work which I know best, i.e., work that has been done in the triangle Stanford, Munich and Münster. I am of course well aware that there are as important results coming from outside this triangle and I apologize for not displaying these results as well.Moreover the audience should be aware that in some points I have to oversimplify matters. Those who complain about that are invited to consult the original papers.1.1. General. Proof theory startedwithHilbert's Programme which aimed at a finitistic consistency proof for mathematics.By Gödel's Theorems, however, we know that we can neither formalize all mathematics nor even prove the consistency of formalized fragments by finitistic means. Inspite of this fact I want to give some reasons why I consider proof theory in the style of Gentzen's work still as an important and exciting field of Mathematical Logic. I will not go into applications of Gentzen's cut-elimination technique to computer science problems—this may be considered as applied proof theory—but want to concentrate on metamathematical problems and results. In this sense I am talking about Pure Proof Theory.Mathematicians are interested in structures. There is only one way to find the theorems of a structure. Start with an axiom system for the structure and deduce the theorems logically. These axiom systems are the objects of proof-theoretical research. Studying axiom systems there is a series of more or less obvious questions.

scholarly journals Prolegomena to any theory of proof simplicity

2019 ◽  
Vol 377 (2140) ◽  
pp. 20180035 ◽  
Author(s):  
Victor Pambuccian
Keyword(s):  
Simple Proof ◽  
Axiom System ◽  
Elementary Geometry ◽  
Theme Issue ◽  
Pasch Axiom ◽  
Axiom Systems ◽  
The Pasch Axiom

By looking at concrete examples from elementary geometry, we analyse the manner in which the simplicity of proofs could be defined. We first find that, when presented with two proofs coming from mutually incompatible sets of assumptions, the decision regarding which one is simplest can be made, if at all, only on the basis of reasoning outside of the formal aspects of the axiom systems involved. We then show that, if the axiom system is fixed, a measure of proof simplicity can be defined based on the number of uses of axioms deemed to be deep or valuable, and prove a number of new results regarding the need to use at least three times some axioms in the proof of others. One such major example is Pappus implies Desargues, which is shown to require three uses of Pappus. A similar situation is encountered with Veblen's proof that the outer form of the Pasch axiom implies the inner form thereof. The outer form needs to be used at least three times in any such proof. We also mention the likely conflicting requirements of directness of a proof and the length of a proof. This article is part of the theme issue ‘The notion of ‘simple proof’ - Hilbert's 24th problem’.

scholarly journals Matroids, Cyclic Flats, and Polyhedra

2021 ◽  
Author(s):  
◽  
Kadin Prideaux
Keyword(s):  
Polynomial Time ◽  
Solution Space ◽  
Axiom System ◽  
Linear Program ◽  
Integral Points ◽  
The Matrix ◽  
Axiom Systems

<p>Matroids have a wide variety of distinct, cryptomorphic axiom systems that are capable of defining them. A common feature of these is that they are able to be efficiently tested, certifying whether a given input complies with such an axiom system in polynomial time. Joseph Bonin and Anna de Mier, rediscovering a theorem first proved by Julie Sims, developed an axiom system for matroids in terms of their cyclic flats and the ranks of those cyclic flats. As with other matroid axiom systems, this is able to be tested in polynomial time. Distinct, non-isomorphic matroids may each have the same lattice of cyclic flats, and so matroids cannot be defined solely in terms of their cyclic flats. We do not have a clean characterisation of families of sets that are cyclic flats of matroids. However, it may be possible to tell in polynomial time whether there is any matroid that has a given lattice of subsets as its cyclic flats. We use Bonin and de Mier’s cyclic flat axioms to reduce the problem to a linear program, and show that determining whether a given lattice is the lattice of cyclic flats of any matroid corresponds to finding integral points in the solution space of this program, these points representing the possible ranks that may be assigned to the cyclic flats. We distinguish several classes of lattice for which solutions may be efficiently found, based upon the nature of the matrix of coefficients of the linear program, and of the polyhedron it defines, and then identify families of lattice that belong to those classes. We define operations and transformations on lattices of sets by examining matroid operations, and examine how these operations affect membership in the aforementioned classes. We conjecture that it is always possible to determine, in polynomial time, whether a given collection of subsets makes up the lattice of cyclic flats of any matroid.</p>

Sign in / Sign up

Export Citation Format

Share Document