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.

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.

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

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.

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.

First-Order Logic Reasoning Support for the Semantic Web

2009 ◽  
Vol 19 (12) ◽  
pp. 3091-3099 ◽  
Author(s):  
Gui-Hong XU ◽  
Jian ZHANG
Keyword(s):  
Semantic Web ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Logic Reasoning

Boolean-valued structures

2018 ◽  
Author(s):  
Tim Button ◽  
Sean Walsh
Keyword(s):  
Model Theory ◽  
Order Logic ◽  
First Order Logic ◽  
Inference Rules ◽  
Mathematical Concepts ◽  
Semantic Framework ◽  
First Order ◽  
Standard Models ◽  
Boolean Valued Model ◽  
Semantic Values

Chapters 6-12 are driven by questions about the ability to pin down mathematical entities and to articulate mathematical concepts. This chapter is driven by similar questions about the ability to pin down the semantic frameworks of language. It transpires that there are not just non-standard models, but non-standard ways of doing model theory itself. In more detail: whilst we normally outline a two-valued semantics which makes sentences True or False in a model, the inference rules for first-order logic are compatible with a four-valued semantics; or a semantics with countably many values; or what-have-you. The appropriate level of generality here is that of a Boolean-valued model, which we introduce. And the plurality of possible semantic values gives rise to perhaps the ‘deepest’ level of indeterminacy questions: How can humans pin down the semantic framework for their languages? We consider three different ways for inferentialists to respond to this question.

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.

Sign in / Sign up

Export Citation Format

Share Document