Some New Exceptions for the Semantic Tableaux Version of the Second Incompleteness Theorem

2002 ◽  
pp. 281-297 ◽  
Author(s):  
Dan E. Willard
Keyword(s):  
Incompleteness Theorem ◽  
Semantic Tableaux

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.

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].)

scholarly journals FINDING THE LIMIT OF INCOMPLETENESS I

2020 ◽  
Vol 26 (3-4) ◽  
pp. 268-286
Author(s):  
YONG CHENG
Keyword(s):  
Model Theory ◽  
Recursion Theory ◽  
Minimal Degree ◽  
Incompleteness Theorem ◽  
Turing Degree ◽  
Turing Reducibility ◽  
Inseparable Pair

AbstractIn this paper, we examine the limit of applicability of Gödel’s first incompleteness theorem ($\textsf {G1}$ for short). We first define the notion “$\textsf {G1}$ holds for the theory $T$”. This paper is motivated by the following question: can we find a theory with a minimal degree of interpretation for which $\textsf {G1}$ holds. To approach this question, we first examine the following question: is there a theory T such that Robinson’s $\mathbf {R}$ interprets T but T does not interpret $\mathbf {R}$ (i.e., T is weaker than $\mathbf {R}$ w.r.t. interpretation) and $\textsf {G1}$ holds for T? In this paper, we show that there are many such theories based on Jeřábek’s work using some model theory. We prove that for each recursively inseparable pair $\langle A,B\rangle $, we can construct a r.e. theory $U_{\langle A,B\rangle }$ such that $U_{\langle A,B\rangle }$ is weaker than $\mathbf {R}$ w.r.t. interpretation and $\textsf {G1}$ holds for $U_{\langle A,B\rangle }$. As a corollary, we answer a question from Albert Visser. Moreover, we prove that for any Turing degree $\mathbf {0}< \mathbf {d}<\mathbf {0}^{\prime }$, there is a theory T with Turing degree $\mathbf {d}$ such that $\textsf {G1}$ holds for T and T is weaker than $\mathbf {R}$ w.r.t. Turing reducibility. As a corollary, based on Shoenfield’s work using some recursion theory, we show that there is no theory with a minimal degree of Turing reducibility for which $\textsf {G1}$ holds.

An algebraic study of Diodorean modal systems

1965 ◽  
Vol 30 (1) ◽  
pp. 58-64 ◽  
Author(s):  
R. A. Bull
Keyword(s):  
Discrete Time ◽  
Decision Procedure ◽  
John Locke ◽  
Original Model ◽  
Completeness Proof ◽  
Semantic Tableaux ◽  
Algebraic Treatment ◽  
Algebraic Result ◽  
Modal Systems

Attention was directed to modal systems in which ‘necessarily α’ is interpreted as ‘α. is and always will be the case’ by Prior in his John Locke Lectures of 1956. The present paper shows that S4.3, the extension of S4 withALCLpLqLCLqLp,is complete with respect to this interpretation when time is taken to be continuous, and that D, the extension of S4.3 withALNLpLCLCLCpLpLpLp,is complete with respect to this interpretation when time is taken to be discrete. The method employed depends upon the application of an algebraic result of Garrett Birkhoff's to the models for these systems, in the sense of Tarski.A considerable amount of work on S4.3 and D precedes this paper. The original model with discrete time is given in Prior's [7] (p. 23, but note the correction in [8]); that taking time to be continuous yields a weaker system is pointed out by him in [9]. S4.3 and D are studied in [3] of Dummett and Lemmon, where it is shown that D includes S4.3 andCLCLCpLpLpCMLpLp.While in Oxford in 1963, Kripke proved that these were in fact sufficient for D, using semantic tableaux. A decision procedure for S4.3, using Birkhoff's result, is given in my [2]. Dummett conjectured, in a conversation, that taking time to be continuous yielded S4.3. Thus the originality of this paper lies in giving a suitable completeness proof for S4.3, and in the unified algebraic treatment of the systems. It should be emphasised that the credit for first axiomatising D belongs to Kripke.

End extensions of models of weak arithmetics

2016 ◽  
Author(s):  
Βασίλειος Πασχάλης
Keyword(s):  
Semantic Tableaux

Η διδακτορική διατριβή ασχολείται με τη μελέτη προβλημάτων που αφορούν τελικές επεκτάσεις μοντέλων υποσυστημάτων της πρωτοβάθμιας αριθμητικής Peano. Πιο συγκεκριμένα, το πρόβλημα του J. Paris: «Υπάρχει, για κάθε αριθμήσιμο μοντέλο της Σ_1 συλλογής γνήσια τελική επέκτασή του που ικανοποιεί την ∆_0 επαγωγή;» παραμένει ανοικτό.Το πρόβλημα μελέτησαν οι J. Paris και A. Wilkie (1989), οι οποίοι απέδειξαν ότι ικανή συνθήκη για θετική απάντηση είναι το μοντέλο να είναι I∆_0 -πλήρες (όπου με I∆_0 συμβολίζεται η θεωρία της ∆_0 -επαγωγής). Αποδεικνύουμε ότι η χρήση της έννοιας της I∆_0 -πληρότητας μπορεί να παρακαμφθεί και στη θέση της να χρησιμοποιηθεί η τυποποίηση του κλασικού επιχειρήματος του θεωρήματος πληρότητας (θεώρημα Hilbert-Bernays), με χρήση σημασιολογικών πινάκων (semantic tableaux).Επιπλέον, με την ίδια μεθοδολογία κατάλληλα τροποποιημένη αποδεικνύουμε τη γενίκευση του αποτελέσματος, δηλαδή ότι για κάθε αριθμήσιμο μοντέλο της Σ_n -συλλογής, n > 1, υπάρχει γνήσια Σ_n -στοιχειώδης τελική επέκτασή του που ικανοποιεί την ∆_0 -επαγωγή.

Sign in / Sign up

Export Citation Format

Share Document