Near-equational and equational systems of logic for partial functions. I

1989 ◽  
Vol 54 (3) ◽  
pp. 795-827 ◽  
Author(s):  
William Craig
Keyword(s):  
Proof Theory ◽  
Predicate Symbol ◽  
Expressive Power ◽  
Equational Logic ◽  
Partial Functions ◽  
Logical Connectives ◽  
Similar Proof ◽  
Existence Conditions ◽  
Logical Functions ◽  
Horn Sentences

Equational logic for total functions is a remarkable fragment of first-order logic. Rich enough to lend itself to many uses, it is also quite austere. The only predicate symbol is one for a notion of equality, and there are no logical connectives. Proof theory for equational logic therefore is different from proof theory for other logics and, in some respects, more transparent. The question therefore arises to what extent a logic with a similar proof theory can be constructed when expressive power is increased.The increase mainly studied here allows one both to consider arbitrary partial functions and to express the condition that a function be total. A further increase taken into account is equivalent to a change to universal Horn sentences for partial and for total functions.Two ways of increasing expressive power will be considered. In both cases, the notion of equality is modified and nonlogical function symbols are interpreted as ranging over partial functions, instead of ranging only over total functions. In one case, the only further change is the addition of symbols that denote logical functions, such as the binary projection function Ae that maps each pair ‹a0, a1› of elements of a set A into the element a0. An addition of this kind results in a language, and also in a system of logic based on this language, which we call equational In the other case, instead of adding a symbol for Ae, one admits those special universal Horn sentences in which the conditions expressed by the antecedent are, in a sense, pure conditions of existence. Languages and systems of logic that result from a change of this kind will be called near-equational. According to whether the number of existence conditions that one may express in antecedents is finite or arbitrary, the resulting language and logic shall be finite or infinitary, respectively. Each of our finite near-equational languages turns out to be equivalent to one of our equational languages, and vice versa.

A system of logic for partial functions under existence-dependent kleene equality

1988 ◽  
Vol 53 (3) ◽  
pp. 834-839 ◽  
Author(s):  
H. Andréka ◽  
W. Craig ◽  
I. Németi
Keyword(s):  
Practical Interest ◽  
Order Logic ◽  
First Order Logic ◽  
Basic Relation ◽  
Equational Logic ◽  
Partial Functions ◽  
First Order ◽  
Complete Set ◽  
The Subject ◽  
Relationship Of

Ordinary equational logic is a connective-free fragment of first-order logic which is concerned with total functions under the relation of ordinary equality. In [AN] (see also [AN1]) and in [Cr] it has been extended in two equivalent ways into a near-equational system of logic for partial functions. The extension given in [Cr] deals with partial functions under two relationships: a relationship of existence-dependent existence and one of existence-dependent Kleene equality. For the language that involves both relationships a set of rules was given that is complete. Those rules in the set that involve only existence-dependent existence turned out to be complete for the sublanguage that involves this relationship only. In the present paper we give a set of rules that is complete for the other sublanguage, namely the language of partial functions under existence-dependent Kleene equality.This language lacks a certain, often needed, power of expressing existence and fails, in particular, to be an extension of the language that underlies ordinary equational logic. That it possesses a fairly simple complete set of rules is therefore perhaps more of theoretical than of practical interest. The present paper is thus intended to serve as a supplement to [Cr] and, less directly, to [AN]. The subject is further rounded out, and some contrast is provided, by [Rob]. The systems of logic treated there are based on the weaker language in which partial functions are considered under the more basic relation of Kleene equality.

scholarly journals Proof Theory and Computational Analysis

1997 ◽  
Vol 4 (30) ◽  
Author(s):  
Ulrich Kohlenbach
Keyword(s):  
Proof Theory ◽  
Computational Analysis ◽  
Numerical Data ◽  
Expressive Power ◽  
Rates Of Convergence ◽  
Uniform Bounds ◽  
Survey Paper ◽  
Constructive Proofs ◽  
Polynomial Bounds ◽  
The Relationship

In this survey paper we start with a discussion how functionals of finite type can be used for the proof-theoretic extraction of numerical data (e.g. effective<br />uniform bounds and rates of convergence) from non-constructive proofs in numerical analysis. We focus on the case where the extractability of polynomial bounds is guaranteed.<br />This leads to the concept of hereditarily polynomial bounded analysis (PBA). We indicate the mathematical range of PBA which turns out to be surprisingly large. Finally we discuss the relationship between PBA and so-called feasible analysis<br />FA. It turns out that both frameworks are incomparable. We argue in favor of the thesis that PBA offers the more useful approach for the purpose of extracting mathematically interesting bounds from proofs. In a sequel of appendices to this paper we indicate the expressive power of PBA.

Beth’s theorem and Craig’s theorem

2018 ◽  
Author(s):  
Zeno Swijtink
Keyword(s):  
Sufficient Conditions ◽  
Predicate Symbol ◽  
Expressive Power ◽  
Order Logic ◽  
First Order Logic ◽  
Infinite Length ◽  
First Order ◽  
Explicit Definition ◽  
Central Result ◽  
Definition Of

Beth’s theorem is a central result about definability of non-logical symbols in classical first-order theories. It states that a symbol P is implicitly defined by a theory T if and only if an explicit definition of P in terms of some other expressions of the theory T can be deduced from the theory T. Intuitively, the symbol P is implicitly defined by T if, given the extension of these other symbols, T fixes the extension of the symbol P uniquely. In a precise statement of Beth’s theorem this will be replaced by a condition on the models of T. An explicit definition of a predicate symbol states necessary and sufficient conditions: for example, if P is a one-place predicate symbol, an explicit definition is a sentence of the form (x) (Px ≡φ(x)), where φ(x) is a formula with free variable x in which P does not occur. Thus, Beth’s theorem says something about the expressive power of first-order logic: there is a balance between the syntax (the deducibility of an explicit definition) and the semantics (across models of T the extension of P is uniquely determined by the extension of other symbols). Beth’s definability theorem follows immediately from Craig’s interpolation theorem. For first-order logic with identity, Craig’s theorem says that if φ is deducible from ψ, there is an interpolant θ, a sentence whose non-logical symbols are common to φ and ψ, such that θ is deducible from ψ, while φ is deducible from θ. Craig’s theorem and Beth’s theorem also hold for a number of non-classical logics, such as intuitionistic first-order logic and classical second-order logic, but fail for other logics, such as logics with expressions of infinite length.

scholarly journals Algebraic properties of if-then-else and commutative three-valued tests

2019 ◽  
Vol 29 (04) ◽  
pp. 743-759
Author(s):  
Khí-Uí Soo ◽  
Tim Stokes
Keyword(s):  
Short Circuit ◽  
The Other ◽  
Partial Functions ◽  
Evaluation Strategy ◽  
Algebraic Properties ◽  
Logical Connectives ◽  
The Common ◽  
Parallel Evaluation ◽  
Partial Predicates ◽  
Main Operation

This paper establishes a finite axiomatization of possibly non-halting computer programs and tests, with the if-then-else operation. The model is a two-sorted algebra, with one sort being the programs and the other being the tests. The main operation on programs is composition, and 1 and 0 represent the programs skip and loop (i.e. never halts) respectively. Programs are modeled as partial functions on some state space [Formula: see text], with tests modeled as partial predicates on [Formula: see text]. The operations on the tests are the usual logical connectives ∧, ∨, [Formula: see text], [Formula: see text] and [Formula: see text]. In addition, there is the hybrid operation of if-then-else, and the test-valued operation [Formula: see text] on programs which is true when a program halts, and undefined otherwise. The halting operation [Formula: see text] implies that operations of domain [Formula: see text] and domain join ∨ may also be expressed. When tests are assumed to be possibly non-halting, the evaluation strategy of the logical connectives affects the result. Here we model parallel evaluation, as opposed to the common sequential (or short-circuit) evaluation strategy. For example, we view [Formula: see text] as false if either [Formula: see text] or [Formula: see text] is false, even if the other does not halt.

LINEAR TIME IN HYPERSEQUENT FRAMEWORK

2016 ◽  
Vol 22 (1) ◽  
pp. 121-144 ◽  
Author(s):  
ANDRZEJ INDRZEJCZAK
Keyword(s):  
Proof Theory ◽  
Linear Time ◽  
Expressive Power ◽  
Sequent Calculi ◽  
Temporal Logics ◽  
Structural Rules ◽  
Proof Systems ◽  
Nonclassical Logics ◽  
Time Flow ◽  
Basic Calculus

AbstractHypersequent calculus (HC), developed by A. Avron, is one of the most interesting proof systems suitable for nonclassical logics. Although HC has rather simple form, it increases significantly the expressive power of standard sequent calculi (SC). In particular, HC proved to be very useful in the field of proof theory of various nonclassical logics. It may seem surprising that it was not applied to temporal logics so far. In what follows, we discuss different approaches to formalization of logics of linear frames and provide a cut-free HC formalization ofKt4.3, the minimal temporal logic of linear frames, and some of its extensions. The novelty of our approach is that hypersequents are defined not as finite (multi)sets but as finite lists of ordinary sequents. Such a solution allows both linearity of time flow, and symmetry of past and future, to be incorporated by means of six temporal rules (three for future-necessity and three dual rules for past-necessity). Extensions of the basic calculus with simple structural rules cover logics of serial and dense frames. Completeness is proved by Schütte/Hintikka-style argument using models built from saturated hypersequents.

Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory

1957 ◽  
Vol 22 (3) ◽  
pp. 269-285 ◽  
Author(s):  
William Craig
Keyword(s):  
Model Theory ◽  
Proof Theory ◽  
Functional Relationship ◽  
Elementary Proof ◽  
Expressive Power ◽  
Second Order ◽  
Order System ◽  
First Order ◽  
Herbrand’S Theorem ◽  
Opening Up

One task of metamathematics is to relate suggestive but nonelementary modeltheoretic concepts to more elementary proof-theoretic concepts, thereby opening up modeltheoretic problems to proof-theoretic methods of attack. Herbrand's Theorem (see [8] or also [9], vol. 2) or Gentzen's Extended Hauptsatz (see [5] or also [10]) was first used along these lines by Beth [1]. Using a modified version he showed that for all first-order systems a certain modeltheoretic notion of definability coincides with a certain proof theoretic notion. In the present paper the Herbrand-Gentzen Theorem will be applied to generalize Beth's results from primitive predicate symbols to arbitrary formulas and terms.This may be interpreted as showing that (apart from some relatively minor exceptions which will be made apparent below) the expressive power of each first-order system is rounded out, or the system is functionally complete, in the following sense: Any functional relationship which obtains between concepts that are expressible in the system is itself expressible and provable in the system.A second application is concerned with the hierarchy of second-order formulas. A certain relationship is shown to hold between first-order formulas and those second-order formulas which are of the form (∃T1)…(∃Tk)A or (T1)…(Tk)A with A being a first-order formula. Modeltheoretically this can be regarded as a relationship between the class AC and the class PC⊿ of sets of models, investigated by Tarski in [12] and [13].

scholarly journals Corrigendum to: V. A. Sokolov, “On the Existence Problem of Finite Bases of Identities in the Algebras of Recursive Functions”, Modeling and analysis of information systems, vol. 27, no. 3, pp. 304-315, 2020. DOI: https://doi.org/10.18255/1818-1015-2020-3-304-315

2020 ◽  
Vol 27 (4) ◽  
pp. 510-511
Author(s):  
Valery Anatolyevich Demidov
Keyword(s):  
New York ◽  
American Mathematical Society ◽  
Mathematical Society ◽  
Reference List ◽  
Equational Logic ◽  
Partial Functions ◽  
Article Title ◽  
Modeling And Analysis ◽  
Recursive Functions ◽  
Primitive Recursive

The author regrets that in the original list the references [3] and [4] are in the wrong places and they should be rearranged. In addition, [3] has the wrong article title. The corrected reference list is shown below.The author would like to apologize for an inconvenience caused.References[1] A. I. Mal'tsev, “Constructive algebras I”, Russian Mathematical Surveys, vol. 16, no. 3, pp. 77-129, 1961.[2] A. I. Mal'tsev, Algoritmy i rekursivnye funktsii. Moscow: Nauka, 1965, In Russian.[3] R. M. Robinson, “Primitive recursive functions”, Bulletin of the American Mathematical Society, vol. 53, no. 10,pp. 925-942, 1947.[4] J. Robinson, “General recursive functions”, Proceedings of the American Mathematical Society, vol. 1, no. 6,pp. 703-718, 1950.[5] V. A. Sokolov, “Ob odnom klasse tozhdestv v algebre Robinsona”, in 14-ya Vsesoyuznaya algebraicheskaya konferentsiya: tezisy dokladov, In Russian, vol. 2, Novosibirsk, 1977, pp. 123-124.[6] P. M. Cohn, Universal Algebra. New York, Evanston, and London: Harper & Row, 1965.[7] A. Robinson, “Equational logic for partial functions under Kleene equality: a complete and an incomplete set of rules”, The Journal of Symbolic Logic, vol. 54, no. 2, pp. 354-362, 1989.

Equational logic of partial functions under Kleene equality: a complete and an incomplete set of rules

1989 ◽  
Vol 54 (2) ◽  
pp. 354-362 ◽  
Author(s):  
Anthony Robinson
Keyword(s):  
Inference Rule ◽  
Logical Consequence ◽  
Equational Logic ◽  
Inference Rules ◽  
Partial Functions ◽  
Substitution Rule ◽  
Valid Inference ◽  
Recursively Enumerable ◽  
Complete Set ◽  
Recursive Set

When equational logic for partial functions is interpreted using Kleene equality as the predicate, the relation of logical consequence may be said to express what identities of partial functions follow from a given set of identities. In the analogous situation for total functions, there is a complete set of inference rules consisting of reflexivity, symmetry, transitivity, replacement, and substitution; in the case of partial functions, unrestricted substitution fails to be a valid inference rule, and there remains the question of how to obtain a complete set of rules. The first part of the present paper shows that completeness cannot be obtained by a mere restriction of the substitution rule, for a counterexample shows that even a rule allowing substitution in all consequentially valid instances fails, in conjunction with the other four rules, to yield a complete set of rules.The second part of the paper defines a combined rule of transitivity-substitution which, in conjunction with reflexivity, symmetry, replacement, and substitution only of variables, yields a complete set of rules. The new rule is first stated in a form that allows an unbounded number of premises, and then is altered to a three-premise form. In both forms, the rule suffers from the shortcoming that in its formulation an auxiliary notion of conditional existence is involved, which is given by a recursive syntactic definition. As a result, the set of instantiations of the rule is recursively enumerable, but not (apparently) recursive (assuming a recursive set of premises).

Sign in / Sign up

Export Citation Format

Share Document