Full-text resources of CEJSH and other databases are now available in the new Library of Science.
Visit https://bibliotekanauki.pl

Results found: 8

first rewind previous Page / 1 next fast forward last

Search results

Search:
in the keywords:  natural deduction
help Sort By:

help Limit search:
first rewind previous Page / 1 next fast forward last
EN
We argue that the need for commentary in commonly used linear calculi of natural deduction is connected to the “deletion” of illocutionary expressions that express the role of propositions as reasons, assumptions, or inferred propositions. We first analyze the formalization of an informal proof in some common calculi which do not formalize natural language illocutionary expressions, and show that in these calculi the formalizations of the example proof rely on commentary devices that have no counterpart in the original proof. We then present a linear natural deduction calculus that makes use of formal illocutionary expressions in such a way that unique readability for derivations is guaranteed – thus showing that formalizing illocutionary expressions can eliminate the need for commentary.
2
Content available remote

Natural Deduction for Three-Valued Regular Logics

100%
EN
In this paper, I consider a family of three-valued regular logics: the well-known strong and weak S.C. Kleene’s logics and two intermediate logics, where one was discovered by M. Fitting and the other one by E. Komendantskaya. All these systems were originally presented in the semantical way and based on the theory of recursion. However, the proof theory of them still is not fully developed. Thus, natural deduction systems are built only for strong Kleene’s logic both with one (A. Urquhart, G. Priest, A. Tamminga) and two designated values (G. Priest, B. Kooi, A. Tamminga). The purpose of this paper is to provide natural deduction systems for weak and intermediate regular logics both with one and two designated values.
3
88%
EN
The paper introduces NJ g , a variant of Gentzen’s NJ natural deduction system, in which the implication elimination rule has no minor premise. The NJ g -systems extends traditional ND-system with a new kind of action in derivations, assumption incorporation, a kind of dual to the assumption discharge action. As a result, the implication (I/E)-rules are invertible and, almost by definition, harmonious and stable, a major condition imposed by proof-theoretic semantics on ND-systems to qualify as meaning-conferring. There is also a proof-term assignment to NJ g -derivations, materialising the Curry-Howard correspondence for this system.
4
88%
EN
We consider four natural deduction systems: Fitch-style systems, Gentzen-style systems (in the form of dags), general deduction Frege systems and nested deduction Frege systems, as well as dag-like Gentzen-style sequent calculi. All these calculi soundly and completely formalize classical propositional logic. We show that general deduction Frege systems and Gentzen-style natural calculi provide at most quadratic speedup over nested deduction Frege systems and Fitch-style natural calculi and at most cubic speedup over Gentzen-style sequent calculi.
EN
The development of recursion theory motivated Kleene to create regular three-valued logics. Remove it taking his inspiration from the computer science, Fitting later continued to investigate regular three-valued logics and defined them as monotonic ones. Afterwards, Komendantskaya proved that there are four regular three-valued logics and in the three-valued case the set of regular logics coincides with the set of monotonic logics. Next, Tomova showed that in the four-valued case regularity and monotonicity do not coincide. She counted that there are 6400 four-valued regular logics, but only six of them are monotonic. The purpose of this paper is to create natural deduction systems for them. We also describe some functional properties of these logics.
EN
Using the method of correspondence analysis, Tamminga obtains sound and complete natural deduction systems for all the unary and binary truth-functional extensions of Kleene’s strong three-valued logic K3 . In this paper, we extend Tamminga’s result by presenting an original finite, sound and complete proof-searching technique for all the truth-functional binary extensions of K3.
PL
Dzięki zdobytej wiedzy filozoficznej Ludwik Borkowski widział problemy formalne w szer­szym kontekście. Był w uprawianiu logiki kontynuatorem tradycji szkoły lwowsko-warszawskiej. Podejmował problemy podstawowe dla szeroko pojętej logiki oraz mające doniosłe konsek­wen­cje filozoficzne, np. logiki nieklasyczne, teoria prawdy, metoda założeniowa, teoria konsekwen­cji, teoria definicji. Dbał o intuicyjną interpretację swych wyników logicznych, a samą logikę traktował jako naukę autonomiczną, która ma pełnić funkcję służebną wobec innych nauk. Choć nie pisał typowych dzieł filozoficzno-logicznych, dociekanie filozoficznych źródeł, inspiracji i kon­sekwencji wyników logiki towarzyszyło mu przez cały czas twórczej aktywności.
EN
Ludwik Borkowski’s vast knowledge of philosophy allowed him to put his logical studies in a philosophical context. As a logician, he continued the tradition of the Lvov-Warsaw school. He dealt with the basic issues of the widely understood logic as well as with those having strong philosophical implications (e.g. non-classical logics, the theory of truth, natural deduction, the theory of consequence). He also worked on the theory of definition and the intuitive interpre­tation of logical results. For Borkowski, logic was an autonomous science whose function is supposed to be ancillary towards the other sciences. Although he did not write any typical philo­sophical-logical works, investigating philosophical sources, inspirations and the implications of logi­cal results was something he did throughout the whole period of his creative activity.
EN
Gentzen’s rules of natural deduction define the basic inference patterns which govern the use of logical constants within the logical system of natural deduction. In general, these rules are considered to represent a model that significantly approximates the actual use of counterparts of logical constants by competent speakers in everyday communication. Despite the fact that Gentzen’s system is assumed to approximate the inferential patterns of the use of counterparts of logical constants in natural languages, empirical studies mapping the system’s deviations from natural languages are rather rare. The aim of our research is, therefore, to find out to what extent the rules of natural deduction are in accordance with the use of counterparts of logical constants by competent Czech speakers. In our research, we employ the method of validity judgment tasks, in which respondents assess whether a sentence can be inferred from a short text. The results confirm that seven rules of natural deduction (conjunction introduction, conjunction elimination, disjunction elimination, implication elimination, existential quantifier introduction, universal quantifier introduction, universal quantifier elimination) are in accordance with the use of their counterparts by competent Czech speakers, and three rules (implication introduction, negation introduction, disjunction introduction) exhibit various levels of deviation.
first rewind previous Page / 1 next fast forward last
JavaScript is turned off in your web browser. Turn it on to take full advantage of this site, then refresh the page.