Hilbert's program and the omega-rule

1994 ◽  
Vol 59 (1) ◽  
pp. 322-343 ◽  
Author(s):  
Aleksandar Ignjatović
Keyword(s):  
Number Theory ◽  
Reverse Mathematics ◽  
Order Logic ◽  
Incompleteness Theorem ◽  
The Other ◽  
First Order Logic ◽  
Elementary Number Theory ◽  
First Order ◽  
Philosophical Significance ◽  
Mathematics Program

AbstractIn the first part of this paper we discuss some aspects of Detlefsen's attempt to save Hilbert's Program from the consequences of Gödel's Second Incompleteness Theorem. His arguments are based on his interpretation of the long standing and well-known controversy on what, exactly, finitistic means are. In his paper [1] Detlefsen takes the position that there is a form of the ω-rule which is a finitistically valid means of proof, sufficient to prove the consistency of elementary number theory Z. On the other hand, he claims that Z with its first-order logic is not strong enough to allow a formalization of such an ω-rule. This would explain why the unprovability of Con(Z) in Z does not imply that the consistency of Z cannot be proved by finitistic means. We show that Detlefsen's proposal is unacceptable as originally formulated in [1], but that a reasonable modification of the rule he suggest leads to a partial program already studied for many years. We investigate the scope of such a program in terms of proof-theoretic reducibilities. We also show that this partial program encompasses mathematically important theories studied in the “Reverse Mathematics” program. In order to investigate the provability with such a modified rule, we define new consistency and provability predicates which are weaker than the usual ones. We then investigate their properties, including a few that have no apparent philosophical significance but compare interestingly with the properties of the program based on the iteration of our ω-rule. We determine some of the limitations of such programs, pointing out that these limitations partly explain why partial programs that have been successfully carried out use quite different and substantially more radical extensions of finitistic methods with more general forms of restricted reasoning.

Fictional Propositions and the Unprovability of Consistency

2006 ◽  
Vol 72 (1) ◽  
pp. 201-210
Author(s):  
Enrico Martino
Keyword(s):  
Order Logic ◽  
Incompleteness Theorem ◽  
First Order Logic ◽  
First Order

We introduce an epistemic version of validity and completeness of first order logic, based on the notions of and . We then show how the perspective here considered may help to solve an epistemic puzzle arising from Gödel's second incompleteness theorem.

scholarly journals Taking Plurals at Face Value

2021 ◽  
pp. 8-30
Author(s):  
Salvatore Florio ◽  
Øystein Linnebo
Keyword(s):  
Philosophy Of Mathematics ◽  
Expressive Power ◽  
Order Logic ◽  
First Order Logic ◽  
Logical System ◽  
Plural Logic ◽  
First Order ◽  
Philosophical Significance ◽  
Pure Logic

Plural logic is a logical system in which plural terms and predicates figure as primitive expressions alongside the singular resources of ordinary first-order logic. The philosophical significance of this system depends on two of its alleged features: being pure logic and providing more expressive power than first-order logic. This chapter first introduces the language and axioms of plural logic and then analyzes this logic’s main philosophical applications in metaphysics, philosophy of mathematics, and semantics.

ON LÖWENHEIM–SKOLEM–TARSKI NUMBERS FOR EXTENSIONS OF FIRST ORDER LOGIC

2011 ◽  
Vol 11 (01) ◽  
pp. 87-113 ◽  
Author(s):  
MENACHEM MAGIDOR ◽  
JOUKO VÄÄNÄNEN
Keyword(s):  
Order Logic ◽  
Strong Form ◽  
The Other ◽  
First Order Logic ◽  
Supercompact Cardinal ◽  
Inaccessible Cardinal ◽  
First Order ◽  
Inner Model ◽  
Singular Cardinals ◽  
Second Order Logic

We show that, assuming the consistency of a supercompact cardinal, the first (weakly) inaccessible cardinal can satisfy a strong form of a Löwenheim–Skolem–Tarski theorem for the equicardinality logic L(I), a logic introduced in [5] strictly between first order logic and second order logic. On the other hand we show that in the light of present day inner model technology, nothing short of a supercompact cardinal suffices for this result. In particular, we show that the Löwenheim–Skolem–Tarski theorem for the equicardinality logic at κ implies the Singular Cardinals Hypothesis above κ as well as Projective Determinacy.

Finite Axiomatizability using additional predicates

1958 ◽  
Vol 23 (3) ◽  
pp. 289-308 ◽  
Author(s):  
W. Craig ◽  
R. L. Vaught
Keyword(s):  
Order Logic ◽  
The Other ◽  
First Order Logic ◽  
Logical Constant ◽  
Finite Axiomatizability ◽  
Logical Constants ◽  
First Order

By a theory we shall always mean one of first order, having finitely many non-logical constants. Then for theories with identity (as a logical constant, the theory being closed under deduction in first-order logic with identity), and also likewise for theories without identity, one may distinguish the following three notions of axiomatizability. First, a theory may be recursively axiomatizable, or, as we shall say, simply, axiomatizable. Second, a theory may be finitely axiomatizable using additional predicates (f. a.+), in the syntactical sense introduced by Kleene [9]. Finally, the italicized phrase may also be interpreted semantically. The resulting notion will be called s. f. a.+. It is closely related to the modeltheoretic notion PC introduced by Tarski [16], or rather, more strictly speaking, to PC∩ACδ.For arbitrary theories with or without identity, it is easily seen that s. f. a.+ implies f. a.+ and it is known that f. a.+ implies axiomatizability. Thus it is natural to ask under what conditions the converse implications hold, since then the notions concerned coincide and one can pass from one to the other.Kleene [9] has shown: (1) For arbitrary theories without identity, axiomatizability implies f. a.+. It also follows from his work that : (2) For theories with identity which have only infinite models, axiomatizability implies f. a.+.

The relative expressive power of some logics extending first-order logic

1979 ◽  
Vol 44 (2) ◽  
pp. 129-146 ◽  
Author(s):  
John Cowles
Keyword(s):  
Model Theory ◽  
Expressive Power ◽  
Second Order ◽  
Order Logic ◽  
The Other ◽  
First Order Logic ◽  
Finite Sets ◽  
Limited Ability ◽  
First Order ◽  
Second Order Logic

In recent years there has been a proliferation of logics which extend first-order logic, e.g., logics with infinite sentences, logics with cardinal quantifiers such as “there exist infinitely many…” and “there exist uncountably many…”, and a weak second-order logic with variables and quantifiers for finite sets of individuals. It is well known that first-order logic has a limited ability to express many of the concepts studied by mathematicians, e.g., the concept of a wellordering. However, first-order logic, being among the simplest logics with applications to mathematics, does have an extensively developed and well understood model theory. On the other hand, full second-order logic has all the expressive power needed to do mathematics, but has an unworkable model theory. Indeed, the search for a logic with a semantics complex enough to say something, yet at the same time simple enough to say something about, accounts for the proliferation of logics mentioned above. In this paper, a number of proposed strengthenings of first-order logic are examined with respect to their relative expressive power, i.e., given two logics, what concepts can be expressed in one but not the other?For the most part, the notation is standard. Most of the notation is either explained in the text or can be found in the book [2] of Chang and Keisler. Some notational conventions used throughout the text are listed below: the empty set is denoted by ∅.

Semantics for first-order superposition logic

2019 ◽  
Vol 27 (4) ◽  
pp. 570-595
Author(s):  
Athanassios Tzouvaras
Keyword(s):  
Order Logic ◽  
The Other ◽  
First Order Logic ◽  
Choice Functions ◽  
First Order ◽  
Total Failure ◽  
Syntactic Restrictions

Abstract We investigate how the sentence choice semantics (SCS) for propositional superposition logic (PLS) developed in Tzouvaras (2018, Logic Journal of the IGPL, 26, 149–190) could be extended so as to successfully apply to first-order superposition logic (FOLS). There are two options for such an extension. The apparently more natural one is the formula choice semantics (FCS) based on choice functions for pairs of arbitrary formulas of the basis language. It is proved however that the universal instantiation scheme of first-order logic, $(\forall v)\varphi (v)\rightarrow \varphi (t)$, is false, as a scheme of tautologies, with respect to FCS. This causes the total failure of FCS as a candidate semantics. Then we turn to the other option, which is a variant of SCS, since it uses again choice functions for pairs of sentences only. This semantics however presupposes that the applicability of the connective | is restricted to quantifier-free sentences, and thus the class of well-formed formulas and sentences of the language is restricted too. Granted these syntactic restrictions, the usual axiomatizations of FOLS turn out to be sound and conditionally complete with respect to this second semantics, just like the corresponding systems of PLS.

scholarly journals Goldbach Conjecture, Twin Primes Conjecture, and Bounded Gap Theorem in the language of number theory

2021 ◽  
Author(s):  
Matheus Pereira Lobo
Keyword(s):  
Number Theory ◽  
White Paper ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Twin Primes ◽  
Gap Theorem

We write the formulas of the theorem and the conjectures highlighted in the title of this white paper in the language of number theory for pedagogical purpose in first-order logic.

scholarly journals Parameterized Synthesis for Fragments of First-Order Logic Over Data Words

2020 ◽  
pp. 97-118
Author(s):  
Béatrice Bérard ◽  
Benedikt Bollig ◽  
Mathieu Lehaut ◽  
Nathalie Sznajder
Keyword(s):  
Finite Number ◽  
Classical Case ◽  
Order Logic ◽  
The Other ◽  
Synthesis Problem ◽  
First Order Logic ◽  
First Order ◽  
Bounded Number ◽  
Other Hand

AbstractWe study the synthesis problem for systems with a parameterized number of processes. As in the classical case due to Church, the system selects actions depending on the program run so far, with the aim of fulfilling a given specification. The difficulty is that, at the same time, the environment executes actions that the system cannot control. In contrast to the case of fixed, finite alphabets, here we consider the case of parameterized alphabets. An alphabet reflects the number of processes, which is static but unknown. The synthesis problem then asks whether there is a finite number of processes for which the system can satisfy the specification. This variant is already undecidable for very limited logics. Therefore, we consider a first-order logic without the order on word positions. We show that even in this restricted case synthesis is undecidable if both the system and the environment have access to all processes. On the other hand, we prove that the problem is decidable if the environment only has access to a bounded number of processes. In that case, there is even a cutoff meaning that it is enough to examine a bounded number of process architectures to solve the synthesis problem.

CAPTURING CONSEQUENCE

2019 ◽  
Vol 12 (2) ◽  
pp. 271-295
Author(s):  
ALEXANDER PASEAU
Keyword(s):  
Propositional Logic ◽  
Semantic Theory ◽  
Second Order ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Philosophical Significance ◽  
The Third ◽  
Important Sense ◽  
Compare And Contrast

AbstractFirst-order formalisations are often preferred to propositional ones because they are thought to underwrite the validity of more arguments. We compare and contrast the ability of some well-known logics—these two in particular—to formally capture valid and invalid arguments. We show that there is a precise and important sense in which first-order logic does not improve on propositional logic in this respect. We also prove some generalisations and related results of philosophical interest. The rest of the article investigates the results’ philosophical significance. A first moral is that the correct way to state the oft-cited superiority of first-order logic vis-à-vis propositional logic is more nuanced than often thought. The second moral concerns semantic theory; the third logic’s use as a tool for discovery. A fourth and final moral is that second-order logic’s transcendence of first-order logic is greater than first-order logic’s transcendence of propositional logic.

scholarly journals Blocked Clauses in First-Order Logic

10.29007/c3wq ◽  
2018 ◽  
Author(s):  
Benjamin Kiesl ◽  
Martin Suda ◽  
Martina Seidl ◽  
Hans Tompits ◽  
Armin Biere
Keyword(s):  
Polynomial Algorithm ◽  
Order Logic ◽  
The Other ◽  
First Order Logic ◽  
First Order ◽  
Theorem Provers ◽  
Problem Instances

Blocked clauses provide the basis for powerful reasoning techniques used in SAT, QBF, and DQBF solving. Their definition, which relies on a simple syntactic criterion, guarantees that they are both redundant and easy to find. In this paper, we lift the notion of blocked clauses to first-order logic. We introduce two types of blocked clauses, one for first-order logic with equality and the other for first-order logic without equality, and prove their redundancy. In addition, we give a polynomial algorithm for checking whether a clause is blocked. Based on our new notions of blocking, we implemented a novel first-order preprocessing tool. Our experiments showed that many first-order problems in the TPTP library contain a large number of blocked clauses whose elimination can improve the performance of modern theorem provers, especially on satisfiable problem instances.

Sign in / Sign up

Export Citation Format

Share Document