scholarly journals Maximum cuts in extended natural deduction

2010 ◽  
Vol 87 (101) ◽  
pp. 59-74
Author(s):  
Mirjana Borisavljevic
Keyword(s):  
Natural Deduction ◽  
Predicate Logic ◽  
Standard System

We consider a standard system of sequents and a system of extended natural deduction (which is a modification of natural deduction) for intuitionistic predicate logic and connect the special cuts, maximum cuts, from sequent derivations and maximum segments from derivations of extended natural deduction. We show that the image of a sequent derivation without maximum cuts is a derivation without maximum segments (i.e., a normal derivation) in extended natural deduction.

AN INTENSIONAL LEIBNIZ SEMANTICS FOR ARISTOTELIAN LOGIC

2010 ◽  
Vol 3 (2) ◽  
pp. 262-272 ◽  
Author(s):  
KLAUS GLASHOFF
Keyword(s):  
Natural Deduction ◽  
Predicate Logic ◽  
Formal System ◽  
Aristotelian Logic ◽  
Categorical Logic ◽  
Characteristic Numbers ◽  
Formal Syntax ◽  
Philosophical Standpoint ◽  
Classical Philosophy

Since Frege’s predicate logical transcription of Aristotelian categorical logic, the standard semantics of Aristotelian logic considers terms as standing for sets of individuals. From a philosophical standpoint, this extensional model poses problems: There exist serious doubts that Aristotle’s terms were meant to refer always to sets, that is, entities composed of individuals. Classical philosophy up to Leibniz and Kant had a different view on this question—they looked at terms as standing for concepts (“Begriffe”). In 1972, Corcoran presented a formal system for Aristotelian logic containing a calculus of natural deduction, while, with respect to semantics, he still made use of an extensional interpretation. In this paper we deal with a simple intensional semantics for Corcoran’s syntax—intensional in the sense that no individuals are needed for the construction of a complete Tarski model of Aristotelian syntax. Instead, we view concepts as containing or excluding other, “higher” concepts—corresponding to the idea which Leibniz used in the construction of his characteristic numbers. Thus, this paper is an addendum to Corcoran’s work, furnishing his formal syntax with an adequate semantics which is free from presuppositions which have entered into modern interpretations of Aristotle’s theory via predicate logic.

scholarly journals The normalization theorem for extended natural deduction

2017 ◽  
Vol 101 (115) ◽  
pp. 75-98
Author(s):  
Mirjana Borisavljevic
Keyword(s):  
Natural Deduction ◽  
Standard System ◽  
Cut Elimination ◽  
Normalization Theorem

The normalization theorem for the system of extended natural deduction will be proved as a consequence of the cut-elimination theorem, by using the connections between the system of extended natural deduction and a standard system of sequents.

Nonstandard theories of quantification and identity

1970 ◽  
Vol 35 (2) ◽  
pp. 267-294 ◽  
Author(s):  
A. Trew
Keyword(s):  
Predicate Logic ◽  
Type A ◽  
The Other ◽  
Standard System ◽  
Free Logic ◽  
Quantification Theory ◽  
Singular Terms ◽  
Free Variables

In this paper a number of nonstandard systems of predicate logic with or without identity, are translated with subsystems of applied standard system of predicate logic with identity. There are nonstandard theories of quantification which, following [16], are described as inclusive systems; their theorems are valid in all domains, including the empty domain. Theories of quantification which allow for the substitution of denotationless terms for free variables, are described, following [21], as systems of free logic; they are said to be free of the requirement that all singular terms must have denotations. Free logics and inclusive logics may each be of the other type. A nonstandard theory of identity, described, following [12] as a theory of nonreflexive identity, may be combined with a standard or with a nonstandard theory of quantification. Another kind of nonstandard system of predicate logic examined is a nonstandard version of a system of monadic predicate logic in which a distinction is made between sentence and predicate negation, and which is nonstandard in the sense that the laws relating sentence and predicate negation diverge from the standard ones. In the systems examined, this is combined with an inclusive quantification theory.

Proof systems for lattice theory

2004 ◽  
Vol 14 (4) ◽  
pp. 507-526 ◽  
Author(s):  
SARA NEGRI ◽  
JAN VON PLATO
Keyword(s):  
Lattice Theory ◽  
Natural Deduction ◽  
Sequent Calculus ◽  
Predicate Logic ◽  
Relational Theory ◽  
Predicate Calculus ◽  
Alternative Formulation ◽  
Proof Systems ◽  
Decidable Classes ◽  
Classical Predicate

A formulation of lattice theory as a system of rules added to sequent calculus is given. The analysis of proofs for the contraction-free calculus of classical predicate logic known as G3c extends to derivations with the mathematical rules of lattice theory. It is shown that minimal derivations of quantifier-free sequents enjoy a subterm property: all terms in such derivations are terms in the endsequent.An alternative formulation of lattice theory as a system of rules in natural deduction style is given, both with explicit meet and join constructions and as a relational theory with existence axioms. A subterm property for the latter extends the standard decidable classes of quantificational formulas of pure predicate calculus to lattice theory.

Natural deduction

2021 ◽  
pp. 65-100
Author(s):  
Paolo Mancosu ◽  
Sergio Galvan ◽  
Richard Zach
Keyword(s):  
Classical Logic ◽  
Natural Deduction ◽  
Final Section ◽  
Predicate Logic ◽  
Original System ◽  
Axiomatic System ◽  
Proof System ◽  
Ordinary Life ◽  
Classical Predicate

Natural deduction is a philosophically as well as pedagogically important logical proof system. This chapter introduces Gerhard Gentzen’s original system of natural deduction for minimal, intuitionistic, and classical predicate logic. Natural deduction reflects the ways we reason under assumption in mathematics and ordinary life. Its rules display a pleasing symmetry, in that connectives and quantifiers are each governed by a pair of introduction and elimination rules. After providing several examples of how to find proofs in natural deduction, it is shown how deductions in such systems can be manipulated and measured according to various notions of complexity, such as size and height. The final section shows that the axiomatic system of classical logic presented in Chapter 2 and the system of natural deduction for classical logic introduced in this chapter are equivalent.

The Grammatical Background of Kant's General Logic

2008 ◽  
Vol 13 (1) ◽  
pp. 116-140
Author(s):  
Kurt Mosser
Keyword(s):  
Natural Deduction ◽  
Necessary Conditions ◽  
Predicate Logic ◽  
Specific Model ◽  
Symbolic Logic ◽  
Pure Reason ◽  
Critique Of Pure Reason ◽  
First Order ◽  
General Logic ◽  
First Order Predicate Logic

In theCritique of Pure Reason, Kant conceives of general logic as a set of universal and necessary rules for the possibility of thought, or as a set of minimal necessary conditions for ascribing rationality to an agent (exemplified by the principle of non-contradiction). Such a conception, of course, contrasts with contemporary notions of formal, mathematical or symbolic logic. Yet, in so far as Kant seeks to identify those conditions that must hold for the possibility of thought in general, such conditions must holda fortiorifor any specific model of thought, including axiomatic treatments of logic and standard natural deduction models of first-order predicate logic. Kant's general logic seeks to isolate those conditions by thinking through – or better, reflecting on – those conditions that themselves make thought possible.

scholarly journals Minimum segments in sequent derivations

2003 ◽  
Vol 74 (88) ◽  
pp. 5-18
Author(s):  
Mirjana Borisavljevic
Keyword(s):  
Natural Deduction ◽  
Predicate Logic ◽  
Special Kind

In a system of sequents for intuitionistic predicate logic derivations without a special kind of cuts (maximum cuts) will be considered. The following be shown: in a derivation without maximum cuts there are paths of the same form as paths in a normal derivation of natural deduction, i.e., these paths have the E-part, the I-part, and one minimum part which corresponds to a minimum segment in a normal derivation.

scholarly journals Normal form theorem for systems of sequents

2007 ◽  
pp. 37-53
Author(s):  
Mirjana Borisavljevic
Keyword(s):  
Normal Form ◽  
Natural Deduction ◽  
Predicate Logic ◽  
Special Kind ◽  
Form Theorem ◽  
Normal Form Theorem

In a system of sequents for intuitionistic predicate logic a theorem, which corresponds to Prawitz?s Normal Form Theorem for natural deduction, are proved. In sequent derivations a special kind of cuts, maximum cuts, are defined. Maximum cuts from sequent derivations are connected with maximum segments from natural deduction derivations, i.e., sequent derivations without maximum cuts correspond to normal derivations in natural deduction. By that connection the theorem for the system of sequents (which correspond to Normal Form Theorem for natural deduction) will have the following form for each sequent derivation whose end sequent is ??A there is a sequent derivation without maximum cuts whose end sequent is ??A.

Sign in / Sign up

Export Citation Format

Share Document