Equivalences between logics and their representing type theories

1995 ◽  
Vol 5 (3) ◽  
pp. 323-349 ◽  
Author(s):  
Philippa Gardner
Keyword(s):  
Natural Deduction ◽  
Order Logic ◽  
First Order Logic ◽  
Logical Framework ◽  
Simple Formulation ◽  
First Order ◽  
Relevant Logics ◽  
First Time ◽  
New Framework

We propose a new framework for representing logics, called LF+, which is based on the Edinburgh Logical Framework. The new framework allows us to give, apparently for the first time, general definitions that capture how well a logic has been represented. These definitions are possible because we are able to distinguish in a generic way that part of the LF+ entailment corresponding to the underlying logic. This distinction does not seem to be possible with other frameworks. Using our definitions, we show that, for example, natural deduction first-order logic can be well-represented in LF+, whereas linear and relevant logics cannot. We also show that our syntactic definitions of representation have a simple formulation as indexed isomorphisms, which both confirms that our approach is a natural one and provides a link between type-theoretic and categorical approaches to frameworks.

scholarly journals Reduction in first-order logic compared with reduction in implicational logic

2007 ◽  
Vol 5 ◽  
Author(s):  
Tigran M. Galoyan
Keyword(s):  
Natural Deduction ◽  
Order Logic ◽  
First Order Logic ◽  
Strong Normalization ◽  
First Order ◽  
Reduction Sequence

In this paper we discuss strong normalization for natural deduction in the →∀-fragment of first-order logic. The method of collapsing types is used to transfer the result (concerning strong normalization) from implicational logic to first-order logic. The result is improved by a complement, which states that the length of any reduction sequence of derivation term r in first-order logic is equal to the length of the corresponding reduction sequence of its collapse term rc in implicational logic.

scholarly journals Towards closed world reasoning in dynamic open worlds

2010 ◽  
Vol 10 (4-6) ◽  
pp. 547-563 ◽  
Author(s):  
MARTIN SLOTA ◽  
JOÃO LEITE
Keyword(s):  
Semantic Web ◽  
State Of The Art ◽  
Knowledge Bases ◽  
Order Logic ◽  
First Order Logic ◽  
Static Case ◽  
First Order ◽  
Closed World ◽  
Hybrid Knowledge ◽  
First Time

AbstractThe need for integration of ontologies with nonmonotonic rules has been gaining importance in a number of areas, such as the Semantic Web. A number of researchers addressed this problem by proposing a unified semantics forhybrid knowledge basescomposed of both an ontology (expressed in a fragment of first-order logic) and nonmonotonic rules. These semantics have matured over the years, but only provide solutions for the static case when knowledge does not need to evolve.In this paper we take a first step towards addressing the dynamics of hybrid knowledge bases. We focus on knowledge updates and, considering the state of the art of belief update, ontology update and rule update, we show that current solutions are only partial and difficult to combine. Then we extend the existing work on ABox updates with rules, provide a semantics for such evolving hybrid knowledge bases and study its basic properties.To the best of our knowledge, this is the first time that an update operator is proposed for hybrid knowledge bases.

scholarly journals A universal inductive inference machine

1991 ◽  
Vol 56 (2) ◽  
pp. 661-672 ◽  
Author(s):  
Daniel N. Osherson ◽  
Michael Stob ◽  
Scott Weinstein
Keyword(s):  
Inductive Inference ◽  
Scientific Discovery ◽  
Order Logic ◽  
First Order Logic ◽  
Logical Framework ◽  
First Order

AbstractA paradigm of scientific discovery is defined within a first-order logical framework. It is shown that within this paradigm there exists a formal scientist that is Turing computable and universal in the sense that it solves every problem that any scientist can solve. It is also shown that universal scientists exist for no regular logics that extend first-order logic and satisfy the Löwenheim-Skolem condition.

scholarly journals Formalization Of Theories of Design Using: First Order Logic Augmented With A Causal Calculus; And Entropy of a Design Defined In Terms Of The Function, Behavior and Structure Ontology.

2021 ◽  
Author(s):  
KARTHIK GURUMURTHI
Keyword(s):  
High Probability ◽  
Formal Proof ◽  
Order Logic ◽  
First Order Logic ◽  
Logical Framework ◽  
Seamless Integration ◽  
Good Design ◽  
First Order ◽  
Individual Variables ◽  
And Behavior

A symbolic logical framework (L) consisting of first order logic augmented with a causal calculus has been provided to formalize, axiomatize and integrate theories of design. L is used to represent designs in the Function-Behavior-Structure (FBS) ontology in a single, widely applicable language that enables the following: seamless integration of representations of function, behavior and structure; and generality in the formalization of theories of design. FRs, constraints, structure and behavior are represented as sentences in L. FRs are represented (as abstractions of behavior) in the form of existentially quantified sentences, the instantiation of whose individual variables yields the representation of behavior. This enables the logical implication of FRs by behavior, without recourse to apriori criteria for satisfaction of FRs by behavior. Functional decomposition is represented to enable lower level FRs to logically imply the satisfaction of higher level FRs. The theory of whether and how structure and behavior satisfy FRs and constraints is represented as a formal proof in L. Important general attributes of designs such as solution-neutrality of FRs, probability of satisfaction of requirements and constraints (calculated in a Bayesian framework using Monte Carlo simulation), extent and nature of coupling, etc. have been defined in terms of the representation of a design in L. The entropy of a design is defined in terms of the above attributes of a design, based on which a general theory of what constitutes a good design has been formalized to include the desirability of solution-neutrality of (especially higher level) FRs, high probability of satisfaction of requirements and constraints, wide specifications, low variability and bias, use of fewer attributes to specify the design, less coupling (especially circular coupling at higher levels of FRs), parametrization, standardization, etc..

SKEPTICAL ABDUCTION

1993 ◽  
Vol 02 (04) ◽  
pp. 511-540 ◽  
Author(s):  
P. MARQUIS
Keyword(s):  
Propositional Logic ◽  
Order Logic ◽  
First Order Logic ◽  
Real Problem ◽  
Logical Framework ◽  
First Order ◽  
Selective Generation ◽  
The Given ◽  
Reasonable Prospect

Abduction is the process of generating the best explanation as to why a fact is observed given what is already known. A real problem in this area is the selective generation of hypotheses that have some reasonable prospect of being valid. In this paper, we propose the notion of skeptical abduction as a model to face this problem. Intuitively, the hypotheses pointed out by skeptical abduction are all the explanations that are consistent with the given knowledge and that are minimal, i.e. not unnecessarily general. Our contribution is twofold. First, we present a formal characterization of skeptical abduction in a logical framework. On this ground, we address the problem of mechanizing skeptical abduction. A new method to compute minimal and consistent hypotheses in propositional logic is put forward. The extent to which skeptical abduction can be mechanized in first—order logic is also investigated. In particular, two classes of first-order formulas in which skeptical abduction is effective are provided. As an illustration, we finally sketch how our notion of skeptical abduction applies as a theoretical tool to some artificial intelligence problems (e.g. diagnosis, machine learning).

scholarly journals SUBFORMULA AND SEPARATION PROPERTIES IN NATURAL DEDUCTION VIA SMALL KRIPKE MODELS

2010 ◽  
Vol 3 (2) ◽  
pp. 175-227 ◽  
Author(s):  
PETER MILNE
Keyword(s):  
Propositional Logic ◽  
Natural Deduction ◽  
Order Logic ◽  
First Order Logic ◽  
Kripke Models ◽  
Careful Attention ◽  
Classical Propositional Logic ◽  
First Order ◽  
Invalid Inference ◽  
Subformula Property

Various natural deduction formulations of classical, minimal, intuitionist, and intermediate propositional and first-order logics are presented and investigated with respect to satisfaction of the separation and subformula properties. The technique employed is, for the most part, semantic, based on general versions of the Lindenbaum and Lindenbaum–Henkin constructions. Careful attention is paid (i) to which properties of theories result in the presence of which rules of inference, and (ii) to restrictions on the sets of formulas to which the rules may be employed, restrictions determined by the formulas occurring as premises and conclusion of the invalid inference for which a counterexample is to be constructed. We obtain an elegant formulation of classical propositional logic with the subformula property and a singularly inelegant formulation of classical first-order logic with the subformula property, the latter, unfortunately, not a product of the strategy otherwise used throughout the article. Along the way, we arrive at an optimal strengthening of the subformula results for classical first-order logic obtained as consequences of normalization theorems by Dag Prawitz and Gunnar Stålmarck.

THE SUBFORMULA PROPERTY IN CLASSICAL NATURAL DEDUCTION ESTABLISHED CONSTRUCTIVELY

2012 ◽  
Vol 5 (4) ◽  
pp. 710-719 ◽  
Author(s):  
TOR SANDQVIST
Keyword(s):  
Natural Deduction ◽  
Order Logic ◽  
First Order Logic ◽  
Constructive Proof ◽  
First Order ◽  
Subformula Property

AbstractA constructive proof is provided for the claim that classical first-order logic admits of a natural deduction formulation featuring the subformula property.

Natural deduction based set theories: a new resolution of the old paradoxes

1986 ◽  
Vol 51 (2) ◽  
pp. 393-411 ◽  
Author(s):  
Paul C. Gilmore
Keyword(s):  
Set Theory ◽  
Classical Logic ◽  
Natural Deduction ◽  
Order Logic ◽  
First Order Logic ◽  
Truth Values ◽  
First Order ◽  
Axiom Scheme ◽  
Universe Of Sets ◽  
Comprehension Axiom

AbstractThe comprehension principle of set theory asserts that a set can be formed from the objects satisfying any given property. The principle leads to immediate contradictions if it is formalized as an axiom scheme within classical first order logic. A resolution of the set paradoxes results if the principle is formalized instead as two rules of deduction in a natural deduction presentation of logic. This presentation of the comprehension principle for sets as semantic rules, instead of as a comprehension axiom scheme, can be viewed as an extension of classical logic, in contrast to the assertion of extra-logical axioms expressing truths about a pre-existing or constructed universe of sets. The paradoxes are disarmed in the extended classical semantics because truth values are only assigned to those sentences that can be grounded in atomic sentences.

Sign in / Sign up

Export Citation Format

Share Document