A Logical Theory of Truth-Makers and Falsity-Makers

2018 ◽  
Author(s):  
Neil Tennant
Keyword(s):  
Logical Consequence ◽  
Suitable Method ◽  
Elimination Rule ◽  
Logical Theory ◽  
Relative Truth ◽  
Logical Operator ◽  
First Order ◽  
Introduction Rule ◽  
Infinite Case ◽  
Ways Of Being

We explicate the different ways that a first-order sentence can be true (resp., false) in a model M, as formal objects, called (M-relative) truth-makers (resp., falsity-makers). M-relative truth-makers and falsity-makers are co-inductively definable, by appeal to the “atomic facts” in M, and to certain rules of verification and of falsification, collectively called rules of evaluation. Each logical operator has a rule of verification, much like an introduction rule; and a rule of falsification, much like an elimination rule. Applications of the rules (∀) and (∃) involve infinite furcation when the domain of M is infinite. But even in the infinite case, truth-makers and falsity-makers are tree-like objects whose branches are at most finitely long. A sentence φ is true (resp., false) in a model M (in the sense of Tarski) if and only if there existsπ such that π is an M-relative truth-maker (resp., falsity-maker) for φ. With “ways of being true” explicated as these logical truthmakers, one can re-conceive logical consequence between given premises and a conclusion. It obtains just in case there is a suitable method for transforming M-relative truthmakers for the premises into an M-relative truthmaker for the conclusion, whatever the model M may be.

A TYPE-FREE THEORY OF HALF-MONOTONE INDUCTIVE DEFINITIONS

1995 ◽  
Vol 06 (03) ◽  
pp. 203-234 ◽  
Author(s):  
YUKIYOSHI KAMEYAMA
Keyword(s):  
Type Theory ◽  
Characteristic Point ◽  
Logical Theory ◽  
Inductive Definition ◽  
Program Extraction ◽  
First Order ◽  
Inductive Definitions ◽  
Free Theory ◽  
Program Proof ◽  
Definition Of

This paper studies an extension of inductive definitions in the context of a type-free theory. It is a kind of simultaneous inductive definition of two predicates where the defining formulas are monotone with respect to the first predicate, but not monotone with respect to the second predicate. We call this inductive definition half-monotone in analogy of Allen’s term half-positive. We can regard this definition as a variant of monotone inductive definitions by introducing a refined order between tuples of predicates. We give a general theory for half-monotone inductive definitions in a type-free first-order logic. We then give a realizability interpretation to our theory, and prove its soundness by extending Tatsuta’s technique. The mechanism of half-monotone inductive definitions is shown to be useful in interpreting many theories, including the Logical Theory of Constructions, and Martin-Löf’s Type Theory. We can also formalize the provability relation “a term p is a proof of a proposition P” naturally. As an application of this formalization, several techniques of program/proof-improvement can be formalized in our theory, and we can make use of this fact to develop programs in the paradigm of Constructive Programming. A characteristic point of our approach is that we can extract an optimization program since our theory enjoys the program extraction theorem.

scholarly journals LOGIC OF RELATIVITY

2021 ◽  
pp. 42-52
Author(s):  
Ihor Ohirko ◽  
Zinovii Partyko
Keyword(s):  
Modal Logic ◽  
Symbolic Logic ◽  
Logical Theory ◽  
Relative Truth ◽  
Time Space ◽  
Different Types ◽  
Logical Method ◽  
Standard Values ◽  
The Difference ◽  
Modal Values

The problem of the truth of statements is considered. This study had the goal to develop a logical theory that would allow considering the context (the paradigm) from which would depend on the truth of the statement. For the development of such a theory, called the logic of relativity, the following methods of research are used as abstraction, analysis (traditional), synthesis, deduction, formalisation, axiomatisation, logical method. In order to develop the logic of relativity, it is expedient to use the achievements in the area of situational logic. Under the situation, it is proposed to understand two circumstances (time and space) and a condition that creates a context (paradigm) statement. Specifies the modal values that these three parameters can acquire and examines different types of situations. In order to write statements in the logic of relativity, a form of the statement of statements is proposed in the language of extended symbolic logic. For the theory of the logic of relativity, a set of four axioms is proposed and a series of laws. In particular, it is indicated that the values of the assertions in the logic of relativity are the following five estimates: truth, relative truth, relative is absurd, unclear, uncertain. Some theorems of the logic of relativity are proposed. A number of examples of texts in the natural language are given to interpret the statements of the logic of relativity. It is indicated that the proposed apparatus of the logic of relativity should be regarded as a kind of modal logic. The difference in the logic of relativity from situational logic is that it considers the factor of movement (motion) of statements in time, space and environment conditions, which was not considered by situational logic. The logic of relativity should be used wherever it is necessary to take into account the possibility of moving allegations regarding time, space and environment of conditions. One of the most important conclusions of the study is that in the logic to the standard values of truth (true, probably true, false, uncertain), it is expedient to add another value: relatively true (and accordingly: relatively false).

Bases for first-order theories and subtheories

1960 ◽  
Vol 25 (2) ◽  
pp. 97-142 ◽  
Author(s):  
William Craig
Keyword(s):  
Axiom System ◽  
Logical Theory ◽  
Theoretical Terms ◽  
First Order ◽  
Right Turns

The extent to which we can grasp the content of a (non-logical) theory, expressing it economically by means of an axiom system or basis, varies greatly. In this paper we shall investigate what degree of economy, or at least regularity, can be achieved for all recursively axiomatizable first-order theories. A useful approach, also of interest in its own right, turns out to be the study of bases for subtheories, where a subtheory of a given theory consists of those theorems from which certain predicate symbols are absent. These predicate symbols might be thought of as the formal counterparts of the “purely theoretical” terms employed by a science, the theory corresponding to the science itself and the subtheory to its “observational consequences”. Roughly speaking, the types of operations involving such predicate symbols will be reduced to a minimum, so that their syntactical role in deductions will emerge more clearly.

Logical consequence relations in logics of monotone predicates and logics of antitone predicates

2017 ◽  
pp. 021-029
Author(s):  
O.S. Shkilniak ◽  
Keyword(s):  
Logical Consequence ◽  
Consequence Relations ◽  
Consequence Relation ◽  
First Order ◽  
Different Types ◽  
Composition Algebras

Logical consequence is one of the fundamental concepts in logic. In this paper we study logical consequence relations for program-oriented logical formalisms: pure first-order composition nominative logics of quasiary predicates. In our research we are giving special attention to different types of logical consequence relations in various semantics of logics of monotone predicates and logics of antitone predicates. For pure first-order logics of quasiary predicates we specify composition algebras of predicates, languages, interpretation classes (sematics) and logical consequence relations. We obtain the pairwise distinct relations: irrefutability consequence P |= IR , consequence on truth P |= T , consequence on falsity P |= F, strong consequence P |= TF in P-sеmantics of partial singlevalued predicates and strong consequence R |= TF in R-sеmantics of partial multi-valued predicates. Of the total of 20 of defined logical consequence relations in logics of monotone predicates and of antitone predicates, the following ones are pairwise distinct: PE |= IR, PE |= T, PE |= F, PE |= TF, RM |= T, RM |= F, RM |= TF. A number of examples showing the differences between various types of logical consequence relations is given. We summarize the results concerning the existence of a particular logical consequence relation for certain sets of formulas in a table and determine interrelations between different types of logical consequence relations.

Some consistency proofs and a characterization of inconsistency proofs in illative combinatory logic

1987 ◽  
Vol 52 (1) ◽  
pp. 89-110 ◽  
Author(s):  
M. W. Bunder
Keyword(s):  
Normal Form ◽  
Propositional Calculus ◽  
Weak Form ◽  
Combinatory Logic ◽  
Major Premise ◽  
Elimination Rule ◽  
Introduction Rule ◽  
Consistency Proofs ◽  
Arbitrary Term

It is well known that combinatory logic with unrestricted introduction and elimination rules for implication is inconsistent in the strong sense that an arbitrary term Y is provable. The simplest proof of this, now usually called Curry's paradox, involves for an arbitrary term Y, a term X defined by X = Y(CPy).The fact that X = PXY = X ⊃ Y is an essential part of the proof.The paradox can be avoided by placing restrictions on the implication introduction rule or on the axioms from which it can be proved.In this paper we determine the forms that must be taken by inconsistency proofs of systems of propositional calculus based on combinatory logic, with arbitrary restrictions on both the introduction and elimination rules for the connectives. Generally such a proof will involve terms without normal form and cut formulas, i.e. formulas formed by an introduction rule that are immediately removed by an elimination with at most some equality steps intervening. (Such a sequence of steps we call a “cut”.)The above applies not only to the strong form of inconsistency defined above, but also to the weak form of inconsistency defined by: all propositions are provable, if this can be represented in the system.Any inconsistency proof of this kind of system can be reduced to one where the major premise of the elimination rule involved in the cut and its deduction must also appear in the deduction of the minor premise involved in the cut.We can, using this characterization of inconsistency proofs, put appropriate restrictions on certain introduction rules so that the systems, including a full classical propositional one, become provably consistent.

A normalization theorem for set theory

1988 ◽  
Vol 53 (3) ◽  
pp. 673-695 ◽  
Author(s):  
Sidney C. Bailin
Keyword(s):  
Set Theory ◽  
Natural Deduction ◽  
Inference Rule ◽  
Major Premise ◽  
Elimination Rule ◽  
Introduction Rule ◽  
Normalization Theorem ◽  
Image Position ◽  
Well Foundedness

In this paper we present a normalization theorem for a natural deduction formulation of Zermelo set theory. Our result gets around M. Crabbe's counterexample to normalizability (Hallnäs [3]) by adding an inference rule of the formand requiring that this rule be used wherever it is applicable. Alternatively, we can regard the result as pertaining to a modified notion of normalization, in which an inferenceis never considered reducible if A is T Є T, even if R is an elimination rule and the major premise of R is the conclusion of an introduction rule. A third alternative is to regard (1) as a derived rule: using the general well-foundedness rulewe can derive (1). If we regard (2) as neutral with respect to the normality of derivations (i.e., (2) counts as neither an introduction nor an elimination rule), then the resulting proofs are normal.

scholarly journals Proving Semantic Properties as First-Order Satisfiability (Extended Abstract)

2020 ◽  
Author(s):  
Salvador Lucas
Keyword(s):  
Logic Programming ◽  
Programming Languages ◽  
Answer Set Programming ◽  
Deductive Databases ◽  
Query Answering ◽  
Logical Theory ◽  
Data Bases ◽  
First Order ◽  
Computational Systems ◽  
Semantic Properties

The semantics of computational systems (e.g., relational and knowledge data bases, query-answering systems, programming languages, etc.) can often be expressed as (the specification of) a logical theory Th. Queries, goals, and claims about the behavior or features of the system can be expressed as formulas φ which should be checked with respect to the intended model of Th, which is often huge or even incomputable. In this paper we show how to prove such semantic properties φ of Th by just finding a model A of Th∪{φ}∪Zφ, where Zφ is an appropriate (possibly empty) theory depending on φ only. Applications to relational and deductive databases, rewriting-based systems, logic programming, and answer set programming are discussed.

scholarly journals Introducing Identity

2021 ◽  
Author(s):  
Owen Griffiths ◽  
Arif Ahmed
Keyword(s):  
Standard Approach ◽  
Logical Constant ◽  
Inference Rules ◽  
Elimination Rule ◽  
Leibniz’S Law ◽  
Logical Constants ◽  
Introduction Rule

AbstractThe best-known syntactic account of the logical constants is inferentialism . Following Wittgenstein’s thought that meaning is use, inferentialists argue that meanings of expressions are given by introduction and elimination rules. This is especially plausible for the logical constants, where standard presentations divide inference rules in just this way. But not just any rules will do, as we’ve learnt from Prior’s famous example of tonk, and the usual extra constraint is harmony. Where does this leave identity? It’s usually taken as a logical constant but it doesn’t seem harmonious: standardly, the introduction rule (reflexivity) only concerns a subset of the formulas canvassed by the elimination rule (Leibniz’s law). In response, Read [5, 8] and Klev [3] amend the standard approach. We argue that both attempts fail, in part because of a misconception regarding inferentialism and identity that we aim to identify and clear up.

Fragments of first order logic, I: universal Horn logic

1977 ◽  
Vol 42 (2) ◽  
pp. 221-237 ◽  
Author(s):  
George F. McNulty
Keyword(s):  
Existence Theorem ◽  
Predicate Logic ◽  
Logical Consequence ◽  
Horn Logic ◽  
First Order ◽  
Consistency Properties ◽  
Model Existence ◽  
Model Existence Theorem ◽  
Sharp Version ◽  
Horn Sentences

Let L be any finitary language. By restricting our attention to the universal Horn sentences of L and appealing to a semantical notion of logical consequence, we can formulate the universal Horn logic of L. The present paper provides some theorems about universal Horn logic that serve to distinguish it from the full first order predicate logic. Universal Horn equivalence between structures is characterized in two ways, one resembling Kochen's ultralimit theorem. A sharp version of Beth's definability theorem is established for universal Horn logic by means of a reduced product construction. The notion of a consistency property is relativized to universal Horn logic and the corresponding model existence theorem is proven. Using the model existence theorem another proof of the definability result is presented. The relativized consistency properties also suggest a syntactical notion of proof that lies entirely within the universal Horn logic. Finally, a decision problem in universal Horn logic is discussed. It is shown that the set of universal Horn sentences preserved under the formation of homomorphic images (or direct factors) is not recursive, provided the language has at least two unary function symbols or at least one function symbol of rank more than one.This paper begins with a discussion of how algebraic relations between structures can be used to obtain fragments of a given logic. Only two such fragments seem to be under current investigation: equational logic and universal Horn logic. Other fragments which seem interesting are pointed out.

Sign in / Sign up

Export Citation Format

Share Document